From b6f2ab19367661f35605cfce30dc8746fb90960a Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Tue, 20 Mar 2012 03:59:03 +0000 Subject: [PATCH] Improvement. Use the default node factory rather than specifying a node factory in some places like I used to do. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1603 e59a4935-1847-0410-ae03-e826735625c1 --- src/AST/ArrayTransformer.h | 7 +----- src/AST/NodeFactory/HashingNodeFactory.h | 1 + src/AST/NodeFactory/NodeFactory.h | 1 + src/AST/NodeFactory/SimplifyingNodeFactory.h | 1 + src/AST/NodeFactory/TypeChecker.h | 1 + src/STPManager/STP.cpp | 24 ++++++++----------- src/main/main.cpp | 18 ++++++++------ src/simplifier/AIGSimplifyPropositionalCore.h | 7 ++---- src/simplifier/EstablishIntervals.h | 7 +++--- src/simplifier/RemoveUnconstrained.cpp | 7 +----- src/simplifier/RemoveUnconstrained.h | 3 --- src/simplifier/SubstitutionMap.cpp | 1 - src/simplifier/SubstitutionMap.h | 2 +- src/simplifier/UseITEContext.h | 7 ++---- src/simplifier/bvsolver.h | 3 +-- src/simplifier/simplifier.h | 3 +-- 16 files changed, 37 insertions(+), 56 deletions(-) diff --git a/src/AST/ArrayTransformer.h b/src/AST/ArrayTransformer.h index 40930c0..d2bfcfb 100644 --- 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 0d77fc2..5ef9487 100644 --- 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 c165591..41e2f3a 100644 --- 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 e55178f..d1df19b 100644 --- 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 da5588d..87a3d27 100644 --- 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 c803811..58a1c39 100644 --- 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 bb(&bbnm, simp, &nf , &(bm->UserFlags)); + BitBlaster 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 bb(&bbnm, simp, &nf , &(bm->UserFlags)); + BitBlaster 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 25de099..fd8f6e0 100644 --- 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 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 simpCleaner(simp); @@ -120,10 +124,6 @@ int main(int argc, char ** argv) { Ctr_Example); - auto_ptr 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 99b9ddd..354285f 100644 --- 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 8e7a5f3..7b720bf 100644 --- 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 e889fd6..482734b 100644 --- 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 34f0961..a744813 100644 --- 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 1f78584..7d6ca39 100644 --- 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 c1292bc..0a11f0b 100644 --- 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 2769681..5d960c4 100644 --- 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 5b250b6..5dcb4de 100644 --- 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 cc3f864..95f384c 100644 --- 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; } /**************************************************************** -- 2.47.3