From f9546315ab6ece42f48fa8b2e2e53abcd1f00b74 Mon Sep 17 00:00:00 2001 From: bdemsky Date: Sat, 2 Sep 2017 15:24:53 -0700 Subject: [PATCH] Work on canonicalizing the AST so our analysis can handle fewer cases --- src/AST/rewriter.cc | 70 +++----------------- src/AST/rewriter.h | 2 +- src/ASTAnalyses/polarityassignment.cc | 31 +-------- src/Backend/satencoder.cc | 8 +-- src/csolver.cc | 93 ++++++++++----------------- src/csolver.h | 5 +- 6 files changed, 48 insertions(+), 161 deletions(-) diff --git a/src/AST/rewriter.cc b/src/AST/rewriter.cc index a7df7c8..9751e05 100644 --- 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 5387e4e..3e3488f 100644 --- 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 1478930..2aa9e5d 100644 --- 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 1d6b4f4..fd60f45 100644 --- 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 22b0661..c3208b9 100644 --- a/src/csolver.cc +++ b/src/csolver.cc @@ -17,6 +17,7 @@ #include "structs.h" #include "orderresolver.h" #include "integerencoding.h" +#include 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 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;iinputs.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 8f5d697..618f88e 100644 --- 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; -- 2.34.1