1 An SMT-solver for Racket
1.1 The SMT-Solver interface
Types are detailed below. The main function of the SMT solver is
| |||||||||||||||||||||||||||||||||||
cnf : dimacscnf? | |||||||||||||||||||||||||||||||||||
t-state : any/c | |||||||||||||||||||||||||||||||||||
strength : strength? | |||||||||||||||||||||||||||||||||||
seed : (or/c exact-nonnegative-integer? #f) | |||||||||||||||||||||||||||||||||||
choose-literal : (SMT? . -> . Literal?) |
Derived interfaces are
| ||||||||||||||||||||
→ (or/c 'UNSAT (listof exact-integer?)) | ||||||||||||||||||||
cnf : dimacscnf? | ||||||||||||||||||||
t-state : any/c | ||||||||||||||||||||
strength : strength? | ||||||||||||||||||||
seed : (or/c exact-nonnegative-integer? #f) | ||||||||||||||||||||
choose-literal : (SMT? . -> . Literal?) |
| |||||||||||||||||||||||||||||||||||
cnf : dimacscnf? | |||||||||||||||||||||||||||||||||||
t-state : any/c | |||||||||||||||||||||||||||||||||||
strength : strength? | |||||||||||||||||||||||||||||||||||
seed : (or/c exact-nonnegative-integer? #f) | |||||||||||||||||||||||||||||||||||
choose-literal : (SMT? . -> . Literal?) |
(sat-solve cnf seed choose-literal) → (or/c sat-exn? unsat-exn?) |
cnf : dimacscnf? |
seed : (or/c exact-nonnegative-integer? #f) |
choose-literal : (SMT? . -> . Literal?) |
(sat-assign cnf seed choose-literal) |
→ (or/c 'UNSAT (listof exact-integer?)) |
cnf : dimacscnf? |
seed : (or/c exact-nonnegative-integer? #f) |
choose-literal : (SMT? . -> . Literal?) |
(sat-decide cnf seed choose-literal) → (or/c 'UNSAT 'SAT) |
cnf : dimacscnf? |
seed : (or/c exact-nonnegative-integer? #f) |
choose-literal : (SMT? . -> . Literal?) |
Examples: |
> (sat-assign (list 5 5 '((-1 2) (-1 3) (-2 4) (-3 -4) (1 -3 5)))) |
'(-1 -2 3 -4 5) |
> (sat-decide (list 5 5 '((-1 2) (-1 3) (-2 4) (-3 -4) (1 -3 5)))) |
'SAT |
1.2 The T-Solver interface
This is a fully fledged DPLL(T) SMT solver, but there are no common theories implemented. There are currently no plans to use the FFI to communicate with third party theory solvers. To write a theory solver, you must maintain the following interfaces:
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.
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.
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.
- You must use parameterize to set
T-Satisfy : (any/c exact-integer? . -> . any/c) T-Backjump : (any/c exact-nonnegative-integer? . -> . any/c) T-Propagate : (any/c strength? exact-integer? . -> . any/c) T-Consistent? : (any/c strength? . -> . (or/c boolean? (listof exact-integer?))) which 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-restart t-state) → any/c t-state : any/c (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? Where strength is(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.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.