1 An SMT-solver for Racket

1.1 The SMT-Solver interface

Types are detailed below. The main function of the SMT solver is

Derived interfaces are

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:

• 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-Explain : (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-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.