1 #include "satencoder.h"
5 #include "constraint.h"
9 #include "tableentry.h"
12 #include "predicate.h"
16 SATEncoder::SATEncoder(CSolver *_solver) :
19 vector(allocDefVectorEdge()) {
22 SATEncoder::~SATEncoder() {
24 deleteVectorEdge(vector);
27 void SATEncoder::resetSATEncoder() {
32 int SATEncoder::solve(long timeout) {
33 cnf->solver->timeout = timeout;
37 void SATEncoder::encodeAllSATEncoder(CSolver *csolver) {
38 SetIteratorBooleanEdge *iterator = csolver->getConstraints();
39 while (iterator->hasNext()) {
40 BooleanEdge constraint = iterator->next();
41 Edge c = encodeConstraintSATEncoder(constraint);
42 addConstraintCNF(cnf, c);
47 Edge SATEncoder::encodeConstraintSATEncoder(BooleanEdge c) {
49 Boolean *constraint = c.getBoolean();
51 if (booledgeMap.contains(constraint)) {
52 Edge e = {(Node *) booledgeMap.get(constraint)};
53 return c.isNegated() ? constraintNegate(e) : e;
56 switch (constraint->type) {
58 result = encodeOrderSATEncoder((BooleanOrder *) constraint);
61 result = encodeVarSATEncoder((BooleanVar *) constraint);
64 result = encodeLogicSATEncoder((BooleanLogic *) constraint);
67 result = encodePredicateSATEncoder((BooleanPredicate *) constraint);
70 result = ((BooleanConst *) constraint)->isTrue() ? E_True : E_False;
73 model_print("Unhandled case in encodeConstraintSATEncoder %u", constraint->type);
76 Polarity p = constraint->polarity;
77 uint pSize = constraint->parents.getSize();
79 if ( !edgeIsVarConst(result) && pSize > (uint)solver->getTuner()->getTunable(PROXYVARIABLE, &proxyparameter) ) {
80 Edge e = getNewVarSATEncoder();
81 generateProxy(cnf, result, e, p);
82 booledgeMap.put(constraint, e.node_ptr);
86 return c.isNegated() ? constraintNegate(result) : result;
89 void SATEncoder::getArrayNewVarsSATEncoder(uint num, Edge *carray) {
90 for (uint i = 0; i < num; i++)
91 carray[i] = getNewVarSATEncoder();
94 Edge SATEncoder::getNewVarSATEncoder() {
95 return constraintNewVar(cnf);
98 Edge SATEncoder::encodeVarSATEncoder(BooleanVar *constraint) {
99 if (edgeIsNull(constraint->var)) {
100 constraint->var = getNewVarSATEncoder();
102 return constraint->var;
105 Edge SATEncoder::encodeLogicSATEncoder(BooleanLogic *constraint) {
106 Edge array[constraint->inputs.getSize()];
107 for (uint i = 0; i < constraint->inputs.getSize(); i++)
108 array[i] = encodeConstraintSATEncoder(constraint->inputs.get(i));
110 switch (constraint->op) {
112 return constraintAND(cnf, constraint->inputs.getSize(), array);
114 return constraintNegate(array[0]);
116 ASSERT(constraint->inputs.getSize() == 2);
117 return constraintIFF(cnf, array[0], array[1]);
121 //Don't handle, translate these away...
123 model_print("Unhandled case in encodeLogicSATEncoder %u", constraint->op);
128 Edge SATEncoder::encodePredicateSATEncoder(BooleanPredicate *constraint) {
129 switch (constraint->predicate->type) {
131 return encodeTablePredicateSATEncoder(constraint);
133 return encodeOperatorPredicateSATEncoder(constraint);
140 Edge SATEncoder::encodeTablePredicateSATEncoder(BooleanPredicate *constraint) {
141 switch (constraint->encoding.type) {
142 case ENUMERATEIMPLICATIONS:
143 case ENUMERATEIMPLICATIONSNEGATE:
144 return encodeEnumTablePredicateSATEncoder(constraint);
154 void SATEncoder::encodeElementSATEncoder(Element *element) {
155 /* Check to see if we have already encoded this element. */
156 if (element->getElementEncoding()->variables != NULL)
159 /* Need to encode. */
160 switch ( element->type) {
162 generateElementEncoding(element);
163 encodeElementFunctionSATEncoder((ElementFunction *) element);
166 generateElementEncoding(element);
175 void SATEncoder::encodeElementFunctionSATEncoder(ElementFunction *function) {
176 switch (function->getFunction()->type) {
178 encodeTableElementFunctionSATEncoder(function);
181 encodeOperatorElementFunctionSATEncoder(function);
188 void SATEncoder::encodeTableElementFunctionSATEncoder(ElementFunction *function) {
189 switch (function->getElementFunctionEncoding()->type) {
190 case ENUMERATEIMPLICATIONS:
191 encodeEnumTableElemFunctionSATEncoder(function);