Miscellaneous improvements.

* Use the simplifying node factory in more places.
* If simplifications are turned off, don't simplify in the transformer.

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

diff --git a/src/AST/ArrayTransformer.cpp b/src/AST/ArrayTransformer.cpp
index e82e662e77d2f25f6146b0832df802f02d00c621..0c00bf2f31cafcb64d8d8f17bd8bf69422959dc1 100644 (file)
--- a/src/AST/ArrayTransformer.cpp
+++ b/src/AST/ArrayTransformer.cpp
@@ -301,7 +301,10 @@ namespace BEEV
         {
           ASTNode term1 = TransformTerm(simpleForm[0]);
           ASTNode term2 = TransformTerm(simpleForm[1]);
-          result = simp->CreateSimplifiedEQ(term1, term2);
+          if (bm->UserFlags.optimize_flag)
+                 result = simp->CreateSimplifiedEQ(term1, term2);
+          else
+                 result = nf->CreateNode(EQ,term1, term2);
           break;
         }
       case AND: // These could shortcut. Not sure if the extra effort is justified.
@@ -416,7 +419,10 @@ namespace BEEV
           {
                  thn = TransformTerm(thn);
                  els = TransformTerm(els);
-                 result = simp->CreateSimplifiedTermITE(cond, thn, els);
+                 if (bm->UserFlags.optimize_flag)
+                         result = simp->CreateSimplifiedTermITE(cond, thn, els);
+                 else
+                         result = nf->CreateTerm(ITE, thn.GetValueWidth(), cond, thn, els);
           }
           assert(result.GetIndexWidth() ==term.GetIndexWidth());
           break;

diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
index 2ea03fab9391f2036ecc2d9da44db6716935df2c..2339adefe29e34403544073ea78d6b95c79083c1 100644 (file)
--- a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
+++ b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
@@ -466,6 +466,13 @@ ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width,
 
        switch (kind)
        {
+       case BEEV::ITE:
+               if (children[0]== ASTTrue)
+                       result = children[1];
+               if (children[0]== ASTFalse)
+                       result = children[2];
+
+
 
        case BEEV::BVNEG:
        {

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index 41b6557b9f90b61aaa9310c25cc6da37b88c9c97..da3137ea776ad58d50cd4ce1cf8b5f2e456a1e32 100644 (file)
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -163,17 +163,19 @@ namespace BEEV {
 
     if (bm->UserFlags.bitConstantProp_flag)
       {
-        bm->ASTNodeStats("Before Constant Bit Propagation begins: ",
-            simplified_solved_InputToSAT);
-
         bm->GetRunTimes()->start(RunTimes::ConstantBitPropagation);
-        simplifier::constantBitP::ConstantBitPropagation cb(simp, bm->defaultNodeFactory,simplified_solved_InputToSAT);
+        SimplifyingNodeFactory nf(*(bm->hashingNodeFactory), *bm);
+        simplifier::constantBitP::ConstantBitPropagation cb(simp, &nf,simplified_solved_InputToSAT);
         simplified_solved_InputToSAT = cb.topLevelBothWays(simplified_solved_InputToSAT);
 
         bm->GetRunTimes()->stop(RunTimes::ConstantBitPropagation);
 
         if (cb.isUnsatisfiable())
           simplified_solved_InputToSAT = bm->ASTFalse;
+
+        bm->ASTNodeStats("After Constant Bit Propagation begins: ",
+            simplified_solved_InputToSAT);
+
       }
 
     if (bm->UserFlags.isSet("use-intervals","1"))
@@ -199,13 +201,12 @@ namespace BEEV {
         }
 
         // Simplify using Ite context
-        if (bm->UserFlags.isSet("ite-context","1"))
+        if (bm->UserFlags.optimize_flag &&  bm->UserFlags.isSet("ite-context","1"))
         {
           UseITEContext iteC(bm);
           simplified_solved_InputToSAT  = iteC.topLevel(simplified_solved_InputToSAT);
           bm->ASTNodeStats("After ITE Context: ",
                            simplified_solved_InputToSAT);
-
         }
 
         if (bm->UserFlags.isSet("aig-core-simplify","0"))

diff --git a/src/simplifier/EstablishIntervals.h b/src/simplifier/EstablishIntervals.h
index b08cdb449b2c60fd79fde5c1fcbf956733baea78..07e0c8b2c7baa910d02e3a9fa4e28d373108111f 100644 (file)
--- a/src/simplifier/EstablishIntervals.h
+++ b/src/simplifier/EstablishIntervals.h
@@ -8,6 +8,7 @@
 #include "../AST/AST.h"
 #include "../STPManager/STPManager.h"
 #include "simplifier.h"
+#include "../AST/NodeFactory/SimplifyingNodeFactory.h"
 
 
 namespace BEEV
@@ -88,9 +89,9 @@ private:
 
       if (fromTo.size() > 0)
         {
-          //cerr << "intervals found" << fromTo.size() << endl;
           ASTNodeMap cache;
-          return SubstitutionMap::replace(top,fromTo,cache,bm.defaultNodeFactory);
+          SimplifyingNodeFactory nf(*(top.GetSTPMgr()->defaultNodeFactory), *top.GetSTPMgr());
+          return SubstitutionMap::replace(top,fromTo,cache,&nf);
         }
 
       return top;

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 7d4f650d32fa838aaf9a11202165d550ecec4e87..7819e77c08e03c23f92cc4b575e16107a4e331fc 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -235,7 +235,8 @@ namespace BEEV
                                                bool pushNeg, 
                                                ASTNodeMap* VarConstMap)
   {
-    _bm->GetRunTimes()->start(RunTimes::SimplifyTopLevel);
+       assert(_bm->UserFlags.optimize_flag);
+       _bm->GetRunTimes()->start(RunTimes::SimplifyTopLevel);
     ASTNode out = SimplifyFormula(b, pushNeg, VarConstMap);
     ASTNodeSet visited;
     //checkIfInSimplifyMap(out,visited);
@@ -246,6 +247,7 @@ namespace BEEV
 
   ASTNode Simplifier::SimplifyTerm_TopLevel(const ASTNode& b)
   {
+       assert(_bm->UserFlags.optimize_flag);
     _bm->GetRunTimes()->start(RunTimes::SimplifyTopLevel);
     ASTNode out = SimplifyTerm(b);
     ResetSimplifyMaps();
@@ -505,7 +507,7 @@ namespace BEEV
        FatalError("never here",n);
     }
 
-    bool getPossibleValues(const ASTNode&n, ASTNodeSet& visited, vector<ASTNode>& found, int maxCount = 25)
+    bool getPossibleValues(const ASTNode&n, ASTNodeSet& visited, vector<ASTNode>& found, int maxCount = 45)
     {
        if (maxCount <=0)
                return false;