Fixing bugs + renaming ...

diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c
index 4b7d4474fed603db72fb2985febfeb7d645eac1f..d51e2519934f847901c9f41e75c1094d587fa577 100644 (file)
--- a/src/Backend/satencoder.c
+++ b/src/Backend/satencoder.c
@@ -356,8 +356,7 @@ Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate *
 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;
@@ -366,7 +365,7 @@ void encodeElementSATEncoder(SATEncoder* encoder, Element *This){
        }
 }
 
-Edge encodeFunctionElementSATEncoder(SATEncoder* encoder, ElementFunction *This){
+Edge encodeElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction *This){
        switch(GETFUNCTIONTYPE(This->function)){
                case TABLEFUNC:
                        return encodeTableElementFunctionSATEncoder(encoder, This);
@@ -465,12 +464,7 @@ Edge encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder, ElementFunctio
                        }
                }
        }
-       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){

diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index 22b1b2edd1002932e1af7a206027177034b9e6d6..dfcb8868dbbedb0ad3db22de4a1f4937f6fc194c 100644 (file)
--- a/src/Backend/satencoder.h
+++ b/src/Backend/satencoder.h
@@ -34,8 +34,8 @@ Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate *
 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);