Get rid of functions returning Edges
authorbdemsky <bdemsky@uci.edu>
Wed, 12 Jul 2017 00:32:41 +0000 (17:32 -0700)
committerbdemsky <bdemsky@uci.edu>
Wed, 12 Jul 2017 00:32:41 +0000 (17:32 -0700)
src/Backend/satencoder.c
src/Backend/satencoder.h
src/Backend/satfuncencoder.c
src/Backend/satfuncencoder.h

index b79dc0bda5ea09823575ba0e7977efa3223e5e4d..5b5d4aacf51d352f1d0f7fe789f0ca24c25e1b3a 100644 (file)
@@ -122,7 +122,7 @@ Edge encodeTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constr
 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;
@@ -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:
-                       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);
@@ -154,5 +155,4 @@ Edge encodeTableElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction*
                default:
                        ASSERT(0);
        }
-       return E_BOGUS;
 }
index 2b2298b3e47f27a97c4dde09bf8a6028465e0941..8241b939154a4393ffef3d0da80987c2843795c9 100644 (file)
@@ -29,7 +29,7 @@ Edge encodeTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constr
 
 
 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
index 03681657c34715eecce48cd076bccd2396c11cbe..801d4ffd7b925290e6d0c5e490ef1bef4f5c470c 100644 (file)
@@ -114,7 +114,7 @@ Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate *
 }
 
 
-Edge encodeOperatorElementFunctionSATEncoder(SATEncoder* This, ElementFunction* func) {
+void encodeOperatorElementFunctionSATEncoder(SATEncoder* This, ElementFunction* func) {
        FunctionOperator * function = (FunctionOperator *) func->function;
        uint numDomains=getSizeArrayElement(&func->inputs);
 
@@ -213,15 +213,15 @@ Edge encodeOperatorElementFunctionSATEncoder(SATEncoder* This, ElementFunction*
        }
 
        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++) {
@@ -230,11 +230,11 @@ Edge encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction*
                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));
 }
index 1246b0ec1556572054ceb887a82dc217ae655ac6..b24fc1f3c2b8889e71d2dcd46b0c7f8fcfc17254 100644 (file)
@@ -4,7 +4,7 @@
 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