Improvement. Use the default node factory rather than specifying a node factory in...

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

diff --git a/src/AST/ArrayTransformer.h b/src/AST/ArrayTransformer.h
index 40930c05ae1d64ff648a0ae1e3048cb58b0756e6..d2bfcfb799f7030a03b5ff35a555127302d2f0b4 100644 (file)
--- a/src/AST/ArrayTransformer.h
+++ b/src/AST/ArrayTransformer.h
@@ -113,7 +113,7 @@ namespace BEEV
       debug_transform(0),
       TransformMap(NULL)
     {
-      nf = new SimplifyingNodeFactory(*(bm->hashingNodeFactory), *bm);
+      nf = bm->defaultNodeFactory;
 
       runTimes = bm->GetRunTimes();
       ASTTrue  = bm->CreateNode(TRUE);
@@ -121,11 +121,6 @@ namespace BEEV
       ASTUndefined = bm->CreateNode(UNDEFINED);
     }
 
-    ~ArrayTransformer()
-    {
-      delete nf;
-    }
-
     // Takes a formula, transforms it by replacing array reads with
     // variables, and returns the transformed formula
     ASTNode TransformFormula_TopLevel(const ASTNode& form);

diff --git a/src/AST/NodeFactory/HashingNodeFactory.h b/src/AST/NodeFactory/HashingNodeFactory.h
index 0d77fc22e02c187161af024e0f8711a5e1844186..5ef94879be370123e41b89c0c109623989f4b947 100644 (file)
--- a/src/AST/NodeFactory/HashingNodeFactory.h
+++ b/src/AST/NodeFactory/HashingNodeFactory.h
@@ -21,6 +21,7 @@ public:
        BEEV::ASTNode CreateNode(const BEEV::Kind kind, const BEEV::ASTVec & back_children);
        BEEV::ASTNode CreateTerm(BEEV::Kind kind, unsigned int width,const BEEV::ASTVec &children);
 
+       virtual std::string getName() {return "hashing";}
 };
 
 #endif /* HASHINGNODEFACTORY_H_ */

diff --git a/src/AST/NodeFactory/NodeFactory.h b/src/AST/NodeFactory/NodeFactory.h
index c16559155efa7934ad4724368544edab14e3bf02..41e2f3ac2a523c3283f0b5dea5133242298baf48 100644 (file)
--- a/src/AST/NodeFactory/NodeFactory.h
+++ b/src/AST/NodeFactory/NodeFactory.h
@@ -67,6 +67,7 @@ public:
 
        ASTNode CreateConstant(BEEV::CBV cbv, unsigned width);
 
+       virtual std::string getName()=0;
 };
 
 #endif

diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.h b/src/AST/NodeFactory/SimplifyingNodeFactory.h
index e55178f53913ca729bf5c3a7c53c2390ef2039f0..d1df19bb573b42c9a86e7f0e82114bc39483c4fe 100644 (file)
--- a/src/AST/NodeFactory/SimplifyingNodeFactory.h
+++ b/src/AST/NodeFactory/SimplifyingNodeFactory.h
@@ -56,6 +56,7 @@ public:
        virtual BEEV::ASTNode CreateNode(BEEV::Kind kind, const BEEV::ASTVec & children);
        virtual BEEV::ASTNode CreateTerm(BEEV::Kind kind, unsigned int width, const BEEV::ASTVec &children);
 
+       virtual std::string getName() {return "simplifying";}
 
        SimplifyingNodeFactory(NodeFactory& raw_, BEEV::STPMgr& bm_)
        :hashing(raw_), NodeFactory(bm_), ASTTrue(bm_.ASTTrue), ASTFalse(bm_.ASTFalse), ASTUndefined(bm_.ASTUndefined)

