1 #include "satencoder.h"
8 #include "tableentry.h"
12 #include "satfuncopencoder.h"
14 Edge encodeOperatorPredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint) {
15 switch (constraint->encoding.type) {
16 case ENUMERATEIMPLICATIONS:
17 return encodeEnumOperatorPredicateSATEncoder(This, constraint);
19 return encodeCircuitOperatorPredicateEncoder(This, constraint);
26 Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint) {
27 PredicateOperator *predicate = (PredicateOperator *)constraint->predicate;
28 uint numDomains = getSizeArraySet(&predicate->domains);
30 FunctionEncodingType encType = constraint->encoding.type;
31 bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
33 /* Call base encoders for children */
34 for (uint i = 0; i < numDomains; i++) {
35 Element *elem = getArrayElement( &constraint->inputs, i);
36 encodeElementSATEncoder(This, elem);
38 VectorEdge *clauses = allocDefVectorEdge(); // Setup array of clauses
40 uint indices[numDomains]; //setup indices
41 bzero(indices, sizeof(uint) * numDomains);
43 uint64_t vals[numDomains];//setup value array
44 for (uint i = 0; i < numDomains; i++) {
45 Set *set = getArraySet(&predicate->domains, i);
46 vals[i] = getSetElement(set, indices[i]);
49 bool notfinished = true;
51 Edge carray[numDomains];
53 if (evalPredicateOperator(predicate, vals) ^ generateNegation) {
54 //Include this in the set of terms
55 for (uint i = 0; i < numDomains; i++) {
56 Element *elem = getArrayElement(&constraint->inputs, i);
57 carray[i] = getElementValueConstraint(This, elem, vals[i]);
59 Edge term = constraintAND(This->cnf, numDomains, carray);
60 pushVectorEdge(clauses, term);
64 for (uint i = 0; i < numDomains; i++) {
65 uint index = ++indices[i];
66 Set *set = getArraySet(&predicate->domains, i);
68 if (index < getSetSize(set)) {
69 vals[i] = getSetElement(set, index);
74 vals[i] = getSetElement(set, 0);
78 if (getSizeVectorEdge(clauses) == 0) {
79 deleteVectorEdge(clauses);
82 Edge cor = constraintOR(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
83 deleteVectorEdge(clauses);
84 return generateNegation ? constraintNegate(cor) : cor;
88 void encodeOperatorElementFunctionSATEncoder(SATEncoder *This, ElementFunction *func) {
90 model_print("Operator Function ...\n");
92 FunctionOperator *function = (FunctionOperator *) func->function;
93 uint numDomains = getSizeArrayElement(&func->inputs);
95 /* Call base encoders for children */
96 for (uint i = 0; i < numDomains; i++) {
97 Element *elem = getArrayElement( &func->inputs, i);
98 encodeElementSATEncoder(This, elem);
101 VectorEdge *clauses = allocDefVectorEdge(); // Setup array of clauses
103 uint indices[numDomains]; //setup indices
104 bzero(indices, sizeof(uint) * numDomains);
106 uint64_t vals[numDomains];//setup value array
107 for (uint i = 0; i < numDomains; i++) {
108 Set *set = getElementSet(getArrayElement(&func->inputs, i));
109 vals[i] = getSetElement(set, indices[i]);
112 Edge overFlowConstraint = ((BooleanVar *) func->overflowstatus)->var;
114 bool notfinished = true;
115 while (notfinished) {
116 Edge carray[numDomains + 1];
118 uint64_t result = applyFunctionOperator(function, numDomains, vals);
119 bool isInRange = isInRangeFunction((FunctionOperator *)func->function, result);
120 bool needClause = isInRange;
121 if (function->overflowbehavior == OVERFLOWSETSFLAG || function->overflowbehavior == FLAGIFFOVERFLOW) {
126 //Include this in the set of terms
127 for (uint i = 0; i < numDomains; i++) {
128 Element *elem = getArrayElement(&func->inputs, i);
129 carray[i] = getElementValueConstraint(This, elem, vals[i]);
132 carray[numDomains] = getElementValueConstraint(This, func, result);
136 switch (function->overflowbehavior) {
140 clause = constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]);
143 case FLAGFORCESOVERFLOW: {
144 clause = constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintAND2(This->cnf, carray[numDomains], constraintNegate(overFlowConstraint)));
147 case OVERFLOWSETSFLAG: {
149 clause = constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]);
151 clause = constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), overFlowConstraint);
155 case FLAGIFFOVERFLOW: {
157 clause = constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintAND2(This->cnf, carray[numDomains], constraintNegate(overFlowConstraint)));
159 clause = constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), overFlowConstraint);
167 model_print("added clause in operator function\n");
171 pushVectorEdge(clauses, clause);
175 for (uint i = 0; i < numDomains; i++) {
176 uint index = ++indices[i];
177 Set *set = getElementSet(getArrayElement(&func->inputs, i));
179 if (index < getSetSize(set)) {
180 vals[i] = getSetElement(set, index);
185 vals[i] = getSetElement(set, 0);
189 if (getSizeVectorEdge(clauses) == 0) {
190 deleteVectorEdge(clauses);
193 Edge cor = constraintAND(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
194 addConstraintCNF(This->cnf, cor);
195 deleteVectorEdge(clauses);
198 Edge encodeCircuitOperatorPredicateEncoder(SATEncoder *This, BooleanPredicate *constraint) {
199 PredicateOperator *predicate = (PredicateOperator *) constraint->predicate;
200 ASSERT(getSizeArraySet(&predicate->domains) == 2);
201 Element *elem0 = getArrayElement( &constraint->inputs, 0);
202 encodeElementSATEncoder(This, elem0);
203 Element *elem1 = getArrayElement( &constraint->inputs, 1);
204 encodeElementSATEncoder(This, elem1);
205 ElementEncoding *ee0 = getElementEncoding(elem0);
206 ElementEncoding *ee1 = getElementEncoding(elem1);
207 ASSERT(ee0->numVars == ee1->numVars);
208 uint numVars = ee0->numVars;
209 switch (predicate->op) {
211 return generateEquivNVConstraint(This->cnf, numVars, ee0->variables, ee1->variables);
213 return generateLTConstraint(This->cnf, numVars, ee0->variables, ee1->variables);
215 return generateLTConstraint(This->cnf, numVars, ee1->variables, ee0->variables);