From cd69090eafb404ec3a690dfa2624c732dc047dbc Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Tue, 22 Feb 2011 00:19:08 +0000 Subject: [PATCH] Improvement. The start of an unsigned interval simplification. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1157 e59a4935-1847-0410-ae03-e826735625c1 --- src/STPManager/STP.cpp | 21 ++-- src/simplifier/EstablishIntervals.cpp | 8 ++ src/simplifier/EstablishIntervals.h | 169 ++++++++++++++++++++++++++ 3 files changed, 191 insertions(+), 7 deletions(-) create mode 100644 src/simplifier/EstablishIntervals.cpp create mode 100644 src/simplifier/EstablishIntervals.h diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp index c7f137a..cb45371 100644 --- a/src/STPManager/STP.cpp +++ b/src/STPManager/STP.cpp @@ -17,6 +17,7 @@ #include "../sat/CryptoMinisat.h" #include "../simplifier/RemoveUnconstrained.h" #include "../simplifier/FindPureLiterals.h" +#include "../simplifier/EstablishIntervals.h" #include namespace BEEV { @@ -170,9 +171,14 @@ namespace BEEV { if (cb.isUnsatisfiable()) simplified_solved_InputToSAT = bm->ASTFalse; - } + { + EstablishIntervals intervals(*bm); + simplified_solved_InputToSAT = intervals.topLevel_unsignedIntervals(simplified_solved_InputToSAT ); + } + + // Find pure literals. if (bm->UserFlags.isSet("pure-literals","1")) { @@ -212,7 +218,7 @@ namespace BEEV { bm->ASTNodeStats("after pure substitution: ", simplified_solved_InputToSAT); - simplified_solved_InputToSAT = + simplified_solved_InputToSAT = simp->SimplifyFormula_TopLevel(simplified_solved_InputToSAT, false); bm->ASTNodeStats("after simplification: ", @@ -236,13 +242,14 @@ namespace BEEV { if (bm->UserFlags.isSet("enable-unconstrained","1")) { - // Remove unconstrained. - RemoveUnconstrained r(*bm); - simplified_solved_InputToSAT = r.topLevel(simplified_solved_InputToSAT, simp); - bm->ASTNodeStats("After Unconstrained Remove begins: ", - simplified_solved_InputToSAT); + // Remove unconstrained. + RemoveUnconstrained r(*bm); + simplified_solved_InputToSAT = r.topLevel(simplified_solved_InputToSAT, simp); + bm->ASTNodeStats("After Unconstrained Remove begins: ", + simplified_solved_InputToSAT); } + bm->TermsAlreadySeenMap_Clear(); bm->start_abstracting = false; diff --git a/src/simplifier/EstablishIntervals.cpp b/src/simplifier/EstablishIntervals.cpp new file mode 100644 index 0000000..eafde83 --- /dev/null +++ b/src/simplifier/EstablishIntervals.cpp @@ -0,0 +1,8 @@ +#include "EstablishIntervals.h" +namespace BEEV +{ + + vector EstablishIntervals::toDeleteLater; + vector EstablishIntervals::likeAutoPtr; + +}; diff --git a/src/simplifier/EstablishIntervals.h b/src/simplifier/EstablishIntervals.h new file mode 100644 index 0000000..dff603d --- /dev/null +++ b/src/simplifier/EstablishIntervals.h @@ -0,0 +1,169 @@ +/* + * Performs a very basic unsigned interval analysis. + * Currently it only has a couple of basic operations. + */ + +#ifndef ESTABLISHINTERVALS_H_ +#define ESTABLISHINTERVALS_H_ +#include "../AST/AST.h" +#include "../STPManager/STPManager.h" +#include "simplifier.h" + + +namespace BEEV +{ + + class EstablishIntervals + { + public: + struct IntervalType + { + CBV minV; + CBV maxV; + IntervalType(CBV _min, CBV _max) + { + minV = _min; + maxV = _max; + } + + void print() + { + cout << *(minV) << " " << *(maxV) << endl; + } + }; + + static vector toDeleteLater; + static vector likeAutoPtr; + +private: + + IntervalType * freshUnsignedInterval(int width) + { + IntervalType *it = createInterval(makeCBV(width), makeCBV(width)); + CONSTANTBV::BitVector_Fill(it->maxV); + return it; + } + + static IntervalType * createInterval(CBV min, CBV max) + { + IntervalType *it = new IntervalType(min,max); + toDeleteLater.push_back(it); + return it ; + } + + CBV makeCBV(int width) + { + CBV result = CONSTANTBV::BitVector_Create(width, true); + likeAutoPtr.push_back(result); + return result; + } + + + public: + // Replace some of the things that unsigned intervals can figure out for us. + ASTNode topLevel_unsignedIntervals(const ASTNode&top) + { + map visited; + visit(top,visited); + ASTNodeMap fromTo; + for (map::const_iterator it = visited.begin(); it != visited.end(); it++) + { + const ASTNode& n = it->first; + IntervalType *interval = it->second; + + if (interval == NULL) + continue; + if (n.isConstant()) + continue; + if (interval->maxV == interval->minV && n.GetType() == BOOLEAN_TYPE) + { + if (0== CONSTANTBV::BitVector_Lexicompare(interval->maxV,littleOne)) + fromTo.insert(make_pair(n,bm.ASTTrue)); + else + fromTo.insert(make_pair(n,bm.ASTFalse)); + } + } + + if (fromTo.size() > 0) + { + //cerr << "intervals found" << fromTo.size() << endl; + ASTNodeMap cache; + return SubstitutionMap::replace(top,fromTo,cache,bm.defaultNodeFactory); + } + + return top; + } + + private: + // A single pass through the problem replacing things that must be true of false. + IntervalType* visit(const ASTNode& n, map & visited) + { + if (visited.find(n) != visited.end()) + return visited.find(n)->second; + + vector children_intervals; + children_intervals.reserve(n.Degree()); + for (int i=0; i < n.Degree();i++) + { + children_intervals.push_back(visit(n[i],visited)); + } + + IntervalType * result = NULL; + + if (BVCONST == n.GetKind() || BITVECTOR == n.GetKind()) // If it's a constant, make it. + { + // the CBV doesn't leak. it is a copy of the cbv inside the node. + CBV cbv = n.GetBVConst(); + result = createInterval(cbv,cbv); + } + else if (BVGE == n.GetKind() && children_intervals[0] != NULL && children_intervals[1] != NULL) + { + if (CONSTANTBV::BitVector_Lexicompare(children_intervals[0]->minV,children_intervals[1]->maxV) >=0) + result = createInterval(littleOne, littleOne); + } + else if (BVMOD == n.GetKind() && children_intervals[1] != NULL) + { + // When we're dividing by zero, we know nothing. + if (!CONSTANTBV::BitVector_is_empty(children_intervals[1]->maxV)) + { + result = freshUnsignedInterval(n.GetValueWidth()); + CONSTANTBV::BitVector_Copy(result->maxV , children_intervals[1]->maxV); + CONSTANTBV::BitVector_decrement(result->maxV); + } + } + + // result will often be null (which we take to mean the maximum range). + visited.insert(make_pair(n,result)); + return result; + } + + STPMgr& bm; + CBV littleOne; + CBV littleZero; + public: + EstablishIntervals(STPMgr& _bm) : bm(_bm) + { + littleZero = makeCBV(1); + littleOne = makeCBV(1); + CONSTANTBV::BitVector_Fill(littleOne); + } + + ~EstablishIntervals() + { + for (int i =0; i < toDeleteLater.size();i++) + delete toDeleteLater[i]; + + for (int i =0; i < likeAutoPtr.size();i++) + CONSTANTBV::BitVector_Destroy(likeAutoPtr[i]); + + likeAutoPtr.clear(); + toDeleteLater.clear(); + } + + + + + }; +} +; +#endif /* ESTABLISHINTERVALS_H_ */ -- 2.47.3