diff --git a/src/AST/NodeFactory/TypeChecker.h b/src/AST/NodeFactory/TypeChecker.h
index da5588dc74b5355d4a2a420361a6b7286f862ac6..87a3d27b5253e04f492780abfb2590d12291b945 100644 (file)
--- a/src/AST/NodeFactory/TypeChecker.h
+++ b/src/AST/NodeFactory/TypeChecker.h
@@ -26,6 +26,7 @@ public:
        BEEV::ASTNode CreateNode(BEEV::Kind kind, const BEEV::ASTVec& children);
        BEEV::ASTNode CreateArrayTerm(Kind kind, unsigned int index,unsigned int width, const BEEV::ASTVec &children);
 
+       virtual string getName() {return "type checking";}
 };
 
 #endif /* TYPECHECKER_H_ */

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index c8038111757fdaebe4572a0c6797ff769eb86681..58a1c39f73400153b5844871256a4a3d0deef4bd 100644 (file)
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -109,8 +109,7 @@ namespace BEEV {
     if (bm->UserFlags.isSet("bitblast-simplification", "1") && initial_difficulty_score < 250000)
       {
         BBNodeManagerAIG bbnm;
-        SimplifyingNodeFactory nf(*(bm->hashingNodeFactory), *bm);
-        BitBlaster<BBNodeAIG, BBNodeManagerAIG> bb(&bbnm, simp, &nf , &(bm->UserFlags));
+        BitBlaster<BBNodeAIG, BBNodeManagerAIG> bb(&bbnm, simp, bm->defaultNodeFactory , &(bm->UserFlags));
         ASTNodeMap fromTo;
         ASTNodeMap equivs;
         bb.getConsts(simplified_solved_InputToSAT, fromTo,equivs);
@@ -124,14 +123,14 @@ namespace BEEV {
              * difficult looking ASTNodes.
             */
             ASTNodeMap cache;
-            simplified_solved_InputToSAT = SubstitutionMap::replace(simplified_solved_InputToSAT, equivs, cache,&nf,false,true);
+            simplified_solved_InputToSAT = SubstitutionMap::replace(simplified_solved_InputToSAT, equivs, cache,bm->defaultNodeFactory,false,true);
             bm->ASTNodeStats(bb_message.c_str(), simplified_solved_InputToSAT);
           }
 
         if (fromTo.size() > 0)
           {
             ASTNodeMap cache;
-            simplified_solved_InputToSAT = SubstitutionMap:: replace(simplified_solved_InputToSAT, fromTo, cache,&nf);
+            simplified_solved_InputToSAT = SubstitutionMap:: replace(simplified_solved_InputToSAT, fromTo, cache,bm->defaultNodeFactory);
             bm->ASTNodeStats(bb_message.c_str(), simplified_solved_InputToSAT);
           }
         actualBBSize =  bbnm.totalNumberOfNodes();
@@ -144,6 +143,7 @@ namespace BEEV {
    ASTNode
   STP::sizeReducing(ASTNode simplified_solved_InputToSAT, BVSolver* bvSolver, PropagateEqualities *pe)
   {
+
     simplified_solved_InputToSAT = pe->topLevel(simplified_solved_InputToSAT, arrayTransformer);
     if (simp->hasUnappliedSubstitutions())
       {
@@ -170,8 +170,7 @@ namespace BEEV {
     if (bm->UserFlags.bitConstantProp_flag)
       {
         bm->GetRunTimes()->start(RunTimes::ConstantBitPropagation);
-        SimplifyingNodeFactory nf(*(bm->hashingNodeFactory), *bm);
-        simplifier::constantBitP::ConstantBitPropagation cb(simp, &nf, simplified_solved_InputToSAT);
+        simplifier::constantBitP::ConstantBitPropagation cb(simp, bm->defaultNodeFactory, simplified_solved_InputToSAT);
         simplified_solved_InputToSAT = cb.topLevelBothWays(simplified_solved_InputToSAT, true,false);
 
         bm->GetRunTimes()->stop(RunTimes::ConstantBitPropagation);
@@ -181,8 +180,8 @@ namespace BEEV {
 
         if (simp->hasUnappliedSubstitutions())
           {
-            simplified_solved_InputToSAT = simp->applySubstitutionMap(simplified_solved_InputToSAT);
-            simp->haveAppliedSubstitutionMap();
+          simplified_solved_InputToSAT = simp->applySubstitutionMap(simplified_solved_InputToSAT);
+          simp->haveAppliedSubstitutionMap();
           }
 
         bm->ASTNodeStats(cb_message.c_str(), simplified_solved_InputToSAT);
@@ -203,8 +202,7 @@ namespace BEEV {
 
     if (bm->UserFlags.isSet("always-true", "0"))
       {
-        SimplifyingNodeFactory nf(*(bm->hashingNodeFactory), *bm);
-        AlwaysTrue always (simp,bm,&nf);
+        AlwaysTrue always (simp,bm,bm->defaultNodeFactory);
         simplified_solved_InputToSAT = always.topLevel(simplified_solved_InputToSAT);
         bm->ASTNodeStats("After removing always true: ", simplified_solved_InputToSAT);
       }
@@ -345,8 +343,7 @@ namespace BEEV {
     if (bm->UserFlags.bitConstantProp_flag)
       {
         bm->GetRunTimes()->start(RunTimes::ConstantBitPropagation);
-        SimplifyingNodeFactory nf(*(bm->hashingNodeFactory), *bm);
-        simplifier::constantBitP::ConstantBitPropagation cb(simp, &nf, simplified_solved_InputToSAT);
+        simplifier::constantBitP::ConstantBitPropagation cb(simp, bm->defaultNodeFactory, simplified_solved_InputToSAT);
         simplified_solved_InputToSAT = cb.topLevelBothWays(simplified_solved_InputToSAT);
 
         bm->GetRunTimes()->stop(RunTimes::ConstantBitPropagation);
@@ -474,8 +471,7 @@ namespace BEEV {
     if (!worse && (bitblasted_difficulty != -1))
      {
         BBNodeManagerAIG bbnm;
-        SimplifyingNodeFactory nf(*(bm->hashingNodeFactory), *bm);
-        BitBlaster<BBNodeAIG, BBNodeManagerAIG> bb(&bbnm, simp, &nf , &(bm->UserFlags));
+        BitBlaster<BBNodeAIG, BBNodeManagerAIG> bb(&bbnm, simp, bm->defaultNodeFactory , &(bm->UserFlags));
         bb.BBForm(simplified_solved_InputToSAT);
         int newBB=  bbnm.totalNumberOfNodes();
         if (bm->UserFlags.stats_flag)

diff --git a/src/main/main.cpp b/src/main/main.cpp
index 25de09965f8501638298733582f29e5e484ed820..fd8f6e08cf1286598e74891b77c70eebf31d7de3 100644 (file)
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -78,7 +78,7 @@ static const intptr_t INITIAL_MEMORY_PREALLOCATION_SIZE = 4000000;
  * step 5. Call SAT to determine if input is SAT or UNSAT
  ********************************************************************/
 
-typedef enum {PRINT_BACK_C=1, PRINT_BACK_CVC, PRINT_BACK_SMTLIB2,PRINT_BACK_SMTLIB1, PRINT_BACK_GDL, PRINT_BACK_DOT, OUTPUT_BENCH, OUTPUT_CNF, USE_SIMPLIFYING_SOLVER, SMT_LIB2_FORMAT, SMT_LIB1_FORMAT, DISABLE_CBITP,EXIT_AFTER_CNF,USE_CRYPTOMINISAT_SOLVER,USE_MINISAT_SOLVER, DISABLE_SIMPLIFICATIONS, OLDSTYLE_REFINEMENT, DISABLE_EQUALITY, RANDOM_SEED} OptionType;
+typedef enum {PRINT_BACK_C=1, PRINT_BACK_CVC, PRINT_BACK_SMTLIB2,PRINT_BACK_SMTLIB1, PRINT_BACK_GDL, PRINT_BACK_DOT, OUTPUT_BENCH, OUTPUT_CNF, USE_SIMPLIFYING_SOLVER, SMT_LIB2_FORMAT, SMT_LIB1_FORMAT, DISABLE_CBITP,EXIT_AFTER_CNF,USE_CRYPTOMINISAT_SOLVER,USE_MINISAT_SOLVER, DISABLE_SIMPLIFICATIONS, OLDSTYLE_REFINEMENT, DISABLE_EQUALITY, RANDOM_SEED,HASHING_NF} OptionType;
 
 
 int main(int argc, char ** argv) {
@@ -97,6 +97,10 @@ int main(int argc, char ** argv) {
 
   STPMgr * bm       = new STPMgr();
 
+  auto_ptr<SimplifyingNodeFactory> simplifyingNF( new SimplifyingNodeFactory(*bm->hashingNodeFactory, *bm));
+  bm->defaultNodeFactory = simplifyingNF.get();
+
+  // The simplified keeps a pointer to whatever is set as the default node factory.
   Simplifier * simp  = new Simplifier(bm);
   auto_ptr<Simplifier> simpCleaner(simp);
 
@@ -120,10 +124,6 @@ int main(int argc, char ** argv) {
             Ctr_Example);
   
 
-  auto_ptr<SimplifyingNodeFactory> simplifyingNF( new SimplifyingNodeFactory(*bm->hashingNodeFactory, *bm));
-  bm->defaultNodeFactory = simplifyingNF.get();
-
-
   //populate the help string
   helpstring += 
     "STP version            : " + version + "\n"
@@ -196,6 +196,7 @@ int main(int argc, char ** argv) {
                          lookup.insert(make_pair(tolower("--oldstyle-refinement"),OLDSTYLE_REFINEMENT));
                          lookup.insert(make_pair(tolower("--disable-equality"),DISABLE_EQUALITY));
                          lookup.insert(make_pair(tolower("--random-seed"),RANDOM_SEED));
+                         lookup.insert(make_pair(tolower("--hash-nf"),HASHING_NF));
 
 
                          if (!strncmp(argv[i],"--config_",strlen("--config_")))
@@ -297,6 +298,9 @@ int main(int argc, char ** argv) {
                                 bm->UserFlags.random_seed = rand();
                             }
                             break;
+                          case HASHING_NF:
+                              bm->defaultNodeFactory = bm->hashingNodeFactory;
+                              break;
 
                          default:
                                  fprintf(stderr,usage,prog);
@@ -417,8 +421,8 @@ int main(int argc, char ** argv) {
 
   bm->GetRunTimes()->start(RunTimes::Parsing);
        {
-                TypeChecker nfTypeCheckSimp(*simplifyingNF.get(), *bm);
-               TypeChecker nfTypeCheckDefault(*bm->defaultNodeFactory, *bm);
+                TypeChecker nfTypeCheckSimp(*bm->defaultNodeFactory, *bm);
+               TypeChecker nfTypeCheckDefault(*bm->hashingNodeFactory, *bm);
 
                Cpp_interface piTypeCheckSimp(*bm, &nfTypeCheckSimp);
                Cpp_interface piTypeCheckDefault(*bm, &nfTypeCheckDefault);

diff --git a/src/simplifier/AIGSimplifyPropositionalCore.h b/src/simplifier/AIGSimplifyPropositionalCore.h
index 99b9dddb631a1626cc258b883d45fa10442d3fa2..354285f2c63a97447f46ef57e1bb8e59f0d2b591 100644 (file)
--- a/src/simplifier/AIGSimplifyPropositionalCore.h
+++ b/src/simplifier/AIGSimplifyPropositionalCore.h
@@ -33,13 +33,10 @@ public:
        AIGSimplifyPropositionalCore(STPMgr *_bm)
        {
                bm = _bm;
-               nf = new SimplifyingNodeFactory(*bm->hashingNodeFactory,*bm);
+               nf = _bm->defaultNodeFactory;
        }
 
-       virtual ~AIGSimplifyPropositionalCore()
-       {
-               delete nf;
-       }
+
 private:
 
        // Convert theory nodes to fresh variables.

diff --git a/src/simplifier/EstablishIntervals.h b/src/simplifier/EstablishIntervals.h
index 8e7a5f3ff3abc8dd73371a6f741b9afa8044baeb..7b720bf41ef105984619bf8ba2c9a983ac7014d4 100644 (file)
--- a/src/simplifier/EstablishIntervals.h
+++ b/src/simplifier/EstablishIntervals.h
@@ -308,9 +308,9 @@ namespace BEEV
       if (fromTo.size() > 0)
         {
           ASTNodeMap cache;
-          SimplifyingNodeFactory nf(*(top.GetSTPMgr()->hashingNodeFactory), *top.GetSTPMgr());
+
           bm.GetRunTimes()->stop(RunTimes::IntervalPropagation);
-          return SubstitutionMap::replace(result,fromTo,cache,&nf);
+          return SubstitutionMap::replace(result,fromTo,cache,top.GetSTPMgr()->defaultNodeFactory);
         }
 
       bm.GetRunTimes()->stop(RunTimes::IntervalPropagation);
@@ -792,7 +792,7 @@ namespace BEEV
       littleZero = makeCBV(1);
       littleOne = makeCBV(1);
       CONSTANTBV::BitVector_Fill(littleOne);
-      nf = new SimplifyingNodeFactory(*(bm.hashingNodeFactory), bm);
+      nf = bm.defaultNodeFactory;
     }
 
     ~EstablishIntervals()
@@ -805,7 +805,6 @@ namespace BEEV
 
       likeAutoPtr.clear();
       toDeleteLater.clear();
-      delete nf;
     }
   };
 }

diff --git a/src/simplifier/RemoveUnconstrained.cpp b/src/simplifier/RemoveUnconstrained.cpp
index e889fd608634d3af2dacedc419b6a6bc9f218a83..482734b988f5bc915113d745d815e0a5808a02ab 100644 (file)
--- a/src/simplifier/RemoveUnconstrained.cpp
+++ b/src/simplifier/RemoveUnconstrained.cpp
@@ -16,14 +16,9 @@ namespace BEEV
   RemoveUnconstrained::RemoveUnconstrained(STPMgr& _bm) :
     bm(_bm)
   {
-    nf = new SimplifyingNodeFactory(*(_bm.hashingNodeFactory),_bm);
+    nf = _bm.defaultNodeFactory;
  }
 
-  RemoveUnconstrained::~RemoveUnconstrained()
-  {
-    delete nf;
-  }
-
   const bool debug_unconstrained = false;
 
   ASTNode

diff --git a/src/simplifier/RemoveUnconstrained.h b/src/simplifier/RemoveUnconstrained.h
index 34f0961f7396c76007eee9ec2148212ed032b880..a7448130fcd69569d18bbe652ef3f2f8d5c7fe4b 100644 (file)
--- a/src/simplifier/RemoveUnconstrained.h
+++ b/src/simplifier/RemoveUnconstrained.h
@@ -41,10 +41,7 @@ namespace BEEV
 
   public:
 
-
     RemoveUnconstrained(STPMgr& bm);
-    virtual
-    ~RemoveUnconstrained();
 
     ASTNode
     topLevel(const ASTNode &n, Simplifier *s);

diff --git a/src/simplifier/SubstitutionMap.cpp b/src/simplifier/SubstitutionMap.cpp
index 1f785843acf28d52696d3bd755bf95f990204063..7d6ca39ae780ccad5069e5c83834163d29775262 100644 (file)
--- a/src/simplifier/SubstitutionMap.cpp
+++ b/src/simplifier/SubstitutionMap.cpp
@@ -8,7 +8,6 @@ namespace BEEV
   SubstitutionMap::~SubstitutionMap()
   {
     delete SolverMap;
-    delete nf;
   }
 
 // if false. Don't simplify while creating the substitution map.

diff --git a/src/simplifier/SubstitutionMap.h b/src/simplifier/SubstitutionMap.h
index c1292bc7357ee472a782ba59171ff56de808d906..0a11f0bf92bbdaeb79d3494b56fddb49d22a541e 100644 (file)
--- a/src/simplifier/SubstitutionMap.h
+++ b/src/simplifier/SubstitutionMap.h
@@ -75,7 +75,7 @@ namespace BEEV
       SolverMap = new ASTNodeMap(INITIAL_TABLE_SIZE);
       loopCount = 0;
       substitutionsLastApplied = 0;
-      nf = new SimplifyingNodeFactory(*bm->hashingNodeFactory, *bm);
+      nf = bm->defaultNodeFactory;
     }
 
     void

diff --git a/src/simplifier/UseITEContext.h b/src/simplifier/UseITEContext.h
index 2769681b728dd1266492140fb0e5a1d8239a25be..5d960c425d9e7466a47014b8a3727ba7671645de 100644 (file)
--- a/src/simplifier/UseITEContext.h
+++ b/src/simplifier/UseITEContext.h
@@ -119,15 +119,12 @@ namespace BEEV
     UseITEContext(STPMgr *bm)
     {
       runtimes = bm->GetRunTimes();
-      nf = new SimplifyingNodeFactory(*(bm->hashingNodeFactory) ,*bm);
+      nf = bm->defaultNodeFactory;
       ASTTrue = bm->ASTTrue;
       ASTFalse = bm->ASTFalse;
     }
 
-    ~UseITEContext()
-    {
-      delete nf;
-    }
+
   };
 }
 ;

diff --git a/src/simplifier/bvsolver.h b/src/simplifier/bvsolver.h
index 5b250b6d78fe7307bfb731f79cd54fac2ae54f3d..5dcb4dec43846106f42df7c07814df6ec2c33c38 100644 (file)
--- a/src/simplifier/bvsolver.h
+++ b/src/simplifier/bvsolver.h
@@ -118,14 +118,13 @@ namespace BEEV
       ASTFalse = _bm->CreateNode(FALSE);
       ASTUndefined = _bm->CreateNode(UNDEFINED);
       simplify=true;
-      nf = new SimplifyingNodeFactory(*bm->hashingNodeFactory,*bm);
+      nf = bm->defaultNodeFactory;
     };
 
      //Destructor
     ~BVSolver()
       {
        ClearAllTables();
-       delete nf;
       }
 
     //Top Level Solver: Goes over the input DAG, identifies the

diff --git a/src/simplifier/simplifier.h b/src/simplifier/simplifier.h
index cc3f864b90be72426b7ac1cf3ee67f015d16130f..95f384cd9f52c1d462b2d79e37fb901d054b378e 100644 (file)
--- a/src/simplifier/simplifier.h
+++ b/src/simplifier/simplifier.h
@@ -80,7 +80,7 @@ namespace BEEV
       ASTFalse = bm->CreateNode(FALSE);
       ASTUndefined = bm->CreateNode(UNDEFINED);
 
-      nf = new SimplifyingNodeFactory(*bm->hashingNodeFactory,*bm);
+      nf = bm->defaultNodeFactory;
     }
       
     ~Simplifier()
@@ -88,7 +88,6 @@ namespace BEEV
       delete SimplifyMap;
       delete SimplifyNegMap;
       //delete ReadOverWrite_NewName_Map;
-      delete nf;
     }
 
     /****************************************************************