From e5749ef5913a98b4ec2c104664a610e691262499 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Sun, 1 May 2011 12:48:53 +0000 Subject: [PATCH] Code to apply the alwaysTrueSet. Not currently enabled. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1297 e59a4935-1847-0410-ae03-e826735625c1 --- src/AST/RunTimes.cpp | 2 +- src/AST/RunTimes.h | 3 +- src/STPManager/STP.cpp | 19 ++++++ src/simplifier/AlwaysTrue.h | 113 ++++++++++++++++++++++++++++++++++++ 4 files changed, 135 insertions(+), 2 deletions(-) create mode 100644 src/simplifier/AlwaysTrue.h diff --git a/src/AST/RunTimes.cpp b/src/AST/RunTimes.cpp index 74bda59..a7adb9c 100644 --- a/src/AST/RunTimes.cpp +++ b/src/AST/RunTimes.cpp @@ -16,7 +16,7 @@ #include "../sat/utils/System.h" // BE VERY CAREFUL> Update the Category Names to match. -std::string RunTimes::CategoryNames[] = { "Transforming", "Simplifying", "Parsing", "CNF Conversion", "Bit Blasting", "SAT Solving", "Bitvector Solving","Variable Elimination", "Sending to SAT Solver", "Counter Example Generation","SAT Simplification", "Constant Bit Propagation","Array Read Refinement", "Applying Substitutions", "Removing Unconstrained", "Pure Literals" , "ITE Contexts", "AIG core simplification", "Interval Propagation"}; +std::string RunTimes::CategoryNames[] = { "Transforming", "Simplifying", "Parsing", "CNF Conversion", "Bit Blasting", "SAT Solving", "Bitvector Solving","Variable Elimination", "Sending to SAT Solver", "Counter Example Generation","SAT Simplification", "Constant Bit Propagation","Array Read Refinement", "Applying Substitutions", "Removing Unconstrained", "Pure Literals" , "ITE Contexts", "AIG core simplification", "Interval Propagation", "Always True"}; namespace BEEV { diff --git a/src/AST/RunTimes.h b/src/AST/RunTimes.h index 4a558e6..f198397 100644 --- a/src/AST/RunTimes.h +++ b/src/AST/RunTimes.h @@ -37,7 +37,8 @@ public: PureLiterals, UseITEContext, AIGSimplifyCore, - IntervalPropagation + IntervalPropagation, + AlwaysTrue }; static std::string CategoryNames[]; diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp index e87ea4c..1c5478f 100644 --- a/src/STPManager/STP.cpp +++ b/src/STPManager/STP.cpp @@ -19,6 +19,7 @@ #include "../simplifier/FindPureLiterals.h" #include "../simplifier/EstablishIntervals.h" #include "../simplifier/UseITEContext.h" +#include "../simplifier/AlwaysTrue.h" #include "../simplifier/AIGSimplifyPropositionalCore.h" #include @@ -146,6 +147,15 @@ namespace BEEV { bm->ASTNodeStats("After Pure Literals: ", simplified_solved_InputToSAT); } } + + if (bm->UserFlags.isSet("always-true", "0")) + { + SimplifyingNodeFactory nf(*(bm->hashingNodeFactory), *bm); + AlwaysTrue always (simp,bm,&nf); + simplified_solved_InputToSAT = always.topLevel(simplified_solved_InputToSAT); + bm->ASTNodeStats("After removing always true: ", simplified_solved_InputToSAT); + } + if (bm->UserFlags.wordlevel_solve_flag && bm->UserFlags.optimize_flag) { simplified_solved_InputToSAT = bvSolver->TopLevelBVSolve(simplified_solved_InputToSAT, false); @@ -341,6 +351,15 @@ namespace BEEV { simplified_solved_InputToSAT = simp->SimplifyFormula_TopLevel(simplified_solved_InputToSAT, false); bm->ASTNodeStats("after simplification: ", simplified_solved_InputToSAT); + + + if (bm->UserFlags.isSet("always-true", "0")) + { + SimplifyingNodeFactory nf(*(bm->hashingNodeFactory), *bm); + AlwaysTrue always (simp,bm,&nf); + simplified_solved_InputToSAT = always.topLevel(simplified_solved_InputToSAT); + bm->ASTNodeStats("After removing always true: ", simplified_solved_InputToSAT); + } } // The word level solver uses the simplifier to apply the rewrites it makes, diff --git a/src/simplifier/AlwaysTrue.h b/src/simplifier/AlwaysTrue.h new file mode 100644 index 0000000..878e01f --- /dev/null +++ b/src/simplifier/AlwaysTrue.h @@ -0,0 +1,113 @@ +#ifndef ALWAYSTRUE_H_ +#define ALWAYSTRUE_H_ + +//Applies the AlwaysTrueSet to the input node. + +#include +#include "../AST/AST.h" +#include "../STPManager/STPManager.h" +#include "../simplifier/simplifier.h" + +namespace BEEV +{ + +class AlwaysTrue +{ + Simplifier *simplifier; + STPMgr* stp; + NodeFactory *nf; + + enum State {AND_STATE, NOT_STATE, BOTTOM_STATE}; + +public: + AlwaysTrue(Simplifier *simplifier_, STPMgr* stp_, NodeFactory *nf_) + { + simplifier = simplifier_; + stp = stp_; + nf = nf_; + } + + virtual + ~AlwaysTrue() + {} + + ASTNode topLevel(ASTNode& n) + { + stp->GetRunTimes()->start(RunTimes::AlwaysTrue); + ASTNodeMap fromTo; + ASTNode result = visit(n,AND_STATE,fromTo); + stp->GetRunTimes()->stop(RunTimes::AlwaysTrue); + return result; + } + + // Replace nodes that aren't conjoined to the top with TRUE/FALSE, + // if that node is conjoined.. + // The "state" tracks whether we are still at nodes that are conjoined to the top, + // only after we get out of the top part can we replace nodes that we know to be + // true or false. + ASTNode visit(const ASTNode&n, State state, ASTNodeMap& fromTo) + { + if (n.isConstant()) + return n; + + if (fromTo.find(n) != fromTo.end()) + { + // It has been visited as BOTTOM_STATE once before. + return fromTo.find(n)->second; + } + + ASTVec newChildren; + newChildren.reserve(n.Degree()); + State new_state; + + if (state == BOTTOM_STATE) + { + bool result; + if (simplifier->CheckAlwaysTrueFormSet(n,result)) + { + cerr << "+"; + if (result) + return stp->ASTTrue; + else + return stp->ASTFalse; + } + } + + if (n.GetKind() == SYMBOL) + return n; + + if (n.GetKind() != AND && state == AND_STATE ) + { + if (n.GetKind() == NOT) + new_state = NOT_STATE; + else + new_state = BOTTOM_STATE; + } + else if (state == NOT_STATE) + new_state = BOTTOM_STATE; + else + new_state = state; + + for (int i=0; i < n.Degree(); i++) + { + newChildren.push_back(visit(n[i],new_state,fromTo)); + } + + ASTNode result = n; + if (newChildren != n.GetChildren()) + { + if (n.GetType() == BOOLEAN_TYPE) + result = nf->CreateNode(n.GetKind(), newChildren); + else + result = nf->CreateArrayTerm(n.GetKind(), n.GetIndexWidth(), n.GetValueWidth(), newChildren); + } + + if (state == BOTTOM_STATE) + { + fromTo.insert(make_pair(n,result)); + } + return result; + } +}; +}; +#endif -- 2.47.3