Sammy is a SMT checker written in OCaml and C based on the DPLL(T) architecture being developed at the University of Iowa. This architecture defines a DPLL-style engine for propositional solving, DPLL(X), parametrized (in X) by a solver for a theory of interest. A DPLL(T) system is obtained by plugging in a solver for a background theory T conforming to a certain interface. The solver is in essence a ground decision procedure for T, although it must provide additional functionalities than simple yes-no answers.
By and large, Sammy is the implementation of the DPLL(X) engine. The theory solver used in this version of Sammy is the combined decision procedure of the CVC Lite prover. This procedure decides the satisfiability of a set of literals modulo a background theory which is a rich combination of several background theories commonly used in SMT applications. CVC Lite is written in a highly modular way, with many of its core functionalities provided as libraries. Through a selection of CVC Lite's library functions one can carve out of CVC Lite a theory solver for the DPLL(T) architecture, which is what is done in this case. Sammy's DPLL(X) engine relies on a satbox derived from the SATO propositional solver. The satbox module is responsible for such DPLL operation as unit propagation, (propositional) lemma learning, and backjumping.
The DPLL(T) architecture accepts sets of ground CNF formulas in the signature of the theory T possibly expanded with free function or predicate symbols. Sammy on the other hand accepts arbitrary first-order formulas, in the SMT-LIB format.
Quantified, non-CNF formulas are dealt with by an additional wrapper around Sammy's DPLL(T) subsystem. In essence, this wrapper generates ground clauses from an input formula as needed, and feeds them into the DPLL(T) subsystem. At any time, the current set of generated ground clauses is logically entailed by the input formula. The clause generation feature is based on new (incomplete) heuristics to be described in forthcoming work.
Sammy has competed in the 2005 SMT-Comp competition (CAV 2005).
DPLL(T) Framework:
Sammy v0.9 (SMT-COMP'05) source: sammy-smtcomp2005.tar.gz
Installation instructions for sammy can be found here. A brief user's guide can be found here.
Under Construction
Under Construction
The material on this site is based upon work partailly supported by the National Science Foundation under Grant No. 237422.
Any opinions, findings and conclusions or recomendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation (NSF).