void encodeElementSATEncoder(SATEncoder* encoder, Element *This){
switch( GETELEMENTTYPE(This) ){
case ELEMFUNCRETURN:
- addConstraintCNF(encoder->cnf, encodeElementFunctionSATEncoder(encoder, (ElementFunction*) This));
+ encodeElementFunctionSATEncoder(encoder, (ElementFunction*) This);
break;
case ELEMSET:
return;
}
}
-Edge encodeElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction *This){
+void encodeElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction *This){
switch(GETFUNCTIONTYPE(This->function)){
case TABLEFUNC:
- return encodeTableElementFunctionSATEncoder(encoder, This);
+ encodeTableElementFunctionSATEncoder(encoder, This);
+ break;
case OPERATORFUNC:
- return encodeOperatorElementFunctionSATEncoder(encoder, This);
+ encodeOperatorElementFunctionSATEncoder(encoder, This);
+ break;
default:
ASSERT(0);
}
- return E_BOGUS;
}
-Edge encodeTableElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
+void encodeTableElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
switch(getElementFunctionEncoding(This)->type){
case ENUMERATEIMPLICATIONS:
- return encodeEnumTableElemFunctionSATEncoder(encoder, This);
+ encodeEnumTableElemFunctionSATEncoder(encoder, This);
break;
case CIRCUIT:
ASSERT(0);
default:
ASSERT(0);
}
- return E_BOGUS;
}
void encodeElementSATEncoder(SATEncoder* encoder, Element *This);
-Edge encodeElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction *This);
-Edge encodeTableElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This);
+void encodeElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction *This);
+void encodeTableElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This);
#endif
}
-Edge encodeOperatorElementFunctionSATEncoder(SATEncoder* This, ElementFunction* func) {
+void encodeOperatorElementFunctionSATEncoder(SATEncoder* This, ElementFunction* func) {
FunctionOperator * function = (FunctionOperator *) func->function;
uint numDomains=getSizeArrayElement(&func->inputs);
}
Edge cor=constraintOR(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
+ addConstraintCNF(This->cnf, cor);
deleteVectorEdge(clauses);
- return cor;
}
-Edge encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
+void encodeEnumTableElemFunctionSATEncoder(SATEncoder* This, ElementFunction* func){
//FIXME: HANDLE UNDEFINED BEHAVIORS
- ASSERT(GETFUNCTIONTYPE(This->function)==TABLEFUNC);
- ArrayElement* elements= &This->inputs;
- Table* table = ((FunctionTable*) (This->function))->table;
+ ASSERT(GETFUNCTIONTYPE(func->function)==TABLEFUNC);
+ ArrayElement* elements= &func->inputs;
+ Table* table = ((FunctionTable*) (func->function))->table;
uint size = getSizeVectorTableEntry(&table->entries);
Edge constraints[size]; //FIXME: should add a space for the case that didn't match any entries
for(uint i=0; i<size; i++) {
Edge carray[inputNum];
for(uint j=0; j<inputNum; j++){
Element* el= getArrayElement(elements, j);
- carray[j] = getElementValueConstraint(encoder, el, entry->inputs[j]);
+ carray[j] = getElementValueConstraint(This, el, entry->inputs[j]);
}
- Edge output = getElementValueConstraint(encoder, (Element*)This, entry->output);
- Edge row= constraintIMPLIES(encoder->cnf, constraintAND(encoder->cnf, inputNum, carray), output);
+ Edge output = getElementValueConstraint(This, (Element*)func, entry->output);
+ Edge row= constraintIMPLIES(This->cnf, constraintAND(This->cnf, inputNum, carray), output);
constraints[i]=row;
}
- return constraintOR(encoder->cnf, size, constraints);
+ addConstraintCNF(This->cnf, constraintOR(This->cnf, size, constraints));
}
Edge encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint);
Edge encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint);
Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint);
-Edge encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder,ElementFunction* This);
-Edge encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This);
+void encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder,ElementFunction* This);
+void encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This);
#endif