Pull up ITEs when two ITEs with the same conditional are arguments to a binary operation.

e.g. turns (bvslt (ite a  b c) (ite a d e)) INTO (ite a (bvslt b d) (bvslt c e)

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@97 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/AST/AST.h b/AST/AST.h
index d8862c495438b6bbc3d0a3cd07077b310b11020c..a170dc5f294697dafe0da0cc398a21c8d6bc9ef8 100644 (file)
--- a/AST/AST.h
+++ b/AST/AST.h
@@ -1580,6 +1580,8 @@ public:
        ASTNode SimplifyAtomicFormula(const ASTNode& a, bool pushNeg);
        ASTNode CreateSimplifiedEQ(const ASTNode& t1, const ASTNode& t2);
        ASTNode ITEOpt_InEqs(const ASTNode& in1);
+       ASTNode PullUpITE(const ASTNode& in);
+       ASTNode RemoveContradictionsFromAND(const ASTNode& in);
        ASTNode CreateSimplifiedTermITE(const ASTNode& t1, const ASTNode& t2, const ASTNode& t3);
        ASTNode CreateSimplifiedFormulaITE(const ASTNode& in0, const ASTNode& in1, const ASTNode& in2);
        ASTNode CreateSimplifiedINEQ(Kind k, const ASTNode& a0, const ASTNode& a1, bool pushNeg);

diff --git a/Makefile.common b/Makefile.common
index d160e627352e11b8e317740d229363a65c2d12db..fcc665a35d37745106769a0c2f9a5db07d0ae652 100644 (file)
--- a/Makefile.common
+++ b/Makefile.common
@@ -9,7 +9,7 @@
 
 #OPTIMIZE = -g -pg # Debugging and gprof-style profiling
 #OPTIMIZE = -g     # Debugging
-OPTIMIZE = -O3     # Maximum optimization
+OPTIMIZE = -O3 -DNDEBUG     # Maximum optimization
 
 CFLAGS_BASE = $(OPTIMIZE) $(OPTIONS1) $(OPTIONS2) 
 # You can compile using make STATIC=true to compile a statically linked executable

diff --git a/simplifier/simplifier.cpp b/simplifier/simplifier.cpp
index 90b49c8c9dbdcd83e76c72d33b77103949292849..4a6b7af9311962a6cb5d4e6aa1755da4816e0af1 100644 (file)
--- a/simplifier/simplifier.cpp
+++ b/simplifier/simplifier.cpp
@@ -227,6 +227,9 @@ ASTNode BeevMgr::SimplifyFormula(const ASTNode& b, bool pushNeg)
        if (CheckSimplifyMap(a, output, pushNeg))
                return output;
 
+       a = PullUpITE(a);
+       kind = a.GetKind(); // pullUpITE can change the Kind of the node.
+
        switch (kind)
        {
                case AND:
@@ -476,6 +479,72 @@ ASTNode BeevMgr::CreateSimplifiedINEQ(Kind k, const ASTNode& left, const ASTNode
        return output;
 }
 
+//Look through the AND Node for terms that contradict.
+//Should be made significantly more general..
+ASTNode BeevMgr::RemoveContradictionsFromAND(const ASTNode& in)
+{
+       assert(AND == in.GetKind());
+       const int childrenSize = in.GetChildren().size();
+
+       for (int i = 0; i < childrenSize; i++)
+       {
+               if (BVLT != in[i].GetKind())
+                       continue;
+
+               for (int j = i + 1; j < childrenSize; j++)
+               {
+                       if (BVLT != in[j].GetKind())
+                               continue;
+                       if (in[i][0] == in[j][1] && in[i][1] == in[j][0]) // parameters are swapped.
+                               return ASTFalse;
+               }
+       }
+       return in;
+}
+
+// turns say (bvslt (ite a  b c) (ite a d e)) INTO (ite a (bvslt b d) (bvslt c e))
+// Expensive. But makes some other simplifications possible.
+ASTNode BeevMgr::PullUpITE(const ASTNode& in)
+{
+       if (2 != in.GetChildren().size())
+               return in;
+       if (ITE != in[0].GetKind())
+               return in;
+       if (ITE != in[1].GetKind())
+               return in;
+       if (in[0][0] != in[1][0]) // if the conditional is not equal.
+               return in;
+
+       // Consider equals. It takes bitvectors and returns a boolean.
+       // Consider add. It takes bitvectors and returns bitvectors.
+       // Consider concat. The bitwidth of each side could vary.
+
+       ASTNode l1;
+       ASTNode l2;
+       ASTNode result;
+
+       if (in.GetType() == BOOLEAN_TYPE)
+       {
+               l1 = CreateNode(in.GetKind(), in[0][1], in[1][1]);
+               l2 = CreateNode(in.GetKind(), in[0][2], in[1][2]);
+               result = CreateNode(ITE, in[0][0], l1, l2);
+       }
+       else
+       {
+               l1 = CreateTerm(in.GetKind(), in.GetValueWidth(), in[0][1], in[1][1]);
+               l2 = CreateTerm(in.GetKind(), in.GetValueWidth(), in[0][2], in[1][2]);
+               result = CreateTerm(ITE, in.GetValueWidth(), in[0][0], l1, l2);
+       }
+
+       assert(result.GetType() == in.GetType());
+       assert(result.GetValueWidth() == in.GetValueWidth());
+       assert(result.GetIndexWidth() == in.GetIndexWidth());
+       assert(BVTypeCheck(result));
+
+       return result;
+}
+
+
 //takes care of some simple ITE Optimizations in the context of equations
 ASTNode BeevMgr::ITEOpt_InEqs(const ASTNode& in)
 {
@@ -753,6 +822,11 @@ ASTNode BeevMgr::SimplifyAndOrFormula(const ASTNode& a, bool pushNeg)
                        break;
                }
        }
+
+       // I haven't verified this is useful.
+       //if (output.GetKind() == AND)
+       //      output = RemoveContradictionsFromAND(output);
+
        //memoize
        UpdateSimplifyMap(a, output, pushNeg);
        //cerr << "output:\n" << output << endl;
@@ -1162,8 +1236,10 @@ ASTNode BeevMgr::SimplifyTerm_TopLevel(const ASTNode& b)
 }
 
 //This function simplifies terms based on their kind
-ASTNode BeevMgr::SimplifyTerm(const ASTNode& inputterm)
+ASTNode BeevMgr::SimplifyTerm(const ASTNode& actualInputterm)
 {
+       ASTNode inputterm(actualInputterm); // mutable local copy.
+
        //cout << "SimplifyTerm: input: " << a << endl;
        if (!optimize)
        {
@@ -1197,6 +1273,10 @@ ASTNode BeevMgr::SimplifyTerm(const ASTNode& inputterm)
        }
 
        unsigned int inputValueWidth = inputterm.GetValueWidth();
+
+       inputterm = PullUpITE(inputterm);
+       k = inputterm.GetKind(); // pull up ITE can change the kind of the node
+
        switch (k)
        {
                case BVCONST:
@@ -3075,7 +3155,7 @@ ASTNode BeevMgr::ConvertBVSXToITE(const ASTNode& a)
 
 ASTNode BeevMgr::RemoveWrites_TopLevel(const ASTNode& term)
 {
-       if (READ != term.GetKind() && WRITE != term[0].GetKind())
+       if (READ != term.GetKind() || WRITE != term[0].GetKind())
        {
                FatalError("RemovesWrites: Input must be a READ over a WRITE", term);
        }