2 Visible data-structures
There are a few datatypes that are exposed through the SMT/T-Solver interface.
| (dimacscnf? x) → boolean? |
| x : any/c |
DIMACS CNF is a simple format for describing propositional formulae in conjunctive normal form.
Here it is an s-expression containing first the variable count, then clause count, then the list of clauses.
DIMACS literals are non-zero integers whose absolute value is less than or equal to the variable count.
A clause is a list of DIMACS literals.
Example: |
| > "(dimacscnf? (list 5 5 '((-1 2) (-1 3) (-2 4) (-3 -4) (1 -3 5))))" |
"(dimacscnf? (list 5 5 '((-1 2) (-1 3) (-2 4) (-3 -4) (1 -3 5))))" |
| ||||||
| smt : SMT? |
| ||||||
| smt : SMT? |
Predicate for recognizing the internal representation of the SMT solver.
Predicate for recognizing the internal of a literal.