On this page:
1.1 The SMT-Solver interface
smt-solve
smt-assign
smt-decide
sat-solve
sat-assign
sat-decide
1.2 The T-Solver interface
T-Satisfy
T-Backjump
T-Propagate
T-Explain
T-Consistent?
sat-satisfy
sat-backjump
sat-propagate
sat-explain
sat-consistent?
strength?

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: