From 0b5f6592c4a16e9dc6103bc6035bc7b4dc81ec68 Mon Sep 17 00:00:00 2001 From: bdemsky Date: Tue, 11 Jul 2017 17:32:41 -0700 Subject: [PATCH] Get rid of functions returning Edges --- src/Backend/satencoder.c | 16 ++++++++-------- src/Backend/satencoder.h | 4 ++-- src/Backend/satfuncencoder.c | 20 ++++++++++---------- src/Backend/satfuncencoder.h | 4 ++-- 4 files changed, 22 insertions(+), 22 deletions(-) diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c index b79dc0b..5b5d4aa 100644 --- 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: - 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; } diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h index 2b2298b..8241b93 100644 --- a/src/Backend/satencoder.h +++ b/src/Backend/satencoder.h @@ -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 diff --git a/src/Backend/satfuncencoder.c b/src/Backend/satfuncencoder.c index 0368165..801d4ff 100644 --- a/src/Backend/satfuncencoder.c +++ b/src/Backend/satfuncencoder.c @@ -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; iinputs[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)); } diff --git a/src/Backend/satfuncencoder.h b/src/Backend/satfuncencoder.h index 1246b0e..b24fc1f 100644 --- a/src/Backend/satfuncencoder.h +++ b/src/Backend/satfuncencoder.h @@ -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 -- 2.34.1