Merge branch 'master' into msoos-no-const-as-macro-2
diff --git a/include/stp/STPManager/UserDefinedFlags.h b/include/stp/STPManager/UserDefinedFlags.h
index 1f0f145..b9c8dc9 100644
--- a/include/stp/STPManager/UserDefinedFlags.h
+++ b/include/stp/STPManager/UserDefinedFlags.h
@@ -162,7 +162,7 @@
enable_bitblast_simplification = false;
wordlevel_solve_flag = false;
propagate_equalities = false;
- enable_flatten = false;
+ enable_flatten = true;
}
UserDefinedFlags()
diff --git a/lib/Simplifier/PropagateEqualities.cpp b/lib/Simplifier/PropagateEqualities.cpp
index bb8c11a..c00f081 100644
--- a/lib/Simplifier/PropagateEqualities.cpp
+++ b/lib/Simplifier/PropagateEqualities.cpp
@@ -243,98 +243,101 @@
if (updated)
return output;
-// The below block should be subsumed by the searchXOR function which
-// generalises it.
-// So the below block should never do anything..
-#ifndef NDEBUG
- if (a.Degree() != 2)
- return output;
-
- int to = TermOrder(a[0], a[1]);
- if (0 == to)
+ // The below block should be subsumed by the searchXOR function which
+ // generalises it.
+ // So the below block should never do anything..
+ if (!timeOut)
{
- 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(BVNOT, 1, a[0][0][0]));
+ #ifndef NDEBUG
+ if (a.Degree() != 2)
+ return output;
- if (simp->UpdateSolverMap(symbol, newN))
+ int to = TermOrder(a[0], a[1]);
+ if (0 == to)
{
- assert(false);
- 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(BVNOT, 1, a[1][0][0]));
+ 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(BVNOT, 1, a[0][0][0]));
- if (simp->UpdateSolverMap(symbol, newN))
+ if (simp->UpdateSolverMap(symbol, newN))
+ {
+ assert(false);
+ 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(BVNOT, 1, a[1][0][0]));
+
+ if (simp->UpdateSolverMap(symbol, newN))
+ {
+ assert(false);
+ 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(BVNOT, 1, a[0][0]), a[0][0]);
+
+ if (simp->UpdateSolverMap(symbol, newN))
+ {
+ assert(false);
+ 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(BVNOT, 1, a[1][0]), a[1][0]);
+
+ if (simp->UpdateSolverMap(symbol, newN))
+ {
+ assert(false);
+ output = ASTTrue;
+ }
+ }
+ else
+ return output;
+ }
+ else
{
- assert(false);
- output = ASTTrue;
- }
- }
- else if (a[0].GetKind() == EQ && a[0][0].GetValueWidth() == 1 &&
- a[0][1].GetKind() == SYMBOL)
- {
- // XOR ((= 1 v) ... )
+ ASTNode symbol, rhs;
+ if (to == 1)
+ {
+ symbol = a[0];
+ rhs = a[1];
+ }
+ else
+ {
+ symbol = a[1];
+ rhs = a[0];
+ }
- const ASTNode& symbol = a[0][1];
- const ASTNode newN = nf->CreateTerm(
- ITE, 1, a[1], nf->CreateTerm(BVNOT, 1, a[0][0]), a[0][0]);
+ assert(symbol.GetKind() == SYMBOL);
- if (simp->UpdateSolverMap(symbol, newN))
- {
- assert(false);
- output = ASTTrue;
+ if (simp->UpdateSolverMap(symbol, nf->CreateNode(NOT, rhs)))
+ {
+ assert(false);
+ 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(BVNOT, 1, a[1][0]), a[1][0]);
-
- if (simp->UpdateSolverMap(symbol, newN))
- {
- assert(false);
- output = ASTTrue;
- }
- }
- else
- return output;
+ #endif
}
- 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)))
- {
- assert(false);
- output = ASTTrue;
- }
- }
-#endif
}
else if (AND == k)
{
