#include "boolean.h"
#include "element.h"
-bool compareArray(Array<Boolean *> *inputs1, Array<Boolean *> *inputs2) {
+bool compareArray(Array<BooleanEdge> *inputs1, Array<BooleanEdge> *inputs2) {
if (inputs1->getSize() != inputs2->getSize())
return false;
for (uint i = 0; i < inputs1->getSize(); i++) {
return true;
}
-uint hashArray(Array<Boolean *> *inputs) {
+uint hashArray(Array<BooleanEdge> *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);
}
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),
}
}
-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) {
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();
}
#include "functionencoding.h"
#include "constraint.h"
+
+
class Boolean : public ASTNode {
public:
Boolean(ASTNodeType _type);
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<Element *> 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<Boolean *> inputs;
+ Array<BooleanEdge> inputs;
CMEMALLOC;
};
#endif
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),
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<Element *> inputs;
- Boolean *overflowstatus;
+ BooleanEdge overflowstatus;
FunctionEncoding functionencoding;
Element *clone(CSolver *solver, CloneMap *map);
CMEMALLOC;
#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);
}
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:
}
}
-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);
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());
}
#define REWRITER_H
#include "classlist.h"
-void handleIFFFalse(BooleanLogic *bexpr, Boolean *child);
-
#endif
#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;
}
}
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());
}
}
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());
}
}
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:
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:
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);
}
}
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) {
exit(-1);
}
booledgeMap.put(constraint, result.node_ptr);
- return result;
+ return c.isNegated() ? constraintNegate(result) : result;
}
void SATEncoder::getArrayNewVarsSATEncoder(uint num, Edge *carray) {
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; }
vals[i] = set->getElement(indices[i]);
}
- Edge overFlowConstraint = ((BooleanVar *) func->overflowstatus)->var;
+ Edge overFlowConstraint = encodeConstraintSATEncoder(func->overflowstatus);
bool notfinished = true;
while (notfinished) {
#include "cppvector.h"
#include "hashset.h"
-typedef Hashset<Boolean *, uintptr_t, 4> 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<BooleanEdge, uintptr_t, 4, & boolEdgeHash, & boolEdgeEquals> HashsetBooleanEdge;
typedef Hashset<Order *, uintptr_t, 4> HashsetOrder;
-typedef SetIterator<Boolean *, uintptr_t, 4> SetIteratorBoolean;
+typedef SetIterator<BooleanEdge, uintptr_t, 4, & boolEdgeHash, & boolEdgeEquals> SetIteratorBooleanEdge;
typedef SetIterator<Order *, uintptr_t, 4> SetIteratorOrder;
#endif
#include <strings.h>
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;
}
void naiveEncodingLogicOp(BooleanLogic *This) {
for (uint i = 0; i < This->inputs.getSize(); i++) {
- naiveEncodingConstraint(This->inputs.get(i));
+ naiveEncodingConstraint(This->inputs.get(i).getBoolean());
}
}
#include <stdlib.h>
CSolver::CSolver() :
- boolTrue(new BooleanConst(true)),
- boolFalse(new BooleanConst(false)),
+ boolTrue(BooleanEdge(new BooleanConst(true))),
+ boolFalse(boolTrue.negate()),
unsat(false),
tuner(NULL),
elapsedTime(0)
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;
}
}
-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) {
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);
}
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++) {
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;
} else if (newindex == 1) {
return newarray[0];
} else {
- qsort(newarray, asize, sizeof(Boolean *), ptrcompares);
+ qsort(newarray, asize, sizeof(BooleanEdge), ptrcompares);
array = newarray;
asize = newindex;
}
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;i<b->inputs.getSize();i++) {
addConstraint(b->inputs.get(i));
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);
/** 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. */
/** 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();
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; }
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);
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<Boolean *> allBooleans;
/** This is a vector of all function structs that we have allocated. */
Vector<Function *> allFunctions;
- Boolean *boolTrue;
- Boolean *boolFalse;
+ BooleanEdge boolTrue;
+ BooleanEdge boolFalse;
/** These two tables are used for deduplicating entries. */
BooleanMatchMap boolMap;