From b4519ef43d6e87754dc2f46108daf3cb9bbc312a Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Wed, 9 Mar 2011 06:42:07 +0000 Subject: [PATCH] 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 --- src/AST/ArrayTransformer.cpp | 10 ++++++++-- src/AST/NodeFactory/SimplifyingNodeFactory.cpp | 7 +++++++ src/STPManager/STP.cpp | 13 +++++++------ src/simplifier/EstablishIntervals.h | 5 +++-- src/simplifier/simplifier.cpp | 6 ++++-- 5 files changed, 29 insertions(+), 12 deletions(-) diff --git a/src/AST/ArrayTransformer.cpp b/src/AST/ArrayTransformer.cpp index e82e662..0c00bf2 100644 --- 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 2ea03fa..2339ade 100644 --- 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 41b6557..da3137e 100644 --- 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 b08cdb4..07e0c8b 100644 --- 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 7d4f650..7819e77 100644 --- 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& found, int maxCount = 25) + bool getPossibleValues(const ASTNode&n, ASTNodeSet& visited, vector& found, int maxCount = 45) { if (maxCount <=0) return false; -- 2.47.3