Work on canonicalizing the AST so our analysis can handle fewer cases

diff --git a/src/AST/rewriter.cc b/src/AST/rewriter.cc
index a7df7c847a4160cde70c800df880855188bfb34f..9751e057f3e599ce320571fb6cc7bd98bc29b087 100644 (file)
--- a/src/AST/rewriter.cc
+++ b/src/AST/rewriter.cc
@@ -15,21 +15,16 @@ void CSolver::replaceBooleanWithTrue(Boolean *bexpr) {
                case SATC_AND:
                        handleANDTrue(logicop, bexpr);
                        break;
-               case SATC_OR:
-                       replaceBooleanWithTrue(parent);
-                       break;
                case SATC_NOT:
                        replaceBooleanWithFalse(parent);
                        break;
                case SATC_IFF:
-                       handleXORFalse(logicop, bexpr);
+                       handleIFFTrue(logicop, bexpr);
                        break;
+               case SATC_OR:
                case SATC_XOR:
-                       handleXORTrue(logicop, bexpr);
-                       break;
                case SATC_IMPLIES:
-                       handleIMPLIESTrue(logicop, bexpr);
-                       break;
+                       ASSERT(0);
                }
        }
 }
@@ -57,7 +52,7 @@ void CSolver::replaceBooleanWithBoolean(Boolean *oldb, Boolean *newb) {
        }
 }
 
