Build your solver

OpenSMT was designed with an idea of easy extension and customization in mind. Building a new solver requires to implement a simple interface derived from TSolver class.

  class TSolver 
  {
   void   inform        ( Enode * ); 
   bool   assertLit     ( Enode * ); 
   bool   check         ( bool ); 

   void   pushBktPoint  ( ); 
   void   popBktPoint   ( ); 
   bool   belongsToT    ( Enode * ); 
   void   computeModel  ( ); 

   vector <  Enode *  >  & explanation; 
   vector <  Enode *  >  & deductions; 
   vector <  Enode *  >  & suggestions; 
  }

Interface that T-solver is required to implement is minimalistic. inform is used to communicate the existence of a new T-atom to the T-solver. assertLit asserts a (previously informed) T-atom in the T-solver with the right polarity; it may also perform some cheap form of consistency check. check determines the T-satisfiability of the current set of asserted T-atoms. pushBktPoint and popBktPoint are used respectively to save and to restore the state of the T-solver, in order to cope with backtracking within the SAT-Solver. belongsToT is used to determine if a given T-atom belongs to the theory solved by the T-solver. Finally computeModel forces T-solverto save the model (if any) inside Enode's field.

Three vectors, explanation, deductions, suggestions, are shared among the T-solvers, and they are used to simplify the communication of conflicts, T-atoms to be deduced and "suggested" T-atoms. Suggestions are atoms consistent with the current state of the T-solver, but that they cannot be directly deduced. Suggestions are used to perform decisions in the SAT-Solver.

Explanations for deductions are computed on demand. When an explanation for a deduction l is required, the literal not(l) is pushed in the T-solver, and the explanation is computed by calling check. This process is completely transparent for the T-solverthus avoiding any burden for generating and tracking explanations for deductions on the T-solver side.

How-to extend OpenSMT with your solver

In this tutorial we show how to extend OpenSMT with a new theory solver. For the sake of explanation, we will assume the following:

• we have an alternative decision procedure (X-solver) for a logic QF_X, defined as a class Xdp implemented in Xdp.C and Xdp.h files
• the procedure implements the interface described above
• we are working in a common Unix/Linux environment

The integration of the new decision procedure can be executed in three simple macro steps.

Step 1: setting up the environment for the new solver.

This is usually the most tedious operation, as it requires to understand the software organization and compilation mechanism. However we provide a script create_tsolver.sh that takes care of setting up the environment automatically.

In OpenSMT, the ordinary theory solvers are defined in the subdirectory src/tsolvers

  user:~$ ls
  OpenSMT xsolver
  user:~$ cd OpenSMT
  user:OpenSMT$ ls src/tsolvers
  bvsolver dlsolver  emptysolver  lrasolver  Makefile.am
  Makefile.in THandler.C  THandler.h  tsolver  TSolver.h

We use the script create_tsolver.sh to create a wrapper for the X - solver as follows:

  user:OpenSMT$ ./create_tsolver.sh XSolver xsolver
  Creating src/tsolvers/xsolver/XSolver.C src/tsolvers/xsolver/XSolver.h
  Creating src/tsolvers/xsolver/Makefile.am
  [Backing up src/tsolvers/Makefile.am as src/tsolvers/.Makefile.am.old]
  Modifying src/tsolvers/xsolver/Makefile.am
  [Backing up configure.ac as .configure.ac.old]
  Modifying configure.ac
  Reconfiguring

The script above created a wrapper XSolver.C , XSolver.h in a subdirectory xsolver, and it adjusted the makefiles to support the new files in the compilation. The configure script was also updated.

  user:OpenSMT$ ls src/tsolvers
  bvsolver dlsolver  emptysolver  lrasolver  Makefile.am  
  Makefile.in THandler.C  THandler.h  tsolver  TSolver.h
  xsolver
  user:OpenSMT$ ls src/tsolvers/xsolver
  Makefile.am  Makefile.in  XSolver.C  XSolver.h

Step 2: integration with the new solver.

In this step we link the wrapper with the actual implementation for the procedure. First, we copy the X-solver's files in the created subdirectoy under src/tsolvers .

  user:OpenSMT$ cp ../xsolver/Xdp.* src/tsolvers/xsolver

The connection with the methods of Xdp has to be specified inside XSolver.h and XSolver.C . In XSolver.h we add the right header file and a pointer to Xdp class

  #include "Xdp.h" // Header file
  ...
  Xdp * xdp;       // Pointer to dp class
  ...

In XSolver.C we link the methods of the wrapper with the ones of Xdp

  ...
  XSolver::XSolver( ... )
  {
    xdp = new Xdp( ); 
  }

  XSolver::~XSolver( )
  {
    delete xdp;
  }
  ...
  bool XSolver::check( bool complete )
  {
    return xdp->check( );
  }
  ...

Then we edit src/tsolvers/xsolver/Makefile.am to include the compilation of Xdp.C and Xdp.h .

Step 3: implementation of translation methods.

This step is required to translate the data structures for representing terms of OpenSMT. These are the only functions whose implementation depends on the particular procedure to consider. Examples can be found in the already existing solvers under src/tsolvers . The initialization of the solver can be set up in src/EgraphSolver.C .