From 8ebb6a3335e45301095d4e0af49e4a65a7399a70 Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Mon, 14 Mar 2011 03:38:14 +0000
Subject: [PATCH] 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
---
 src/simplifier/bvsolver.cpp | 6 +++---
 src/simplifier/bvsolver.h   | 6 +++++-
 2 files changed, 8 insertions(+), 4 deletions(-)

diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp
index 4701444..49d306a 100644
--- 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 7de29c9..bb3456f 100644
--- 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
-- 
2.47.3