VectorTableEntry* entries = &(((PredicateTable*)constraint->predicate)->table->entries);
FunctionEncodingType encType = constraint->encoding.type;
uint size = getSizeVectorTableEntry(entries);
+ bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
+
Edge constraints[size];
for(uint i=0; i<size; i++){
TableEntry* entry = getVectorTableEntry(entries, i);
- if(encType==ENUMERATEIMPLICATIONS && entry->output!= true)
- continue;
- else if(encType==ENUMERATEIMPLICATIONSNEGATE && entry->output !=false)
+
+ if(generateNegation == entry->output) {
+ //Skip the irrelevant entries
continue;
+ }
+
ArrayElement* inputs = &constraint->inputs;
uint inputNum =getSizeArrayElement(inputs);
Edge carray[inputNum];
Element* el = getArrayElement(inputs, j);
Edge tmpc = getElementValueConstraint(This, el, entry->inputs[j]);
if( GETELEMENTTYPE(el) == ELEMFUNCRETURN){
+ // HAMED : THIS IS COMPLETELY BROKEN....
Edge func =encodeFunctionElementSATEncoder(This, (ElementFunction*) el);
carray[j] = constraintAND2(This->cnf, func, tmpc);
} else {
constraints[i]=constraintAND(This->cnf, inputNum, carray);
}
Edge result=constraintOR(This->cnf, size, constraints);
- //FIXME: if it didn't match with any entry
- return encType==ENUMERATEIMPLICATIONS? result: constraintNegate(result);
+
+ return generationNegation ? result: constraintNegate(result);
}
Edge encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
Edge carray[size];
Element* elem1 = getArrayElement( &constraint->inputs, 0);
Edge elemc1 = E_NULL, elemc2 = E_NULL;
- if( GETELEMENTTYPE(elem1) == ELEMFUNCRETURN)
+ if( GETELEMENTTYPE(elem1) == ELEMFUNCRETURN) //HAMED: THIS IS PRETTY BROKEN...
elemc1 = encodeFunctionElementSATEncoder(This, (ElementFunction*) elem1);
Element* elem2 = getArrayElement( &constraint->inputs, 1);
- if( GETELEMENTTYPE(elem2) == ELEMFUNCRETURN)
+ if( GETELEMENTTYPE(elem2) == ELEMFUNCRETURN) //HAMED: THIS IS PRETTY BROKEN
elemc2 = encodeFunctionElementSATEncoder(This, (ElementFunction*) elem2);
for(uint i=0; i<size; i++){
Edge arg1 = getElementValueConstraint(This, elem1, commonElements[i]);