Get rid of functions returning Edges

[satune.git] / src / Backend / satencoder.c

diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c
index b79dc0bda5ea09823575ba0e7977efa3223e5e4d..5b5d4aacf51d352f1d0f7fe789f0ca24c25e1b3a 100644 (file)
--- a/src/Backend/satencoder.c
+++ b/src/Backend/satencoder.c
@@ -122,7 +122,7 @@ Edge encodeTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constr
 void encodeElementSATEncoder(SATEncoder* encoder, Element *This){
        switch( GETELEMENTTYPE(This) ){
                case ELEMFUNCRETURN:
 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;
                        break;
                case ELEMSET:
                        return;


@@ -131,22 +131,23 @@ void encodeElementSATEncoder(SATEncoder* encoder, Element *This){
        }
 }
 
        }
 }
 

-Edge encodeElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction *This){
+void encodeElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction *This){

        switch(GETFUNCTIONTYPE(This->function)){
                case TABLEFUNC:
        switch(GETFUNCTIONTYPE(This->function)){
                case TABLEFUNC:

-                       return encodeTableElementFunctionSATEncoder(encoder, This);
+                       encodeTableElementFunctionSATEncoder(encoder, This);
+                       break;

                case OPERATORFUNC:
                case OPERATORFUNC:

-                       return encodeOperatorElementFunctionSATEncoder(encoder, This);
+                       encodeOperatorElementFunctionSATEncoder(encoder, This);
+                       break;

                default:
                        ASSERT(0);
        }
                default:
                        ASSERT(0);
        }

-       return E_BOGUS;

 }
 
 }
 

-Edge encodeTableElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
+void encodeTableElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){

        switch(getElementFunctionEncoding(This)->type){
                case ENUMERATEIMPLICATIONS:
        switch(getElementFunctionEncoding(This)->type){
                case ENUMERATEIMPLICATIONS:

-                       return encodeEnumTableElemFunctionSATEncoder(encoder, This);
+                       encodeEnumTableElemFunctionSATEncoder(encoder, This);

                        break;
                case CIRCUIT:
                        ASSERT(0);
                        break;
                case CIRCUIT:
                        ASSERT(0);


@@ -154,5 +155,4 @@ Edge encodeTableElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction*
                default:
                        ASSERT(0);
        }
                default:
                        ASSERT(0);
        }

-       return E_BOGUS;

 }
 }