void encodeElementSATEncoder(SATEncoder* encoder, Element *This){
switch( GETELEMENTTYPE(This) ){
case ELEMFUNCRETURN:
- Edge c = encodeFunctionElementSATEncoder(This, (ElementFunction*) This);
- addConstraint(encoder->cnf, c);
+ addConstraintCNF(encoder->cnf, encodeElementFunctionSATEncoder(encoder, (ElementFunction*) This));
break;
case ELEMSET:
return;
}
}
-Edge encodeFunctionElementSATEncoder(SATEncoder* encoder, ElementFunction *This){
+Edge encodeElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction *This){
switch(GETFUNCTIONTYPE(This->function)){
case TABLEFUNC:
return encodeTableElementFunctionSATEncoder(encoder, This);
}
}
}
- Edge result = constraintAND(encoder->cnf, size, carray);
- if (!edgeIsNull(elemc1))
- result = constraintAND2(encoder->cnf, result, elemc1);
- if (!edgeIsNull(elemc2))
- result = constraintAND2(encoder->cnf, result, elemc2);
- return result;
+ return constraintAND(encoder->cnf, size, carray);
}
Edge encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
Edge getElementValueBinaryIndexConstraint(SATEncoder * This, Element* element, uint64_t value);
Edge getElementValueConstraint(SATEncoder* encoder, Element* This, uint64_t value);
-Edge encodeElementSATEncoder(SATEncoder* encoder, Element *This);
-Edge encodeFunctionElementSATEncoder(SATEncoder* encoder, ElementFunction *This);
+void encodeElementSATEncoder(SATEncoder* encoder, Element *This);
+Edge encodeElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction *This);
Edge encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This);
Edge encodeTableElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This);
Edge encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder,ElementFunction* This);