1 An SMT-solver for Racket
1.1 The SMT-Solver interface
Types are detailed below.
The main function of the SMT solver is
| (smt-solve | | cnf | | | | | | | | t-state | | | | | | | | strength | | | | | | | | choose-literal) | | → | | (or/c sat-exn? unsat-exn?) |
|
| cnf : dimacscnf? |
| t-state : any/c |
| strength : strength? |
| choose-literal : (SMT? . -> . Literal?) |
Which takes a CNF, initial T-State, initial Strength and possibly a choice function and returns
the result as a struct encapsulating the final SMT state.
Derived interfaces are
| (smt-assign | | cnf | | | | | t-state | | | | | strength | | | | | choose-literal) | |
|
| → (or/c 'UNSAT (listof exact-integer?)) |
| cnf : dimacscnf? |
| t-state : any/c |
| strength : strength? |
| choose-literal : (SMT? . -> . Literal?) |
Uses smt-solve to return 'UNSAT or the partial model in the form of all satisfied DimacsLits.
| (smt-decide | | cnf | | | | | | | | t-state | | | | | | | | strength | | | | | | | | choose-literal) | | → | | (or/c 'UNSAT 'SAT) |
|
| cnf : dimacscnf? |
| t-state : any/c |
| strength : strength? |
| choose-literal : (SMT? . -> . Literal?) |
Like smt-assign, but does not extract the final model.
| (sat-solve cnf choose-literal) → (or/c sat-exn? unsat-exn?) |
| cnf : dimacscnf? |
| choose-literal : (SMT? . -> . Literal?) |
| (sat-assign cnf choose-literal) |
| → (or/c 'UNSAT (listof exact-integer?)) |
| cnf : dimacscnf? |
| choose-literal : (SMT? . -> . Literal?) |
| (sat-decide cnf choose-literal) → (or/c 'UNSAT 'SAT) |
| cnf : dimacscnf? |
| choose-literal : (SMT? . -> . Literal?) |
Like smt-x, but initially parameterizes by the trivial theory.
1.2 The T-Solver interface
This is a fully fledged DPLL(T) SMT solver, but there are so common theories implemented.
To write a theory solver, you must maintain the following interfaces:
(itemlist
(item
Your theory solver may encapsulate its state into a value that will be passed between
the SMT solver and the SAT solver. This is what is meant by the type T-State.
It is opaque to the SAT solver, but is maintained through interfacing calls. You may choose
not to use this feature and use global state, using some dummy value like #f.)
(item
Strength is a Natural or +inf.0. You may use this to control eagerness of the T-Solver.
Currently there is no logic to modify strength in the SAT solver, so it is coarse-grained.
The SMT solver takes an initial strength value.
At a time the SAT solver has a model, it will call T-Consistent? with +inf.0 strength.
This is paramount for completeness. If this is not what you want, you can change it in sat-solve.rkt
at its only callsite.)
(item
The SMT solver should be driven externally. We mean that the SAT solver only understands DimacsLits,
so any atomic propositions your T-solver interprets should already be in the T-State.
This is why the SMT solver takes in initial T-State.)
(item
You must use parameterize to set T-Satisfy, T-Backjump,
T-Propagate, T-Explain and T-Consistent?
that are briefly summarized in smt-interface.rkt, and detailed in
Nieuwenhuis & Oliveras: Abstract DPLL and Abstract DPLL modulo theories. They are exected to have the
same signatures as their respective default values given below.
| (sat-satisfy t-state lit) → any/c |
| t-state : any/c |
| lit : exact-integer? |
| (sat-backjump t-state backjump-by-sats) → any/c |
| t-state : any/c |
| backjump-by-sats : exact-nonnegative-integer? |
| (sat-propagate t-state strength lit) → any/c |
| t-state : any/c |
| strength : strength? |
| lit : exact-integer? |
| (sat-explain t-state strength lit) → any/c |
| t-state : any/c |
| strength : strength? |
| lit : exact-integer? |
| (sat-consistent? t-state strength) |
| → (or/c boolean? (listof exact-integer?)) |
| t-state : any/c |
| strength : strength? |
Because the SAT-solver is unaware of which literals are theory-interpreted,
T-Satisfy, T-Propagate and T-Explain must be able to make the distinction.