From 5f444449a2d60364789010a9264959fab1e2fbcc Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Sun, 27 Feb 2011 11:04:04 +0000 Subject: [PATCH] Improvement. An analysis that simplifies ITES by determining what must be true/false down each branch. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1175 e59a4935-1847-0410-ae03-e826735625c1 --- src/AST/RunTimes.cpp | 2 +- src/AST/RunTimes.h | 3 +- src/STPManager/STP.cpp | 7 ++ src/simplifier/UseITEContext.h | 129 +++++++++++++++++++++++++++++++++ unit_test/ite.smt2 | 42 +++++++++++ 5 files changed, 181 insertions(+), 2 deletions(-) create mode 100644 src/simplifier/UseITEContext.h create mode 100644 unit_test/ite.smt2 diff --git a/src/AST/RunTimes.cpp b/src/AST/RunTimes.cpp index e411c7b..5d7abc4 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","Create SubstitutionMap", "Sending to SAT Solver", "Counter Example Generation","SAT Simplification", "Constant Bit Propagation","Array Read Refinement", "Applying Substitutions", "Remove Unconstrained", "Pure Literals" }; +std::string RunTimes::CategoryNames[] = { "Transforming", "Simplifying", "Parsing", "CNF Conversion", "Bit Blasting", "SAT Solving", "Bitvector Solving","Create SubstitutionMap", "Sending to SAT Solver", "Counter Example Generation","SAT Simplification", "Constant Bit Propagation","Array Read Refinement", "Applying Substitutions", "Remove Unconstrained", "Pure Literals" , "ITE Contexts"}; namespace BEEV { diff --git a/src/AST/RunTimes.h b/src/AST/RunTimes.h index 0c9bbd7..cde2269 100644 --- a/src/AST/RunTimes.h +++ b/src/AST/RunTimes.h @@ -34,7 +34,8 @@ public: ArrayReadRefinement, ApplyingSubstitutions, RemoveUnconstrained, - PureLiterals + PureLiterals, + UseITEContext }; static std::string CategoryNames[]; diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp index 5c32d9b..af29b22 100644 --- a/src/STPManager/STP.cpp +++ b/src/STPManager/STP.cpp @@ -18,6 +18,7 @@ #include "../simplifier/RemoveUnconstrained.h" #include "../simplifier/FindPureLiterals.h" #include "../simplifier/EstablishIntervals.h" +#include "../simplifier/UseITEContext.h" #include namespace BEEV { @@ -192,6 +193,12 @@ namespace BEEV { } } + // Simplify using Ite context + { + UseITEContext iteC(bm); + simplified_solved_InputToSAT = iteC.topLevel(simplified_solved_InputToSAT); + } + bm->ASTNodeStats("Before SimplifyWrites_Inplace begins: ", simplified_solved_InputToSAT); diff --git a/src/simplifier/UseITEContext.h b/src/simplifier/UseITEContext.h new file mode 100644 index 0000000..ba32f9d --- /dev/null +++ b/src/simplifier/UseITEContext.h @@ -0,0 +1,129 @@ +/* + * Descend through ITEs keeping a stack of what must be true/false. + * For instance. In the following: + * (ite (or a b) (not (or a b)) c ) + * + * In the lhs of the ITE, we know that a or b are true, so, we can rewrite it to: + * (ite (or a b) false c) + * + */ + +#ifndef UseITEContext_H_ +#define UseITEContext_H_ + +#include "../AST/AST.h" +#include "../STPManager/STPManager.h" + +namespace BEEV +{ + class UseITEContext + { + NodeFactory *nf; + RunTimes *runtimes; + ASTNode ASTTrue, ASTFalse; + + void addToContext(const ASTNode&n , ASTNodeSet& context) + { + if (n.GetKind() == NOT && n[0].GetKind() == OR) + { + ASTVec flat = FlattenKind(OR, n[0].GetChildren()); + for (int i = 0; i < flat.size(); i++) + context.insert(nf->CreateNode(NOT, flat[i])); + } + else if (n.GetKind() == AND) + { + ASTVec flat = FlattenKind(AND, n.GetChildren()); + context.insert(flat.begin(), flat.end()); + } + else + context.insert(n); + + //ASTNodeSet::iterator it = context.begin(); + //cout << "NEW CONTEXT"; + //while(it!=context.end()) + // { + // cout << *it; + // it++; + // } + } + + ASTNode + visit(const ASTNode &n, ASTNodeMap& visited, ASTNodeSet& context) + { + if (n.isConstant()) + return n; + + ASTNodeMap::iterator it; + if ((it = visited.find(n)) != visited.end()) + return it->second; + + if (context.find(n) != context.end()) + return ASTTrue; + + if (context.find(nf->CreateNode(NOT,n)) != context.end()) + return ASTFalse; + + if (n.isAtom()) + return n; + + ASTVec new_children; + + if (n.GetKind() == ITE) + { + ASTNodeSet lhsContext(context), rhsContext(context); + addToContext(n[0],lhsContext); + addToContext(nf->CreateNode(NOT,n[0]),rhsContext); + new_children.push_back(visit(n[0], visited,context)); + new_children.push_back(visit(n[1], visited,lhsContext)); + new_children.push_back(visit(n[2], visited,rhsContext)); + } + else + { + for (int i = 0; i < n.GetChildren().size(); i++) + new_children.push_back(visit(n[i], visited, context)); + } + + ASTNode result; + if (new_children != n.GetChildren()) + if (n.GetType() == BOOLEAN_TYPE) + result = nf->CreateNode(n.GetKind(), new_children); + else + result = nf->CreateArrayTerm(n.GetKind(), n.GetIndexWidth(), n.GetValueWidth(), new_children); + else + result = n; + + visited.insert(make_pair(n,result)); + return result; + + } + + public: + + ASTNode + topLevel(const ASTNode& n) + { + runtimes->start(RunTimes::UseITEContext); + ASTNodeMap visited; + ASTNodeSet context; + ASTNode result= visit(n,visited,context); + runtimes->stop(RunTimes::UseITEContext); + return result; + } + + UseITEContext(STPMgr *bm) + { + runtimes = bm->GetRunTimes(); + nf = new SimplifyingNodeFactory(*(bm->hashingNodeFactory) ,*bm); + ASTTrue = bm->ASTTrue; + ASTFalse = bm->ASTFalse; + } + + ~UseITEContext() + { + delete nf; + } + }; +} +; + +#endif diff --git a/unit_test/ite.smt2 b/unit_test/ite.smt2 new file mode 100644 index 0000000..ae7f809 --- /dev/null +++ b/unit_test/ite.smt2 @@ -0,0 +1,42 @@ + +(set-logic QF_BV) +(set-info :smt-lib-version 2.0) +(set-info :category "check") +(set-info :status sat) + +; These can be simplified by considering the context +; of the ITES they contain. + +(declare-fun a () Bool) +(declare-fun b () Bool) +(declare-fun c () Bool) +(assert (ite (or a b) (not (or a b)) c ) ) + +(declare-fun d () Bool) +(declare-fun e () Bool) +(assert (ite (and e d) e (and e d) ) ) + +(declare-fun f () Bool) +(declare-fun g () Bool) +(declare-fun h () Bool) +(assert (ite (or f g) (and g f) g ) ) + +(declare-fun i () Bool) +(declare-fun j () Bool) +(declare-fun k () Bool) +(assert (ite i (ite j i (not i)) i )) + +; This doesn't simplify nicely down yet:: +; 108:(OR +; 50:m +; 52:(AND +; 48:l +; 50:m)) +(declare-fun l () Bool) +(declare-fun m () Bool) +(assert (ite (not (and l m)) m l ) ) + + +(check-sat) +(exit) + -- 2.47.3