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;
34 long long startTime = getTimeNano();
35 finishedClauses(cnf->solver);
36 cnf->encodeTime = getTimeNano() - startTime;
37 if(solver->isIncrementalMode()){
38 solver->freezeElementsVariables();
43 void SATEncoder::encodeAllSATEncoder(CSolver *csolver) {
44 if (csolver->isUnSAT()) {
47 SetIteratorBooleanEdge *iterator = csolver->getConstraints();
48 while (iterator->hasNext()) {
49 BooleanEdge constraint = iterator->next();
50 if(!csolver->isConstraintEncoded(constraint)){
51 Edge c = encodeConstraintSATEncoder(constraint);
52 addConstraintCNF(cnf, c);
53 csolver->addEncodedConstraint(constraint);
59 Edge SATEncoder::encodeConstraintSATEncoder(BooleanEdge c) {
61 Boolean *constraint = c.getBoolean();
63 if (booledgeMap.contains(constraint)) {
64 Edge e = {(Node *) booledgeMap.get(constraint)};
65 return c.isNegated() ? constraintNegate(e) : e;
68 switch (constraint->type) {
70 result = encodeOrderSATEncoder((BooleanOrder *) constraint);
73 result = encodeVarSATEncoder((BooleanVar *) constraint);
76 result = encodeLogicSATEncoder((BooleanLogic *) constraint);
79 result = encodePredicateSATEncoder((BooleanPredicate *) constraint);
82 result = ((BooleanConst *) constraint)->isTrue() ? E_True : E_False;
85 model_print("Unhandled case in encodeConstraintSATEncoder %u", constraint->type);
88 Polarity p = constraint->polarity;
89 uint pSize = constraint->parents.getSize();
91 if ( !edgeIsVarConst(result) && pSize > (uint)solver->getTuner()->getTunable(PROXYVARIABLE, &proxyparameter) ) {
92 Edge e = getNewVarSATEncoder();
93 generateProxy(cnf, result, e, p);
94 booledgeMap.put(constraint, e.node_ptr);
98 return c.isNegated() ? constraintNegate(result) : result;
101 void SATEncoder::getArrayNewVarsSATEncoder(uint num, Edge *carray) {
102 for (uint i = 0; i < num; i++)
103 carray[i] = getNewVarSATEncoder();
106 Edge SATEncoder::getNewVarSATEncoder() {
107 return constraintNewVar(cnf);
110 Edge SATEncoder::encodeVarSATEncoder(BooleanVar *constraint) {
111 if (edgeIsNull(constraint->var)) {
112 constraint->var = getNewVarSATEncoder();
114 return constraint->var;
117 Edge SATEncoder::encodeLogicSATEncoder(BooleanLogic *constraint) {
118 Edge array[constraint->inputs.getSize()];
119 for (uint i = 0; i < constraint->inputs.getSize(); i++)
120 array[i] = encodeConstraintSATEncoder(constraint->inputs.get(i));
122 switch (constraint->op) {
124 return constraintAND(cnf, constraint->inputs.getSize(), array);
126 return constraintNegate(array[0]);
128 ASSERT(constraint->inputs.getSize() == 2);
129 return constraintIFF(cnf, array[0], array[1]);
133 //Don't handle, translate these away...
135 model_print("Unhandled case in encodeLogicSATEncoder %u", constraint->op);
140 Edge SATEncoder::encodePredicateSATEncoder(BooleanPredicate *constraint) {
141 switch (constraint->predicate->type) {
143 return encodeTablePredicateSATEncoder(constraint);
145 return encodeOperatorPredicateSATEncoder(constraint);
152 Edge SATEncoder::encodeTablePredicateSATEncoder(BooleanPredicate *constraint) {
153 switch (constraint->encoding.type) {
154 case ENUMERATEIMPLICATIONS:
155 case ENUMERATEIMPLICATIONSNEGATE:
156 return encodeEnumTablePredicateSATEncoder(constraint);
166 void SATEncoder::encodeElementSATEncoder(Element *element) {
167 /* Check to see if we have already encoded this element. */
168 if (element->getElementEncoding()->variables != NULL)
171 /* Need to encode. */
172 switch ( element->type) {
174 generateElementEncoding(element);
175 encodeElementFunctionSATEncoder((ElementFunction *) element);
178 generateElementEncoding(element);
187 void SATEncoder::encodeElementFunctionSATEncoder(ElementFunction *function) {
188 switch (function->getFunction()->type) {
190 encodeTableElementFunctionSATEncoder(function);
193 encodeOperatorElementFunctionSATEncoder(function);
200 void SATEncoder::encodeTableElementFunctionSATEncoder(ElementFunction *function) {
201 switch (function->getElementFunctionEncoding()->type) {
202 case ENUMERATEIMPLICATIONS:
203 encodeEnumTableElemFunctionSATEncoder(function);