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
* 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);
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 *
****************************************************************/
// 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;
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);
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);
--- /dev/null
+/*
+ * 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()
+
+};
--- /dev/null
+/*
+ * 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_ */
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())
{
ASTNode OutputNode;
- if (CheckSolverMap(t, OutputNode))
+ if (CheckSubstitutionMap(t, OutputNode))
return OutputNode;
OutputNode = NonMemberBVConstEvaluator(t);
(*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)
{
output = pushNeg ? ASTTrue : ASTFalse;
break;
case SYMBOL:
- if (!CheckSolverMap(a, output))
+ if (!CheckSubstitutionMap(a, output))
{
output = a;
}
{
return output;
}
- if (CheckSolverMap(inputterm, output))
+ if (CheckSubstitutionMap(inputterm, output))
{
return SimplifyTerm(output, VarConstMap);
}
#include "../AST/AST.h"
#include "../STPManager/STPManager.h"
#include "../AST/NodeFactory/SimplifyingNodeFactory.h"
+#include "SubstitutionMap.h"
namespace BEEV
{
// value is simplified node.
ASTNodeMap * SimplifyMap;
ASTNodeMap * SimplifyNegMap;
- ASTNodeMap * SolverMap;
ASTNodeSet AlwaysTrueFormMap;
ASTNodeMap MultInverseMap;
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);
{
delete SimplifyMap;
delete SimplifyNegMap;
- delete SolverMap;
delete ReadOverWrite_NewName_Map;
delete nf;
}
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,
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);
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
projects / francis / stp.git / commitdiff