From d77b4a202aa9932c9073efda6b322d20168ac591 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Fri, 11 Jun 2010 03:05:51 +0000 Subject: [PATCH] Refactoring. Move all the substitutionmap functions into the one class. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@831 e59a4935-1847-0410-ae03-e826735625c1 --- src/AST/ArrayTransformer.cpp | 100 ------------------------ src/AST/ArrayTransformer.h | 11 ++- src/STPManager/STP.cpp | 12 +-- src/simplifier/SubstitutionMap.cpp | 121 +++++++++++++++++++++++++++++ src/simplifier/SubstitutionMap.h | 114 +++++++++++++++++++++++++++ src/simplifier/bvsolver.cpp | 33 -------- src/simplifier/consteval.cpp | 2 +- src/simplifier/simplifier.cpp | 65 ++++++---------- src/simplifier/simplifier.h | 27 ++++--- 9 files changed, 282 insertions(+), 203 deletions(-) create mode 100644 src/simplifier/SubstitutionMap.cpp create mode 100644 src/simplifier/SubstitutionMap.h diff --git a/src/AST/ArrayTransformer.cpp b/src/AST/ArrayTransformer.cpp index e96696b..497669d 100644 --- a/src/AST/ArrayTransformer.cpp +++ b/src/AST/ArrayTransformer.cpp @@ -775,106 +775,6 @@ namespace BEEV return result; } //end of TransformArray() - //The big substitution function - ASTNode ArrayTransformer::CreateSubstitutionMap(const ASTNode& a) - { - if (!bm->UserFlags.wordlevel_solve_flag) - return a; - - ASTNode output = a; - //if the variable has been solved for, then simply return it - if (simp->CheckSolverMap(a, output)) - return output; - - //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; - return output; - } - if (NOT == k && SYMBOL == a[0].GetKind()) - { - bool updated = simp->UpdateSubstitutionMap(a[0], ASTFalse); - output = updated ? ASTTrue : a; - return output; - } - - if (IFF == k) - { - ASTVec c = a.GetChildren(); - SortByArith(c); - if (SYMBOL != c[0].GetKind() || - bm->VarSeenInTerm(c[0], - simp->SimplifyFormula_NoRemoveWrites(c[1], false))) - { - return a; - } - bool updated = - simp->UpdateSubstitutionMap(c[0], - simp->SimplifyFormula(c[1], false)); - output = updated ? ASTTrue : a; - return output; - } - - if (EQ == k) - { - //fill the arrayname readindices vector if e0 is a - //READ(Arr,index) and index is a BVCONST - ASTVec c = a.GetChildren(); - SortByArith(c); - ASTNode c1 = simp->SimplifyTerm(c[1]); - FillUp_ArrReadIndex_Vec(c[0], c1); - - if (SYMBOL == c[0].GetKind() - && bm->VarSeenInTerm(c[0], c1)) - { - return a; - } - - if (1 == TermOrder(c[0], c1) - && READ == c[0].GetKind() - && bm->VarSeenInTerm(c[0][1], c1)) - { - return a; - } - bool updated = simp->UpdateSubstitutionMap(c[0], c1); - output = updated ? ASTTrue : a; - return output; - } - - if (AND == k) - { - ASTVec o; - ASTVec c = a.GetChildren(); - for (ASTVec::iterator - it = c.begin(), itend = c.end(); - it != itend; it++) - { - simp->UpdateAlwaysTrueFormMap(*it); - ASTNode aaa = CreateSubstitutionMap(*it); - - if (ASTTrue != aaa) - { - if (ASTFalse == aaa) - return ASTFalse; - else - o.push_back(aaa); - } - } - if (o.size() == 0) - return ASTTrue; - - if (o.size() == 1) - return o[0]; - - return nf->CreateNode(AND, o); - } - - //printf("I gave up on kind: %d node: %d\n", k, a.GetNodeNum()); - return output; - } //end of CreateSubstitutionMap() //This function records all the const-indices seen so far for each //array. It populates the map 'Arrayname_ReadindicesMap' whose key is diff --git a/src/AST/ArrayTransformer.h b/src/AST/ArrayTransformer.h index e2da1b7..c941b43 100644 --- a/src/AST/ArrayTransformer.h +++ b/src/AST/ArrayTransformer.h @@ -98,9 +98,6 @@ namespace BEEV * Helper functions to for creating substitution map * ****************************************************************/ - //fill the arrayname_readindices vector if e0 is a READ(Arr,index) - //and index is a BVCONST - void FillUp_ArrReadIndex_Vec(const ASTNode& e0, const ASTNode& e1); ASTNode TransformArrayRead(const ASTNode& term); @@ -108,6 +105,11 @@ namespace BEEV public: + //fill the arrayname_readindices vector if e0 is a READ(Arr,index) + //and index is a BVCONST + void FillUp_ArrReadIndex_Vec(const ASTNode& e0, const ASTNode& e1); + + /**************************************************************** * Public Member Functions * ****************************************************************/ @@ -152,9 +154,6 @@ namespace BEEV // variables, and returns the transformed formula ASTNode TransformFormula_TopLevel(const ASTNode& form); - // Create Substitution Map function - ASTNode CreateSubstitutionMap(const ASTNode& a); - const ASTNodeToVecMap * ArrayName_ReadIndicesMap() { return Arrayname_ReadindicesMap; diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp index 820877a..8dd54f4 100644 --- a/src/STPManager/STP.cpp +++ b/src/STPManager/STP.cpp @@ -94,12 +94,10 @@ namespace BEEV { if(bm->UserFlags.optimize_flag) { - bm->GetRunTimes()->start(RunTimes::CreateSubstitutionMap); + simplified_solved_InputToSAT = - arrayTransformer-> - CreateSubstitutionMap(simplified_solved_InputToSAT); + simp->CreateSubstitutionMap(simplified_solved_InputToSAT, arrayTransformer); - bm->GetRunTimes()->stop(RunTimes::CreateSubstitutionMap); //printf("##################################################\n"); bm->ASTNodeStats("after pure substitution: ", simplified_solved_InputToSAT); @@ -136,11 +134,9 @@ namespace BEEV { if(bm->UserFlags.optimize_flag) { - bm->GetRunTimes()->start(RunTimes::CreateSubstitutionMap); simplified_solved_InputToSAT = - arrayTransformer-> - CreateSubstitutionMap(simplified_solved_InputToSAT); - bm->GetRunTimes()->stop(RunTimes::CreateSubstitutionMap); + simp->CreateSubstitutionMap(simplified_solved_InputToSAT, arrayTransformer); + bm->ASTNodeStats("after pure substitution: ", simplified_solved_InputToSAT); diff --git a/src/simplifier/SubstitutionMap.cpp b/src/simplifier/SubstitutionMap.cpp new file mode 100644 index 0000000..5d29df8 --- /dev/null +++ b/src/simplifier/SubstitutionMap.cpp @@ -0,0 +1,121 @@ +/* + * substitutionMap.cpp + * + */ + +#include "SubstitutionMap.h" +#include "simplifier.h" +#include "../AST/ArrayTransformer.h" + +namespace BEEV +{ + +SubstitutionMap::~SubstitutionMap() +{ + delete SolverMap; +} + + +//The big substitution function +ASTNode SubstitutionMap::CreateSubstitutionMap(const ASTNode& a, ArrayTransformer*at +) +{ + if (!bm->UserFlags.wordlevel_solve_flag) + return a; + + ASTNode output = a; + //if the variable has been solved for, then simply return it + if (CheckSubstitutionMap(a, output)) + return output; + + //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; + return output; + } + if (NOT == k && SYMBOL == a[0].GetKind()) + { + bool updated = UpdateSubstitutionMap(a[0], ASTFalse); + output = updated ? ASTTrue : a; + return output; + } + + if (IFF == k) + { + ASTVec c = a.GetChildren(); + SortByArith(c); + if (SYMBOL != c[0].GetKind() || + bm->VarSeenInTerm(c[0], + simp->SimplifyFormula_NoRemoveWrites(c[1], false))) + { + return a; + } + bool updated = + UpdateSubstitutionMap(c[0], + simp->SimplifyFormula(c[1], false)); + output = updated ? ASTTrue : a; + return output; + } + + if (EQ == k) + { + //fill the arrayname readindices vector if e0 is a + //READ(Arr,index) and index is a BVCONST + ASTVec c = a.GetChildren(); + SortByArith(c); + ASTNode c1 = simp->SimplifyTerm(c[1]); + at->FillUp_ArrReadIndex_Vec(c[0], c1); + + if (SYMBOL == c[0].GetKind() + && bm->VarSeenInTerm(c[0], c1)) + { + return a; + } + + if (1 == TermOrder(c[0], c1) + && READ == c[0].GetKind() + && bm->VarSeenInTerm(c[0][1], c1)) + { + return a; + } + bool updated = UpdateSubstitutionMap(c[0], c1); + output = updated ? ASTTrue : a; + return output; + } + + if (AND == k) + { + ASTVec o; + ASTVec c = a.GetChildren(); + for (ASTVec::iterator + it = c.begin(), itend = c.end(); + it != itend; it++) + { + simp->UpdateAlwaysTrueFormMap(*it); + ASTNode aaa = CreateSubstitutionMap(*it,at); + + if (ASTTrue != aaa) + { + if (ASTFalse == aaa) + return ASTFalse; + else + o.push_back(aaa); + } + } + if (o.size() == 0) + return ASTTrue; + + if (o.size() == 1) + return o[0]; + + return bm->CreateNode(AND, o); + } + + //printf("I gave up on kind: %d node: %d\n", k, a.GetNodeNum()); + return output; +} //end of CreateSubstitutionMap() + +}; diff --git a/src/simplifier/SubstitutionMap.h b/src/simplifier/SubstitutionMap.h new file mode 100644 index 0000000..dc46d77 --- /dev/null +++ b/src/simplifier/SubstitutionMap.h @@ -0,0 +1,114 @@ +/* + * substitutionMap.h + * + */ + +#ifndef SUBSTITUTIONMAP_H_ +#define SUBSTITUTIONMAP_H_ + +#include "../AST/AST.h" +#include "../STPManager/STPManager.h" +#include "../AST/NodeFactory/SimplifyingNodeFactory.h" + +namespace BEEV { + +class Simplifier; +class ArrayTransformer; + +class SubstitutionMap { + + ASTNodeMap * SolverMap; + Simplifier *simp; + STPMgr* bm; + ASTNode ASTTrue, ASTFalse, ASTUndefined; + +public: + SubstitutionMap(Simplifier *_simp, STPMgr* _bm) { + simp = _simp; + bm = _bm; + + ASTTrue = bm->CreateNode(TRUE); + ASTFalse = bm->CreateNode(FALSE); + ASTUndefined = bm->CreateNode(UNDEFINED); + + SolverMap = new ASTNodeMap(INITIAL_TABLE_SIZE); + + } + + void clear() { + SolverMap->clear(); + } + + virtual ~SubstitutionMap(); + + //check the solver map for 'key'. If key is present, then return the + //value by reference in the argument 'output' + bool CheckSubstitutionMap(const ASTNode& key, ASTNode& output) { + ASTNodeMap::iterator it = SolverMap->find(key); + if (it != SolverMap->end()) { + output = it->second; + return true; + } + return false; + } + + //update solvermap with (key,value) pair + bool UpdateSolverMap(const ASTNode& key, const ASTNode& value) { + ASTNode var = (BVEXTRACT == key.GetKind()) ? key[0] : key; + if (!CheckSubstitutionMap(var) && key != value) { + (*SolverMap)[key] = value; + return true; + } + return false; + } //end of UpdateSolverMap() + + const ASTNodeMap * Return_SolverMap() { + return SolverMap; + } // End of SolverMap() + + + + bool CheckSubstitutionMap(const ASTNode& key) { + if (SolverMap->find(key) != SolverMap->end()) + return true; + else + return false; + } + + bool UpdateSubstitutionMap(const ASTNode& e0, const ASTNode& e1) { + int i = TermOrder(e0, e1); + if (0 == i) + return false; + + assert(e0 != e1); // One side should be a variable, the other a constant. + + //e0 is of the form READ(Arr,const), and e1 is const, or + //e0 is of the form var, and e1 is const + if (1 == i && !CheckSubstitutionMap(e0)) { + assert((e1.GetKind() == TRUE) || + (e1.GetKind() == FALSE) || + (e1.GetKind() == BVCONST)); + (*SolverMap)[e0] = e1; + return true; + } + + //e1 is of the form READ(Arr,const), and e0 is const, or + //e1 is of the form var, and e0 is const + if (-1 == i && !CheckSubstitutionMap(e1)) { + assert((e0.GetKind() == TRUE) || + (e0.GetKind() == FALSE) || + (e0.GetKind() == BVCONST)); + (*SolverMap)[e1] = e0; + return true; + } + + return false; + } + + ASTNode CreateSubstitutionMap(const ASTNode& a, ArrayTransformer*at); + +}; + +} +; +#endif /* SUBSTITUTIONMAP_H_ */ diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp index bca6fdd..95d5400 100644 --- a/src/simplifier/bvsolver.cpp +++ b/src/simplifier/bvsolver.cpp @@ -164,39 +164,6 @@ namespace BEEV return false; } //end of CheckForArrayReads() - //check the solver map for 'key'. If key is present, then return the - //value by reference in the argument 'output' - bool Simplifier::CheckSolverMap(const ASTNode& key, ASTNode& output) - { - ASTNodeMap::iterator it; - if ((it = SolverMap->find(key)) != SolverMap->end()) - { - output = it->second; - return true; - } - return false; - } //end of CheckSolverMap() - - bool Simplifier::CheckSolverMap(const ASTNode& key) - { - if (SolverMap->find(key) != SolverMap->end()) - return true; - else - return false; - } //end of CheckSolverMap() - - //update solvermap with (key,value) pair - bool Simplifier::UpdateSolverMap(const ASTNode& key, const ASTNode& value) - { - ASTNode var = (BVEXTRACT == key.GetKind()) ? key[0] : key; - if (!CheckSolverMap(var) && key != value) - { - (*SolverMap)[key] = value; - return true; - } - return false; - } //end of UpdateSolverMap() - bool BVSolver::DoNotSolveThis(const ASTNode& var) { if (DoNotSolve_TheseVars.find(var) != DoNotSolve_TheseVars.end()) diff --git a/src/simplifier/consteval.cpp b/src/simplifier/consteval.cpp index fb9df82..d81f238 100644 --- a/src/simplifier/consteval.cpp +++ b/src/simplifier/consteval.cpp @@ -696,7 +696,7 @@ namespace BEEV { ASTNode OutputNode; - if (CheckSolverMap(t, OutputNode)) + if (CheckSubstitutionMap(t, OutputNode)) return OutputNode; OutputNode = NonMemberBVConstEvaluator(t); diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp index 183adbe..d2a2680 100644 --- a/src/simplifier/simplifier.cpp +++ b/src/simplifier/simplifier.cpp @@ -130,58 +130,37 @@ namespace BEEV (*SimplifyMap)[key] = value; } + // 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) + { + return substitutionMap.UpdateSolverMap(key,value); + } + bool Simplifier::CheckSubstitutionMap(const ASTNode& key, ASTNode& output) { - ASTNode k = key; - ASTNodeMap::iterator it = SolverMap->find(key); - if (it != SolverMap->end()) - { - output = it->second; - return true; - } - return false; + return substitutionMap.CheckSubstitutionMap(key,output); } bool Simplifier::CheckSubstitutionMap(const ASTNode& key) { - if (SolverMap->find(key) != SolverMap->end()) - return true; - else - return false; + return substitutionMap.CheckSubstitutionMap(key); } bool Simplifier::UpdateSubstitutionMap(const ASTNode& e0, const ASTNode& e1) { - int i = TermOrder(e0, e1); - if (0 == i) - return false; - - assert(e0 != e1); // One side should be a variable, the other a constant. - - //e0 is of the form READ(Arr,const), and e1 is const, or - //e0 is of the form var, and e1 is const - if (1 == i && !CheckSubstitutionMap(e0)) - { - assert((e1.GetKind() == TRUE) || - (e1.GetKind() == FALSE) || - (e1.GetKind() == BVCONST)); - (*SolverMap)[e0] = e1; - return true; - } - - //e1 is of the form READ(Arr,const), and e0 is const, or - //e1 is of the form var, and e0 is const - if (-1 == i && !CheckSubstitutionMap(e1)) - { - assert((e0.GetKind() == TRUE) || - (e0.GetKind() == FALSE) || - (e0.GetKind() == BVCONST)); - (*SolverMap)[e1] = e0; - return true; - } - - return false; + return substitutionMap.UpdateSubstitutionMap(e0,e1); } + // --- Substitution Map methods.... + bool Simplifier::CheckMultInverseMap(const ASTNode& key, ASTNode& output) { @@ -426,7 +405,7 @@ namespace BEEV output = pushNeg ? ASTTrue : ASTFalse; break; case SYMBOL: - if (!CheckSolverMap(a, output)) + if (!CheckSubstitutionMap(a, output)) { output = a; } @@ -1710,7 +1689,7 @@ namespace BEEV { return output; } - if (CheckSolverMap(inputterm, output)) + if (CheckSubstitutionMap(inputterm, output)) { return SimplifyTerm(output, VarConstMap); } diff --git a/src/simplifier/simplifier.h b/src/simplifier/simplifier.h index 928b25c..b78924d 100644 --- a/src/simplifier/simplifier.h +++ b/src/simplifier/simplifier.h @@ -13,6 +13,7 @@ #include "../AST/AST.h" #include "../STPManager/STPManager.h" #include "../AST/NodeFactory/SimplifyingNodeFactory.h" +#include "SubstitutionMap.h" namespace BEEV { @@ -34,7 +35,6 @@ namespace BEEV // value is simplified node. ASTNodeMap * SimplifyMap; ASTNodeMap * SimplifyNegMap; - ASTNodeMap * SolverMap; ASTNodeSet AlwaysTrueFormMap; ASTNodeMap MultInverseMap; @@ -51,17 +51,19 @@ namespace BEEV NodeFactory * nf; + SubstitutionMap substitutionMap; + void checkIfInSimplifyMap(const ASTNode& n, ASTNodeSet visited); public: /**************************************************************** * Public Member Functions * ****************************************************************/ - Simplifier(STPMgr * bm) : _bm(bm) + Simplifier(STPMgr * bm) : _bm(bm), + substitutionMap(this,bm) { SimplifyMap = new ASTNodeMap(INITIAL_TABLE_SIZE); SimplifyNegMap = new ASTNodeMap(INITIAL_TABLE_SIZE); - SolverMap = new ASTNodeMap(INITIAL_TABLE_SIZE); ReadOverWrite_NewName_Map = new ASTNodeMap(); ASTTrue = bm->CreateNode(TRUE); @@ -75,7 +77,6 @@ namespace BEEV { delete SimplifyMap; delete SimplifyNegMap; - delete SolverMap; delete ReadOverWrite_NewName_Map; delete nf; } @@ -88,10 +89,6 @@ namespace BEEV bool CheckMap(ASTNodeMap* VarConstMap, const ASTNode& key, ASTNode& output); - //substitution - bool CheckSubstitutionMap(const ASTNode& a, ASTNode& output); - bool CheckSubstitutionMap(const ASTNode& a); - bool UpdateSubstitutionMap(const ASTNode& e0, const ASTNode& e1); //functions for checking and updating simplifcation map bool CheckSimplifyMap(const ASTNode& key, @@ -106,9 +103,15 @@ namespace BEEV void UpdateMultInverseMap(const ASTNode& key, const ASTNode& value); //Map for solved variables - bool CheckSolverMap(const ASTNode& a, ASTNode& output); - bool CheckSolverMap(const ASTNode& a); bool UpdateSolverMap(const ASTNode& e0, const ASTNode& e1); + ASTNode CreateSubstitutionMap(const ASTNode& a, + ArrayTransformer *at); + + //substitution + bool CheckSubstitutionMap(const ASTNode& a, ASTNode& output); + bool CheckSubstitutionMap(const ASTNode& a); + bool UpdateSubstitutionMap(const ASTNode& e0, const ASTNode& e1); + void ResetSimplifyMaps(void); @@ -236,18 +239,18 @@ namespace BEEV const ASTNodeMap * Return_SolverMap() { - return SolverMap; + return substitutionMap.Return_SolverMap(); } // End of SolverMap() void ClearAllTables(void) { SimplifyMap->clear(); SimplifyNegMap->clear(); - SolverMap->clear(); ReadOverWrite_NewName_Map->clear(); NewName_ReadOverWrite_Map.clear(); AlwaysTrueFormMap.clear(); MultInverseMap.clear(); + substitutionMap.clear(); } };//end of class Simplifier }; //end of namespace -- 2.47.3