From 1b60c92055d71765ed33e670cef483d5199cfbf9 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Thu, 29 Dec 2011 00:56:02 +0000 Subject: [PATCH] Refactor. Remove propagate equalities to its own class. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1446 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, 266 insertions(+), 197 deletions(-) create mode 100644 src/simplifier/PropagateEqualities.cpp create mode 100644 src/simplifier/PropagateEqualities.h diff --git a/src/AST/RunTimes.h b/src/AST/RunTimes.h index df1e2bb..49537fa 100644 --- a/src/AST/RunTimes.h +++ b/src/AST/RunTimes.h @@ -28,7 +28,7 @@ public: BitBlasting, Solving, BVSolver, - CreateSubstitutionMap, + PropagateEqualities, SendingToSAT, CounterExampleGeneration, SATSimplifying, diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp index d790488..183f1c3 100644 --- a/src/STPManager/STP.cpp +++ b/src/STPManager/STP.cpp @@ -21,6 +21,7 @@ #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 @@ -83,12 +84,12 @@ namespace BEEV { } //End of TopLevelSTP() ASTNode - STP::callSizeReducing(ASTNode simplified_solved_InputToSAT, BVSolver* bvSolver, const int initial_difficulty_score) + STP::callSizeReducing(ASTNode simplified_solved_InputToSAT, BVSolver* bvSolver, PropagateEqualities *pe, const int initial_difficulty_score) { while (true) { ASTNode last = simplified_solved_InputToSAT; - simplified_solved_InputToSAT = sizeReducing(last, bvSolver); + simplified_solved_InputToSAT = sizeReducing(last, bvSolver,pe); if (last == simplified_solved_InputToSAT) break; } @@ -114,14 +115,14 @@ namespace BEEV { // These transformations should never increase the size of the DAG. ASTNode - STP::sizeReducing(ASTNode simplified_solved_InputToSAT, BVSolver* bvSolver) + STP::sizeReducing(ASTNode simplified_solved_InputToSAT, BVSolver* bvSolver, PropagateEqualities* pe) { - simplified_solved_InputToSAT = simp->CreateSubstitutionMap(simplified_solved_InputToSAT, arrayTransformer); + simplified_solved_InputToSAT = pe->topLevel(simplified_solved_InputToSAT, arrayTransformer); if (simp->hasUnappliedSubstitutions()) { simplified_solved_InputToSAT = simp->applySubstitutionMap(simplified_solved_InputToSAT); simp->haveAppliedSubstitutionMap(); - bm->ASTNodeStats("After Propagating Equalities: ", simplified_solved_InputToSAT); + bm->ASTNodeStats(pe->message.c_str(), simplified_solved_InputToSAT); } if (bm->UserFlags.isSet("enable-unconstrained", "1")) @@ -204,6 +205,7 @@ 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; @@ -228,7 +230,7 @@ namespace BEEV { assert(!arrayops); // Run size reducing just once. - simplified_solved_InputToSAT = sizeReducing(simplified_solved_InputToSAT, bvSolver); + simplified_solved_InputToSAT = sizeReducing(simplified_solved_InputToSAT, bvSolver,pe); unsigned initial_difficulty_score = difficulty.score(simplified_solved_InputToSAT); @@ -236,7 +238,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, initial_difficulty_score); + simplified_solved_InputToSAT = callSizeReducing(simplified_solved_InputToSAT, bvSolver,pe, initial_difficulty_score); if ((!arrayops || bm->UserFlags.isSet("array-difficulty-reversion", "1"))) { @@ -271,7 +273,7 @@ namespace BEEV { if (bm->UserFlags.optimize_flag) { - simplified_solved_InputToSAT = simp->CreateSubstitutionMap(simplified_solved_InputToSAT, arrayTransformer); + simplified_solved_InputToSAT = pe->topLevel(simplified_solved_InputToSAT, arrayTransformer); // Imagine: // The simplifier simplifies (0 + T) to T @@ -287,7 +289,7 @@ namespace BEEV { simp->haveAppliedSubstitutionMap(); } - bm->ASTNodeStats("after pure substitution: ", simplified_solved_InputToSAT); + bm->ASTNodeStats(pe->message.c_str(), simplified_solved_InputToSAT); simplified_solved_InputToSAT = simp->SimplifyFormula_TopLevel(simplified_solved_InputToSAT, false); @@ -364,7 +366,7 @@ namespace BEEV { if (bm->UserFlags.optimize_flag) { - simplified_solved_InputToSAT = simp->CreateSubstitutionMap(simplified_solved_InputToSAT, arrayTransformer); + simplified_solved_InputToSAT = pe->topLevel(simplified_solved_InputToSAT, arrayTransformer); if (simp->hasUnappliedSubstitutions()) { @@ -372,7 +374,7 @@ namespace BEEV { simp->haveAppliedSubstitutionMap(); } - bm->ASTNodeStats("after pure substitution: ", simplified_solved_InputToSAT); + bm->ASTNodeStats(pe->message.c_str(), simplified_solved_InputToSAT); simplified_solved_InputToSAT = simp->SimplifyFormula_TopLevel(simplified_solved_InputToSAT, false); bm->ASTNodeStats("after simplification: ", simplified_solved_InputToSAT); @@ -474,6 +476,8 @@ 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 ca2d372..d782822 100644 --- a/src/STPManager/STP.h +++ b/src/STPManager/STP.h @@ -15,17 +15,19 @@ #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); + ASTNode sizeReducing(ASTNode input, BVSolver* bvSolver, PropagateEqualities*pe); // A copy of all the state we need to restore to a prior expression. struct Revert_to @@ -46,7 +48,7 @@ namespace BEEV public: // calls sizeReducing and the bitblasting simplification. - ASTNode callSizeReducing(ASTNode simplified_solved_InputToSAT, BVSolver* bvSolver, const int initial_difficulty_score); + ASTNode callSizeReducing(ASTNode simplified_solved_InputToSAT, BVSolver* bvSolver, PropagateEqualities *pe, const int initial_difficulty_score); /**************************************************************** diff --git a/src/simplifier/PropagateEqualities.cpp b/src/simplifier/PropagateEqualities.cpp new file mode 100644 index 0000000..71fcb46 --- /dev/null +++ b/src/simplifier/PropagateEqualities.cpp @@ -0,0 +1,191 @@ +#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 new file mode 100644 index 0000000..de1094d --- /dev/null +++ b/src/simplifier/PropagateEqualities.h @@ -0,0 +1,49 @@ +#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 e889fd6..dc6f54c 100644 --- a/src/simplifier/RemoveUnconstrained.cpp +++ b/src/simplifier/RemoveUnconstrained.cpp @@ -13,6 +13,8 @@ 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 a8856dd..a9d0b49 100644 --- a/src/simplifier/RemoveUnconstrained.h +++ b/src/simplifier/RemoveUnconstrained.h @@ -39,6 +39,7 @@ namespace BEEV public: + static const string message; RemoveUnconstrained(STPMgr& bm); virtual diff --git a/src/simplifier/SubstitutionMap.cpp b/src/simplifier/SubstitutionMap.cpp index 4734e7f..aac8574 100644 --- a/src/simplifier/SubstitutionMap.cpp +++ b/src/simplifier/SubstitutionMap.cpp @@ -16,9 +16,6 @@ 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. @@ -58,171 +55,6 @@ 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 bc4bff8..fc11b5d 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 f7e97c8..9f16750 100644 --- a/src/simplifier/simplifier.cpp +++ b/src/simplifier/simplifier.cpp @@ -119,16 +119,6 @@ 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 9002cff..5018421 100644 --- a/src/simplifier/simplifier.h +++ b/src/simplifier/simplifier.h @@ -113,8 +113,6 @@ 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