#lang scribble/doc
@(require scribble/manual
scribble/eval
scribble/basic
(planet cce/scheme:7)
(only-in unstable/scribble declare-exporting/this-package)
(for-label (this-package-in smt-solver/smt-solve)
(this-package-in smt-solver/smt-interface)
(this-package-in smt-solver/dimacs)))
@title[#:tag "top"]{An SMT-solver for Racket}
@author[(author+email "Ian Johnson" "ianj@ccs.neu.edu")
(author+email "Paul Stansifer" "pauls@ccs.neu.edu")]
This package contains an SMT-solver written using the DPLL(T) framework.
Its mechanics include conflict-based learned with the first unique implication point heuristic,
efficient unit resolution with the 2-literal watching heuristic,
and ``smart'' literal choice with the variable state independent, decaying sum heuristic (popularized by the CHAFF solver).
Soon to be implemented: clause forgetting with the Minisat policy, and random restarts with the Picosat policy.
@table-of-contents[]
@section{An SMT-solver for Racket}
@declare-exporting/this-package[(smt-solver/dimacs) ()]
@subsection{The SMT-Solver interface}
@declare-exporting/this-package[(smt-solver/smt-solve) ()]
Types are detailed below.
The main function of the SMT solver is
@defproc[(smt-solve [cnf dimacscnf?]
[t-state any/c]
[strength strength?]
[choose-literal (SMT? . -> . Literal?)])
(or/c sat-exn? unsat-exn?)]{
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
@defproc[(smt-assign [cnf dimacscnf?]
[t-state any/c]
[strength strength?]
[choose-literal (SMT? . -> . Literal?)])
(or/c 'UNSAT (listof exact-integer?))]{
Uses @racket[smt-solve] to return @racket['UNSAT] or the partial model in the form of all satisfied DimacsLits.}
@defproc[(smt-decide [cnf dimacscnf?]
[t-state any/c]
[strength strength?]
[choose-literal (SMT? . -> . Literal?)])
(or/c 'UNSAT 'SAT)]{
Like @racket[smt-assign], but does not extract the final model.}
@defproc[(sat-solve [cnf dimacscnf?]
[choose-literal (SMT? . -> . Literal?)])
(or/c sat-exn? unsat-exn?)]
@defproc[(sat-assign [cnf dimacscnf?]
[choose-literal (SMT? . -> . Literal?)])
(or/c 'UNSAT (listof exact-integer?))]
@defproc[(sat-decide [cnf dimacscnf?]
[choose-literal (SMT? . -> . Literal?)])
(or/c 'UNSAT 'SAT)]{
Like smt-x, but initially parameterizes by the trivial theory.}
@subsection{The T-Solver interface}
@declare-exporting/this-package[(smt-solver/smt-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 @racket[#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 @racket[+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 @racket[T-Satisfy], @racket[T-Backjump],
@racket[T-Propagate], @racket[T-Explain] and @racket[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.
@defproc[(sat-satisfy [t-state any/c]
[lit exact-integer?])
any/c]
@defproc[(sat-backjump [t-state any/c]
[backjump-by-sats exact-nonnegative-integer?])
any/c]
@defproc[(sat-propagate [t-state any/c]
[strength strength?]
[lit exact-integer?])
any/c]
@defproc[(sat-explain [t-state any/c]
[strength strength?]
[lit exact-integer?])
any/c]
@defproc[(sat-consistent? [t-state any/c]
[strength strength?])
(or/c boolean? (listof exact-integer?))]
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.
@index-section[]
@section{Acknowledgments}
The package uses the DPLL(T) framework described in
@link["http://portal.acm.org/citation.cfm?id=1217856.1217859"]{Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL (T)} by R. Nieuwenhuis and A. Oliveras.