From: trevor_hansen Date: Thu, 29 Dec 2011 02:48:43 +0000 (+0000) Subject: Refactor X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=4527eaebdb38327ada5f7d85bda753f5d9040bb9;p=francis%2Fstp.git Refactor git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1450 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp index d790488..819a1bd 100644 --- a/src/STPManager/STP.cpp +++ b/src/STPManager/STP.cpp @@ -116,7 +116,7 @@ namespace BEEV { ASTNode STP::sizeReducing(ASTNode simplified_solved_InputToSAT, BVSolver* bvSolver) { - simplified_solved_InputToSAT = simp->CreateSubstitutionMap(simplified_solved_InputToSAT, arrayTransformer); + simplified_solved_InputToSAT = simp->topLevel(simplified_solved_InputToSAT, arrayTransformer); if (simp->hasUnappliedSubstitutions()) { simplified_solved_InputToSAT = simp->applySubstitutionMap(simplified_solved_InputToSAT); @@ -271,7 +271,7 @@ namespace BEEV { if (bm->UserFlags.optimize_flag) { - simplified_solved_InputToSAT = simp->CreateSubstitutionMap(simplified_solved_InputToSAT, arrayTransformer); + simplified_solved_InputToSAT = simp->topLevel(simplified_solved_InputToSAT, arrayTransformer); // Imagine: // The simplifier simplifies (0 + T) to T @@ -364,7 +364,7 @@ namespace BEEV { if (bm->UserFlags.optimize_flag) { - simplified_solved_InputToSAT = simp->CreateSubstitutionMap(simplified_solved_InputToSAT, arrayTransformer); + simplified_solved_InputToSAT = simp->topLevel(simplified_solved_InputToSAT, arrayTransformer); if (simp->hasUnappliedSubstitutions()) { diff --git a/src/simplifier/PropagateEqualities.cpp b/src/simplifier/PropagateEqualities.cpp new file mode 100644 index 0000000..d2fd504 --- /dev/null +++ b/src/simplifier/PropagateEqualities.cpp @@ -0,0 +1,182 @@ +#include +#include "PropagateEqualities.h" +#include "simplifier.h" +#include "../AST/ArrayTransformer.h" + +namespace BEEV +{ + const string PropagateEqualities::message = "After Propagating Equalities: "; + + // if false. Don't simplify while creating the substitution map. + // This makes it easier to spot how long is spent in the simplifier. + const bool simplify_during_create_subM = false; + + + //This finds conjuncts which are one of: (= SYMBOL BVCONST), (= BVCONST (READ SYMBOL BVCONST)), + // (IFF SYMBOL TRUE), (IFF SYMBOL FALSE), (IFF SYMBOL SYMBOL), (=SYMBOL SYMBOL) + // or (=SYMBOL BVCONST). + // It tries to remove the conjunct, storing it in the substitutionmap. It replaces it in the + // formula by true. + // The bvsolver puts expressions of the form (= SYMBOL TERM) into the solverMap. + + ASTNode PropagateEqualities::propagate(const ASTNode& a, ArrayTransformer*at) + { + if (!bm->UserFlags.wordlevel_solve_flag) + return a; + + ASTNode output; + //if the variable has been solved for, then simply return it + if (simp->CheckSubstitutionMap(a, output)) + return output; + + if (!alreadyVisited.insert(a.GetNodeNum()).second) + { + return a; + } + + output = a; + + //traverse a and populate the SubstitutionMap + const Kind k = a.GetKind(); + if (SYMBOL == k && BOOLEAN_TYPE == a.GetType()) + { + bool updated = simp->UpdateSubstitutionMap(a, ASTTrue); + output = updated ? ASTTrue : a; + } + else if (NOT == k && SYMBOL == a[0].GetKind()) + { + bool updated = simp->UpdateSubstitutionMap(a[0], ASTFalse); + output = updated ? ASTTrue : a; + } + else if (IFF == k || EQ == k) + { + ASTVec c = a.GetChildren(); + + if (simplify_during_create_subM) + SortByArith(c); + + if (c[0] == c[1]) + return ASTTrue; + + ASTNode c1; + if (EQ == k) + c1 = simplify_during_create_subM ? simp->SimplifyTerm(c[1]) : c[1]; + else// (IFF == k ) + c1= simplify_during_create_subM ? simp->SimplifyFormula_NoRemoveWrites(c[1], false) : c[1]; + + bool updated = simp->UpdateSubstitutionMap(c[0], c1); + output = updated ? ASTTrue : a; + + if (updated) + { + //fill the arrayname readindices vector if e0 is a + //READ(Arr,index) and index is a BVCONST + int to; + if ((to =TermOrder(c[0],c1))==1 && c[0].GetKind() == READ) + at->FillUp_ArrReadIndex_Vec(c[0], c1); + else if (to ==-1 && c1.GetKind() == READ) + at->FillUp_ArrReadIndex_Vec(c1,c[0]); + } + } + else if (XOR == k) + { + if (a.Degree() !=2) + return output; + + int to = TermOrder(a[0],a[1]); + if (0 == to) + { + if (a[0].GetKind() == NOT && a[0][0].GetKind() == EQ && a[0][0][0].GetValueWidth() ==1 && a[0][0][1].GetKind() == SYMBOL) + { + // (XOR (NOT(= (1 v))) ... ) + const ASTNode& symbol = a[0][0][1]; + const ASTNode newN = nf->CreateTerm(ITE, 1, a[1], a[0][0][0], nf->CreateTerm(BVNEG, 1,a[0][0][0])); + + if (simp->UpdateSolverMap(symbol, newN)) + output = ASTTrue; + } + else if (a[1].GetKind() == NOT && a[1][0].GetKind() == EQ && a[1][0][0].GetValueWidth() ==1 && a[1][0][1].GetKind() == SYMBOL) + { + const ASTNode& symbol = a[1][0][1]; + const ASTNode newN = nf->CreateTerm(ITE, 1, a[0], a[1][0][0], nf->CreateTerm(BVNEG, 1,a[1][0][0])); + + if (simp->UpdateSolverMap(symbol, newN)) + output = ASTTrue; + } + else if (a[0].GetKind() == EQ && a[0][0].GetValueWidth() ==1 && a[0][1].GetKind() == SYMBOL) + { + // XOR ((= 1 v) ... ) + + const ASTNode& symbol = a[0][1]; + const ASTNode newN = nf->CreateTerm(ITE, 1, a[1], nf->CreateTerm(BVNEG, 1,a[0][0]), a[0][0]); + + if (simp->UpdateSolverMap(symbol, newN)) + output = ASTTrue; + } + else if (a[1].GetKind() == EQ && a[1][0].GetValueWidth() ==1 && a[1][1].GetKind() == SYMBOL) + { + const ASTNode& symbol = a[1][1]; + const ASTNode newN = nf->CreateTerm(ITE, 1, a[0], nf->CreateTerm(BVNEG, 1,a[1][0]), a[1][0]); + + if (simp->UpdateSolverMap(symbol, newN)) + output = ASTTrue; + } + else + return output; + } + else + { + ASTNode symbol,rhs; + if (to==1) + { + symbol = a[0]; + rhs = a[1]; + } + else + { + symbol = a[1]; + rhs = a[0]; + } + + assert(symbol.GetKind() == SYMBOL); + + if (simp->UpdateSolverMap(symbol, nf->CreateNode(NOT, rhs))) + output = ASTTrue; + } + } + else if (AND == k) + { + const ASTVec& c = a.GetChildren(); + ASTVec o; + o.reserve(c.size()); + + for (ASTVec::const_iterator + it = c.begin(), itend = c.end(); + it != itend; it++) + { + simp->UpdateAlwaysTrueFormSet(*it); + ASTNode aaa = propagate(*it,at); + + if (ASTTrue != aaa) + { + if (ASTFalse == aaa) + return ASTFalse; + else + o.push_back(aaa); + } + } + if (o.size() == 0) + output = ASTTrue; + else if (o.size() == 1) + output = o[0]; + else if (o != c) + output = nf->CreateNode(AND, o); + else + output = a; + } + + return output; + } //end of CreateSubstitutionMap() + + +}; diff --git a/src/simplifier/PropagateEqualities.h b/src/simplifier/PropagateEqualities.h new file mode 100644 index 0000000..a1fb618 --- /dev/null +++ b/src/simplifier/PropagateEqualities.h @@ -0,0 +1,43 @@ +#ifndef PROPAGATEEQUALITIES_H_ +#define PROPAGATEEQUALITIES_H_ + +#include "../AST/AST.h" +#include "../STPManager/STPManager.h" + + //This finds conjuncts which are one of: (= SYMBOL BVCONST), (= BVCONST (READ SYMBOL BVCONST)), + // (IFF SYMBOL TRUE), (IFF SYMBOL FALSE), (IFF SYMBOL SYMBOL), (=SYMBOL SYMBOL) + // or (=SYMBOL BVCONST). + // It tries to remove the conjunct, storing it in the substitutionmap. It replaces it in the + // formula by true. + + +namespace BEEV +{ + class Simplifier; + class ArrayTransformer; + + class PropagateEqualities + { + Simplifier *simp; + NodeFactory *nf; + STPMgr *bm; + const ASTNode ASTTrue, ASTFalse; + + public: + HASHSET alreadyVisited; + const static string message; + + PropagateEqualities(Simplifier *simp_, NodeFactory *nf_, STPMgr *bm_) : + ASTTrue(bm_->ASTTrue), ASTFalse(bm_->ASTFalse) + { + simp = simp_; + nf = nf_; + bm = bm_; + } + + ASTNode + propagate(const ASTNode& a, ArrayTransformer*at); + }; +} + +#endif diff --git a/src/simplifier/SubstitutionMap.cpp b/src/simplifier/SubstitutionMap.cpp index 8ff1b21..cd7d9c9 100644 --- a/src/simplifier/SubstitutionMap.cpp +++ b/src/simplifier/SubstitutionMap.cpp @@ -14,6 +14,7 @@ SubstitutionMap::~SubstitutionMap() { delete SolverMap; delete nf; + delete pe; } // if false. Don't simplify while creating the substitution map. @@ -57,173 +58,6 @@ int TermOrder(const ASTNode& a, const ASTNode& b) } //End of TermOrder() - -//This finds conjuncts which are one of: (= SYMBOL BVCONST), (= BVCONST (READ SYMBOL BVCONST)), -// (IFF SYMBOL TRUE), (IFF SYMBOL FALSE), (IFF SYMBOL SYMBOL), (=SYMBOL SYMBOL) -// or (=SYMBOL BVCONST). -// It tries to remove the conjunct, storing it in the substitutionmap. It replaces it in the -// formula by true. -// The bvsolver puts expressions of the form (= SYMBOL TERM) into the solverMap. - -ASTNode SubstitutionMap::propagate(const ASTNode& a, ArrayTransformer*at) -{ - if (!bm->UserFlags.wordlevel_solve_flag) - return a; - - ASTNode output; - //if the variable has been solved for, then simply return it - if (CheckSubstitutionMap(a, output)) - return output; - - if (!alreadyVisited.insert(a.GetNodeNum()).second) - { - return a; - } - - output = a; - - //traverse a and populate the SubstitutionMap - const Kind k = a.GetKind(); - if (SYMBOL == k && BOOLEAN_TYPE == a.GetType()) - { - bool updated = simp->UpdateSubstitutionMap(a, ASTTrue); - output = updated ? ASTTrue : a; - } - else if (NOT == k && SYMBOL == a[0].GetKind()) - { - bool updated = simp->UpdateSubstitutionMap(a[0], ASTFalse); - output = updated ? ASTTrue : a; - } - else if (IFF == k || EQ == k) - { - ASTVec c = a.GetChildren(); - - if (simplify_during_create_subM) - SortByArith(c); - - if (c[0] == c[1]) - return ASTTrue; - - ASTNode c1; - if (EQ == k) - c1 = simplify_during_create_subM ? simp->SimplifyTerm(c[1]) : c[1]; - else// (IFF == k ) - c1= simplify_during_create_subM ? simp->SimplifyFormula_NoRemoveWrites(c[1], false) : c[1]; - - bool updated = simp->UpdateSubstitutionMap(c[0], c1); - output = updated ? ASTTrue : a; - - if (updated) - { - //fill the arrayname readindices vector if e0 is a - //READ(Arr,index) and index is a BVCONST - int to; - if ((to =TermOrder(c[0],c1))==1 && c[0].GetKind() == READ) - at->FillUp_ArrReadIndex_Vec(c[0], c1); - else if (to ==-1 && c1.GetKind() == READ) - at->FillUp_ArrReadIndex_Vec(c1,c[0]); - } - } - else if (XOR == k) - { - if (a.Degree() !=2) - return output; - - int to = TermOrder(a[0],a[1]); - if (0 == to) - { - if (a[0].GetKind() == NOT && a[0][0].GetKind() == EQ && a[0][0][0].GetValueWidth() ==1 && a[0][0][1].GetKind() == SYMBOL) - { - // (XOR (NOT(= (1 v))) ... ) - const ASTNode& symbol = a[0][0][1]; - const ASTNode newN = nf->CreateTerm(ITE, 1, a[1], a[0][0][0], nf->CreateTerm(BVNEG, 1,a[0][0][0])); - - if (simp->UpdateSolverMap(symbol, newN)) - output = ASTTrue; - } - else if (a[1].GetKind() == NOT && a[1][0].GetKind() == EQ && a[1][0][0].GetValueWidth() ==1 && a[1][0][1].GetKind() == SYMBOL) - { - const ASTNode& symbol = a[1][0][1]; - const ASTNode newN = nf->CreateTerm(ITE, 1, a[0], a[1][0][0], nf->CreateTerm(BVNEG, 1,a[1][0][0])); - - if (simp->UpdateSolverMap(symbol, newN)) - output = ASTTrue; - } - else if (a[0].GetKind() == EQ && a[0][0].GetValueWidth() ==1 && a[0][1].GetKind() == SYMBOL) - { - // XOR ((= 1 v) ... ) - - const ASTNode& symbol = a[0][1]; - const ASTNode newN = nf->CreateTerm(ITE, 1, a[1], nf->CreateTerm(BVNEG, 1,a[0][0]), a[0][0]); - - if (simp->UpdateSolverMap(symbol, newN)) - output = ASTTrue; - } - else if (a[1].GetKind() == EQ && a[1][0].GetValueWidth() ==1 && a[1][1].GetKind() == SYMBOL) - { - const ASTNode& symbol = a[1][1]; - const ASTNode newN = nf->CreateTerm(ITE, 1, a[0], nf->CreateTerm(BVNEG, 1,a[1][0]), a[1][0]); - - if (simp->UpdateSolverMap(symbol, newN)) - output = ASTTrue; - } - else - return output; - } - else - { - ASTNode symbol,rhs; - if (to==1) - { - symbol = a[0]; - rhs = a[1]; - } - else - { - symbol = a[1]; - rhs = a[0]; - } - - assert(symbol.GetKind() == SYMBOL); - - if (simp->UpdateSolverMap(symbol, nf->CreateNode(NOT, rhs))) - output = ASTTrue; - } - } - else if (AND == k) - { - const ASTVec& c = a.GetChildren(); - ASTVec o; - o.reserve(c.size()); - - for (ASTVec::const_iterator - it = c.begin(), itend = c.end(); - it != itend; it++) - { - simp->UpdateAlwaysTrueFormSet(*it); - ASTNode aaa = propagate(*it,at); - - if (ASTTrue != aaa) - { - if (ASTFalse == aaa) - return ASTFalse; - else - o.push_back(aaa); - } - } - if (o.size() == 0) - output = ASTTrue; - else if (o.size() == 1) - output = o[0]; - else if (o != c) - output = nf->CreateNode(AND, o); - else - output = a; - } - - return output; -} //end of CreateSubstitutionMap() - // idempotent. ASTNode SubstitutionMap::applySubstitutionMap(const ASTNode& n) { @@ -242,6 +76,12 @@ ASTNode SubstitutionMap::applySubstitutionMap(const ASTNode& n) return result; } + +ASTNode SubstitutionMap::propagate(const ASTNode& a, ArrayTransformer*at) +{ + return pe->propagate(a,at); +} + // not always idempotent. ASTNode SubstitutionMap::applySubstitutionMapUntilArrays(const ASTNode& n) { diff --git a/src/simplifier/SubstitutionMap.h b/src/simplifier/SubstitutionMap.h index d3f4e35..7115561 100644 --- a/src/simplifier/SubstitutionMap.h +++ b/src/simplifier/SubstitutionMap.h @@ -10,6 +10,7 @@ #include "../STPManager/STPManager.h" #include "../AST/NodeFactory/SimplifyingNodeFactory.h" #include "VariablesInExpression.h" +#include "PropagateEqualities.h" namespace BEEV { @@ -25,6 +26,7 @@ class SubstitutionMap { STPMgr* bm; ASTNode ASTTrue, ASTFalse, ASTUndefined; NodeFactory *nf; + PropagateEqualities *pe; // These are used to avoid substituting {x = f(y,z), z = f(x)} typedef hash_map DependsType; @@ -32,7 +34,7 @@ class SubstitutionMap { ASTNodeSet rhs; // All the rhs that have been seeen. set rhsAlreadyAdded; VariablesInExpression::SymbolPtrSet rhs_visited; // the rhs contains all the variables in here already. - HASHSET alreadyVisited; + int loopCount; @@ -74,13 +76,14 @@ public: loopCount = 0; substitutionsLastApplied =0; nf = new SimplifyingNodeFactory (*bm->hashingNodeFactory, *bm); + pe = new PropagateEqualities(_simp, nf, bm); } void clear() { SolverMap->clear(); haveAppliedSubstitutionMap(); - alreadyVisited.clear(); + pe->alreadyVisited.clear(); } virtual ~SubstitutionMap(); diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp index 13d6d23..2abba22 100644 --- a/src/simplifier/simplifier.cpp +++ b/src/simplifier/simplifier.cpp @@ -122,7 +122,7 @@ namespace BEEV // Substitution Map methods.... ASTNode - Simplifier::CreateSubstitutionMap(const ASTNode& a, ArrayTransformer* at) + Simplifier::topLevel(const ASTNode& a, ArrayTransformer* at) { _bm->GetRunTimes()->start(RunTimes::PropagateEqualities); ASTNode result = substitutionMap.propagate(a, at); diff --git a/src/simplifier/simplifier.h b/src/simplifier/simplifier.h index 9002cff..2aebf64 100644 --- a/src/simplifier/simplifier.h +++ b/src/simplifier/simplifier.h @@ -113,7 +113,7 @@ namespace BEEV //Map for solved variables bool UpdateSolverMap(const ASTNode& e0, const ASTNode& e1); - ASTNode CreateSubstitutionMap(const ASTNode& a, + ASTNode topLevel(const ASTNode& a, ArrayTransformer *at); //substitution