BitBlasting,
Solving,
BVSolver,
- PropagateEqualities,
+ CreateSubstitutionMap,
SendingToSAT,
CounterExampleGeneration,
SATSimplifying,
#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 <memory>
} //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;
}
// 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"))
// 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;
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);
// 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")))
{
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
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);
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())
{
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);
// 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();
#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
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);
/****************************************************************
+++ /dev/null
-#include <string>
-#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;
- }
-
-}
-;
+++ /dev/null
-#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<int> 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
{
using simplifier::constantBitP::Dependencies;
- const string RemoveUnconstrained::message = "After Unconstrained variable:";
-
RemoveUnconstrained::RemoveUnconstrained(STPMgr& _bm) :
bm(_bm)
{
public:
- static const string message;
RemoveUnconstrained(STPMgr& bm);
virtual
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.
+//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)
ASTNodeSet rhs; // All the rhs that have been seeen.
set<ASTNodeSet*> rhsAlreadyAdded;
VariablesInExpression::SymbolPtrSet rhs_visited; // the rhs contains all the variables in here already.
-
+ HASHSET<int> alreadyVisited;
int loopCount;
{
SolverMap->clear();
haveAppliedSubstitutionMap();
- //alreadyVisited.clear();
+ alreadyVisited.clear();
}
virtual ~SubstitutionMap();
return false;
}
-
+ ASTNode CreateSubstitutionMap(const ASTNode& a, ArrayTransformer*at);
ASTNode applySubstitutionMap(const ASTNode& n);
}
}
+ // 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)
//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);
projects / francis / stp.git / commitdiff