BitBlasting,
Solving,
BVSolver,
- CreateSubstitutionMap,
+ PropagateEqualities,
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, 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;
}
// 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"))
// 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);
+ simplified_solved_InputToSAT = sizeReducing(simplified_solved_InputToSAT, bvSolver,pe);
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, initial_difficulty_score);
+ simplified_solved_InputToSAT = callSizeReducing(simplified_solved_InputToSAT, bvSolver,pe, initial_difficulty_score);
if ((!arrayops || bm->UserFlags.isSet("array-difficulty-reversion", "1")))
{
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
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);
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())
{
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);
// 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);
+ 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
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);
/****************************************************************
--- /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