#include "order.h"
#include "predicate.h"
#include "set.h"
-#include "satfuncopencoder.h"
+#include "tunable.h"
-//TODO: Should handle sharing of AST Nodes without recoding them a second time
-
-SATEncoder::SATEncoder(CSolver * _solver) :
- varcount(1),
+SATEncoder::SATEncoder(CSolver *_solver) :
cnf(createCNF()),
- solver(_solver) {
+ solver(_solver),
+ vector(allocDefVectorEdge()) {
}
SATEncoder::~SATEncoder() {
deleteCNF(cnf);
+ deleteVectorEdge(vector);
+}
+
+void SATEncoder::resetSATEncoder() {
+ resetCNF(cnf);
+ booledgeMap.reset();
+}
+
+int SATEncoder::solve(long timeout) {
+ cnf->solver->timeout = timeout;
+ return solveCNF(cnf);
}
void SATEncoder::encodeAllSATEncoder(CSolver *csolver) {
- HSIteratorBoolean *iterator = csolver->getConstraints();
+ if (csolver->isUnSAT()) {
+ return;
+ }
+ SetIteratorBooleanEdge *iterator = csolver->getConstraints();
while (iterator->hasNext()) {
- Boolean *constraint = iterator->next();
- model_print("Encoding All ...\n\n");
+ BooleanEdge constraint = iterator->next();
Edge c = encodeConstraintSATEncoder(constraint);
- model_print("Returned Constraint in EncodingAll:\n");
- ASSERT( !equalsEdge(c, E_BOGUS));
addConstraintCNF(cnf, c);
}
delete iterator;
}
-Edge SATEncoder::encodeConstraintSATEncoder(Boolean *constraint) {
- switch (GETBOOLEANTYPE(constraint)) {
+Edge SATEncoder::encodeConstraintSATEncoder(BooleanEdge c) {
+ Edge result;
+ Boolean *constraint = c.getBoolean();
+
+ if (booledgeMap.contains(constraint)) {
+ Edge e = {(Node *) booledgeMap.get(constraint)};
+ return c.isNegated() ? constraintNegate(e) : e;
+ }
+
+ switch (constraint->type) {
case ORDERCONST:
- return encodeOrderSATEncoder(this, (BooleanOrder *) constraint);
+ result = encodeOrderSATEncoder((BooleanOrder *) constraint);
+ break;
case BOOLEANVAR:
- return encodeVarSATEncoder(this, (BooleanVar *) constraint);
+ result = encodeVarSATEncoder((BooleanVar *) constraint);
+ break;
case LOGICOP:
- return encodeLogicSATEncoder(this, (BooleanLogic *) constraint);
+ result = encodeLogicSATEncoder((BooleanLogic *) constraint);
+ break;
case PREDICATEOP:
- return encodePredicateSATEncoder(this, (BooleanPredicate *) constraint);
+ result = encodePredicateSATEncoder((BooleanPredicate *) constraint);
+ break;
+ case BOOLCONST:
+ result = ((BooleanConst *) constraint)->isTrue() ? E_True : E_False;
+ break;
default:
- model_print("Unhandled case in encodeConstraintSATEncoder %u", GETBOOLEANTYPE(constraint));
+ model_print("Unhandled case in encodeConstraintSATEncoder %u", constraint->type);
exit(-1);
}
+ Polarity p = constraint->polarity;
+ uint pSize = constraint->parents.getSize();
+
+ if ( !edgeIsVarConst(result) && pSize > (uint)solver->getTuner()->getTunable(PROXYVARIABLE, &proxyparameter) ) {
+ Edge e = getNewVarSATEncoder();
+ generateProxy(cnf, result, e, p);
+ booledgeMap.put(constraint, e.node_ptr);
+ result = e;
+ }
+
+ return c.isNegated() ? constraintNegate(result) : result;
}
-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->cnf);
+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->cnf, constraint->inputs.getSize(), array);
- case L_OR:
- return constraintOR(This->cnf, constraint->inputs.getSize(), array);
- case L_NOT:
+ case SATC_AND:
+ return constraintAND(cnf, constraint->inputs.getSize(), array);
+ case SATC_NOT:
return constraintNegate(array[0]);
- case L_XOR:
- return constraintXOR(This->cnf, array[0], array[1]);
- case L_IMPLIES:
- return constraintIMPLIES(This->cnf, array[0], array[1]);
+ case SATC_IFF:
+ ASSERT(constraint->inputs.getSize() == 2);
+ return constraintIFF(cnf, array[0], array[1]);
+ case SATC_OR:
+ case SATC_XOR:
+ case SATC_IMPLIES:
+ //Don't handle, translate these away...
default:
model_print("Unhandled case in encodeLogicSATEncoder %u", constraint->op);
exit(-1);
}
}
-Edge encodePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint) {
- switch (GETPREDICATETYPE(constraint->predicate) ) {
+Edge SATEncoder::encodePredicateSATEncoder(BooleanPredicate *constraint) {
+ switch (constraint->predicate->type) {
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) {
+ /* Check to see if we have already encoded this element. */
+ if (element->getElementEncoding()->variables != NULL)
+ return;
+
+ /* Need to encode. */
+ switch ( element->type) {
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 (function->getFunction()->type) {
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 (function->getElementFunctionEncoding()->type) {
case ENUMERATEIMPLICATIONS:
- encodeEnumTableElemFunctionSATEncoder(encoder, This);
+ encodeEnumTableElemFunctionSATEncoder(function);
break;
case CIRCUIT:
ASSERT(0);
projects / satune.git / blobdiff