On this page:
strength?
dimacscnf?

2 Visible data-structures

There are a few datatypes that are exposed through the SMT/T-Solver interface.

(strength? x)  boolean?
  x : any/c
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))))"