2 Visible data-structures
There are a few datatypes that are exposed through the SMT/T-Solver interface.
Strength describes how eager a T-Solver should be. It can be a natural number to denote some amount of approximation,
or +inf.0 to denote exhaustiveness/completeness.
| (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.
Examples: |
| > "(dimacscnf? (list 5 5" |
"(dimacscnf? (list 5 5" |
| > "\n" |
"\n" |
| > " " |
" " |
| > "'((-1 2)" |
"'((-1 2)" |
| > "\n" |
"\n" |
| > " " |
" " |
| > "(-1 3)" |
"(-1 3)" |
| > "\n" |
"\n" |
| > " " |
" " |
| > "(-2 4)" |
"(-2 4)" |
| > "\n" |
"\n" |
| > " " |
" " |
| > "(-3 -4)" |
"(-3 -4)" |
| > "\n" |
"\n" |
| > " " |
" " |
| > "(1 -3 5))))" |
"(1 -3 5))))" |