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
sat-exn
unsat-exn
T-Satisfy
T-Backjump
T-Restart?
T-Propagate
T-Explain
T-Consistent?
sat-satisfy
sat-backjump
sat-restart
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    
  seed    
  choose-literal)  (or/c sat-exn? unsat-exn?)
  cnf : dimacscnf?
  t-state : any/c
  strength : strength?
  seed : (or/c exact-nonnegative-integer? #f)
  choose-literal : (SMT? . -> . Literal?)
Which takes a CNF, initial T-State, initial Strength, the seed to give to random-seed (or #f to use the current clock) 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 
  seed 
  choose-literal) 
  (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?)
Uses smt-solve to return 'UNSAT or the partial model in the form of all satisfied DimacsLits.

(smt-decide cnf    
  t-state    
  strength    
  seed    
  choose-literal)  (or/c 'UNSAT 'SAT)
  cnf : dimacscnf?
  t-state : any/c
  strength : strength?
  seed : (or/c exact-nonnegative-integer? #f)
  choose-literal : (SMT? . -> . Literal?)
Like smt-assign, but does not extract the final model.

(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?)
Like smt-x, but initially parameterizes by the trivial theory.

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

(struct sat-exn (smt)
  #:extra-constructor-name make-sat-exn)
  smt : SMT?
(struct unsat-exn (smt)
  #:extra-constructor-name make-unsat-exn)
  smt : SMT?
The structs that are the result of smt-solve, which encapsulate the final state of the SMT solver.

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: