#include "table.h"
#include "tableentry.h"
#include "order.h"
+#include "tunable.h"
#include <strings.h>
void naiveEncodingDecision(CSolver *This) {
- HSIteratorBoolean *iterator=This->constraints.iterator();
- while(iterator->hasNext()) {
- Boolean *boolean = iterator->next();
- naiveEncodingConstraint(boolean);
+ if (This->isUnSAT()) {
+ return;
+ }
+ SetIteratorBooleanEdge *iterator = This->getConstraints();
+ while (iterator->hasNext()) {
+ BooleanEdge b = iterator->next();
+ naiveEncodingConstraint(This, b.getBoolean());
}
delete iterator;
}
-void naiveEncodingConstraint(Boolean *This) {
- switch (GETBOOLEANTYPE(This)) {
+void naiveEncodingConstraint(CSolver *csolver, Boolean *This) {
+ switch (This->type) {
case BOOLEANVAR: {
return;
}
case ORDERCONST: {
- ((BooleanOrder *) This)->order->setOrderEncodingType(PAIRWISE);
+ if (((BooleanOrder *) This)->order->encoding.type == ORDER_UNASSIGNED)
+ ((BooleanOrder *) This)->order->setOrderEncodingType(PAIRWISE);
return;
}
case LOGICOP: {
- naiveEncodingLogicOp((BooleanLogic *) This);
+ naiveEncodingLogicOp(csolver, (BooleanLogic *) This);
return;
}
case PREDICATEOP: {
- naiveEncodingPredicate((BooleanPredicate *) This);
+ naiveEncodingPredicate(csolver, (BooleanPredicate *) This);
return;
}
default:
}
}
-void naiveEncodingLogicOp(BooleanLogic *This) {
+void naiveEncodingLogicOp(CSolver *csolver, BooleanLogic *This) {
for (uint i = 0; i < This->inputs.getSize(); i++) {
- naiveEncodingConstraint(This->inputs.get(i));
+ naiveEncodingConstraint(csolver, This->inputs.get(i).getBoolean());
}
}
-void naiveEncodingPredicate(BooleanPredicate *This) {
+void naiveEncodingPredicate(CSolver *csolver, BooleanPredicate *This) {
FunctionEncoding *encoding = This->getFunctionEncoding();
- if (getFunctionEncodingType(encoding) == FUNC_UNASSIGNED)
- setFunctionEncodingType(This->getFunctionEncoding(), ENUMERATEIMPLICATIONS);
+ if (encoding->getFunctionEncodingType() == FUNC_UNASSIGNED)
+ This->getFunctionEncoding()->setFunctionEncodingType(ENUMERATEIMPLICATIONS);
for (uint i = 0; i < This->inputs.getSize(); i++) {
Element *element = This->inputs.get(i);
- naiveEncodingElement(element);
+ naiveEncodingElement(csolver, element);
}
}
-void naiveEncodingElement(Element *This) {
- ElementEncoding *encoding = getElementEncoding(This);
- if (getElementEncodingType(encoding) == ELEM_UNASSIGNED) {
- setElementEncodingType(encoding, BINARYINDEX);
- encodingArrayInitialization(encoding);
+void naiveEncodingElement(CSolver *csolver, Element *This) {
+ ElementEncoding *encoding = This->getElementEncoding();
+ if (encoding->getElementEncodingType() == ELEM_UNASSIGNED) {
+ if (This->type != ELEMCONST) {
+ model_print("INFO: naive encoder is making the decision about element %p....\n", This);
+ }
+ uint enc = csolver->getTuner()->getVarTunable(This->getRange()->getType(), NODEENCODING, &NodeEncodingDesc);
+ if (enc == ELEM_UNASSIGNED)
+ enc = csolver->getTuner()->getTunable(NAIVEENCODER, &NaiveEncodingDesc);
+ encoding->setElementEncodingType((ElementEncodingType)enc);
+ encoding->encodingArrayInitialization();
}
- if (GETELEMENTTYPE(This) == ELEMFUNCRETURN) {
+ if (This->type == ELEMFUNCRETURN) {
ElementFunction *function = (ElementFunction *) This;
for (uint i = 0; i < function->inputs.getSize(); i++) {
Element *element = function->inputs.get(i);
- naiveEncodingElement(element);
+ naiveEncodingElement(csolver, element);
}
- FunctionEncoding *encoding = getElementFunctionEncoding(function);
- if (getFunctionEncodingType(encoding) == FUNC_UNASSIGNED)
- setFunctionEncodingType(getElementFunctionEncoding(function), ENUMERATEIMPLICATIONS);
- }
-}
-
-uint getSizeEncodingArray(ElementEncoding *This, uint setSize) {
- switch (This->type) {
- case BINARYINDEX:
- return NEXTPOW2(setSize);
- case ONEHOT:
- case UNARY:
- return setSize;
- default:
- ASSERT(0);
+ FunctionEncoding *encoding = function->getElementFunctionEncoding();
+ if (encoding->getFunctionEncodingType() == FUNC_UNASSIGNED)
+ function->getElementFunctionEncoding()->setFunctionEncodingType(ENUMERATEIMPLICATIONS);
}
- return -1;
}
-void encodingArrayInitialization(ElementEncoding *This) {
- Element *element = This->element;
- Set *set = getElementSet(element);
- ASSERT(set->isRange == false);
- uint size = set->members->getSize();
- uint encSize = getSizeEncodingArray(This, size);
- allocEncodingArrayElement(This, encSize);
- allocInUseArrayElement(This, encSize);
- for (uint i = 0; i < size; i++) {
- This->encodingArray[i] = set->members->get(i);
- setInUseElement(This, i);
- }
-}