▼An SMT-solver for Racket
  ← prev  up  next → 

An SMT-solver for Racket

Ian Johnson <ianj@ccs.neu.edu>
and 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.

    1 An SMT-solver for Racket

      1.1 The SMT-Solver interface

      1.2 The T-Solver interface

    2 Visible data-structures

    Index

    3 Acknowledgments

  ← prev  up  next →