#include "element.h"
#include "set.h"
-Edge getElementValueConstraint(SATEncoder *This, Element *elem, uint64_t value) {
+Edge SATEncoder::getElementValueConstraint(Element *elem, uint64_t value) {
switch (getElementEncoding(elem)->type) {
case ONEHOT:
- return getElementValueOneHotConstraint(This, elem, value);
+ return getElementValueOneHotConstraint(elem, value);
case UNARY:
- return getElementValueUnaryConstraint(This, elem, value);
+ return getElementValueUnaryConstraint(elem, value);
case BINARYINDEX:
- return getElementValueBinaryIndexConstraint(This, elem, value);
+ return getElementValueBinaryIndexConstraint(elem, value);
case ONEHOTBINARY:
ASSERT(0);
break;
case BINARYVAL:
- return getElementValueBinaryValueConstraint(This, elem, value);
+ return getElementValueBinaryValueConstraint(elem, value);
break;
default:
ASSERT(0);
return E_BOGUS;
}
-Edge getElementValueBinaryIndexConstraint(SATEncoder *This, Element *elem, uint64_t value) {
+Edge SATEncoder::getElementValueBinaryIndexConstraint(Element *elem, uint64_t value) {
ASTNodeType type = GETELEMENTTYPE(elem);
ASSERT(type == ELEMSET || type == ELEMFUNCRETURN || type == ELEMCONST);
ElementEncoding *elemEnc = getElementEncoding(elem);
for (uint i = 0; i < elemEnc->encArraySize; i++) {
if (elemEnc->isinUseElement(i) && elemEnc->encodingArray[i] == value) {
- return (elemEnc->numVars == 0) ? E_True : generateBinaryConstraint(This->getCNF(), elemEnc->numVars, elemEnc->variables, i);
+ return (elemEnc->numVars == 0) ? E_True : generateBinaryConstraint(cnf, elemEnc->numVars, elemEnc->variables, i);
}
}
return E_False;
}
-Edge getElementValueOneHotConstraint(SATEncoder *This, Element *elem, uint64_t value) {
+Edge SATEncoder::getElementValueOneHotConstraint(Element *elem, uint64_t value) {
ASTNodeType type = GETELEMENTTYPE(elem);
ASSERT(type == ELEMSET || type == ELEMFUNCRETURN || type == ELEMCONST);
ElementEncoding *elemEnc = getElementEncoding(elem);
return E_False;
}
-Edge getElementValueUnaryConstraint(SATEncoder *This, Element *elem, uint64_t value) {
+Edge SATEncoder::getElementValueUnaryConstraint(Element *elem, uint64_t value) {
ASTNodeType type = GETELEMENTTYPE(elem);
ASSERT(type == ELEMSET || type == ELEMFUNCRETURN || type == ELEMCONST);
ElementEncoding *elemEnc = getElementEncoding(elem);
else if ((i + 1) == elemEnc->encArraySize)
return elemEnc->variables[i - 1];
else
- return constraintAND2(This->getCNF(), elemEnc->variables[i - 1], constraintNegate(elemEnc->variables[i]));
+ return constraintAND2(cnf, elemEnc->variables[i - 1], constraintNegate(elemEnc->variables[i]));
}
}
return E_False;
}
-Edge getElementValueBinaryValueConstraint(SATEncoder *This, Element *element, uint64_t value) {
+Edge SATEncoder::getElementValueBinaryValueConstraint(Element *element, uint64_t value) {
ASTNodeType type = GETELEMENTTYPE(element);
ASSERT(type == ELEMSET || type == ELEMFUNCRETURN);
ElementEncoding *elemEnc = getElementEncoding(element);
}
uint64_t valueminusoffset = value - elemEnc->offset;
- return generateBinaryConstraint(This->getCNF(), elemEnc->numVars, elemEnc->variables, valueminusoffset);
+ return generateBinaryConstraint(cnf, elemEnc->numVars, elemEnc->variables, valueminusoffset);
}
void allocElementConstraintVariables(ElementEncoding *This, uint numVars) {
This->variables = (Edge *)ourmalloc(sizeof(Edge) * numVars);
}
-void generateBinaryValueEncodingVars(SATEncoder *This, ElementEncoding *encoding) {
+void SATEncoder::generateBinaryValueEncodingVars(ElementEncoding *encoding) {
ASSERT(encoding->type == BINARYVAL);
allocElementConstraintVariables(encoding, encoding->numBits);
- getArrayNewVarsSATEncoder(This, encoding->numVars, encoding->variables);
+ getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables);
}
-void generateBinaryIndexEncodingVars(SATEncoder *This, ElementEncoding *encoding) {
+void SATEncoder::generateBinaryIndexEncodingVars(ElementEncoding *encoding) {
ASSERT(encoding->type == BINARYINDEX);
allocElementConstraintVariables(encoding, NUMBITS(encoding->encArraySize - 1));
- getArrayNewVarsSATEncoder(This, encoding->numVars, encoding->variables);
+ getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables);
}
-void generateOneHotEncodingVars(SATEncoder *This, ElementEncoding *encoding) {
+void SATEncoder::generateOneHotEncodingVars(ElementEncoding *encoding) {
allocElementConstraintVariables(encoding, encoding->encArraySize);
- getArrayNewVarsSATEncoder(This, encoding->numVars, encoding->variables);
+ getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables);
for (uint i = 0; i < encoding->numVars; i++) {
for (uint j = i + 1; j < encoding->numVars; j++) {
- addConstraintCNF(This->getCNF(), constraintNegate(constraintAND2(This->getCNF(), encoding->variables[i], encoding->variables[j])));
+ addConstraintCNF(cnf, constraintNegate(constraintAND2(cnf, encoding->variables[i], encoding->variables[j])));
}
}
- addConstraintCNF(This->getCNF(), constraintOR(This->getCNF(), encoding->numVars, encoding->variables));
+ addConstraintCNF(cnf, constraintOR(cnf, encoding->numVars, encoding->variables));
}
-void generateUnaryEncodingVars(SATEncoder *This, ElementEncoding *encoding) {
+void SATEncoder::generateUnaryEncodingVars(ElementEncoding *encoding) {
allocElementConstraintVariables(encoding, encoding->encArraySize - 1);
- getArrayNewVarsSATEncoder(This, encoding->numVars, encoding->variables);
+ getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables);
//Add unary constraint
for (uint i = 1; i < encoding->numVars; i++) {
- addConstraintCNF(This->getCNF(), constraintOR2(This->getCNF(), encoding->variables[i - 1], constraintNegate(encoding->variables[i])));
+ addConstraintCNF(cnf, constraintOR2(cnf, encoding->variables[i - 1], constraintNegate(encoding->variables[i])));
}
}
-void generateElementEncoding(SATEncoder *This, Element *element) {
+void SATEncoder::generateElementEncoding(Element *element) {
ElementEncoding *encoding = getElementEncoding(element);
ASSERT(encoding->type != ELEM_UNASSIGNED);
if (encoding->variables != NULL)
return;
switch (encoding->type) {
case ONEHOT:
- generateOneHotEncodingVars(This, encoding);
+ generateOneHotEncodingVars(encoding);
return;
case BINARYINDEX:
- generateBinaryIndexEncodingVars(This, encoding);
+ generateBinaryIndexEncodingVars(encoding);
return;
case UNARY:
- generateUnaryEncodingVars(This, encoding);
+ generateUnaryEncodingVars(encoding);
return;
case ONEHOTBINARY:
return;
case BINARYVAL:
- generateBinaryValueEncodingVars(This, encoding);
+ generateBinaryValueEncodingVars(encoding);
return;
default:
ASSERT(0);
+++ /dev/null
-#ifndef SATELEMENTENCODER_H
-#define SATELEMENTENCODER_H
-
-Edge getElementValueOneHotConstraint(SATEncoder *This, Element *elem, uint64_t value);
-Edge getElementValueUnaryConstraint(SATEncoder *This, Element *elem, uint64_t value);
-Edge getElementValueBinaryIndexConstraint(SATEncoder *This, Element *element, uint64_t value);
-Edge getElementValueBinaryValueConstraint(SATEncoder *This, Element *element, uint64_t value);
-Edge getElementValueConstraint(SATEncoder *encoder, Element *This, uint64_t value);
-void allocElementConstraintVariables(ElementEncoding *This, uint numVars);
-void generateOneHotEncodingVars(SATEncoder *This, ElementEncoding *encoding);
-void generateUnaryEncodingVars(SATEncoder *This, ElementEncoding *encoding);
-void generateBinaryIndexEncodingVars(SATEncoder *This, ElementEncoding *encoding);
-void generateBinaryValueEncodingVars(SATEncoder *This, ElementEncoding *encoding);
-void generateElementEncoding(SATEncoder *This, Element *element);
-#endif
#include "order.h"
#include "predicate.h"
#include "set.h"
-#include "satfuncopencoder.h"
//TODO: Should handle sharing of AST Nodes without recoding them a second time
Edge SATEncoder::encodeConstraintSATEncoder(Boolean *constraint) {
switch (GETBOOLEANTYPE(constraint)) {
case ORDERCONST:
- return encodeOrderSATEncoder(this, (BooleanOrder *) constraint);
+ return encodeOrderSATEncoder((BooleanOrder *) constraint);
case BOOLEANVAR:
- return encodeVarSATEncoder(this, (BooleanVar *) constraint);
+ return encodeVarSATEncoder((BooleanVar *) constraint);
case LOGICOP:
- return encodeLogicSATEncoder(this, (BooleanLogic *) constraint);
+ return encodeLogicSATEncoder((BooleanLogic *) constraint);
case PREDICATEOP:
- return encodePredicateSATEncoder(this, (BooleanPredicate *) constraint);
+ return encodePredicateSATEncoder((BooleanPredicate *) constraint);
default:
model_print("Unhandled case in encodeConstraintSATEncoder %u", GETBOOLEANTYPE(constraint));
exit(-1);
}
}
-void getArrayNewVarsSATEncoder(SATEncoder *encoder, uint num, Edge *carray) {
+void SATEncoder::getArrayNewVarsSATEncoder(uint num, Edge *carray) {
for (uint i = 0; i < num; i++)
- carray[i] = getNewVarSATEncoder(encoder);
+ carray[i] = getNewVarSATEncoder();
}
-Edge getNewVarSATEncoder(SATEncoder *This) {
- return constraintNewVar(This->getCNF());
+Edge SATEncoder::getNewVarSATEncoder() {
+ return constraintNewVar(cnf);
}
-Edge encodeVarSATEncoder(SATEncoder *This, BooleanVar *constraint) {
+Edge SATEncoder::encodeVarSATEncoder(BooleanVar *constraint) {
if (edgeIsNull(constraint->var)) {
- constraint->var = getNewVarSATEncoder(This);
+ constraint->var = getNewVarSATEncoder();
}
return constraint->var;
}
-Edge encodeLogicSATEncoder(SATEncoder *This, BooleanLogic *constraint) {
+Edge SATEncoder::encodeLogicSATEncoder(BooleanLogic *constraint) {
Edge array[constraint->inputs.getSize()];
for (uint i = 0; i < constraint->inputs.getSize(); i++)
- array[i] = This->encodeConstraintSATEncoder(constraint->inputs.get(i));
+ array[i] = encodeConstraintSATEncoder(constraint->inputs.get(i));
switch (constraint->op) {
case L_AND:
- return constraintAND(This->getCNF(), constraint->inputs.getSize(), array);
+ return constraintAND(cnf, constraint->inputs.getSize(), array);
case L_OR:
- return constraintOR(This->getCNF(), constraint->inputs.getSize(), array);
+ return constraintOR(cnf, constraint->inputs.getSize(), array);
case L_NOT:
return constraintNegate(array[0]);
case L_XOR:
- return constraintXOR(This->getCNF(), array[0], array[1]);
+ return constraintXOR(cnf, array[0], array[1]);
case L_IMPLIES:
- return constraintIMPLIES(This->getCNF(), array[0], array[1]);
+ return constraintIMPLIES(cnf, array[0], array[1]);
default:
model_print("Unhandled case in encodeLogicSATEncoder %u", constraint->op);
exit(-1);
}
}
-Edge encodePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint) {
+Edge SATEncoder::encodePredicateSATEncoder(BooleanPredicate *constraint) {
switch (GETPREDICATETYPE(constraint->predicate) ) {
case TABLEPRED:
- return encodeTablePredicateSATEncoder(This, constraint);
+ return encodeTablePredicateSATEncoder(constraint);
case OPERATORPRED:
- return encodeOperatorPredicateSATEncoder(This, constraint);
+ return encodeOperatorPredicateSATEncoder(constraint);
default:
ASSERT(0);
}
return E_BOGUS;
}
-Edge encodeTablePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint) {
+Edge SATEncoder::encodeTablePredicateSATEncoder(BooleanPredicate *constraint) {
switch (constraint->encoding.type) {
case ENUMERATEIMPLICATIONS:
case ENUMERATEIMPLICATIONSNEGATE:
- return encodeEnumTablePredicateSATEncoder(This, constraint);
+ return encodeEnumTablePredicateSATEncoder(constraint);
case CIRCUIT:
ASSERT(0);
break;
return E_BOGUS;
}
-void encodeElementSATEncoder(SATEncoder *encoder, Element *This) {
- switch ( GETELEMENTTYPE(This) ) {
+void SATEncoder::encodeElementSATEncoder(Element *element) {
+ switch ( GETELEMENTTYPE(element) ) {
case ELEMFUNCRETURN:
- generateElementEncoding(encoder, This);
- encodeElementFunctionSATEncoder(encoder, (ElementFunction *) This);
+ generateElementEncoding(element);
+ encodeElementFunctionSATEncoder((ElementFunction *) element);
break;
case ELEMSET:
- generateElementEncoding(encoder, This);
+ generateElementEncoding(element);
return;
case ELEMCONST:
return;
}
}
-void encodeElementFunctionSATEncoder(SATEncoder *encoder, ElementFunction *This) {
- switch (GETFUNCTIONTYPE(This->function)) {
+void SATEncoder::encodeElementFunctionSATEncoder(ElementFunction *function) {
+ switch (GETFUNCTIONTYPE(function->function)) {
case TABLEFUNC:
- encodeTableElementFunctionSATEncoder(encoder, This);
+ encodeTableElementFunctionSATEncoder(function);
break;
case OPERATORFUNC:
- encodeOperatorElementFunctionSATEncoder(encoder, This);
+ encodeOperatorElementFunctionSATEncoder(function);
break;
default:
ASSERT(0);
}
}
-void encodeTableElementFunctionSATEncoder(SATEncoder *encoder, ElementFunction *This) {
- switch (getElementFunctionEncoding(This)->type) {
+void SATEncoder::encodeTableElementFunctionSATEncoder(ElementFunction *function) {
+ switch (getElementFunctionEncoding(function)->type) {
case ENUMERATEIMPLICATIONS:
- encodeEnumTableElemFunctionSATEncoder(encoder, This);
+ encodeEnumTableElemFunctionSATEncoder(function);
break;
case CIRCUIT:
ASSERT(0);
#include "structs.h"
#include "inc_solver.h"
#include "constraint.h"
-#include "satelemencoder.h"
-#include "satorderencoder.h"
-#include "satfunctableencoder.h"
-
class SATEncoder {
public:
void encodeAllSATEncoder(CSolver *csolver);
Edge encodeConstraintSATEncoder(Boolean *constraint);
CNF * getCNF() { return cnf;}
- CSolver * getSolver() { return solver; }
long long getSolveTime() { return cnf->solveTime; }
long long getEncodeTime() { return cnf->encodeTime; }
MEMALLOC;
private:
+ Edge getNewVarSATEncoder();
+ void getArrayNewVarsSATEncoder(uint num, Edge *carray);
+ Edge encodeVarSATEncoder(BooleanVar *constraint);
+ Edge encodeLogicSATEncoder(BooleanLogic *constraint);
+ Edge encodePredicateSATEncoder(BooleanPredicate *constraint);
+ Edge encodeTablePredicateSATEncoder(BooleanPredicate *constraint);
+ void encodeElementSATEncoder(Element *element);
+ void encodeElementFunctionSATEncoder(ElementFunction *function);
+ void encodeTableElementFunctionSATEncoder(ElementFunction *This);
+ Edge getElementValueOneHotConstraint(Element *elem, uint64_t value);
+ Edge getElementValueUnaryConstraint(Element *elem, uint64_t value);
+ Edge getElementValueBinaryIndexConstraint(Element *element, uint64_t value);
+ Edge getElementValueBinaryValueConstraint(Element *element, uint64_t value);
+ Edge getElementValueConstraint(Element *element, uint64_t value);
+ void allocElementConstraintVariables(ElementEncoding *ee, uint numVars);
+ void generateOneHotEncodingVars(ElementEncoding *encoding);
+ void generateUnaryEncodingVars(ElementEncoding *encoding);
+ void generateBinaryIndexEncodingVars(ElementEncoding *encoding);
+ void generateBinaryValueEncodingVars(ElementEncoding *encoding);
+ void generateElementEncoding(Element *element);
+ Edge encodeOperatorPredicateSATEncoder(BooleanPredicate *constraint);
+ Edge encodeEnumOperatorPredicateSATEncoder(BooleanPredicate *constraint);
+ void encodeOperatorElementFunctionSATEncoder(ElementFunction *This);
+ Edge encodeCircuitOperatorPredicateEncoder(BooleanPredicate *constraint);
+ Edge encodeOrderSATEncoder(BooleanOrder *constraint);
+ Edge inferOrderConstraintFromGraph(Order *order, uint64_t _first, uint64_t _second);
+ Edge getPairConstraint(Order *order, OrderPair *pair);
+ Edge encodeTotalOrderSATEncoder(BooleanOrder *constraint);
+ Edge encodePartialOrderSATEncoder(BooleanOrder *constraint);
+ void createAllTotalOrderConstraintsSATEncoder(Order *order);
+ Edge getOrderConstraint(HashTableOrderPair *table, OrderPair *pair);
+ Edge generateTransOrderConstraintSATEncoder(Edge constIJ, Edge constJK, Edge constIK);
+ Edge encodeEnumEntriesTablePredicateSATEncoder(BooleanPredicate *constraint);
+ Edge encodeEnumTablePredicateSATEncoder(BooleanPredicate *constraint);
+ void encodeEnumTableElemFunctionSATEncoder(ElementFunction *This);
+ void encodeEnumEntriesTableElemFuncSATEncoder(ElementFunction *This);
+
CNF *cnf;
CSolver *solver;
};
-Edge getNewVarSATEncoder(SATEncoder *This);
-void getArrayNewVarsSATEncoder(SATEncoder *encoder, uint num, Edge *carray);
-
-Edge encodeVarSATEncoder(SATEncoder *This, BooleanVar *constraint);
-Edge encodeLogicSATEncoder(SATEncoder *This, BooleanLogic *constraint);
-Edge encodePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint);
-Edge encodeTablePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint);
-void encodeElementSATEncoder(SATEncoder *encoder, Element *This);
-void encodeElementFunctionSATEncoder(SATEncoder *encoder, ElementFunction *This);
-void encodeTableElementFunctionSATEncoder(SATEncoder *encoder, ElementFunction *This);
+Edge getOrderConstraint(HashTableOrderPair *table, OrderPair *pair);
#endif
#include "set.h"
#include "element.h"
#include "common.h"
-#include "satfuncopencoder.h"
-Edge encodeOperatorPredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint) {
+Edge SATEncoder::encodeOperatorPredicateSATEncoder(BooleanPredicate *constraint) {
switch (constraint->encoding.type) {
case ENUMERATEIMPLICATIONS:
- return encodeEnumOperatorPredicateSATEncoder(This, constraint);
+ return encodeEnumOperatorPredicateSATEncoder(constraint);
case CIRCUIT:
- return encodeCircuitOperatorPredicateEncoder(This, constraint);
+ return encodeCircuitOperatorPredicateEncoder(constraint);
default:
ASSERT(0);
}
exit(-1);
}
-Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint) {
+Edge SATEncoder::encodeEnumOperatorPredicateSATEncoder(BooleanPredicate *constraint) {
PredicateOperator *predicate = (PredicateOperator *)constraint->predicate;
uint numDomains = predicate->domains.getSize();
/* Call base encoders for children */
for (uint i = 0; i < numDomains; i++) {
Element *elem = constraint->inputs.get(i);
- encodeElementSATEncoder(This, elem);
+ encodeElementSATEncoder(elem);
}
VectorEdge *clauses = allocDefVectorEdge(); // Setup array of clauses
//Include this in the set of terms
for (uint i = 0; i < numDomains; i++) {
Element *elem = constraint->inputs.get(i);
- carray[i] = getElementValueConstraint(This, elem, vals[i]);
+ carray[i] = getElementValueConstraint(elem, vals[i]);
}
- Edge term = constraintAND(This->getCNF(), numDomains, carray);
+ Edge term = constraintAND(cnf, numDomains, carray);
pushVectorEdge(clauses, term);
}
deleteVectorEdge(clauses);
return E_False;
}
- Edge cor = constraintOR(This->getCNF(), getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
+ Edge cor = constraintOR(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
deleteVectorEdge(clauses);
return generateNegation ? constraintNegate(cor) : cor;
}
-void encodeOperatorElementFunctionSATEncoder(SATEncoder *This, ElementFunction *func) {
+void SATEncoder::encodeOperatorElementFunctionSATEncoder(ElementFunction *func) {
#ifdef TRACE_DEBUG
model_print("Operator Function ...\n");
#endif
/* Call base encoders for children */
for (uint i = 0; i < numDomains; i++) {
Element *elem = func->inputs.get(i);
- encodeElementSATEncoder(This, elem);
+ encodeElementSATEncoder(elem);
}
VectorEdge *clauses = allocDefVectorEdge(); // Setup array of clauses
//Include this in the set of terms
for (uint i = 0; i < numDomains; i++) {
Element *elem = func->inputs.get(i);
- carray[i] = getElementValueConstraint(This, elem, vals[i]);
+ carray[i] = getElementValueConstraint(elem, vals[i]);
}
if (isInRange) {
- carray[numDomains] = getElementValueConstraint(This, func, result);
+ carray[numDomains] = getElementValueConstraint(func, result);
}
Edge clause;
case IGNORE:
case NOOVERFLOW:
case WRAPAROUND: {
- clause = constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), numDomains, carray), carray[numDomains]);
+ clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]);
break;
}
case FLAGFORCESOVERFLOW: {
- clause = constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), numDomains, carray), constraintAND2(This->getCNF(), carray[numDomains], constraintNegate(overFlowConstraint)));
+ clause = constraintIMPLIES(cnf,constraintAND(cnf, numDomains, carray), constraintAND2(cnf, carray[numDomains], constraintNegate(overFlowConstraint)));
break;
}
case OVERFLOWSETSFLAG: {
if (isInRange) {
- clause = constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), numDomains, carray), carray[numDomains]);
+ clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]);
} else {
- clause = constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), numDomains, carray), overFlowConstraint);
+ clause = constraintIMPLIES(cnf,constraintAND(cnf, numDomains, carray), overFlowConstraint);
}
break;
}
case FLAGIFFOVERFLOW: {
if (isInRange) {
- clause = constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), numDomains, carray), constraintAND2(This->getCNF(), carray[numDomains], constraintNegate(overFlowConstraint)));
+ clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), constraintAND2(cnf, carray[numDomains], constraintNegate(overFlowConstraint)));
} else {
- clause = constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), numDomains, carray), overFlowConstraint);
+ clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), overFlowConstraint);
}
break;
}
deleteVectorEdge(clauses);
return;
}
- Edge cor = constraintAND(This->getCNF(), getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
- addConstraintCNF(This->getCNF(), cor);
+ Edge cor = constraintAND(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
+ addConstraintCNF(cnf, cor);
deleteVectorEdge(clauses);
}
-Edge encodeCircuitOperatorPredicateEncoder(SATEncoder *This, BooleanPredicate *constraint) {
+Edge SATEncoder::encodeCircuitOperatorPredicateEncoder(BooleanPredicate *constraint) {
PredicateOperator *predicate = (PredicateOperator *) constraint->predicate;
Element *elem0 = constraint->inputs.get(0);
- encodeElementSATEncoder(This, elem0);
+ encodeElementSATEncoder(elem0);
Element *elem1 = constraint->inputs.get(1);
- encodeElementSATEncoder(This, elem1);
+ encodeElementSATEncoder(elem1);
ElementEncoding *ee0 = getElementEncoding(elem0);
ElementEncoding *ee1 = getElementEncoding(elem1);
ASSERT(ee0->numVars == ee1->numVars);
uint numVars = ee0->numVars;
switch (predicate->op) {
case EQUALS:
- return generateEquivNVConstraint(This->getCNF(), numVars, ee0->variables, ee1->variables);
+ return generateEquivNVConstraint(cnf, numVars, ee0->variables, ee1->variables);
case LT:
- return generateLTConstraint(This->getCNF(), numVars, ee0->variables, ee1->variables);
+ return generateLTConstraint(cnf, numVars, ee0->variables, ee1->variables);
case GT:
- return generateLTConstraint(This->getCNF(), numVars, ee1->variables, ee0->variables);
+ return generateLTConstraint(cnf, numVars, ee1->variables, ee0->variables);
default:
ASSERT(0);
}
+++ /dev/null
-#ifndef SATFUNCOPENCODER_H
-#define SATFUNCOPENCODER_H
-
-Edge encodeOperatorPredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint);
-Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint);
-void encodeOperatorElementFunctionSATEncoder(SATEncoder *encoder,ElementFunction *This);
-Edge encodeCircuitOperatorPredicateEncoder(SATEncoder *This, BooleanPredicate *constraint);
-
-#endif
#include "element.h"
#include "common.h"
-Edge encodeEnumEntriesTablePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint) {
+Edge SATEncoder::encodeEnumEntriesTablePredicateSATEncoder(BooleanPredicate *constraint) {
ASSERT(GETPREDICATETYPE(constraint->predicate) == TABLEPRED);
UndefinedBehavior undefStatus = ((PredicateTable *)constraint->predicate)->undefinedbehavior;
ASSERT(undefStatus == IGNOREBEHAVIOR || undefStatus == FLAGFORCEUNDEFINED);
uint size = table->entries->getSize();
bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
Edge constraints[size];
- Edge undefConst = This->encodeConstraintSATEncoder(constraint->undefStatus);
+ Edge undefConst = encodeConstraintSATEncoder(constraint->undefStatus);
printCNF(undefConst);
model_print("**\n");
HSIteratorTableEntry *iterator = table->entries->iterator();
Edge carray[inputNum];
for (uint j = 0; j < inputNum; j++) {
Element *el = inputs->get(j);
- carray[j] = getElementValueConstraint(This, el, entry->inputs[j]);
+ carray[j] = getElementValueConstraint(el, entry->inputs[j]);
printCNF(carray[j]);
model_print("\n");
}
Edge row;
switch (undefStatus) {
case IGNOREBEHAVIOR:
- row = constraintAND(This->getCNF(), inputNum, carray);
+ row = constraintAND(cnf, inputNum, carray);
break;
case FLAGFORCEUNDEFINED: {
- addConstraintCNF(This->getCNF(), constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), inputNum, carray), constraintNegate(undefConst)));
+ addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, inputNum, carray), constraintNegate(undefConst)));
if (generateNegation == (entry->output != 0)) {
continue;
}
- row = constraintAND(This->getCNF(), inputNum, carray);
+ row = constraintAND(cnf, inputNum, carray);
break;
}
default:
}
delete iterator;
ASSERT(i != 0);
- Edge result = generateNegation ? constraintNegate(constraintOR(This->getCNF(), i, constraints))
- : constraintOR(This->getCNF(), i, constraints);
+ Edge result = generateNegation ? constraintNegate(constraintOR(cnf, i, constraints))
+ : constraintOR(cnf, i, constraints);
printCNF(result);
return result;
}
-Edge encodeEnumTablePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint) {
+Edge SATEncoder::encodeEnumTablePredicateSATEncoder(BooleanPredicate *constraint) {
#ifdef TRACE_DEBUG
model_print("Enumeration Table Predicate ...\n");
#endif
uint inputNum = inputs->getSize();
//Encode all the inputs first ...
for (uint i = 0; i < inputNum; i++) {
- encodeElementSATEncoder(This, inputs->get(i));
+ encodeElementSATEncoder(inputs->get(i));
}
PredicateTable *predicate = (PredicateTable *)constraint->predicate;
switch (predicate->undefinedbehavior) {
case IGNOREBEHAVIOR:
case FLAGFORCEUNDEFINED:
- return encodeEnumEntriesTablePredicateSATEncoder(This, constraint);
+ return encodeEnumEntriesTablePredicateSATEncoder(constraint);
default:
break;
}
vals[i] = set->getElement(indices[i]);
}
bool hasOverflow = false;
- Edge undefConstraint = This->encodeConstraintSATEncoder(constraint->undefStatus);
+ Edge undefConstraint = encodeConstraintSATEncoder(constraint->undefStatus);
printCNF(undefConstraint);
bool notfinished = true;
while (notfinished) {
Edge clause;
for (uint i = 0; i < numDomains; i++) {
Element *elem = constraint->inputs.get(i);
- carray[i] = getElementValueConstraint(This, elem, vals[i]);
+ carray[i] = getElementValueConstraint(elem, vals[i]);
}
switch (predicate->undefinedbehavior) {
case UNDEFINEDSETSFLAG:
if (isInRange) {
- clause = constraintAND(This->getCNF(), numDomains, carray);
+ clause = constraintAND(cnf, numDomains, carray);
} else {
- addConstraintCNF(This->getCNF(), constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), numDomains, carray), undefConstraint) );
+ addConstraintCNF(cnf, constraintIMPLIES(cnf,constraintAND(cnf, numDomains, carray), undefConstraint) );
}
break;
case FLAGIFFUNDEFINED:
if (isInRange) {
- clause = constraintAND(This->getCNF(), numDomains, carray);
- addConstraintCNF(This->getCNF(), constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), numDomains, carray), constraintNegate(undefConstraint)));
+ clause = constraintAND(cnf, numDomains, carray);
+ addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), constraintNegate(undefConstraint)));
} else {
- addConstraintCNF(This->getCNF(), constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), numDomains, carray), undefConstraint) );
+ addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), undefConstraint) );
}
break;
}
Edge result = E_NULL;
ASSERT(getSizeVectorEdge(clauses) != 0);
- result = constraintOR(This->getCNF(), getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
+ result = constraintOR(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
if (hasOverflow) {
- result = constraintOR2(This->getCNF(), result, undefConstraint);
+ result = constraintOR2(cnf, result, undefConstraint);
}
if (generateNegation) {
ASSERT(!hasOverflow);
return result;
}
-void encodeEnumEntriesTableElemFuncSATEncoder(SATEncoder *This, ElementFunction *func) {
+void SATEncoder::encodeEnumEntriesTableElemFuncSATEncoder(ElementFunction *func) {
UndefinedBehavior undefStatus = ((FunctionTable *) func->function)->undefBehavior;
ASSERT(undefStatus == IGNOREBEHAVIOR || undefStatus == FLAGFORCEUNDEFINED);
Array<Element *> *elements = &func->inputs;
Edge carray[inputNum];
for (uint j = 0; j < inputNum; j++) {
Element *el = elements->get(j);
- carray[j] = getElementValueConstraint(This, el, entry->inputs[j]);
+ carray[j] = getElementValueConstraint(el, entry->inputs[j]);
}
- Edge output = getElementValueConstraint(This, (Element *)func, entry->output);
+ Edge output = getElementValueConstraint(func, entry->output);
Edge row;
switch (undefStatus ) {
case IGNOREBEHAVIOR: {
- row = constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), inputNum, carray), output);
+ row = constraintIMPLIES(cnf,constraintAND(cnf, inputNum, carray), output);
break;
}
case FLAGFORCEUNDEFINED: {
- Edge undefConst = This->encodeConstraintSATEncoder(func->overflowstatus);
- row = constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), inputNum, carray), constraintAND2(This->getCNF(), output, constraintNegate(undefConst)));
+ Edge undefConst = encodeConstraintSATEncoder(func->overflowstatus);
+ row = constraintIMPLIES(cnf, constraintAND(cnf, inputNum, carray), constraintAND2(cnf, output, constraintNegate(undefConst)));
break;
}
default:
constraints[i++] = row;
}
delete iterator;
- addConstraintCNF(This->getCNF(), constraintAND(This->getCNF(), size, constraints));
+ addConstraintCNF(cnf, constraintAND(cnf, size, constraints));
}
-void encodeEnumTableElemFunctionSATEncoder(SATEncoder *This, ElementFunction *elemFunc) {
+void SATEncoder::encodeEnumTableElemFunctionSATEncoder(ElementFunction *elemFunc) {
#ifdef TRACE_DEBUG
model_print("Enumeration Table functions ...\n");
#endif
Array<Element *> *elements = &elemFunc->inputs;
for (uint i = 0; i < elements->getSize(); i++) {
Element *elem = elements->get(i);
- encodeElementSATEncoder(This, elem);
+ encodeElementSATEncoder(elem);
}
FunctionTable *function = (FunctionTable *)elemFunc->function;
switch (function->undefBehavior) {
case IGNOREBEHAVIOR:
case FLAGFORCEUNDEFINED:
- return encodeEnumEntriesTableElemFuncSATEncoder(This, elemFunc);
+ return encodeEnumEntriesTableElemFuncSATEncoder(elemFunc);
default:
break;
}
vals[i] = set->getElement(indices[i]);
}
- Edge undefConstraint = This->encodeConstraintSATEncoder(elemFunc->overflowstatus);
+ Edge undefConstraint = encodeConstraintSATEncoder(elemFunc->overflowstatus);
bool notfinished = true;
while (notfinished) {
Edge carray[numDomains + 1];
ASSERT(function->undefBehavior == UNDEFINEDSETSFLAG || function->undefBehavior == FLAGIFFUNDEFINED);
for (uint i = 0; i < numDomains; i++) {
Element *elem = elemFunc->inputs.get(i);
- carray[i] = getElementValueConstraint(This, elem, vals[i]);
+ carray[i] = getElementValueConstraint(elem, vals[i]);
}
if (isInRange) {
- carray[numDomains] = getElementValueConstraint(This, (Element *)elemFunc, tableEntry->output);
+ carray[numDomains] = getElementValueConstraint(elemFunc, tableEntry->output);
}
Edge clause;
case UNDEFINEDSETSFLAG: {
if (isInRange) {
//FIXME: Talk to Brian, It should be IFF not only IMPLY. --HG
- clause = constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), numDomains, carray), carray[numDomains]);
+ clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]);
} else {
- addConstraintCNF(This->getCNF(), constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), numDomains, carray), undefConstraint));
+ addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), undefConstraint));
}
break;
}
case FLAGIFFUNDEFINED: {
if (isInRange) {
- clause = constraintIMPLIES(This->getCNF(),constraintAND(This->getCNF(), numDomains, carray), carray[numDomains]);
- addConstraintCNF(This->getCNF(), constraintIMPLIES(This->getCNF(), constraintAND(This->getCNF(), numDomains, carray), constraintNegate(undefConstraint) ));
+ clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]);
+ addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), constraintNegate(undefConstraint) ));
} else {
- addConstraintCNF(This->getCNF(),constraintIMPLIES(This->getCNF(), constraintAND(This->getCNF(), numDomains, carray), undefConstraint));
+ addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), undefConstraint));
}
break;
}
deleteVectorEdge(clauses);
return;
}
- Edge cor = constraintAND(This->getCNF(), getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
- addConstraintCNF(This->getCNF(), cor);
+ Edge cor = constraintAND(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
+ addConstraintCNF(cnf, cor);
deleteVectorEdge(clauses);
}
+++ /dev/null
-#ifndef SATFUNCTABLEENCODER_H
-#define SATFUNCTABLEENCODER_H
-
-Edge encodeEnumEntriesTablePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint);
-Edge encodeEnumTablePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint);
-void encodeEnumTableElemFunctionSATEncoder(SATEncoder *encoder, ElementFunction *This);
-void encodeEnumEntriesTableElemFuncSATEncoder(SATEncoder *encoder, ElementFunction *This);
-
-#endif
#include "predicate.h"
#include "orderelement.h"
-Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint) {
+Edge SATEncoder::encodeOrderSATEncoder(BooleanOrder *constraint) {
switch ( constraint->order->type) {
case PARTIAL:
- return encodePartialOrderSATEncoder(This, constraint);
+ return encodePartialOrderSATEncoder(constraint);
case TOTAL:
- return encodeTotalOrderSATEncoder(This, constraint);
+ return encodeTotalOrderSATEncoder(constraint);
default:
ASSERT(0);
}
return E_NULL;
}
-Edge getPairConstraint(SATEncoder *This, Order *order, OrderPair *pair) {
+Edge SATEncoder::getPairConstraint(Order *order, OrderPair *pair) {
Edge gvalue = inferOrderConstraintFromGraph(order, pair->first, pair->second);
if (!edgeIsNull(gvalue))
return gvalue;
}
Edge constraint;
if (!(table->contains(pair))) {
- constraint = getNewVarSATEncoder(This);
+ constraint = getNewVarSATEncoder();
OrderPair *paircopy = new OrderPair(pair->first, pair->second, constraint);
table->put(paircopy, paircopy);
} else
return negate ? constraintNegate(constraint) : constraint;
}
-Edge encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder *boolOrder) {
+Edge SATEncoder::encodeTotalOrderSATEncoder(BooleanOrder *boolOrder) {
ASSERT(boolOrder->order->type == TOTAL);
if (boolOrder->order->orderPairTable == NULL) {
boolOrder->order->initializeOrderHashTable();
- bool doOptOrderStructure = GETVARTUNABLE(This->getSolver()->getTuner(), boolOrder->order->type, OPTIMIZEORDERSTRUCTURE, &onoff);
+ bool doOptOrderStructure = GETVARTUNABLE(solver->getTuner(), boolOrder->order->type, OPTIMIZEORDERSTRUCTURE, &onoff);
if (doOptOrderStructure) {
boolOrder->order->graph = buildMustOrderGraph(boolOrder->order);
- reachMustAnalysis(This->getSolver(), boolOrder->order->graph, true);
+ reachMustAnalysis(solver, boolOrder->order->graph, true);
}
- createAllTotalOrderConstraintsSATEncoder(This, boolOrder->order);
+ createAllTotalOrderConstraintsSATEncoder(boolOrder->order);
}
OrderPair pair(boolOrder->first, boolOrder->second, E_NULL);
- Edge constraint = getPairConstraint(This, boolOrder->order, &pair);
+ Edge constraint = getPairConstraint(boolOrder->order, &pair);
return constraint;
}
-void createAllTotalOrderConstraintsSATEncoder(SATEncoder *This, Order *order) {
+void SATEncoder::createAllTotalOrderConstraintsSATEncoder(Order *order) {
#ifdef TRACE_DEBUG
model_print("in total order ...\n");
#endif
for (uint j = i + 1; j < size; j++) {
uint64_t valueJ = mems->get(j);
OrderPair pairIJ(valueI, valueJ, E_NULL);
- Edge constIJ = getPairConstraint(This, order, &pairIJ);
+ Edge constIJ = getPairConstraint(order, &pairIJ);
for (uint k = j + 1; k < size; k++) {
uint64_t valueK = mems->get(k);
OrderPair pairJK(valueJ, valueK, E_NULL);
OrderPair pairIK(valueI, valueK, E_NULL);
- Edge constIK = getPairConstraint(This, order, &pairIK);
- Edge constJK = getPairConstraint(This, order, &pairJK);
- addConstraintCNF(This->getCNF(), generateTransOrderConstraintSATEncoder(This, constIJ, constJK, constIK));
+ Edge constIK = getPairConstraint(order, &pairIK);
+ Edge constJK = getPairConstraint(order, &pairJK);
+ addConstraintCNF(cnf, generateTransOrderConstraintSATEncoder(constIJ, constJK, constIK));
}
}
}
return negate ? constraintNegate(constraint) : constraint;
}
-Edge generateTransOrderConstraintSATEncoder(SATEncoder *This, Edge constIJ,Edge constJK,Edge constIK) {
+Edge SATEncoder::generateTransOrderConstraintSATEncoder(Edge constIJ,Edge constJK,Edge constIK) {
Edge carray[] = {constIJ, constJK, constraintNegate(constIK)};
- Edge loop1 = constraintOR(This->getCNF(), 3, carray);
+ Edge loop1 = constraintOR(cnf, 3, carray);
Edge carray2[] = {constraintNegate(constIJ), constraintNegate(constJK), constIK};
- Edge loop2 = constraintOR(This->getCNF(), 3, carray2 );
- return constraintAND2(This->getCNF(), loop1, loop2);
+ Edge loop2 = constraintOR(cnf, 3, carray2 );
+ return constraintAND2(cnf, loop1, loop2);
}
-Edge encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint) {
+Edge SATEncoder::encodePartialOrderSATEncoder(BooleanOrder *constraint) {
ASSERT(constraint->order->type == PARTIAL);
return E_BOGUS;
}
+++ /dev/null
-#ifndef SATORDERENCODER_H
-#define SATORDERENCODER_H
-
-Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint);
-Edge inferOrderConstraintFromGraph(Order *order, uint64_t _first, uint64_t _second);
-Edge getPairConstraint(SATEncoder *This, Order *order, OrderPair *pair);
-Edge encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint);
-Edge encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint);
-void createAllTotalOrderConstraintsSATEncoder(SATEncoder *This, Order *order);
-Edge getOrderConstraint(HashTableOrderPair *table, OrderPair *pair);
-Edge generateTransOrderConstraintSATEncoder(SATEncoder *This, Edge constIJ, Edge constJK, Edge constIK);
-#endif
projects / satune.git / commitdiff