Improvement. Start to use the simplifying node factory in the bvsolver.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1212 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp
index 470144473aa28be4526783989f4a3a64b503c4a5..49d306aa2b00ded5d2fd696508b55392dba086a3 100644 (file)
--- a/src/simplifier/bvsolver.cpp
+++ b/src/simplifier/bvsolver.cpp
@@ -670,7 +670,7 @@ namespace BEEV
       output_children.push_back(r);
       }
 
-    return _bm->CreateNode(AND, output_children);
+    return nf->CreateNode(AND, output_children);
 
   }
 
@@ -803,11 +803,11 @@ namespace BEEV
     output = 
       (o.size() > 0) ? 
       ((o.size() > 1) ? 
-       _bm->CreateNode(AND, o) : 
+       nf->CreateNode(AND, o) :
        o[0]) : 
       ASTTrue;
     if (evens != ASTTrue)
-      output = _bm->CreateNode(AND, output, evens);
+      output = nf->CreateNode(AND, output, evens);
 
     if (_bm->UserFlags.isSet("xor-solve","1"))
       output = solveForAndOfXOR(output);

diff --git a/src/simplifier/bvsolver.h b/src/simplifier/bvsolver.h
index 7de29c941770cf78ee1366db37a006283bf48a9e..bb3456f9a3e3112488e236f7cb226ee36327d934 100644 (file)
--- a/src/simplifier/bvsolver.h
+++ b/src/simplifier/bvsolver.h
@@ -115,10 +115,12 @@ namespace BEEV
 
     VariablesInExpression& vars;
 
-    bool simplify;
+    bool simplify; //Whether to apply the simplifyTerm & simplifyFormula functions.
 
     ASTNode simplifyNode(const ASTNode n);
 
+    NodeFactory* nf;
+
   public:
     //constructor
   BVSolver(STPMgr * bm, Simplifier * simp) : _bm(bm), _simp(simp), vars(simp->getVariablesInExpression())
@@ -127,12 +129,14 @@ namespace BEEV
       ASTFalse = _bm->CreateNode(FALSE);
       ASTUndefined = _bm->CreateNode(UNDEFINED);
       simplify=true;
+      nf = new SimplifyingNodeFactory(*bm->hashingNodeFactory,*bm);
     };
 
      //Destructor
     ~BVSolver()
       {
        ClearAllTables();
+       delete nf;
       }
 
     //Top Level Solver: Goes over the input DAG, identifies the