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.
|> (dimacscnf? (list 5 5 '((-1 2) (-1 3) (-2 4) (-3 -4) (1 -3 5))))|
Predicate for recognizing the internal representation of the SMT solver.
Predicate for recognizing the internal representation of a literal.