From: trevor_hansen Date: Mon, 14 Feb 2011 01:01:57 +0000 (+0000) Subject: Improvements. X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=bfaa7f6dd59b3d8bf3ef8dad886d74fabcee6e7a;p=francis%2Fstp.git Improvements. * Add a function to update the substitution map that avoids the expensive checks. This is used by unconstrained variable elimination. * use a --config flag to enable the xor solver. * Update the dependencies with functions for unconstrained elimination. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1144 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/simplifier/SubstitutionMap.h b/src/simplifier/SubstitutionMap.h index 014bec5..5c2bac1 100644 --- a/src/simplifier/SubstitutionMap.h +++ b/src/simplifier/SubstitutionMap.h @@ -112,6 +112,18 @@ public: return false; } + // It's depressingly expensive to perform all of the loop checks etc. + // If you use this function you are promising: + // 1) That UpdateSubstitutionMap(e0,e1) would have returned true. + // 2) That all of the substitutions will be written in fully before other code + bool UpdateSubstitutionMapFewChecks(const ASTNode& e0, const ASTNode& e1) + { + assert(e0.GetKind() == SYMBOL); + assert (!CheckSubstitutionMap(e0)); + (*SolverMap)[e0] = e1; + return true; + } + // The substitutionMap will be updated, given x <-> f(w,z,y), iff, // 1) x doesn't appear in the rhs. // 2) x hasn't already been stored in the substitution map. diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp index 44afb80..56e2dab 100644 --- a/src/simplifier/bvsolver.cpp +++ b/src/simplifier/bvsolver.cpp @@ -541,7 +541,7 @@ namespace BEEV // to do. Flatten the XOR. ASTNode BVSolver::solveForXOR(const ASTNode& xorNode) { - assert(_bm->UserFlags.solve_for_XORS_flag); + assert(_bm->UserFlags.isSet("xor-solve","1")); if (xorNode.GetKind() != XOR) { @@ -628,7 +628,7 @@ namespace BEEV ASTNode BVSolver::solveForAndOfXOR(const ASTNode& n) { - assert(_bm->UserFlags.solve_for_XORS_flag); + assert(_bm->UserFlags.isSet("xor-solve","1")); if (n.GetKind() != AND) return n; @@ -670,7 +670,7 @@ namespace BEEV } Kind k = input.GetKind(); - if (XOR ==k && _bm->UserFlags.solve_for_XORS_flag) + if (XOR ==k && _bm->UserFlags.isSet("xor-solve","1")) { ASTNode output = solveForXOR(_input); UpdateAlreadySolvedMap(_input, output); @@ -787,7 +787,7 @@ namespace BEEV if (evens != ASTTrue) output = _bm->CreateNode(AND, output, evens); - if (_bm->UserFlags.solve_for_XORS_flag) + if (_bm->UserFlags.isSet("xor-solve","1")) output = solveForAndOfXOR(output); // Imagine in the last conjunct A is replaced by B. But there could diff --git a/src/simplifier/constantBitP/Dependencies.h b/src/simplifier/constantBitP/Dependencies.h index f636e9a..2ec2c06 100644 --- a/src/simplifier/constantBitP/Dependencies.h +++ b/src/simplifier/constantBitP/Dependencies.h @@ -20,6 +20,7 @@ namespace simplifier const set empty; + public: // All the nodes that depend on the value of a particular node. void build(const ASTNode & current, const ASTNode & prior) @@ -75,6 +76,18 @@ namespace simplifier } } + void replaceFresh(const ASTNode& old, const ASTNode& newN, set *newNDepends, + ASTVec& variables) + { + NodeToDependentNodeMap::const_iterator it = dependents.find(old); + if (it == dependents.end()) + return; + + it->second->erase(old); + dependents.insert(make_pair(newN,newNDepends)); + variables.push_back(newN); + } + // The "toRemove" node is being removed. Used by unconstrained elimination. void removeNode(const ASTNode& toRemove, ASTVec& variables) { @@ -147,6 +160,17 @@ namespace simplifier return s->count(higher) > 0; } + bool isUnconstrained(const ASTNode& n) + { + if (n.GetKind() != SYMBOL) + return false; + + NodeToDependentNodeMap::const_iterator it = dependents.find(n); + assert(it != dependents.end()); + return it->second->size() ==1; + } + +#if 0 void getAllVariables(ASTVec& v) { @@ -156,6 +180,7 @@ namespace simplifier v.push_back(it->first); } } +#endif }; diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp index be85f95..87b6b45 100644 --- a/src/simplifier/simplifier.cpp +++ b/src/simplifier/simplifier.cpp @@ -151,6 +151,10 @@ namespace BEEV { return substitutionMap.CheckSubstitutionMap(key); } + bool Simplifier::UpdateSubstitutionMapFewChecks(const ASTNode& e0, const ASTNode& e1) + { + return substitutionMap.UpdateSubstitutionMapFewChecks(e0,e1); + } bool Simplifier::UpdateSubstitutionMap(const ASTNode& e0, const ASTNode& e1) { @@ -609,6 +613,9 @@ namespace BEEV const unsigned len = left.GetValueWidth(); + if(_bm->UserFlags.isSet("inequality-simplifications","1")) + { + const int constStart = std::min(mostSignificantConstants(left),mostSignificantConstants(right)); int comparator =0; @@ -633,56 +640,54 @@ namespace BEEV return pushNeg ? nf->CreateNode(NOT, status) : status; } - if (comparator!=0 && (k == BVSGT || k == BVSGE)) - { - // one is bigger than the other. - int sign_a = getConstantBit(left, 0); - int sign_b = getConstantBit(right, 0); - if (sign_a < sign_b) - { - comparator =1; // a > b. - } - if (sign_a > sign_b) - comparator =-1; + if (comparator != 0 && (k == BVSGT || k == BVSGE)) + { + // one is bigger than the other. + int sign_a = getConstantBit(left, 0); + int sign_b = getConstantBit(right, 0); + if (sign_a < sign_b) + { + comparator = 1; // a > b. + } + if (sign_a > sign_b) + comparator = -1; - ASTNode status = (comparator ==1)? ASTTrue: ASTFalse; - return pushNeg ? nf->CreateNode(NOT, status) : status; - } + ASTNode status = (comparator == 1) ? ASTTrue : ASTFalse; + return pushNeg ? nf->CreateNode(NOT, status) : status; + } - { - ASTNodeSet visited0, visited1; - vector l0,l1; + { + ASTNodeSet visited0, visited1; + vector l0, l1; - // Sound overapproximation. Doesn't consider the equalities. - if (getPossibleValues(left, visited0, l0) && getPossibleValues(right,visited1, l1)) - { - { - bool (*comp)(const ASTNode&, const ASTNode&); - if (k == BVSGT || k == BVSGE) - comp = signedGreaterThan; - else - comp = unsignedGreaterThan; - { - ASTNode minLHS = *max_element(l0.begin(), l0.end(), - comp); - ASTNode maxRHS = *min_element(l1.begin(), l1.end(), - comp); - - if (comp(minLHS, maxRHS)) - return pushNeg ? ASTFalse : ASTTrue; - } - { - ASTNode maxLHS = *min_element(l0.begin(), l0.end(), - comp); - ASTNode minRHS = *max_element(l1.begin(), l1.end(), - comp); - - if (comp(minRHS, maxLHS)) - return pushNeg ? ASTTrue : ASTFalse; - } - } - } - } + // Sound overapproximation. Doesn't consider the equalities. + if (getPossibleValues(left, visited0, l0) && getPossibleValues(right, visited1, l1)) + { + { + bool + (*comp)(const ASTNode&, const ASTNode&); + if (k == BVSGT || k == BVSGE) + comp = signedGreaterThan; + else + comp = unsignedGreaterThan; + { + ASTNode minLHS = *max_element(l0.begin(), l0.end(), comp); + ASTNode maxRHS = *min_element(l1.begin(), l1.end(), comp); + + if (comp(minLHS, maxRHS)) + return pushNeg ? ASTFalse : ASTTrue; + } + { + ASTNode maxLHS = *min_element(l0.begin(), l0.end(), comp); + ASTNode minRHS = *max_element(l1.begin(), l1.end(), comp); + + if (comp(minRHS, maxLHS)) + return pushNeg ? ASTTrue : ASTFalse; + } + } + } + } + } const ASTNode unsigned_min = _bm->CreateZeroConst(len); const ASTNode one = _bm->CreateOneConst(len); @@ -1784,15 +1789,15 @@ namespace BEEV { output = zero; } - else if (BVMULT == k - && 1 == nonconstkids.size() + else if (BVMULT == k + && 1 == nonconstkids.size() && constoutput == max) { //useful special case opt: when input is BVMULT(max_const,t), //then output = BVUMINUS(t). this is easier on the bitblaster - output = + output = nf->CreateTerm(BVUMINUS, inputValueWidth, nonconstkids); - } + } else { if (0 < nonconstkids.size()) diff --git a/src/simplifier/simplifier.h b/src/simplifier/simplifier.h index e85572f..0e0d640 100644 --- a/src/simplifier/simplifier.h +++ b/src/simplifier/simplifier.h @@ -115,6 +115,7 @@ namespace BEEV bool CheckSubstitutionMap(const ASTNode& a, ASTNode& output); bool CheckSubstitutionMap(const ASTNode& a); bool UpdateSubstitutionMap(const ASTNode& e0, const ASTNode& e1); + bool UpdateSubstitutionMapFewChecks(const ASTNode& e0, const ASTNode& e1); ASTNode applySubstitutionMap(const ASTNode& n); ASTNode applySubstitutionMapUntilArrays(const ASTNode& n);