#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++) {
+ naiveEncodingConstraint(getVectorBoolean(This->constraints, i));
}
}
-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;
}
-
- 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;
- }
+ case LOGICOP: {
+ naiveEncodingLogicOp((BooleanLogic *) This);
+ }
+ case PREDICATEOP: {
+ naiveEncodingPredicate((BooleanPredicate *) This);
+ return;
+ }
+ 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){
-
-}
-
-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);
- }
+ for(uint i=0; i < getSizeArrayElement(&This->inputs); i++) {
+ Element *element=getArrayElement(&This->inputs, i);
+ naiveEncodingElement(element);
+ }
}
-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
+void naiveEncodingElement(Element * This) {
+ ElementEncoding * encoding = getElementEncoding(This);
+ if (getElementEncodingType(encoding) == ELEM_UNASSIGNED) {
+ setElementEncodingType(encoding, BINARYINDEX);
+ baseBinaryIndexElementAssign(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 naiveEncodeEnumOperatingFunc(ElementFunction* This){
-
-}
\ No newline at end of file
+void baseBinaryIndexElementAssign(ElementEncoding *This) {
+ Element * element=This->element;
+ Set * set= getElementSet(element);
+ 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);
+ }
+}
projects / satune.git / blobdiff