Initial KLEE checkin.

 - Lots more tweaks, documentation, and web page content is needed,
   but this should compile & work on OS X & Linux.


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72205 91177308-0d34-0410-b5e6-96231b3b80d8

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