An SMT-solver for Racket

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.