diff options
Diffstat (limited to 'stp/simplifier/bvsolver.h')
-rw-r--r-- | stp/simplifier/bvsolver.h | 134 |
1 files changed, 134 insertions, 0 deletions
diff --git a/stp/simplifier/bvsolver.h b/stp/simplifier/bvsolver.h new file mode 100644 index 00000000..a8981b12 --- /dev/null +++ b/stp/simplifier/bvsolver.h @@ -0,0 +1,134 @@ +/******************************************************************** + * AUTHORS: Vijay Ganesh, David L. Dill + * + * BEGIN DATE: November, 2005 + * + * LICENSE: Please view LICENSE file in the home dir of this Program + ********************************************************************/ +// -*- c++ -*- + +#include "../AST/AST.h" +#include "../AST/ASTUtil.h" +namespace BEEV { + + //This class represents the bitvector arithmetic linear solver. + // + //The bitvector solver is a partial solver, i.e. it does not solve + //for all variables in the system of equations. it is + //best-effort. it relies on the SAT solver to be complete. + // + //The BVSolver assumes that the input equations are normalized, and + //have liketerms combined etc. + // + //0. Traverse top-down over the input DAG, looking for a conjunction + //0. of equations. if you find one, then for each equation in the + //0. conjunction, do the following steps. + // + //1. check for Linearity of the input equation + // + //2. Solve for a "chosen" variable. The variable should occur + //2. exactly once and must have an odd coeff. Refer STP's CAV 2007 + //2. paper for actual solving procedure + // + //4. Outside the solver, Substitute and Re-normalize the input DAG + class BVSolver { + //Ptr to toplevel manager that manages bit-vector expressions + //(i.e. construct various kinds of expressions), and also has + //member functions that simplify bit-vector expressions + BeevMgr * _bm; + ASTNode ASTTrue, ASTFalse; + + //Those formulas which have already been solved. If the same + //formula occurs twice then do not solve the second occurence, and + //instead drop it + ASTNodeMap FormulasAlreadySolvedMap; + + //this map is useful while traversing terms and uniquely + //identifying variables in the those terms. Prevents double + //counting. + ASTNodeMap TermsAlreadySeenMap; + ASTNodeMap TermsAlreadySeenMap_ForArrays; + + //count is used in the creation of new variables + unsigned int _symbol_count; + + //solved variables list: If a variable has been solved for then do + //not solve for it again + ASTNodeSet DoNotSolve_TheseVars; + + //checks if var has been solved for or not. if yes, then return + //true else return false + bool DoNotSolveThis(const ASTNode& var); + + //traverses a term, and creates a multiset of all variables in the + //term. Does memoization to avoid double counting. + void VarsInTheTerm(const ASTNode& lhs, ASTNodeMultiSet& v); + void VarsInTheTerm_TopLevel(const ASTNode& lhs, ASTNodeMultiSet& v); + + //choose a suitable var from the term + ASTNode ChooseMonom(const ASTNode& eq, ASTNode& modifiedterm); + //accepts an equation and solves for a variable or a monom in it + ASTNode BVSolve_Odd(const ASTNode& eq); + + //solves equations of the form a*x=t where 'a' is even. Has a + //return value, unlike the normal BVSolve() + ASTNode BVSolve_Even(const ASTNode& eq); + ASTNode CheckEvenEqn(const ASTNode& input, bool& evenflag); + + //Checks for arrayreads in a term. if yes then returns true, else + //return false + bool CheckForArrayReads(const ASTNode& term); + bool CheckForArrayReads_TopLevel(const ASTNode& term); + + //Creates new variables used in solving + ASTNode NewVar(unsigned int n); + + //this function return true if the var occurs in term, else the + //function returns false + bool VarSeenInTerm(const ASTNode& var, const ASTNode& term); + + //takes an even number "in" as input, and returns an odd number + //(return value) and a power of 2 (as number_shifts by reference), + //such that in = (odd_number * power_of_2). + // + //Refer STP's CAV 2007 (or Clark Barrett's 1998 paper on + //bit-vector arithmetic published in DAC 1998) paper for precise + //understanding of the algorithm + ASTNode SplitEven_into_Oddnum_PowerOf2(const ASTNode& in, unsigned int& number_shifts); + + //Once a formula has been solved, then update the alreadysolvedmap + //with the formula, and the solved value. The solved value can be + //described using the following example: Suppose input to the + //solver is + // + // input key: x = 2 AND y = x + t + // + // output value: y = 2 + t + void UpdateAlreadySolvedMap(const ASTNode& key, const ASTNode& value); + + //This function checks if the key (formula) has already been + //solved for. + // + //If yes it returns TRUE and fills the "output" with the + //solved-value (call by reference argument), + // + //else returns FALSE + bool CheckAlreadySolvedMap(const ASTNode& key, ASTNode& output); + public: + //constructor + BVSolver(BeevMgr * bm) : _bm(bm), _symbol_count(0) { + ASTTrue = _bm->CreateNode(TRUE); + ASTFalse = _bm->CreateNode(FALSE); + }; + + //Destructor + ~BVSolver() { + TermsAlreadySeenMap.clear(); + DoNotSolve_TheseVars.clear(); + } + + //Top Level Solver: Goes over the input DAG, identifies the + //equation to be solved, solves them, + ASTNode TopLevelBVSolve(const ASTNode& a); + }; //end of class bvsolver +};//end of namespace BEEV |