#include "csolver.h"
#include "boolean.h"
#include "table.h"
+#include "tableentry.h"
+#include "order.h"
#include <strings.h>
-void assignEncoding(CSolver* csolver){
- uint size = getSizeVectorElement(csolver->allElements);
- for(uint i=0; i<size; i++){
- Element* element = getVectorElement(csolver->allElements, i);
- switch(GETELEMENTTYPE(element)){
- case ELEMSET:
- setElementEncodingType(&((ElementSet*)element)->encoding, BINARYINDEX);
- baseBinaryIndexElementAssign(&((ElementSet*)element)->encoding);
- break;
- case ELEMFUNCRETURN:
- setFunctionEncodingType(&((ElementFunction*)element)->functionencoding, ENUMERATEIMPLICATIONS);
- break;
- default:
- ASSERT(0);
- }
- }
-
- size = getSizeVectorBoolean(csolver->allBooleans);
- for(uint i=0; i<size; i++){
- Boolean* predicate = getVectorBoolean(csolver->allBooleans, i);
- switch(GETBOOLEANTYPE(predicate)){
- case PREDICATEOP:
- setFunctionEncodingType(&((BooleanPredicate*)predicate)->encoding, ENUMERATEIMPLICATIONS);
- break;
- default:
- continue;
- }
+void naiveEncodingDecision(CSolver *This) {
+ for (uint i = 0; i < getSizeVectorBoolean(This->constraints); i++) {
+ Boolean *boolean = getVectorBoolean(This->constraints, i);
+ naiveEncodingConstraint(boolean);
}
}
-void baseBinaryIndexElementAssign(ElementEncoding *This) {
- Element * element=This->element;
- ASSERT(element->type == ELEMSET);
- Set * set= ((ElementSet*)element)->set;
- ASSERT(set->isRange==false);
- uint size=getSizeVectorInt(set->members);
- uint encSize=NEXTPOW2(size);
- allocEncodingArrayElement(This, encSize);
- allocInUseArrayElement(This, encSize);
-
- for(uint i=0;i<size;i++) {
- This->encodingArray[i]=getVectorInt(set->members, i);
- setInUseElement(This, i);
+void naiveEncodingConstraint(Boolean *This) {
+ switch (GETBOOLEANTYPE(This)) {
+ case BOOLEANVAR: {
+ return;
}
-}
-
-
-void encode(CSolver* csolver){
- uint size = getSizeVectorElement(csolver->allElements);
- for(uint i=0; i<size; i++){
- Element* element = getVectorElement(csolver->allElements, i);
- switch(GETELEMENTTYPE(element)){
- case ELEMFUNCRETURN:
- naiveEncodeFunctionPredicate(&((ElementFunction*)element)->functionencoding);
- break;
- default:
- continue;
- }
+ case ORDERCONST: {
+ setOrderEncodingType( ((BooleanOrder *)This)->order, PAIRWISE );
+ return;
+ }
+ case LOGICOP: {
+ naiveEncodingLogicOp((BooleanLogic *) This);
+ return;
+ }
+ case PREDICATEOP: {
+ naiveEncodingPredicate((BooleanPredicate *) This);
+ return;
}
-
- size = getSizeVectorBoolean(csolver->allBooleans);
- for(uint i=0; i<size; i++){
- Boolean* predicate = getVectorBoolean(csolver->allBooleans, i);
- switch(GETBOOLEANTYPE(predicate)){
- case PREDICATEOP:
- naiveEncodeFunctionPredicate(&((BooleanPredicate*)predicate)->encoding);
- break;
- default:
- continue;
- }
+ default:
+ ASSERT(0);
}
}
-void naiveEncodeFunctionPredicate(FunctionEncoding *This){
- if(This->isFunction) {
- ASSERT(GETELEMENTTYPE(This->op.function)==ELEMFUNCRETURN);
- switch(This->type){
- case ENUMERATEIMPLICATIONS:
- naiveEncodeEnumeratedFunction(This);
- break;
- case CIRCUIT:
- naiveEncodeCircuitFunction(This);
- break;
- default:
- ASSERT(0);
- }
- }else {
- ASSERT(GETBOOLEANTYPE(This->op.predicate) == PREDICATEOP);
- BooleanPredicate* predicate = (BooleanPredicate*)This->op.predicate;
- //FIXME
-
+void naiveEncodingLogicOp(BooleanLogic *This) {
+ for (uint i = 0; i < getSizeArrayBoolean(&This->inputs); i++) {
+ naiveEncodingConstraint(getArrayBoolean(&This->inputs, i));
}
}
+void naiveEncodingPredicate(BooleanPredicate *This) {
+ FunctionEncoding *encoding = getPredicateFunctionEncoding(This);
+ if (getFunctionEncodingType(encoding) == FUNC_UNASSIGNED)
+ setFunctionEncodingType(getPredicateFunctionEncoding(This), ENUMERATEIMPLICATIONS);
-void naiveEncodeCircuitFunction(FunctionEncoding* This){
-
+ for (uint i = 0; i < getSizeArrayElement(&This->inputs); i++) {
+ Element *element = getArrayElement(&This->inputs, i);
+ naiveEncodingElement(element);
+ }
}
-void naiveEncodeEnumeratedFunction(FunctionEncoding* This){
- ElementFunction* ef =(ElementFunction*)This->op.function;
- Function * function = ef->function;
- switch(GETFUNCTIONTYPE(function)){
- case TABLEFUNC:
- naiveEncodeEnumTableFunc(ef);
- break;
- case OPERATORFUNC:
- naiveEncodeEnumOperatingFunc(ef);
- break;
- default:
- ASSERT(0);
- }
+void naiveEncodingElement(Element *This) {
+ ElementEncoding *encoding = getElementEncoding(This);
+ if (getElementEncodingType(encoding) == ELEM_UNASSIGNED) {
+ setElementEncodingType(encoding, BINARYINDEX);
+ encodingArrayInitialization(encoding);
+ }
+
+ if (GETELEMENTTYPE(This) == ELEMFUNCRETURN) {
+ ElementFunction *function = (ElementFunction *) This;
+ for (uint i = 0; i < getSizeArrayElement(&function->inputs); i++) {
+ Element *element = getArrayElement(&function->inputs, i);
+ naiveEncodingElement(element);
+ }
+ FunctionEncoding *encoding = getElementFunctionEncoding(function);
+ if (getFunctionEncodingType(encoding) == FUNC_UNASSIGNED)
+ setFunctionEncodingType(getElementFunctionEncoding(function), ENUMERATEIMPLICATIONS);
+ }
}
-void naiveEncodeEnumTableFunc(ElementFunction* This){
- ASSERT(GETFUNCTIONTYPE(This->function)==TABLEFUNC);
- ArrayElement* elements= &This->inputs;
- Table* table = ((FunctionTable*) (This->function))->table;
- uint size = getSizeVectorTableEntry(&table->entries);
- for(uint i=0; i<size; i++){
- TableEntry* entry = getVectorTableEntry(&table->entries, i);
- //FIXME: generate Constraints
+uint getSizeEncodingArray(ElementEncoding *This, uint setSize) {
+ switch (This->type) {
+ case BINARYINDEX:
+ return NEXTPOW2(setSize);
+ case ONEHOT:
+ case UNARY:
+ return setSize;
+ default:
+ ASSERT(0);
}
-
+ return -1;
}
-void naiveEncodeEnumOperatingFunc(ElementFunction* This){
-
-}
\ No newline at end of file
+void encodingArrayInitialization(ElementEncoding *This) {
+ Element *element = This->element;
+ Set *set = getElementSet(element);
+ ASSERT(set->isRange == false);
+ uint size = getSizeVectorInt(set->members);
+ uint encSize = getSizeEncodingArray(This, size);
+ allocEncodingArrayElement(This, encSize);
+ allocInUseArrayElement(This, encSize);
+ for (uint i = 0; i < size; i++) {
+ This->encodingArray[i] = getVectorInt(set->members, i);
+ setInUseElement(This, i);
+ }
+}