An SMT-solver for Racket

Ian Johnson <>
and Paul Stansifer <>

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, “smart” literal choice with the variable state independent, decaying sum heuristic (popularized by the CHAFF solver), clause forgetting with the Minisat policy, and random restarts with the Picosat policy.

    1 An SMT-solver for Racket

      1.1 The SMT-Solver interface

      1.2 The T-Solver interface

    2 Visible data-structures

    3 Acknowledgments