This extended abstract describes work in progress on Smt-Switch, an open-source, solver-agnostic API for SMT solving. Smt-Switch provides an abstract interface, which can be implemented by di erent SMT solvers. Smt-Switch provides simple, uniform, and high-performance access to SMT solving for applications in areas such as automated reasoning, planning, and formal veri cation. The interface allows the user to create, traverse, and manipulate terms, as well as to dynamically dispatch queries to di erent underlying SMT solvers.
2
Smt-Switch is designed to be a lightweight wrapper on the C or C++ API of the underlying
SMT solvers. It intentionally delegates as much of the functionality to the underlying solvers
as possible. This reduces redundancy, and results in simpler implementations and lower
memory overhead. The API is implemented in C++11 and also provides Python bindings using
Cython [
Architecture. Smt-Switch provides abstract classes which must be implemented by a
wrapper for each underlying solver. The implementations satisfy the interface requirements of
the abstract classes and wrap the relevant objects needed for that underlying solver's own API.
Throughout this abstract, we use underlying solver to refer to the SMT solver we are wrapping
and backend to refer to the Smt-Switch wrapper. Any solver with a C or C++ API can be
added to Smt-Switch. At the Smt-Switch API level, the user interacts with smart pointers
to the abstract classes. The virtual method functionality of C++ allows the pointer to
dynamically call the relevant method of the derived class (the backend) that is pointed to. This
architecture allows the interface to be agnostic to the underlying solver. The three primary
abstract classes are: (i) AbsSort; (ii) AbsTerm; and (iii) AbsSmtSolver. The interface and
method names are based on SMT-LIB version 2 [
Building and Linking. Smt-Switch uses CMake [
Testing. We use GoogleTest [
Unde ned Behavior. Each backend implementation of a solver needs to recover its relevant objects from a generic abstract object. This is done with a static pointer cast. This results in unde ned behavior if the cast is not valid. In particular, this means that sharing Sorts and Terms between di erent SmtSolvers results in unde ned behavior. To move a Sort or Term between solvers, it must explicitly be transferred. There is a class provided in the API which can transfer terms between solvers. Smt-Switch is intentionally lightweight and thus does not perform much error checking. This design decision was made to reduce overhead and redundancy, since most SMT solvers do error checking already. However, the class hierarchy allows users to extend classes or build wrappers if they would like to insert their own error checking at the Smt-Switch level. 1 /** Abstract solver class to be implemented by each supported solver. */ 2 class AbsSmtSolver 3 { 4 public: 5 /* Add an assertion to the solver 6 * SMTLIB: (assert <t>) 7 * @param t a boolean term to assert */ 8 virtual void assert_formula(const Term & t) = 0; 9 /* Check satisfiability of the current assertions 10 * SMTLIB: (check-sat) 11 * @return a result object - see result.h */ 12 virtual Result check_sat() = 0; 13 /* Get the value of a term after check_sat returns a satisfiable result 14 * SMTLIB: (get-value (<t>)) 15 * @param t the term to get the value of 16 * @return a value term */ 17 virtual Term get_value(const Term & t) const = 0; 18 /* Create a sort 19 * @param sk the SortKind (BOOL, INT, REAL) 20 * @return a Sort object */ 21 virtual Sort make_sort(const SortKind sk) const = 0; 22 /* Create a sort 23 * @param sk the SortKind (BV) 24 * @param size (e.g. bitvector width for BV SortKind) 25 * @return a Sort object */ 26 virtual Sort make_sort(const SortKind sk, uint64_t size) const = 0; 27 /* Create a sort 28 * @param sk the SortKind (FUNCTION) 29 * @param sorts a vector of sorts (last sort is return type) 30 * @return a Sort object 31 * Note: This is the only way to make a function sort */ 32 virtual Sort make_sort(const SortKind sk, const SortVec & sorts) const = 0; 33 /* Make a boolean value term 34 * @param b boolean value 35 * @return a value term with Sort BOOL and value b */ 36 virtual Term make_term(bool b) const = 0; 37 /* Make a symbolic constant or function term 38 * SMTLIB: (declare-fun <name> (s1 ... sn) s) where sort = s1x...xsn -> s 39 * @param name the name of constant or function 40 * @param sort the sort of this constant or function 41 * @return the symbolic constant or function term */ 42 virtual Term make_symbol(const std::string name, const Sort & sort) = 0; 43 /* Make a new term 44 * @param op the operator to use 45 * @param terms vector of children 46 * @return the created term */ 47 virtual Term make_term(const Op op, const TermVec & terms) const = 0; 48 };
Custom Exceptions. Smt-Switch de nes its own set of exceptions that inherit from std::exception. Each of them take a std::string message for describing the problem that can be accessed with the what method.
1. SmtException : the generic Smt-Switch exception - all other custom exceptions inherit from it. 2. NotImplementedException : the exception for an unimplemented feature in a backend solver. 3. IncorrectUsageException : an exception that is thrown when incorrect usage on the users' part is detected. 4. InternalSolverException : an exception that is thrown when there is an error in the underlying solver. 3 We now describe the abstract interface in more detail. We start by describing the AbsSort class which illustrates the supported theories. This is followed by the non-abstract struct for representating operators: Op. Next, we describe the other two important abstract classes: AbsTerm and AbsSmtSolver. Figure 2 depicts the class hierarchy for an AbsSmtSolver. The AbsSort and AbsTerm classes have analogous architectures. Finally, we describe the Result struct which is returned after a satis ability query, and the solver factories that are used to instantiate solvers. 3.1
The AbsSort abstract class represents the type of Terms created in Smt-Switch. Sorts are characterized by an enum, SortKind, which categorizes it and additional parameters based on the SortKind. AbsSort has virtual methods for querying the sort for its SortKind and parameters. This abstract class is implemented by each backend solver and wraps the backend's representation of a sort. For example, the CVC4 backend has a CVC4Sort class which wraps a sort object from CVC4's C++ API. A Sort is a pointer to an AbsSort. Currently supported SortKinds and associated parameters are the following: 1. BOOL: booleans 2. INT: integer numbers 3. REAL: real numbers 4. BV: xed-width bitvectors
(a) parameter: positive integer width
(a) parameter: vector of domain Sorts (b) parameter: the codomain Sort
3.2
Op (a) parameter : index Sort (b) parameter : element Sort
(a) parameter: non-negative integer arity
Op is a struct used to represent builtin operators for constructing terms in Smt-Switch. These can be split into two categories: primitive operators and indexed operators. For unity of representation, an Op is used for both. An Op stores a PrimOp enum and up to two integer indices. Primitive operators are de ned only by the PrimOp and take no indices. Indexed operators have both a PrimOp and one or two indices. For convenience, the Op constructor can be applied implicitly by the compiler. Thus, building terms with a primitive operator can be accomplished by using a PrimOp directly, without explicitly building an Op from it. Smt-Switch uses a straightforward naming scheme such that the PrimOp enums have oneto-one correspondence with SMT-LIB operators.
Ops can be null. All Terms that are a symbol or value have a null operator. Note that terms with null operators are not necessarily leaf nodes. For example, one such edge case is constant arrays (arrays where every element has been set to a given value). Constant arrays are themselves values and thus have a null operator. However, they still have one child which is the value assigned to every element. 3.3
The AbsTerm abstract class represents expressions built through the API. Constructing the term uses methods from the SmtSolver because most underlying solvers use a solver or context object for registering terms. However, once the term is created, the Smt-Switch interface assumes that it can be queried for information. For example, a term has virtual methods for accessing the Sort, the Op used to create it, and the children of the Term. Querying the children is implemented as an iterator. Thus, Terms have a begin and end method that each return a TermIter, which is a class that wraps an abstract class, TermIterBase. Each backend solver must implement a derived class for AbsTerm that wraps its relevant expression representation(s). If the backend solver supports accessing the children of a term, it must also implement a derived class for TermIterBase. For example, the CVC4 backend has both a CVC4Term and CVC4TermIter object that implement the Term and TermIterBase interfaces and store the relevant term and term iteration objects from the CVC4 C++ API. A Term is a pointer to an AbsTerm. Smt-Switch also has type declarations for convenient data structures such as TermVec which is a vector of Terms.
A given Term can be a symbol (uninterpreted constant or function), a value (theory values such as the number 1), or an expression built from symbols and values using operators. All SMT expressions in Smt-Switch are represented as terms. In particular, we take a higherorder logic perspective and represent uninterpreted functions as terms. Thus, applying an uninterpreted function uses an \Apply" operator on the function and the arguments. Some SMT solvers are starting to add higher-order logic features, and this representation is often convenient. For example, an invariant maintained by Smt-Switch is that any term with a non-null operator can always be rebuilt using its operator and children. For a given Term t with a non-null operator, the backend solver implementation should guarantee that the following always returns true:
t == solver->make term(t->get op(), TermVec(t->begin(), t->end())) If the API instead had di erent methods for applying an uninterpreted function versus creating terms with a builtin operator, this invariant would not be maintained. 3.4
AbsSmtSolver declares the main interface that a user interacts with. It has methods for declaring Sorts, building Terms, asserting formulas and checking for satis ability. SmtSolver is a pointer to an AbsSmtSolver. The bulk of the implementation for a backend solver will likely be its implementation of AbsSmtSolver. The interface methods closely match the commands of SMT-LIB. The naming scheme simply replaces \-" with \ ". For example, some methods of AbsSmtSolver include set opt, check sat, and get value. One notable exception is that assertions are added with the assert formula method (as opposed to \assert" as in SMT-LIB), to avoid clashing with the C assert macro.
Each backend solver must implement a derived class for AbsSmtSolver. For example, the CVC4 backend has a CVC4Solver object that inherits AbsSmtSolver. This derived class must store the relevant information for that solver and implement each of the virtual AbsSmtSolver methods in the underlying solver's API. The AbsSmtSolver methods all operate over pointers to the abstract objects as shown in Figure 1. For example, the method at line 47 has signature: make term(Op, const TermVec &). The derived class implementation must cast each of the Term pointers in the TermVec to its own derived class implementation of AbsTerm to be able to access relevant wrapped members. Thus, the CVC4Solver implementation of that method would cast each of the Terms to a CVC4Term with static pointer cast<CVC4Term>(t) for Term t. Then, it would intepret the Op, perform the corresponding operation over the CVC4 objects, and nally wrap the result in a CVC4Term and return it as a Term. 3.5
Result is a struct for representing the return value of a call to check sat or check sat assuming. It currently has three possible values: SAT, UNSAT, and UNKNOWN. In the case of UNKNOWN, the backend solver can optionally provide a std::string with an explanation of the reason for the unknown result. 3.6
A solver factory is a simple class that de nes a single static method: create(bool logging). Each backend solver implementation de nes a factory and has a dedicated header le. The create function is used to create a SmtSolver of that type. The single boolean parameter is to choose whether or not the term DAG is tracked at the Smt-Switch level.
If logging is set to false, the SmtSolver relies on the underlying solver API for querying a term for its Op, Sort and children (e.g. term traversal) by translating back to Smt-Switch objects.
If logging is set to true, the method returns the backend solver but wrapped by a LoggingSolver. This is an implementation of AbsSmtSolver that forwards commands to another backend SmtSolver. Additionally, it keeps a term DAG at the Smt-Switch level. This is accomplished by wrapping every Sort and Term created through the LoggingSolver in a LoggingSort and LoggingTerm, respectively. In addition to storing the underlying objects, these classes also keep relevant data for tracking the expression DAG as it was constructed. For example, a LoggingSort keeps the SortKind and parameters used to create it. A LoggingTerm keeps the Op, (Logging) Sort, and children (Logging) Terms. This optional feature can be useful for underlying solvers that perform on-the- y rewriting or alias sorts (e.g., do not distinguish between bitvectors of width one and booleans). The logging infrastructure ensures that a created term has exactly the same Op, Sort, and children that were used to create it. The implicit assumption is that even though creating a term through a solver API might result in a rewritten term, creating the term again with the same Op and children will result in the same rewritten term. Thus, the logging infrastructure hides the underlying solver's rewriting from the user. To contend with sort aliasing, the LoggingSolver also performs sort inference to compute the expected sort when building terms. The logging infrastructure simplies transferring terms between di erent solvers (which might not alias sorts in the same way) and can be more intuitive. Additionally, some solver backends (currently the Yices2 backend) rely on the logging infrastructure for term traversal. A Yices2 SmtSolver created without logging will create Terms that do not support iterating over the children. 4
In this section we demonstrate the Smt-Switch API with a simple example using both the C++ API and the Python bindings. Figure 3 uses Smt-Switch with the CVC4 backend to solve two simple queries over bitvectors and uninterpreted functions. Lines 1-2 include the necessary Smt-Switch headers, and lines 3-8 are standard C++ includes, using declarations and main function. Line 9 declares a SmtSolver using CVC4 as the backend without logging. In line 10 the solver is set to incremental mode. Lines 11 and 12 declare a bitvector sort of width 9 and a function sort from a width 9 bitvector to a width 9 bitvector. Lines 13-17 declare two bitvector symbolic constants, an uninterpreted function and then applies the function to each of the bitvector symbols. Line 20 uses a C assert to check that the operator of an applied uninterpreted function term is Apply. Line 21 populates a vector with the children of term fx. Line 22 asserts that there are two children (in some solvers this term would have only one child: x). Lines 25 and 26 check that the children are the function, f, and the bitvector, x. Line 29 asserts to the SmtSolver that the returned values from the function applied to x and y are di erent. Lines 30 and 31 extract the bottom 8 bits from x and y, respectively. Line 33 asserts to the SmtSolver that the bottom bits of x and y are equivalent. Line 35 checks the satis ability of the current assertions and line 36 checks that the solver found SAT as expected. The query is satis able because x and y can have di erent most signi cant bits, and thus the function applications could return di erent values. Line 38 asserts to the SmtSolver that the most signi cant bits of x and y are also equivalent. Checking satis ability in line 41 and checking the result in line 42 con rms that the current set of assertions are now unsatis able because of uninterpreted function axioms. Figure 4 shows exactly the same example but through the Python API.
It is very simple to change the solver in these two examples, assuming that the relevant solver libraries have already been built. In the C++ example this amounts to including the relevant solver factory le (similar to line 2), updating line 9 to use a di erent solver factory create function, and nally recompiling and relinking with the new solver library. Assuming the Python bindings were built with the relevant solver, changing the solver in the Python example only requires using a di erent create function in line 5 of Figure 4. 5
The Smt-Switch code is distributed under the BSD 3-clause license. However, not all solvers have BSD-compatible licenses. For these solvers, the user must obtain the solver libraries themselves and ensure they meet all the requirements for the license. There are then instructions for how to properly build smt-switch with that solver as the backend, in which case the license assumes that of the solver. The BSD-compatible backend solvers are Boolector and CVC4. 6
The most closely related work is smt-kit [
Two other related tools are PySMT [
SmtSolver s = CVC4SolverFactory::create(false);
s->set_opt("incremental", "true");
Sort bvsort9 = s->make_sort(BV, 9);
Sort funsort = s->make_sort(FUNCTION, {bvsort9, bvsort9});
Term x = s->make_symbol("x", bvsort9);
Term y = s->make_symbol("y", bvsort9);
Term f = s->make_symbol("f", funsort);
Term fx = s->make_term(Apply, f, x);
Term fy = s->make_term(Apply, f, y);
// Functions are terms
assert(fx->get_op() == Apply);
TermVec fx_children(fx->begin(), fx->end());
assert(fx_children.size() == 2);
// These equalities are structural e.g. the first child *is* f
// These are not SMT equalities
assert(fx_children[0] == f);
assert(fx_children[
We have presented work in progress on Smt-Switch, a solver-agnostic API for performant
prototyping with SMT solvers in C++. This system is available for use on GitHub and has
already been used in projects [