From 99e5a883066ad6e740669e67db3a7e185a1bd484 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Thu, 29 Dec 2011 02:00:01 +0000 Subject: [PATCH] Bugfix. Reverting to r1445. r1446 sometimes broke. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1447 e59a4935-1847-0410-ae03-e826735625c1 --- src/AST/RunTimes.h | 2 +- src/STPManager/STP.cpp | 26 ++-- src/STPManager/STP.h | 6 +- src/simplifier/PropagateEqualities.cpp | 191 ------------------------- src/simplifier/PropagateEqualities.h | 49 ------- src/simplifier/RemoveUnconstrained.cpp | 2 - src/simplifier/RemoveUnconstrained.h | 1 - src/simplifier/SubstitutionMap.cpp | 168 ++++++++++++++++++++++ src/simplifier/SubstitutionMap.h | 6 +- src/simplifier/simplifier.cpp | 10 ++ src/simplifier/simplifier.h | 2 + 11 files changed, 197 insertions(+), 266 deletions(-) delete mode 100644 src/simplifier/PropagateEqualities.cpp delete mode 100644 src/simplifier/PropagateEqualities.h diff --git a/src/AST/RunTimes.h b/src/AST/RunTimes.h index 49537fa..df1e2bb 100644 --- a/src/AST/RunTimes.h +++ b/src/AST/RunTimes.h @@ -28,7 +28,7 @@ public: BitBlasting, Solving, BVSolver, - PropagateEqualities, + CreateSubstitutionMap, SendingToSAT, CounterExampleGeneration, SATSimplifying, diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp index 183f1c3..d790488 100644 --- a/src/STPManager/STP.cpp +++ b/src/STPManager/STP.cpp @@ -21,7 +21,6 @@ #include "../simplifier/FindPureLiterals.h" #include "../simplifier/EstablishIntervals.h" #include "../simplifier/UseITEContext.h" -#include "../simplifier/PropagateEqualities.h" #include "../simplifier/AlwaysTrue.h" #include "../simplifier/AIGSimplifyPropositionalCore.h" #include @@ -84,12 +83,12 @@ namespace BEEV { } //End of TopLevelSTP() ASTNode - STP::callSizeReducing(ASTNode simplified_solved_InputToSAT, BVSolver* bvSolver, PropagateEqualities *pe, const int initial_difficulty_score) + STP::callSizeReducing(ASTNode simplified_solved_InputToSAT, BVSolver* bvSolver, const int initial_difficulty_score) { while (true) { ASTNode last = simplified_solved_InputToSAT; - simplified_solved_InputToSAT = sizeReducing(last, bvSolver,pe); + simplified_solved_InputToSAT = sizeReducing(last, bvSolver); if (last == simplified_solved_InputToSAT) break; } @@ -115,14 +114,14 @@ namespace BEEV { // These transformations should never increase the size of the DAG. ASTNode - STP::sizeReducing(ASTNode simplified_solved_InputToSAT, BVSolver* bvSolver, PropagateEqualities* pe) + STP::sizeReducing(ASTNode simplified_solved_InputToSAT, BVSolver* bvSolver) { - simplified_solved_InputToSAT = pe->topLevel(simplified_solved_InputToSAT, arrayTransformer); + simplified_solved_InputToSAT = simp->CreateSubstitutionMap(simplified_solved_InputToSAT, arrayTransformer); if (simp->hasUnappliedSubstitutions()) { simplified_solved_InputToSAT = simp->applySubstitutionMap(simplified_solved_InputToSAT); simp->haveAppliedSubstitutionMap(); - bm->ASTNodeStats(pe->message.c_str(), simplified_solved_InputToSAT); + bm->ASTNodeStats("After Propagating Equalities: ", simplified_solved_InputToSAT); } if (bm->UserFlags.isSet("enable-unconstrained", "1")) @@ -205,7 +204,6 @@ namespace BEEV { // A heap object so I can easily control its lifetime. BVSolver* bvSolver = new BVSolver(bm, simp); - PropagateEqualities * pe = new PropagateEqualities(simp,bm->defaultNodeFactory,bm); ASTNode simplified_solved_InputToSAT = original_input; @@ -230,7 +228,7 @@ namespace BEEV { assert(!arrayops); // Run size reducing just once. - simplified_solved_InputToSAT = sizeReducing(simplified_solved_InputToSAT, bvSolver,pe); + simplified_solved_InputToSAT = sizeReducing(simplified_solved_InputToSAT, bvSolver); unsigned initial_difficulty_score = difficulty.score(simplified_solved_InputToSAT); @@ -238,7 +236,7 @@ namespace BEEV { // Currently we discards all the state each time sizeReducing is called, // so it's expensive to call. if (!arrayops && initial_difficulty_score < 1000000) - simplified_solved_InputToSAT = callSizeReducing(simplified_solved_InputToSAT, bvSolver,pe, initial_difficulty_score); + simplified_solved_InputToSAT = callSizeReducing(simplified_solved_InputToSAT, bvSolver, initial_difficulty_score); if ((!arrayops || bm->UserFlags.isSet("array-difficulty-reversion", "1"))) { @@ -273,7 +271,7 @@ namespace BEEV { if (bm->UserFlags.optimize_flag) { - simplified_solved_InputToSAT = pe->topLevel(simplified_solved_InputToSAT, arrayTransformer); + simplified_solved_InputToSAT = simp->CreateSubstitutionMap(simplified_solved_InputToSAT, arrayTransformer); // Imagine: // The simplifier simplifies (0 + T) to T @@ -289,7 +287,7 @@ namespace BEEV { simp->haveAppliedSubstitutionMap(); } - bm->ASTNodeStats(pe->message.c_str(), simplified_solved_InputToSAT); + bm->ASTNodeStats("after pure substitution: ", simplified_solved_InputToSAT); simplified_solved_InputToSAT = simp->SimplifyFormula_TopLevel(simplified_solved_InputToSAT, false); @@ -366,7 +364,7 @@ namespace BEEV { if (bm->UserFlags.optimize_flag) { - simplified_solved_InputToSAT = pe->topLevel(simplified_solved_InputToSAT, arrayTransformer); + simplified_solved_InputToSAT = simp->CreateSubstitutionMap(simplified_solved_InputToSAT, arrayTransformer); if (simp->hasUnappliedSubstitutions()) { @@ -374,7 +372,7 @@ namespace BEEV { simp->haveAppliedSubstitutionMap(); } - bm->ASTNodeStats(pe->message.c_str(), simplified_solved_InputToSAT); + bm->ASTNodeStats("after pure substitution: ", simplified_solved_InputToSAT); simplified_solved_InputToSAT = simp->SimplifyFormula_TopLevel(simplified_solved_InputToSAT, false); bm->ASTNodeStats("after simplification: ", simplified_solved_InputToSAT); @@ -476,8 +474,6 @@ namespace BEEV { // Deleting it clears out all the buckets associated with hashmaps etc. too. delete bvSolver; bvSolver = NULL; - delete pe; - pe = NULL; if (bm->UserFlags.stats_flag) simp->printCacheStatus(); diff --git a/src/STPManager/STP.h b/src/STPManager/STP.h index d782822..ca2d372 100644 --- a/src/STPManager/STP.h +++ b/src/STPManager/STP.h @@ -15,19 +15,17 @@ #include "../STPManager/STPManager.h" #include "../simplifier/bvsolver.h" #include "../simplifier/simplifier.h" -#include "../simplifier/PropagateEqualities.h" #include "../to-sat/ASTNode/ToSAT.h" #include "../parser/LetMgr.h" #include "../absrefine_counterexample/AbsRefine_CounterExample.h" - namespace BEEV { class STP { ArrayTransformer * arrayTransformer; - ASTNode sizeReducing(ASTNode input, BVSolver* bvSolver, PropagateEqualities*pe); + ASTNode sizeReducing(ASTNode input, BVSolver* bvSolver); // A copy of all the state we need to restore to a prior expression. struct Revert_to @@ -48,7 +46,7 @@ namespace BEEV public: // calls sizeReducing and the bitblasting simplification. - ASTNode callSizeReducing(ASTNode simplified_solved_InputToSAT, BVSolver* bvSolver, PropagateEqualities *pe, const int initial_difficulty_score); + ASTNode callSizeReducing(ASTNode simplified_solved_InputToSAT, BVSolver* bvSolver, const int initial_difficulty_score); /**************************************************************** diff --git a/src/simplifier/PropagateEqualities.cpp b/src/simplifier/PropagateEqualities.cpp deleted file mode 100644 index 71fcb46..0000000 --- a/src/simplifier/PropagateEqualities.cpp +++ /dev/null @@ -1,191 +0,0 @@ -#include -#include "PropagateEqualities.h" -#include "simplifier.h" -#include "../AST/ArrayTransformer.h" - -namespace BEEV -{ - - // 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; - - const string PropagateEqualities::message = "After Propagating Equalities: "; - - ASTNode - PropagateEqualities::topLevel(const ASTNode& a, ArrayTransformer*at) - { - bm->GetRunTimes()->start(RunTimes::PropagateEqualities); - ASTNode result = topLevelReal(a, at); - bm->GetRunTimes()->stop(RunTimes::PropagateEqualities); - return result; - } - - ASTNode - PropagateEqualities::topLevelReal(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 = topLevel(*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; - } - -} -; diff --git a/src/simplifier/PropagateEqualities.h b/src/simplifier/PropagateEqualities.h deleted file mode 100644 index de1094d..0000000 --- a/src/simplifier/PropagateEqualities.h +++ /dev/null @@ -1,49 +0,0 @@ -#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 - { - - ASTNode - topLevelReal(const ASTNode& a, ArrayTransformer*at); - - Simplifier *simp; - NodeFactory *nf; - STPMgr *bm; - const ASTNode ASTTrue, ASTFalse; - HASHSET alreadyVisited; - - public: - const static string message; - - PropagateEqualities(Simplifier *simp_, NodeFactory *nf_, STPMgr *bm_) : - ASTTrue(bm_->ASTTrue), ASTFalse(bm_->ASTTrue) - - { - simp = simp_; - nf = nf_; - bm = bm_; - } - - ASTNode - topLevel(const ASTNode& a, ArrayTransformer*at); - }; -} - -#endif diff --git a/src/simplifier/RemoveUnconstrained.cpp b/src/simplifier/RemoveUnconstrained.cpp index dc6f54c..e889fd6 100644 --- a/src/simplifier/RemoveUnconstrained.cpp +++ b/src/simplifier/RemoveUnconstrained.cpp @@ -13,8 +13,6 @@ namespace BEEV { using simplifier::constantBitP::Dependencies; - const string RemoveUnconstrained::message = "After Unconstrained variable:"; - RemoveUnconstrained::RemoveUnconstrained(STPMgr& _bm) : bm(_bm) { diff --git a/src/simplifier/RemoveUnconstrained.h b/src/simplifier/RemoveUnconstrained.h index a9d0b49..a8856dd 100644 --- a/src/simplifier/RemoveUnconstrained.h +++ b/src/simplifier/RemoveUnconstrained.h @@ -39,7 +39,6 @@ namespace BEEV public: - static const string message; RemoveUnconstrained(STPMgr& bm); virtual diff --git a/src/simplifier/SubstitutionMap.cpp b/src/simplifier/SubstitutionMap.cpp index aac8574..4734e7f 100644 --- a/src/simplifier/SubstitutionMap.cpp +++ b/src/simplifier/SubstitutionMap.cpp @@ -16,6 +16,9 @@ SubstitutionMap::~SubstitutionMap() delete nf; } +// 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; //if a is READ(Arr,const) and b is BVCONST then return 1. //if a is a symbol SYMBOL, return 1. @@ -55,6 +58,171 @@ int TermOrder(const ASTNode& a, const ASTNode& b) +//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::CreateSubstitutionMap(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 = UpdateSubstitutionMap(a, ASTTrue); + output = updated ? ASTTrue : a; + } + else if (NOT == k && SYMBOL == a[0].GetKind()) + { + bool updated = 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 = 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 (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 (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 (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 (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 (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 = CreateSubstitutionMap(*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) diff --git a/src/simplifier/SubstitutionMap.h b/src/simplifier/SubstitutionMap.h index fc11b5d..bc4bff8 100644 --- a/src/simplifier/SubstitutionMap.h +++ b/src/simplifier/SubstitutionMap.h @@ -32,7 +32,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; @@ -80,7 +80,7 @@ public: { SolverMap->clear(); haveAppliedSubstitutionMap(); - //alreadyVisited.clear(); + alreadyVisited.clear(); } virtual ~SubstitutionMap(); @@ -187,7 +187,7 @@ public: return false; } - + ASTNode CreateSubstitutionMap(const ASTNode& a, ArrayTransformer*at); ASTNode applySubstitutionMap(const ASTNode& n); diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp index 9f16750..f7e97c8 100644 --- a/src/simplifier/simplifier.cpp +++ b/src/simplifier/simplifier.cpp @@ -119,6 +119,16 @@ namespace BEEV } } + // Substitution Map methods.... + + ASTNode + Simplifier::CreateSubstitutionMap(const ASTNode& a, ArrayTransformer* at) + { + _bm->GetRunTimes()->start(RunTimes::CreateSubstitutionMap); + ASTNode result = substitutionMap.CreateSubstitutionMap(a, at); + _bm->GetRunTimes()->stop(RunTimes::CreateSubstitutionMap); + return result; + } bool Simplifier::UpdateSolverMap(const ASTNode& key, const ASTNode& value) diff --git a/src/simplifier/simplifier.h b/src/simplifier/simplifier.h index 5018421..9002cff 100644 --- a/src/simplifier/simplifier.h +++ b/src/simplifier/simplifier.h @@ -113,6 +113,8 @@ namespace BEEV //Map for solved variables bool UpdateSolverMap(const ASTNode& e0, const ASTNode& e1); + ASTNode CreateSubstitutionMap(const ASTNode& a, + ArrayTransformer *at); //substitution bool CheckSubstitutionMap(const ASTNode& a, ASTNode& output); -- 2.47.3