On this page:
dimacscnf?
sat-exn
unsat-exn
SMT?
Literal?

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))))"

(struct sat-exn (smt)
  #:extra-constructor-name make-sat-exn)
  smt : SMT?
(struct unsat-exn (smt)
  #:extra-constructor-name make-unsat-exn)
  smt : SMT?

SMT? : (any/c . -> . boolean?)
Predicate for recognizing the internal representation of the SMT solver.
Literal? : (any/c . -> . boolean?)
Predicate for recognizing the internal of a literal.