-void handleXORTrue(BooleanLogic *bexpr, Boolean *child) {
+void handleIFFFalse(BooleanLogic *bexpr, Boolean *child) {
        uint size = bexpr->inputs.getSize();
        Boolean *b = bexpr->inputs.get(0);
        uint childindex = (b == child) ? 0 : 1;
@@ -65,38 +60,13 @@ void handleXORTrue(BooleanLogic *bexpr, Boolean *child) {
        bexpr->op = SATC_NOT;
 }
 
-void CSolver::handleXORFalse(BooleanLogic *bexpr, Boolean *child) {
+void CSolver::handleIFFTrue(BooleanLogic *bexpr, Boolean *child) {
        uint size = bexpr->inputs.getSize();
        Boolean *b = bexpr->inputs.get(0);
        uint otherindex = (b == child) ? 1 : 0;
        replaceBooleanWithBoolean(bexpr, bexpr->inputs.get(otherindex));
 }
 
-void CSolver::handleIMPLIESTrue(BooleanLogic *bexpr, Boolean *child) {
-       uint size = bexpr->inputs.getSize();
-       Boolean *b = bexpr->inputs.get(0);
-       if (b == child) {
-               //Replace with other term
-               replaceBooleanWithBoolean(bexpr, bexpr->inputs.get(1));
-       } else {
-               //Statement is true...
-               replaceBooleanWithTrue(bexpr);
-       }
-}
-
-void CSolver::handleIMPLIESFalse(BooleanLogic *bexpr, Boolean *child) {
-       uint size = bexpr->inputs.getSize();
-       Boolean *b = bexpr->inputs.get(0);
-       if (b == child) {
-               //Statement is true...
-               replaceBooleanWithTrue(bexpr);
-       } else {
-               //Make into negation of first term
-               bexpr->inputs.get(1);
-               bexpr->op = SATC_NOT;
-       }
-}
-
 void CSolver::handleANDTrue(BooleanLogic *bexpr, Boolean *child) {
        uint size = bexpr->inputs.getSize();
 
@@ -117,25 +87,6 @@ void CSolver::handleANDTrue(BooleanLogic *bexpr, Boolean *child) {
        }
 }
 
-void CSolver::handleORFalse(BooleanLogic *bexpr, Boolean *child) {
-       uint size = bexpr->inputs.getSize();
-
-       if (size == 1) {
-               replaceBooleanWithFalse(bexpr);
-       }
-
-       for (uint i = 0; i < size; i++) {
-               Boolean *b = bexpr->inputs.get(i);
-               if (b == child) {
-                       bexpr->inputs.remove(i);
-               }
-       }
-
-       if (size == 2) {
-               replaceBooleanWithBoolean(bexpr, bexpr->inputs.get(0));
-       }
-}
-
 void CSolver::replaceBooleanWithFalse(Boolean *bexpr) {
        if (constraints.contains(bexpr)) {
                setUnSAT();
@@ -150,21 +101,16 @@ void CSolver::replaceBooleanWithFalse(Boolean *bexpr) {
                case SATC_AND:
                        replaceBooleanWithFalse(parent);
                        break;
-               case SATC_OR:
-                       handleORFalse(logicop, bexpr);
-                       break;
                case SATC_NOT:
                        replaceBooleanWithTrue(parent);
                        break;
                case SATC_IFF:
-                       handleXORTrue(logicop, bexpr);
+                       handleIFFFalse(logicop, bexpr);
                        break;
+               case SATC_OR:
                case SATC_XOR:
-                       handleXORFalse(logicop, bexpr);
-                       break;
                case SATC_IMPLIES:
-                       handleIMPLIESFalse(logicop, bexpr);
-                       break;
+                       ASSERT(0);
                }
        }
 }

diff --git a/src/AST/rewriter.h b/src/AST/rewriter.h
index 5387e4ef15ec0aa37c4a9d98a2be1c88a556bbac..3e3488f67ca5ef29396af60affdc5fbaa4b2816a 100644 (file)
--- a/src/AST/rewriter.h
+++ b/src/AST/rewriter.h
@@ -2,6 +2,6 @@
 #define REWRITER_H
 #include "classlist.h"
 
-void handleXORTrue(BooleanLogic *bexpr, Boolean *child);
+void handleIFFFalse(BooleanLogic *bexpr, Boolean *child);
 
 #endif

diff --git a/src/ASTAnalyses/polarityassignment.cc b/src/ASTAnalyses/polarityassignment.cc
index 14789304b49a797d74a14e4da5af02b6008dcd76..2aa9e5d8e491ac24cf03690243cbb0147339e633 100644 (file)
--- a/src/ASTAnalyses/polarityassignment.cc
+++ b/src/ASTAnalyses/polarityassignment.cc
@@ -81,8 +81,7 @@ BooleanValue negateBooleanValue(BooleanValue This) {
 void computeLogicOpPolarity(BooleanLogic *This) {
        Polarity parentpolarity = This->polarity;
        switch (This->op) {
-       case SATC_AND:
-       case SATC_OR: {
+       case SATC_AND: {
                uint size = This->inputs.getSize();
                for (uint i = 0; i < size; i++) {
                        Boolean *tmp = This->inputs.get(i);
@@ -95,19 +94,11 @@ void computeLogicOpPolarity(BooleanLogic *This) {
                updatePolarity(tmp, negatePolarity(parentpolarity));
                break;
        }
-       case SATC_IFF:
-       case SATC_XOR: {
+       case SATC_IFF: {
                updatePolarity(This->inputs.get(0), P_BOTHTRUEFALSE);
                updatePolarity(This->inputs.get(1), P_BOTHTRUEFALSE);
                break;
        }
-       case SATC_IMPLIES: {
-               Boolean *left = This->inputs.get(0);
-               updatePolarity(left, negatePolarity( parentpolarity));
-               Boolean *right = This->inputs.get(1);
-               updatePolarity(right, parentpolarity);
-               break;
-       }
        default:
                ASSERT(0);
        }
@@ -125,28 +116,10 @@ void computeLogicOpBooleanValue(BooleanLogic *This) {
                }
                return;
        }
-       case SATC_OR: {
-               if (parentbv == BV_MUSTBEFALSE || parentbv == BV_UNSAT) {
-                       uint size = This->inputs.getSize();
-                       for (uint i = 0; i < size; i++) {
-                               updateMustValue(This->inputs.get(i), parentbv);
-                       }
-               }
-               return;
-       }
        case SATC_NOT:
                updateMustValue(This->inputs.get(0), negateBooleanValue(parentbv));
                return;
-       case SATC_IMPLIES:
-               //implies is really an or with the first term negated
-               if (parentbv == BV_MUSTBEFALSE || parentbv == BV_UNSAT) {
-                       uint size = This->inputs.getSize();
-                       updateMustValue(This->inputs.get(0), negateBooleanValue(parentbv));
-                       updateMustValue(This->inputs.get(1), parentbv);
-               }
-               return;
        case SATC_IFF:
-       case SATC_XOR:
                return;
        default:
                ASSERT(0);

diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc
index 1d6b4f4e7dc91c65d1643e92e62333ffba08125d..fd60f45df737ab7ebcab9cbbda7830808a34a075 100644 (file)
--- a/src/Backend/satencoder.cc
+++ b/src/Backend/satencoder.cc
@@ -87,16 +87,14 @@ Edge SATEncoder::encodeLogicSATEncoder(BooleanLogic *constraint) {
        switch (constraint->op) {
        case SATC_AND:
                return constraintAND(cnf, constraint->inputs.getSize(), array);
-       case SATC_OR:
-               return constraintOR(cnf, constraint->inputs.getSize(), array);
        case SATC_NOT:
                return constraintNegate(array[0]);
-       case SATC_XOR:
-               return constraintXOR(cnf, array[0], array[1]);
        case SATC_IFF:
                return constraintIFF(cnf, array[0], array[1]);
+       case SATC_OR:
+       case SATC_XOR:
        case SATC_IMPLIES:
-               return constraintIMPLIES(cnf, array[0], array[1]);
+               //Don't handle, translate these away...
        default:
                model_print("Unhandled case in encodeLogicSATEncoder %u", constraint->op);
                exit(-1);

diff --git a/src/csolver.cc b/src/csolver.cc
index 22b0661cb9228b765f7f7f4111ebecd8dd9bb6a7..c3208b91ec5fdd2747ffc763fa3e3b52dd60291a 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -17,6 +17,7 @@
 #include "structs.h"
 #include "orderresolver.h"
 #include "integerencoding.h"
+#include <stdlib.h>
 
 CSolver::CSolver() :
        boolTrue(new BooleanConst(true)),
@@ -239,6 +240,16 @@ Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean *arg) {
        return applyLogicalOperation(op, array, 1);
 }
 
+static int ptrcompares(const void *p1, const void *p2) {
+       uintptr_t b1 = *(uintptr_t const *) p1;
+  uintptr_t b2 = *(uintptr_t const *) p2;
+       if (b1 < b2)
+               return -1;
+       else if (b1 == b2)
+               return 0;
+       else
+               return 1;
+}
 
 Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize) {
        Boolean *newarray[asize];
@@ -264,53 +275,11 @@ Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize)
                }
                break;
        }
-       case SATC_XOR: {
-               for (uint i = 0; i < 2; i++) {
-                       if (array[i]->type == BOOLCONST) {
-                               if (array[i]->isTrue()) {
-                                       newarray[0] = array[1 - i];
-                                       return applyLogicalOperation(SATC_NOT, newarray, 1);
-                               } else
-                                       return array[1 - i];
-                       }
-               }
-               break;
-       }
        case SATC_OR: {
-               uint newindex = 0;
-               for (uint i = 0; i < asize; i++) {
-                       Boolean *b = array[i];
-                       if (b->type == BOOLCONST) {
-                               if (b->isTrue())
-                                       return boolTrue;
-                               else
-                                       continue;
-                       } else
-                               newarray[newindex++] = b;
+               for (uint i =0; i <asize; i++) {
+                       newarray[i] = applyLogicalOperation(SATC_NOT, array[i]);
                }
-               if (newindex == 0) {
-                       return boolFalse;
-               } else if (newindex == 1)
-                       return newarray[0];
-               else if (newindex == 2) {
-                       bool isNot0 = (newarray[0]->type == BOOLCONST) && ((BooleanLogic *)newarray[0])->op == SATC_NOT;
-                       bool isNot1 = (newarray[1]->type == BOOLCONST) && ((BooleanLogic *)newarray[1])->op == SATC_NOT;
-
-                       if (isNot0 != isNot1) {
-                               if (isNot0) {
-                                       newarray[0] = ((BooleanLogic *) newarray[0])->inputs.get(0);
-                               } else {
-                                       Boolean *tmp =  ((BooleanLogic *) array[1])->inputs.get(0);
-                                       array[1] = array[0];
-                                       array[0] = tmp;
-                               }
-                               return applyLogicalOperation(SATC_IMPLIES, newarray, 2);
-                       }
-               } else {
-                       array = newarray;
-                       asize = newindex;
-               }
-               break;
+               return applyLogicalOperation(SATC_NOT, applyLogicalOperation(SATC_AND, newarray, asize));
        }
        case SATC_AND: {
                uint newindex = 0;
@@ -329,26 +298,19 @@ Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize)
                } else if (newindex == 1) {
                        return newarray[0];
                } else {
+                       qsort(newarray, asize, sizeof(Boolean *), ptrcompares);
                        array = newarray;
                        asize = newindex;
                }
                break;
        }
+       case SATC_XOR: {
+               //handle by translation
+               return applyLogicalOperation(SATC_NOT, applyLogicalOperation(SATC_IFF, array, asize));
+       }
        case SATC_IMPLIES: {
-               if (array[0]->type == BOOLCONST) {
-                       if (array[0]->isTrue()) {
-                               return array[1];
-                       } else {
-                               return boolTrue;
-                       }
-               } else if (array[1]->type == BOOLCONST) {
-                       if (array[1]->isTrue()) {
-                               return array[1];
-                       } else {
-                               return applyLogicalOperation(SATC_NOT, array, 1);
-                       }
-               }
-               break;
+               //handle by translation
+               return applyLogicalOperation(SATC_OR, applyLogicalOperation(SATC_NOT, array[0]), array[1]);
        }
        }
 
@@ -376,8 +338,19 @@ void CSolver::addConstraint(Boolean *constraint) {
                return;
        else if (constraint == boolFalse)
                setUnSAT();
-       else
+       else {
+               if (constraint->type == LOGICOP) {
+                       BooleanLogic *b=(BooleanLogic *) constraint;
+                       if (b->op==SATC_AND) {
+                               for(uint i=0;i<b->inputs.getSize();i++) {
+                                       addConstraint(b->inputs.get(i));
+                               }
+                               return;
+                       }
+               }
+
                constraints.add(constraint);
+       }
 }
 
 Order *CSolver::createOrder(OrderType type, Set *set) {

diff --git a/src/csolver.h b/src/csolver.h
index 8f5d6975b5062bbc5245cf0186d1b1bc955937f5..618f88e0b4ed0635454f8f86d763dbdb70acf687 100644 (file)
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -147,11 +147,8 @@ public:
        CMEMALLOC;
 
 private:
-       void handleXORFalse(BooleanLogic *bexpr, Boolean *child);
-       void handleIMPLIESTrue(BooleanLogic *bexpr, Boolean *child);
-       void handleIMPLIESFalse(BooleanLogic *bexpr, Boolean *child);
+       void handleIFFTrue(BooleanLogic *bexpr, Boolean *child);
        void handleANDTrue(BooleanLogic *bexpr, Boolean *child);
-       void handleORFalse(BooleanLogic *bexpr, Boolean *child);
 
        /** This is a vector of constraints that must be satisfied. */
        HashsetBoolean constraints;