1 #include "naiveencoder.h"
2 #include "elementencoding.h"
4 #include "functionencoding.h"
12 #include "tableentry.h"
17 void naiveEncodingDecision(CSolver *This) {
18 if (This->isUnSAT()) {
21 HashsetBoolean *visited = new HashsetBoolean();
22 SetIteratorBooleanEdge *iterator = This->getConstraints();
23 while (iterator->hasNext()) {
24 BooleanEdge b = iterator->next();
25 naiveEncodingConstraint(This, visited, b.getBoolean());
31 void naiveEncodingConstraint(CSolver *csolver, HashsetBoolean *visited, Boolean *This) {
37 if (((BooleanOrder *) This)->order->encoding.type == ORDER_UNASSIGNED)
38 ((BooleanOrder *) This)->order->setOrderEncodingType(PAIRWISE);
42 naiveEncodingLogicOp(csolver, visited, (BooleanLogic *) This);
46 naiveEncodingPredicate(csolver, (BooleanPredicate *) This);
54 void naiveEncodingLogicOp(CSolver *csolver, HashsetBoolean *visited, BooleanLogic *This) {
55 if (!visited->add(This))
58 for (uint i = 0; i < This->inputs.getSize(); i++) {
59 naiveEncodingConstraint(csolver, visited, This->inputs.get(i).getBoolean());
63 void naiveEncodingPredicate(CSolver *csolver, BooleanPredicate *This) {
64 FunctionEncoding *encoding = This->getFunctionEncoding();
65 if (encoding->getFunctionEncodingType() == FUNC_UNASSIGNED)
66 This->getFunctionEncoding()->setFunctionEncodingType(ENUMERATEIMPLICATIONS);
68 for (uint i = 0; i < This->inputs.getSize(); i++) {
69 Element *element = This->inputs.get(i);
70 naiveEncodingElement(csolver, element);
74 void naiveEncodingElement(CSolver *csolver, Element *This) {
75 ElementEncoding *encoding = This->getElementEncoding();
76 if (encoding->getElementEncodingType() == ELEM_UNASSIGNED) {
77 if (This->type != ELEMCONST) {
78 model_print("INFO: naive encoder is making the decision about element %p....\n", This);
80 uint enc = csolver->getTuner()->getVarTunable(This->getRange()->getType(), NODEENCODING, &NodeEncodingDesc);
81 if (enc == ELEM_UNASSIGNED)
82 enc = csolver->getTuner()->getTunable(NAIVEENCODER, &NaiveEncodingDesc);
83 encoding->setElementEncodingType((ElementEncodingType)enc);
84 encoding->encodingArrayInitialization();
87 if (This->type == ELEMFUNCRETURN) {
88 ElementFunction *function = (ElementFunction *) This;
89 for (uint i = 0; i < function->inputs.getSize(); i++) {
90 Element *element = function->inputs.get(i);
91 naiveEncodingElement(csolver, element);
93 FunctionEncoding *encoding = function->getElementFunctionEncoding();
94 if (encoding->getFunctionEncodingType() == FUNC_UNASSIGNED)
95 function->getElementFunctionEncoding()->setFunctionEncodingType(ENUMERATEIMPLICATIONS);