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() {
36 void SATEncoder::encodeAllSATEncoder(CSolver *csolver) {
37 SetIteratorBooleanEdge *iterator = csolver->getConstraints();
38 while (iterator->hasNext()) {
39 BooleanEdge constraint = iterator->next();
40 Edge c = encodeConstraintSATEncoder(constraint);
41 addConstraintCNF(cnf, c);
46 Edge SATEncoder::encodeConstraintSATEncoder(BooleanEdge c) {
48 Boolean *constraint = c.getBoolean();
50 if (booledgeMap.contains(constraint)) {
51 Edge e = {(Node *) booledgeMap.get(constraint)};
52 return c.isNegated() ? constraintNegate(e) : e;
55 switch (constraint->type) {
57 result = encodeOrderSATEncoder((BooleanOrder *) constraint);
60 result = encodeVarSATEncoder((BooleanVar *) constraint);
63 result = encodeLogicSATEncoder((BooleanLogic *) constraint);
66 result = encodePredicateSATEncoder((BooleanPredicate *) constraint);
69 result = ((BooleanConst *) constraint)->isTrue() ? E_True : E_False;
72 model_print("Unhandled case in encodeConstraintSATEncoder %u", constraint->type);
75 Polarity p = constraint->polarity;
76 uint pSize = constraint->parents.getSize();
77 if (solver->getTuner()->getTunable(PROXYVARIABLE, &offon) == 1) {
78 // if ((pSize > 1 && p != P_BOTHTRUEFALSE ) || pSize > 2) {
79 Edge e = getNewVarSATEncoder();
80 generateProxy(cnf, result, e, p);
81 booledgeMap.put(constraint, e.node_ptr);
84 booledgeMap.put(constraint, result.node_ptr);
87 return c.isNegated() ? constraintNegate(result) : result;
90 void SATEncoder::getArrayNewVarsSATEncoder(uint num, Edge *carray) {
91 for (uint i = 0; i < num; i++)
92 carray[i] = getNewVarSATEncoder();
95 Edge SATEncoder::getNewVarSATEncoder() {
96 return constraintNewVar(cnf);
99 Edge SATEncoder::encodeVarSATEncoder(BooleanVar *constraint) {
100 if (edgeIsNull(constraint->var)) {
101 constraint->var = getNewVarSATEncoder();
103 return constraint->var;
106 Edge SATEncoder::encodeLogicSATEncoder(BooleanLogic *constraint) {
107 Edge array[constraint->inputs.getSize()];
108 for (uint i = 0; i < constraint->inputs.getSize(); i++)
109 array[i] = encodeConstraintSATEncoder(constraint->inputs.get(i));
111 switch (constraint->op) {
113 return constraintAND(cnf, constraint->inputs.getSize(), array);
115 return constraintNegate(array[0]);
117 ASSERT(constraint->inputs.getSize() == 2);
118 return constraintIFF(cnf, array[0], array[1]);
122 //Don't handle, translate these away...
124 model_print("Unhandled case in encodeLogicSATEncoder %u", constraint->op);
129 Edge SATEncoder::encodePredicateSATEncoder(BooleanPredicate *constraint) {
130 switch (constraint->predicate->type) {
132 return encodeTablePredicateSATEncoder(constraint);
134 return encodeOperatorPredicateSATEncoder(constraint);
141 Edge SATEncoder::encodeTablePredicateSATEncoder(BooleanPredicate *constraint) {
142 switch (constraint->encoding.type) {
143 case ENUMERATEIMPLICATIONS:
144 case ENUMERATEIMPLICATIONSNEGATE:
145 return encodeEnumTablePredicateSATEncoder(constraint);
155 void SATEncoder::encodeElementSATEncoder(Element *element) {
156 /* Check to see if we have already encoded this element. */
157 if (element->getElementEncoding()->variables != NULL)
160 /* Need to encode. */
161 switch ( element->type) {
163 generateElementEncoding(element);
164 encodeElementFunctionSATEncoder((ElementFunction *) element);
167 generateElementEncoding(element);
176 void SATEncoder::encodeElementFunctionSATEncoder(ElementFunction *function) {
177 switch (function->getFunction()->type) {
179 encodeTableElementFunctionSATEncoder(function);
182 encodeOperatorElementFunctionSATEncoder(function);
189 void SATEncoder::encodeTableElementFunctionSATEncoder(ElementFunction *function) {
190 switch (function->getElementFunctionEncoding()->type) {
191 case ENUMERATEIMPLICATIONS:
192 encodeEnumTableElemFunctionSATEncoder(function);