#lang scribble/doc @(require scribble/manual scribble/eval scribble/basic ;scribble/bnf ;(planet cce/scheme:6/planet) ;(planet cce/scheme:6/scribble) (for-label "../smt-solve.rkt" "../smt-interface.rkt" "../dimacs.rkt")) @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["../dimacs.rkt"] @subsection{The SMT-Solver interface} @declare-exporting["../smt-solve.rkt"] 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["../smt-interface.rkt"] 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.