From 6b81425e00f5a8e1e563ff268cca3c9bce355bcb Mon Sep 17 00:00:00 2001 From: bdemsky Date: Sat, 2 Sep 2017 18:11:59 -0700 Subject: [PATCH] Compiles --- src/AST/asthash.cc | 6 +- src/AST/boolean.cc | 35 +++++---- src/AST/boolean.h | 10 ++- src/AST/element.cc | 2 +- src/AST/element.h | 4 +- src/AST/rewriter.cc | 108 +++++++++++++------------- src/AST/rewriter.h | 2 - src/ASTAnalyses/polarityassignment.cc | 45 +++++------ src/ASTTransform/integerencoding.cc | 2 +- src/Backend/satencoder.cc | 12 +-- src/Backend/satencoder.h | 2 +- src/Backend/satfuncopencoder.cc | 2 +- src/Collections/corestructs.h | 28 ++++++- src/Encoders/naiveencoder.cc | 8 +- src/csolver.cc | 77 +++++++++--------- src/csolver.h | 46 +++++------ 16 files changed, 207 insertions(+), 182 deletions(-) diff --git a/src/AST/asthash.cc b/src/AST/asthash.cc index 9fed236..827f9e1 100644 --- a/src/AST/asthash.cc +++ b/src/AST/asthash.cc @@ -4,7 +4,7 @@ #include "boolean.h" #include "element.h" -bool compareArray(Array *inputs1, Array *inputs2) { +bool compareArray(Array *inputs1, Array *inputs2) { if (inputs1->getSize() != inputs2->getSize()) return false; for (uint i = 0; i < inputs1->getSize(); i++) { @@ -24,10 +24,10 @@ bool compareArray(Array *inputs1, Array *inputs2) { return true; } -uint hashArray(Array *inputs) { +uint hashArray(Array *inputs) { uint hash = inputs->getSize(); for (uint i = 0; i < inputs->getSize(); i++) { - uint newval = (uint)(uintptr_t) inputs->get(i); + uint newval = (uint)(uintptr_t) inputs->get(i).getRaw(); hash ^= newval; hash = (hash << 3) | (hash >> 29); } diff --git a/src/AST/boolean.cc b/src/AST/boolean.cc index 7c37710..0f9491a 100644 --- a/src/AST/boolean.cc +++ b/src/AST/boolean.cc @@ -31,7 +31,7 @@ BooleanOrder::BooleanOrder(Order *_order, uint64_t _first, uint64_t _second) : order->constraints.push(this); } -BooleanPredicate::BooleanPredicate(Predicate *_predicate, Element **_inputs, uint _numInputs, Boolean *_undefinedStatus) : +BooleanPredicate::BooleanPredicate(Predicate *_predicate, Element **_inputs, uint _numInputs, BooleanEdge _undefinedStatus) : Boolean(PREDICATEOP), predicate(_predicate), encoding(this), @@ -42,39 +42,44 @@ BooleanPredicate::BooleanPredicate(Predicate *_predicate, Element **_inputs, uin } } -BooleanLogic::BooleanLogic(CSolver *solver, LogicOp _op, Boolean **array, uint asize) : +BooleanLogic::BooleanLogic(CSolver *solver, LogicOp _op, BooleanEdge *array, uint asize) : Boolean(LOGICOP), op(_op), inputs(array, asize) { } +BooleanEdge cloneEdge(CSolver *solver, CloneMap *map, BooleanEdge e) { + bool isnegated=e.isNegated(); + Boolean *b=e->clone(solver, map); + BooleanEdge be=BooleanEdge(b); + return isnegated ? be.negate() : be; +} + Boolean *BooleanConst::clone(CSolver *solver, CloneMap *map) { - if (istrue) - return solver->getBooleanTrue(); - else - return solver->getBooleanFalse(); + return solver->getBooleanTrue().getRaw(); } Boolean *BooleanVar::clone(CSolver *solver, CloneMap *map) { Boolean *b = (Boolean *) map->get(this); if (b != NULL) return b; - Boolean *bvar = solver->getBooleanVar(type); - map->put(this, bvar); - return bvar; + BooleanEdge bvar = solver->getBooleanVar(type); + Boolean * base=bvar.getRaw(); + map->put(this, base); + return base; } Boolean *BooleanOrder::clone(CSolver *solver, CloneMap *map) { Order *ordercopy = order->clone(solver, map); - return solver->orderConstraint(ordercopy, first, second); + return solver->orderConstraint(ordercopy, first, second).getRaw(); } Boolean *BooleanLogic::clone(CSolver *solver, CloneMap *map) { - Boolean *array[inputs.getSize()]; + BooleanEdge array[inputs.getSize()]; for (uint i = 0; i < inputs.getSize(); i++) { - array[i] = inputs.get(i)->clone(solver, map); + array[i] = cloneEdge(solver, map, inputs.get(i)); } - return solver->applyLogicalOperation(op, array, inputs.getSize()); + return solver->applyLogicalOperation(op, array, inputs.getSize()).getRaw(); } Boolean *BooleanPredicate::clone(CSolver *solver, CloneMap *map) { @@ -83,7 +88,7 @@ Boolean *BooleanPredicate::clone(CSolver *solver, CloneMap *map) { array[i] = inputs.get(i)->clone(solver, map); } Predicate *pred = predicate->clone(solver, map); - Boolean *defstatus = (undefStatus != NULL) ? undefStatus->clone(solver, map) : NULL; + BooleanEdge defstatus = undefStatus ? cloneEdge(solver, map, undefStatus) : BooleanEdge(); - return solver->applyPredicateTable(pred, array, inputs.getSize(), defstatus); + return solver->applyPredicateTable(pred, array, inputs.getSize(), defstatus).getRaw(); } diff --git a/src/AST/boolean.h b/src/AST/boolean.h index 5a4b5af..218fc50 100644 --- a/src/AST/boolean.h +++ b/src/AST/boolean.h @@ -9,6 +9,8 @@ #include "functionencoding.h" #include "constraint.h" + + class Boolean : public ASTNode { public: Boolean(ASTNodeType _type); @@ -56,24 +58,24 @@ public: class BooleanPredicate : public Boolean { public: - BooleanPredicate(Predicate *_predicate, Element **_inputs, uint _numInputs, Boolean *_undefinedStatus); + BooleanPredicate(Predicate *_predicate, Element **_inputs, uint _numInputs, BooleanEdge _undefinedStatus); Boolean *clone(CSolver *solver, CloneMap *map); Predicate *predicate; FunctionEncoding encoding; Array inputs; - Boolean *undefStatus; + BooleanEdge undefStatus; FunctionEncoding *getFunctionEncoding() {return &encoding;} CMEMALLOC; }; class BooleanLogic : public Boolean { public: - BooleanLogic(CSolver *solver, LogicOp _op, Boolean **array, uint asize); + BooleanLogic(CSolver *solver, LogicOp _op, BooleanEdge *array, uint asize); Boolean *clone(CSolver *solver, CloneMap *map); LogicOp op; - Array inputs; + Array inputs; CMEMALLOC; }; #endif diff --git a/src/AST/element.cc b/src/AST/element.cc index e47d195..3fe8cef 100644 --- a/src/AST/element.cc +++ b/src/AST/element.cc @@ -16,7 +16,7 @@ ElementSet::ElementSet(Set *s) : set(s) { } -ElementFunction::ElementFunction(Function *_function, Element **array, uint numArrays, Boolean *_overflowstatus) : +ElementFunction::ElementFunction(Function *_function, Element **array, uint numArrays, BooleanEdge _overflowstatus) : Element(ELEMFUNCRETURN), function(_function), inputs(array, numArrays), diff --git a/src/AST/element.h b/src/AST/element.h index f1ba4eb..c3a3ed9 100644 --- a/src/AST/element.h +++ b/src/AST/element.h @@ -38,10 +38,10 @@ public: class ElementFunction : public Element { public: - ElementFunction(Function *function, Element **array, uint numArrays, Boolean *overflowstatus); + ElementFunction(Function *function, Element **array, uint numArrays, BooleanEdge overflowstatus); Function *function; Array inputs; - Boolean *overflowstatus; + BooleanEdge overflowstatus; FunctionEncoding functionencoding; Element *clone(CSolver *solver, CloneMap *map); CMEMALLOC; diff --git a/src/AST/rewriter.cc b/src/AST/rewriter.cc index 9751e05..80e1f1a 100644 --- a/src/AST/rewriter.cc +++ b/src/AST/rewriter.cc @@ -2,7 +2,11 @@ #include "boolean.h" #include "csolver.h" -void CSolver::replaceBooleanWithTrue(Boolean *bexpr) { +void CSolver::replaceBooleanWithTrue(BooleanEdge bexpr) { + if (constraints.contains(bexpr.negate())) { + constraints.remove(bexpr.negate()); + setUnSAT(); + } if (constraints.contains(bexpr)) { constraints.remove(bexpr); } @@ -15,12 +19,10 @@ void CSolver::replaceBooleanWithTrue(Boolean *bexpr) { case SATC_AND: handleANDTrue(logicop, bexpr); break; - case SATC_NOT: - replaceBooleanWithFalse(parent); - break; case SATC_IFF: handleIFFTrue(logicop, bexpr); break; + case SATC_NOT: case SATC_OR: case SATC_XOR: case SATC_IMPLIES: @@ -29,12 +31,22 @@ void CSolver::replaceBooleanWithTrue(Boolean *bexpr) { } } -void CSolver::replaceBooleanWithBoolean(Boolean *oldb, Boolean *newb) { +void CSolver::replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb) { + //Canonicalize + if (oldb.isNegated()) { + oldb=oldb.negate(); + newb=newb.negate(); + } if (constraints.contains(oldb)) { constraints.remove(oldb); constraints.add(newb); } + if (constraints.contains(oldb.negate())) { + constraints.remove(oldb.negate()); + constraints.add(newb.negate()); + } + BooleanEdge oldbnegated = oldb.negate(); uint size = oldb->parents.getSize(); for (uint i = 0; i < size; i++) { Boolean *parent = oldb->parents.get(i); @@ -43,74 +55,60 @@ void CSolver::replaceBooleanWithBoolean(Boolean *oldb, Boolean *newb) { uint parentsize = logicop->inputs.getSize(); for (uint j = 0; j < parentsize; j++) { - Boolean *b = logicop->inputs.get(i); + BooleanEdge b = logicop->inputs.get(i); if (b == oldb) { logicop->inputs.set(i, newb); newb->parents.push(parent); + } else if (b == oldbnegated) { + logicop->inputs.set(i, newb.negate()); + newb->parents.push(parent); } } } } -void handleIFFFalse(BooleanLogic *bexpr, Boolean *child) { - uint size = bexpr->inputs.getSize(); - Boolean *b = bexpr->inputs.get(0); - uint childindex = (b == child) ? 0 : 1; - bexpr->inputs.remove(childindex); - bexpr->op = SATC_NOT; -} - -void CSolver::handleIFFTrue(BooleanLogic *bexpr, Boolean *child) { +void CSolver::handleIFFTrue(BooleanLogic *bexpr, BooleanEdge child) { uint size = bexpr->inputs.getSize(); - Boolean *b = bexpr->inputs.get(0); - uint otherindex = (b == child) ? 1 : 0; - replaceBooleanWithBoolean(bexpr, bexpr->inputs.get(otherindex)); + BooleanEdge b0 = bexpr->inputs.get(0); + BooleanEdge b1 = bexpr->inputs.get(1); + BooleanEdge childnegate = child.negate(); + if (b0 == child) { + replaceBooleanWithBoolean(BooleanEdge(bexpr), b1); + } else if (b0 == childnegate) { + replaceBooleanWithBoolean(BooleanEdge(bexpr), b1.negate()); + } else if (b1 == child) { + replaceBooleanWithBoolean(BooleanEdge(bexpr), b0); + } else if (b1 == childnegate) { + replaceBooleanWithBoolean(BooleanEdge(bexpr), b0.negate()); + } else + ASSERT(0); } -void CSolver::handleANDTrue(BooleanLogic *bexpr, Boolean *child) { - uint size = bexpr->inputs.getSize(); - - if (size == 1) { - replaceBooleanWithTrue(bexpr); - return; - } - - for (uint i = 0; i < size; i++) { - Boolean *b = bexpr->inputs.get(i); +void CSolver::handleANDTrue(BooleanLogic *bexpr, BooleanEdge child) { + BooleanEdge childNegate=child.negate(); + + for (uint i = 0; i < bexpr->inputs.getSize(); i++) { + BooleanEdge b = bexpr->inputs.get(i); + if (b == child) { bexpr->inputs.remove(i); + i--; + } + + if (b == childNegate) { + replaceBooleanWithFalse(bexpr); + return; } } - if (size == 2) { + uint size=bexpr->inputs.getSize(); + if (size == 0) { + replaceBooleanWithTrue(bexpr); + } else if (size == 1) { replaceBooleanWithBoolean(bexpr, bexpr->inputs.get(0)); } } -void CSolver::replaceBooleanWithFalse(Boolean *bexpr) { - if (constraints.contains(bexpr)) { - setUnSAT(); - constraints.remove(bexpr); - } - - uint size = bexpr->parents.getSize(); - for (uint i = 0; i < size; i++) { - Boolean *parent = bexpr->parents.get(i); - BooleanLogic *logicop = (BooleanLogic *) parent; - switch (logicop->op) { - case SATC_AND: - replaceBooleanWithFalse(parent); - break; - case SATC_NOT: - replaceBooleanWithTrue(parent); - break; - case SATC_IFF: - handleIFFFalse(logicop, bexpr); - break; - case SATC_OR: - case SATC_XOR: - case SATC_IMPLIES: - ASSERT(0); - } - } +void CSolver::replaceBooleanWithFalse(BooleanEdge bexpr) { + replaceBooleanWithTrue(bexpr.negate()); } diff --git a/src/AST/rewriter.h b/src/AST/rewriter.h index 3e3488f..7c48092 100644 --- a/src/AST/rewriter.h +++ b/src/AST/rewriter.h @@ -2,6 +2,4 @@ #define REWRITER_H #include "classlist.h" -void handleIFFFalse(BooleanLogic *bexpr, Boolean *child); - #endif diff --git a/src/ASTAnalyses/polarityassignment.cc b/src/ASTAnalyses/polarityassignment.cc index 2aa9e5d..6b63436 100644 --- a/src/ASTAnalyses/polarityassignment.cc +++ b/src/ASTAnalyses/polarityassignment.cc @@ -2,12 +2,19 @@ #include "csolver.h" void computePolarities(CSolver *This) { - SetIteratorBoolean *iterator = This->getConstraints(); + SetIteratorBooleanEdge *iterator = This->getConstraints(); while (iterator->hasNext()) { - Boolean *boolean = iterator->next(); - updatePolarity(boolean, P_TRUE); - updateMustValue(boolean, BV_MUSTBETRUE); - computePolarityAndBooleanValue(boolean); + BooleanEdge boolean = iterator->next(); + Boolean *b = boolean.getBoolean(); + bool isNegated = boolean.isNegated(); + if (isNegated) { + updatePolarity(b, P_FALSE); + updateMustValue(b, BV_MUSTBEFALSE); + } else { + updatePolarity(b, P_TRUE); + updateMustValue(b, BV_MUSTBETRUE); + } + computePolarityAndBooleanValue(b); } delete iterator; } @@ -35,9 +42,9 @@ void computePolarityAndBooleanValue(Boolean *This) { } void computePredicatePolarityAndBooleanValue(BooleanPredicate *This) { - if (This->undefStatus != NULL) { - updatePolarity(This->undefStatus, P_BOTHTRUEFALSE); - computePolarityAndBooleanValue(This->undefStatus); + if (This->undefStatus) { + updatePolarity(This->undefStatus.getBoolean(), P_BOTHTRUEFALSE); + computePolarityAndBooleanValue(This->undefStatus.getBoolean()); } } @@ -46,7 +53,7 @@ void computeLogicOpPolarityAndBooleanValue(BooleanLogic *This) { computeLogicOpPolarity(This); uint size = This->inputs.getSize(); for (uint i = 0; i < size; i++) { - computePolarityAndBooleanValue(This->inputs.get(i)); + computePolarityAndBooleanValue(This->inputs.get(i).getBoolean()); } } @@ -84,19 +91,15 @@ void computeLogicOpPolarity(BooleanLogic *This) { case SATC_AND: { uint size = This->inputs.getSize(); for (uint i = 0; i < size; i++) { - Boolean *tmp = This->inputs.get(i); - updatePolarity(tmp, parentpolarity); + BooleanEdge tmp = This->inputs.get(i); + Boolean *btmp = tmp.getBoolean(); + updatePolarity(btmp, tmp.isNegated() ? negatePolarity(parentpolarity) : parentpolarity); } break; } - case SATC_NOT: { - Boolean *tmp = This->inputs.get(0); - updatePolarity(tmp, negatePolarity(parentpolarity)); - break; - } case SATC_IFF: { - updatePolarity(This->inputs.get(0), P_BOTHTRUEFALSE); - updatePolarity(This->inputs.get(1), P_BOTHTRUEFALSE); + updatePolarity(This->inputs.get(0).getBoolean(), P_BOTHTRUEFALSE); + updatePolarity(This->inputs.get(1).getBoolean(), P_BOTHTRUEFALSE); break; } default: @@ -111,14 +114,12 @@ void computeLogicOpBooleanValue(BooleanLogic *This) { if (parentbv == BV_MUSTBETRUE || parentbv == BV_UNSAT) { uint size = This->inputs.getSize(); for (uint i = 0; i < size; i++) { - updateMustValue(This->inputs.get(i), parentbv); + BooleanEdge be=This->inputs.get(i); + updateMustValue(be.getBoolean(), be.isNegated()?negateBooleanValue(parentbv):parentbv); } } return; } - case SATC_NOT: - updateMustValue(This->inputs.get(0), negateBooleanValue(parentbv)); - return; case SATC_IFF: return; default: diff --git a/src/ASTTransform/integerencoding.cc b/src/ASTTransform/integerencoding.cc index 6664a67..a4aacdf 100644 --- a/src/ASTTransform/integerencoding.cc +++ b/src/ASTTransform/integerencoding.cc @@ -55,7 +55,7 @@ void IntegerEncodingTransform::orderIntegerEncodingSATEncoder(Order * currOrder, Set *sarray[] = {ierec->getSecondarySet(), ierec->getSecondarySet()}; Predicate *predicate = solver->createPredicateOperator(SATC_LT, sarray, 2); Element *parray[] = {elem1, elem2}; - Boolean *boolean = solver->applyPredicate(predicate, parray, 2); + BooleanEdge boolean = solver->applyPredicate(predicate, parray, 2); solver->addConstraint(boolean); solver->replaceBooleanWithBoolean(boolOrder, boolean); } diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc index fd60f45..4020ad6 100644 --- a/src/Backend/satencoder.cc +++ b/src/Backend/satencoder.cc @@ -26,20 +26,22 @@ int SATEncoder::solve() { } void SATEncoder::encodeAllSATEncoder(CSolver *csolver) { - SetIteratorBoolean *iterator = csolver->getConstraints(); + SetIteratorBooleanEdge *iterator = csolver->getConstraints(); while (iterator->hasNext()) { - Boolean *constraint = iterator->next(); + BooleanEdge constraint = iterator->next(); Edge c = encodeConstraintSATEncoder(constraint); addConstraintCNF(cnf, c); } delete iterator; } -Edge SATEncoder::encodeConstraintSATEncoder(Boolean *constraint) { +Edge SATEncoder::encodeConstraintSATEncoder(BooleanEdge c) { Edge result; + Boolean * constraint = c.getBoolean(); + if (booledgeMap.contains(constraint)) { Edge e = {(Node *) booledgeMap.get(constraint)}; - return e; + return c.isNegated() ? constraintNegate(e) : e; } switch (constraint->type) { @@ -60,7 +62,7 @@ Edge SATEncoder::encodeConstraintSATEncoder(Boolean *constraint) { exit(-1); } booledgeMap.put(constraint, result.node_ptr); - return result; + return c.isNegated() ? constraintNegate(result) : result; } void SATEncoder::getArrayNewVarsSATEncoder(uint num, Edge *carray) { diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h index 25f6918..7af3e55 100644 --- a/src/Backend/satencoder.h +++ b/src/Backend/satencoder.h @@ -14,7 +14,7 @@ public: SATEncoder(CSolver *solver); ~SATEncoder(); void encodeAllSATEncoder(CSolver *csolver); - Edge encodeConstraintSATEncoder(Boolean *constraint); + Edge encodeConstraintSATEncoder(BooleanEdge constraint); CNF *getCNF() { return cnf;} long long getSolveTime() { return cnf->solveTime; } long long getEncodeTime() { return cnf->encodeTime; } diff --git a/src/Backend/satfuncopencoder.cc b/src/Backend/satfuncopencoder.cc index 41b687e..ba8b32b 100644 --- a/src/Backend/satfuncopencoder.cc +++ b/src/Backend/satfuncopencoder.cc @@ -108,7 +108,7 @@ void SATEncoder::encodeOperatorElementFunctionSATEncoder(ElementFunction *func) vals[i] = set->getElement(indices[i]); } - Edge overFlowConstraint = ((BooleanVar *) func->overflowstatus)->var; + Edge overFlowConstraint = encodeConstraintSATEncoder(func->overflowstatus); bool notfinished = true; while (notfinished) { diff --git a/src/Collections/corestructs.h b/src/Collections/corestructs.h index 982e0c5..e30a530 100644 --- a/src/Collections/corestructs.h +++ b/src/Collections/corestructs.h @@ -4,9 +4,33 @@ #include "cppvector.h" #include "hashset.h" -typedef Hashset HashsetBoolean; +class BooleanEdge { + public: + BooleanEdge() : b(NULL) {} + BooleanEdge(Boolean * _b) : b(_b) {} + BooleanEdge negate() {return BooleanEdge((Boolean *)(((uintptr_t) b) ^ 1));} + bool operator==(BooleanEdge e) { return b==e.b;} + bool operator!=(BooleanEdge e) { return b!=e.b;} + bool isNegated() { return ((uintptr_t) b) & 1; } + Boolean * getBoolean() {return (Boolean *)(((uintptr_t)b) & ~((uintptr_t) 1));} + Boolean * getRaw() {return b;} + Boolean * operator->() {return getBoolean();} + operator bool() const {return b != NULL;} + private: + Boolean *b; +}; + +inline bool boolEdgeEquals(BooleanEdge b1, BooleanEdge b2) { + return b1==b2; +} + +inline unsigned int boolEdgeHash(BooleanEdge b) { + return (unsigned int) (((uintptr_t)b.getRaw())>>4); +} + +typedef Hashset HashsetBooleanEdge; typedef Hashset HashsetOrder; -typedef SetIterator SetIteratorBoolean; +typedef SetIterator SetIteratorBooleanEdge; typedef SetIterator SetIteratorOrder; #endif diff --git a/src/Encoders/naiveencoder.cc b/src/Encoders/naiveencoder.cc index 9b4487e..466d839 100644 --- a/src/Encoders/naiveencoder.cc +++ b/src/Encoders/naiveencoder.cc @@ -14,10 +14,10 @@ #include void naiveEncodingDecision(CSolver *This) { - SetIteratorBoolean *iterator = This->getConstraints(); + SetIteratorBooleanEdge *iterator = This->getConstraints(); while (iterator->hasNext()) { - Boolean *boolean = iterator->next(); - naiveEncodingConstraint(boolean); + BooleanEdge b = iterator->next(); + naiveEncodingConstraint(b.getBoolean()); } delete iterator; } @@ -46,7 +46,7 @@ void naiveEncodingConstraint(Boolean *This) { void naiveEncodingLogicOp(BooleanLogic *This) { for (uint i = 0; i < This->inputs.getSize(); i++) { - naiveEncodingConstraint(This->inputs.get(i)); + naiveEncodingConstraint(This->inputs.get(i).getBoolean()); } } diff --git a/src/csolver.cc b/src/csolver.cc index c3208b9..9112e54 100644 --- a/src/csolver.cc +++ b/src/csolver.cc @@ -20,8 +20,8 @@ #include CSolver::CSolver() : - boolTrue(new BooleanConst(true)), - boolFalse(new BooleanConst(false)), + boolTrue(BooleanEdge(new BooleanConst(true))), + boolFalse(boolTrue.negate()), unsat(false), tuner(NULL), elapsedTime(0) @@ -67,17 +67,16 @@ CSolver::~CSolver() { delete allFunctions.get(i); } - delete boolTrue; - delete boolFalse; + delete boolTrue.getBoolean(); delete satEncoder; } CSolver *CSolver::clone() { CSolver *copy = new CSolver(); CloneMap map; - SetIteratorBoolean *it = getConstraints(); + SetIteratorBooleanEdge *it = getConstraints(); while (it->hasNext()) { - Boolean *b = it->next(); + BooleanEdge b = it->next(); copy->addConstraint(b->clone(copy, &map)); } delete it; @@ -140,7 +139,7 @@ Element *CSolver::getElementConst(VarType type, uint64_t value) { } } -Element *CSolver::applyFunction(Function *function, Element **array, uint numArrays, Boolean *overflowstatus) { +Element *CSolver::applyFunction(Function *function, Element **array, uint numArrays, BooleanEdge overflowstatus) { Element *element = new ElementFunction(function,array,numArrays,overflowstatus); Element *e = elemMap.get(element); if (e == NULL) { @@ -191,52 +190,52 @@ Function *CSolver::completeTable(Table *table, UndefinedBehavior behavior) { return function; } -Boolean *CSolver::getBooleanVar(VarType type) { +BooleanEdge CSolver::getBooleanVar(VarType type) { Boolean *boolean = new BooleanVar(type); allBooleans.push(boolean); - return boolean; + return BooleanEdge(boolean); } -Boolean *CSolver::getBooleanTrue() { +BooleanEdge CSolver::getBooleanTrue() { return boolTrue; } -Boolean *CSolver::getBooleanFalse() { +BooleanEdge CSolver::getBooleanFalse() { return boolFalse; } -Boolean *CSolver::applyPredicate(Predicate *predicate, Element **inputs, uint numInputs) { +BooleanEdge CSolver::applyPredicate(Predicate *predicate, Element **inputs, uint numInputs) { return applyPredicateTable(predicate, inputs, numInputs, NULL); } -Boolean *CSolver::applyPredicateTable(Predicate *predicate, Element **inputs, uint numInputs, Boolean *undefinedStatus) { +BooleanEdge CSolver::applyPredicateTable(Predicate *predicate, Element **inputs, uint numInputs, BooleanEdge undefinedStatus) { BooleanPredicate *boolean = new BooleanPredicate(predicate, inputs, numInputs, undefinedStatus); Boolean *b = boolMap.get(boolean); if (b == NULL) { boolMap.put(boolean, boolean); allBooleans.push(boolean); - return boolean; + return BooleanEdge(boolean); } else { delete boolean; - return b; + return BooleanEdge(b); } } -bool CSolver::isTrue(Boolean *b) { - return b->isTrue(); +bool CSolver::isTrue(BooleanEdge b) { + return b.isNegated()?b->isFalse():b->isTrue(); } -bool CSolver::isFalse(Boolean *b) { - return b->isFalse(); +bool CSolver::isFalse(BooleanEdge b) { + return b.isNegated()?b->isTrue():b->isFalse(); } -Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean *arg1, Boolean *arg2) { - Boolean *array[] = {arg1, arg2}; +BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge arg1, BooleanEdge arg2) { + BooleanEdge array[] = {arg1, arg2}; return applyLogicalOperation(op, array, 2); } -Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean *arg) { - Boolean *array[] = {arg}; +BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge arg) { + BooleanEdge array[] = {arg}; return applyLogicalOperation(op, array, 1); } @@ -251,16 +250,11 @@ static int ptrcompares(const void *p1, const void *p2) { return 1; } -Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize) { - Boolean *newarray[asize]; +BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint asize) { + BooleanEdge newarray[asize]; switch (op) { case SATC_NOT: { - if (array[0]->type == LOGICOP && ((BooleanLogic *)array[0])->op == SATC_NOT) { - return ((BooleanLogic *) array[0])->inputs.get(0); - } else if (array[0]->type == BOOLCONST) { - return array[0]->isTrue() ? boolFalse : boolTrue; - } - break; + return array[0].negate(); } case SATC_IFF: { for (uint i = 0; i < 2; i++) { @@ -284,7 +278,7 @@ Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize) case SATC_AND: { uint newindex = 0; for (uint i = 0; i < asize; i++) { - Boolean *b = array[i]; + BooleanEdge b = array[i]; if (b->type == BOOLCONST) { if (b->isTrue()) continue; @@ -298,7 +292,7 @@ Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize) } else if (newindex == 1) { return newarray[0]; } else { - qsort(newarray, asize, sizeof(Boolean *), ptrcompares); + qsort(newarray, asize, sizeof(BooleanEdge), ptrcompares); array = newarray; asize = newindex; } @@ -320,27 +314,27 @@ Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize) if (b == NULL) { boolMap.put(boolean, boolean); allBooleans.push(boolean); - return boolean; + return BooleanEdge(boolean); } else { delete boolean; - return b; + return BooleanEdge(b); } } -Boolean *CSolver::orderConstraint(Order *order, uint64_t first, uint64_t second) { +BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t second) { Boolean *constraint = new BooleanOrder(order, first, second); allBooleans.push(constraint); - return constraint; + return BooleanEdge(constraint); } -void CSolver::addConstraint(Boolean *constraint) { +void CSolver::addConstraint(BooleanEdge constraint) { if (constraint == boolTrue) return; else if (constraint == boolFalse) setUnSAT(); else { - if (constraint->type == LOGICOP) { - BooleanLogic *b=(BooleanLogic *) constraint; + if (!constraint.isNegated() && constraint->type == LOGICOP) { + BooleanLogic *b=(BooleanLogic *) constraint.getBoolean(); if (b->op==SATC_AND) { for(uint i=0;iinputs.getSize();i++) { addConstraint(b->inputs.get(i)); @@ -401,7 +395,8 @@ uint64_t CSolver::getElementValue(Element *element) { exit(-1); } -bool CSolver::getBooleanValue(Boolean *boolean) { +bool CSolver::getBooleanValue(BooleanEdge bedge) { + Boolean *boolean=bedge.getBoolean(); switch (boolean->type) { case BOOLEANVAR: return getBooleanVariableValueSATTranslator(this, boolean); diff --git a/src/csolver.h b/src/csolver.h index 618f88e..2875a9c 100644 --- a/src/csolver.h +++ b/src/csolver.h @@ -41,13 +41,13 @@ public: /** This function creates an element constrant. */ Element *getElementConst(VarType type, uint64_t value); - Boolean *getBooleanTrue(); + BooleanEdge getBooleanTrue(); - Boolean *getBooleanFalse(); + BooleanEdge getBooleanFalse(); /** This function creates a boolean variable. */ - Boolean *getBooleanVar(VarType type); + BooleanEdge getBooleanVar(VarType type); /** This function creates a function operator. */ @@ -75,36 +75,36 @@ public: /** This function applies a function to the Elements in its input. */ - Element *applyFunction(Function *function, Element **array, uint numArrays, Boolean *overflowstatus); + Element *applyFunction(Function *function, Element **array, uint numArrays, BooleanEdge overflowstatus); /** This function applies a predicate to the Elements in its input. */ - Boolean *applyPredicateTable(Predicate *predicate, Element **inputs, uint numInputs, Boolean *undefinedStatus); + BooleanEdge applyPredicateTable(Predicate *predicate, Element **inputs, uint numInputs, BooleanEdge undefinedStatus); - Boolean *applyPredicate(Predicate *predicate, Element **inputs, uint numInputs); + BooleanEdge applyPredicate(Predicate *predicate, Element **inputs, uint numInputs); /** This function applies a logical operation to the Booleans in its input. */ - Boolean *applyLogicalOperation(LogicOp op, Boolean **array, uint asize); + BooleanEdge applyLogicalOperation(LogicOp op, BooleanEdge *array, uint asize); /** This function applies a logical operation to the Booleans in its input. */ - Boolean *applyLogicalOperation(LogicOp op, Boolean *arg1, Boolean *arg2); + BooleanEdge applyLogicalOperation(LogicOp op, BooleanEdge arg1, BooleanEdge arg2); /** This function applies a logical operation to the Booleans in its input. */ - Boolean *applyLogicalOperation(LogicOp op, Boolean *arg); + BooleanEdge applyLogicalOperation(LogicOp op, BooleanEdge arg); /** This function adds a boolean constraint to the set of constraints to be satisfied */ - void addConstraint(Boolean *constraint); + void addConstraint(BooleanEdge constraint); /** This function instantiates an order of type type over the set set. */ Order *createOrder(OrderType type, Set *set); /** This function instantiates a boolean on two items in an order. */ - Boolean *orderConstraint(Order *order, uint64_t first, uint64_t second); + BooleanEdge orderConstraint(Order *order, uint64_t first, uint64_t second); /** When everything is done, the client calls this function and then csolver starts to encode*/ int solve(); @@ -113,12 +113,12 @@ public: uint64_t getElementValue(Element *element); /** After getting the solution from the SAT solver, client can get the value of a boolean via this function*/ - bool getBooleanValue(Boolean *boolean); + bool getBooleanValue(BooleanEdge boolean); bool getOrderConstraintValue(Order *order, uint64_t first, uint64_t second); - bool isTrue(Boolean *b); - bool isFalse(Boolean *b); + bool isTrue(BooleanEdge b); + bool isFalse(BooleanEdge b); void setUnSAT() { unsat = true; } @@ -129,13 +129,13 @@ public: Tuner *getTuner() { return tuner; } - SetIteratorBoolean *getConstraints() { return constraints.iterator(); } + SetIteratorBooleanEdge * getConstraints() { return constraints.iterator(); } SATEncoder *getSATEncoder() {return satEncoder;} - void replaceBooleanWithTrue(Boolean *bexpr); - void replaceBooleanWithFalse(Boolean *bexpr); - void replaceBooleanWithBoolean(Boolean *oldb, Boolean *newb); + void replaceBooleanWithTrue(BooleanEdge bexpr); + void replaceBooleanWithFalse(BooleanEdge bexpr); + void replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb); CSolver *clone(); void autoTune(uint budget); @@ -147,11 +147,11 @@ public: CMEMALLOC; private: - void handleIFFTrue(BooleanLogic *bexpr, Boolean *child); - void handleANDTrue(BooleanLogic *bexpr, Boolean *child); + void handleIFFTrue(BooleanLogic *bexpr, BooleanEdge child); + void handleANDTrue(BooleanLogic *bexpr, BooleanEdge child); /** This is a vector of constraints that must be satisfied. */ - HashsetBoolean constraints; + HashsetBooleanEdge constraints; /** This is a vector of all boolean structs that we have allocated. */ Vector allBooleans; @@ -176,8 +176,8 @@ private: /** This is a vector of all function structs that we have allocated. */ Vector allFunctions; - Boolean *boolTrue; - Boolean *boolFalse; + BooleanEdge boolTrue; + BooleanEdge boolFalse; /** These two tables are used for deduplicating entries. */ BooleanMatchMap boolMap; -- 2.34.1