From 983556fcda5fb32e24e9ed1e9963a0bd0c748bde Mon Sep 17 00:00:00 2001 From: bdemsky Date: Tue, 11 Jul 2017 16:13:39 -0700 Subject: [PATCH] Split functions into separate file --- src/Backend/satencoder.c | 229 --------------------------------- src/Backend/satencoder.h | 10 +- src/Backend/satfuncencoder.c | 240 +++++++++++++++++++++++++++++++++++ src/Backend/satfuncencoder.h | 10 ++ 4 files changed, 255 insertions(+), 234 deletions(-) create mode 100644 src/Backend/satfuncencoder.c create mode 100644 src/Backend/satfuncencoder.h diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c index 5809a59..b79dc0b 100644 --- a/src/Backend/satencoder.c +++ b/src/Backend/satencoder.c @@ -119,110 +119,6 @@ Edge encodeTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constr return E_BOGUS; } -Edge encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){ - VectorTableEntry* entries = &(((PredicateTable*)constraint->predicate)->table->entries); - FunctionEncodingType encType = constraint->encoding.type; - ArrayElement* inputs = &constraint->inputs; - uint inputNum =getSizeArrayElement(inputs); - //Encode all the inputs first ... - for(uint i=0; ioutput) { - //Skip the irrelevant entries - continue; - } - Edge carray[inputNum]; - for(uint j=0; jinputs[j]); - } - constraints[i]=constraintAND(This->cnf, inputNum, carray); - } - Edge result=constraintOR(This->cnf, size, constraints); - - return generateNegation ? result: constraintNegate(result); -} - -Edge encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) { - switch(constraint->encoding.type){ - case ENUMERATEIMPLICATIONS: - return encodeEnumOperatorPredicateSATEncoder(This, constraint); - case CIRCUIT: - ASSERT(0); - break; - default: - ASSERT(0); - } - return E_BOGUS; -} - -Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) { - PredicateOperator* predicate = (PredicateOperator*)constraint->predicate; - uint numDomains=getSizeArraySet(&predicate->domains); - - FunctionEncodingType encType = constraint->encoding.type; - bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE; - - /* Call base encoders for children */ - for(uint i=0;iinputs, i); - encodeElementSATEncoder(This, elem); - } - VectorEdge * clauses=allocDefVectorEdge(); // Setup array of clauses - - uint indices[numDomains]; //setup indices - bzero(indices, sizeof(uint)*numDomains); - - uint64_t vals[numDomains]; //setup value array - for(uint i=0;idomains, i); - vals[i]=getSetElement(set, indices[i]); - } - - bool notfinished=true; - while(notfinished) { - Edge carray[numDomains]; - - if (evalPredicateOperator(predicate, vals) ^ generateNegation) { - //Include this in the set of terms - for(uint i=0;iinputs, i); - carray[i] = getElementValueConstraint(This, elem, vals[i]); - } - pushVectorEdge(clauses, constraintAND(This->cnf, numDomains, carray)); - } - - notfinished=false; - for(uint i=0;idomains, i); - - if (index < getSetSize(set)) { - vals[i]=getSetElement(set, index); - notfinished=true; - break; - } else { - indices[i]=0; - vals[i]=getSetElement(set, 0); - } - } - } - - Edge cor=constraintOR(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses)); - deleteVectorEdge(clauses); - return generateNegation ? cor : constraintNegate(cor); -} - void encodeElementSATEncoder(SATEncoder* encoder, Element *This){ switch( GETELEMENTTYPE(This) ){ case ELEMFUNCRETURN: @@ -260,128 +156,3 @@ Edge encodeTableElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* } return E_BOGUS; } - -Edge encodeOperatorElementFunctionSATEncoder(SATEncoder* This, ElementFunction* func) { - FunctionOperator * function = (FunctionOperator *) func->function; - uint numDomains=getSizeArrayElement(&func->inputs); - - /* Call base encoders for children */ - for(uint i=0;iinputs, i); - encodeElementSATEncoder(This, elem); - } - - VectorEdge * clauses=allocDefVectorEdge(); // Setup array of clauses - - uint indices[numDomains]; //setup indices - bzero(indices, sizeof(uint)*numDomains); - - uint64_t vals[numDomains]; //setup value array - for(uint i=0;iinputs, i)); - vals[i]=getSetElement(set, indices[i]); - } - - Edge overFlowConstraint = ((BooleanVar*) func->overflowstatus)->var; - - bool notfinished=true; - while(notfinished) { - Edge carray[numDomains+2]; - - uint64_t result=applyFunctionOperator(function, numDomains, vals); - bool isInRange = isInRangeFunction((FunctionOperator*)func->function, result); - bool needClause = isInRange; - if (function->overflowbehavior == OVERFLOWSETSFLAG || function->overflowbehavior == FLAGIFFOVERFLOW) { - needClause=true; - } - - if (needClause) { - //Include this in the set of terms - for(uint i=0;iinputs, i); - carray[i] = getElementValueConstraint(This, elem, vals[i]); - } - if (isInRange) { - carray[numDomains] = getElementValueConstraint(This, &func->base, result); - } - - Edge clause; - switch(function->overflowbehavior) { - case IGNORE: - case NOOVERFLOW: - case WRAPAROUND: { - clause=constraintAND(This->cnf, numDomains+1, carray); - break; - } - case FLAGFORCESOVERFLOW: { - carray[numDomains+1]=constraintNegate(overFlowConstraint); - clause=constraintAND(This->cnf, numDomains+2, carray); - break; - } - case OVERFLOWSETSFLAG: { - if (isInRange) { - clause=constraintAND(This->cnf, numDomains+1, carray); - } else { - carray[numDomains+1]=overFlowConstraint; - clause=constraintAND(This->cnf, numDomains+1, carray); - } - break; - } - case FLAGIFFOVERFLOW: { - if (isInRange) { - carray[numDomains+1]=constraintNegate(overFlowConstraint); - clause=constraintAND(This->cnf, numDomains+2, carray); - } else { - carray[numDomains+1]=overFlowConstraint; - clause=constraintAND(This->cnf, numDomains+1, carray); - } - break; - } - default: - ASSERT(0); - } - pushVectorEdge(clauses, clause); - } - - notfinished=false; - for(uint i=0;iinputs, i)); - - if (index < getSetSize(set)) { - vals[i]=getSetElement(set, index); - notfinished=true; - break; - } else { - indices[i]=0; - vals[i]=getSetElement(set, 0); - } - } - } - - Edge cor=constraintOR(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses)); - deleteVectorEdge(clauses); - return cor; -} - -Edge encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){ - //FIXME: HANDLE UNDEFINED BEHAVIORS - ASSERT(GETFUNCTIONTYPE(This->function)==TABLEFUNC); - ArrayElement* elements= &This->inputs; - Table* table = ((FunctionTable*) (This->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; ientries, i); - uint inputNum = getSizeArrayElement(elements); - Edge carray[inputNum]; - for(uint j=0; jinputs[j]); - } - Edge output = getElementValueConstraint(encoder, (Element*)This, entry->output); - Edge row= constraintIMPLIES(encoder->cnf, constraintAND(encoder->cnf, inputNum, carray), output); - constraints[i]=row; - } - return constraintOR(encoder->cnf, size, constraints); -} diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h index 1f059b7..2b2298b 100644 --- a/src/Backend/satencoder.h +++ b/src/Backend/satencoder.h @@ -13,6 +13,7 @@ struct SATEncoder { #include "satelemencoder.h" #include "satorderencoder.h" +#include "satfuncencoder.h" SATEncoder * allocSATEncoder(); void deleteSATEncoder(SATEncoder *This); @@ -24,12 +25,11 @@ Edge encodeVarSATEncoder(SATEncoder *This, BooleanVar * constraint); Edge encodeLogicSATEncoder(SATEncoder *This, BooleanLogic * constraint); Edge encodePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint); Edge encodeTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint); -Edge encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint); -Edge encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint); -Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint); + + + 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); + #endif diff --git a/src/Backend/satfuncencoder.c b/src/Backend/satfuncencoder.c new file mode 100644 index 0000000..0368165 --- /dev/null +++ b/src/Backend/satfuncencoder.c @@ -0,0 +1,240 @@ +#include "satencoder.h" +#include "common.h" +#include "function.h" +#include "ops.h" +#include "predicate.h" +#include "boolean.h" +#include "table.h" +#include "tableentry.h" +#include "set.h" +#include "element.h" + +Edge encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){ + VectorTableEntry* entries = &(((PredicateTable*)constraint->predicate)->table->entries); + FunctionEncodingType encType = constraint->encoding.type; + ArrayElement* inputs = &constraint->inputs; + uint inputNum =getSizeArrayElement(inputs); + //Encode all the inputs first ... + for(uint i=0; ioutput) { + //Skip the irrelevant entries + continue; + } + Edge carray[inputNum]; + for(uint j=0; jinputs[j]); + } + constraints[i]=constraintAND(This->cnf, inputNum, carray); + } + Edge result=constraintOR(This->cnf, size, constraints); + + return generateNegation ? result: constraintNegate(result); +} + +Edge encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) { + switch(constraint->encoding.type){ + case ENUMERATEIMPLICATIONS: + return encodeEnumOperatorPredicateSATEncoder(This, constraint); + case CIRCUIT: + ASSERT(0); + break; + default: + ASSERT(0); + } + return E_BOGUS; +} + +Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) { + PredicateOperator* predicate = (PredicateOperator*)constraint->predicate; + uint numDomains=getSizeArraySet(&predicate->domains); + + FunctionEncodingType encType = constraint->encoding.type; + bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE; + + /* Call base encoders for children */ + for(uint i=0;iinputs, i); + encodeElementSATEncoder(This, elem); + } + VectorEdge * clauses=allocDefVectorEdge(); // Setup array of clauses + + uint indices[numDomains]; //setup indices + bzero(indices, sizeof(uint)*numDomains); + + uint64_t vals[numDomains]; //setup value array + for(uint i=0;idomains, i); + vals[i]=getSetElement(set, indices[i]); + } + + bool notfinished=true; + while(notfinished) { + Edge carray[numDomains]; + + if (evalPredicateOperator(predicate, vals) ^ generateNegation) { + //Include this in the set of terms + for(uint i=0;iinputs, i); + carray[i] = getElementValueConstraint(This, elem, vals[i]); + } + pushVectorEdge(clauses, constraintAND(This->cnf, numDomains, carray)); + } + + notfinished=false; + for(uint i=0;idomains, i); + + if (index < getSetSize(set)) { + vals[i]=getSetElement(set, index); + notfinished=true; + break; + } else { + indices[i]=0; + vals[i]=getSetElement(set, 0); + } + } + } + + Edge cor=constraintOR(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses)); + deleteVectorEdge(clauses); + return generateNegation ? cor : constraintNegate(cor); +} + + +Edge encodeOperatorElementFunctionSATEncoder(SATEncoder* This, ElementFunction* func) { + FunctionOperator * function = (FunctionOperator *) func->function; + uint numDomains=getSizeArrayElement(&func->inputs); + + /* Call base encoders for children */ + for(uint i=0;iinputs, i); + encodeElementSATEncoder(This, elem); + } + + VectorEdge * clauses=allocDefVectorEdge(); // Setup array of clauses + + uint indices[numDomains]; //setup indices + bzero(indices, sizeof(uint)*numDomains); + + uint64_t vals[numDomains]; //setup value array + for(uint i=0;iinputs, i)); + vals[i]=getSetElement(set, indices[i]); + } + + Edge overFlowConstraint = ((BooleanVar*) func->overflowstatus)->var; + + bool notfinished=true; + while(notfinished) { + Edge carray[numDomains+2]; + + uint64_t result=applyFunctionOperator(function, numDomains, vals); + bool isInRange = isInRangeFunction((FunctionOperator*)func->function, result); + bool needClause = isInRange; + if (function->overflowbehavior == OVERFLOWSETSFLAG || function->overflowbehavior == FLAGIFFOVERFLOW) { + needClause=true; + } + + if (needClause) { + //Include this in the set of terms + for(uint i=0;iinputs, i); + carray[i] = getElementValueConstraint(This, elem, vals[i]); + } + if (isInRange) { + carray[numDomains] = getElementValueConstraint(This, &func->base, result); + } + + Edge clause; + switch(function->overflowbehavior) { + case IGNORE: + case NOOVERFLOW: + case WRAPAROUND: { + clause=constraintAND(This->cnf, numDomains+1, carray); + break; + } + case FLAGFORCESOVERFLOW: { + carray[numDomains+1]=constraintNegate(overFlowConstraint); + clause=constraintAND(This->cnf, numDomains+2, carray); + break; + } + case OVERFLOWSETSFLAG: { + if (isInRange) { + clause=constraintAND(This->cnf, numDomains+1, carray); + } else { + carray[numDomains+1]=overFlowConstraint; + clause=constraintAND(This->cnf, numDomains+1, carray); + } + break; + } + case FLAGIFFOVERFLOW: { + if (isInRange) { + carray[numDomains+1]=constraintNegate(overFlowConstraint); + clause=constraintAND(This->cnf, numDomains+2, carray); + } else { + carray[numDomains+1]=overFlowConstraint; + clause=constraintAND(This->cnf, numDomains+1, carray); + } + break; + } + default: + ASSERT(0); + } + pushVectorEdge(clauses, clause); + } + + notfinished=false; + for(uint i=0;iinputs, i)); + + if (index < getSetSize(set)) { + vals[i]=getSetElement(set, index); + notfinished=true; + break; + } else { + indices[i]=0; + vals[i]=getSetElement(set, 0); + } + } + } + + Edge cor=constraintOR(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses)); + deleteVectorEdge(clauses); + return cor; +} + +Edge encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){ + //FIXME: HANDLE UNDEFINED BEHAVIORS + ASSERT(GETFUNCTIONTYPE(This->function)==TABLEFUNC); + ArrayElement* elements= &This->inputs; + Table* table = ((FunctionTable*) (This->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; ientries, i); + uint inputNum = getSizeArrayElement(elements); + Edge carray[inputNum]; + for(uint j=0; jinputs[j]); + } + Edge output = getElementValueConstraint(encoder, (Element*)This, entry->output); + Edge row= constraintIMPLIES(encoder->cnf, constraintAND(encoder->cnf, inputNum, carray), output); + constraints[i]=row; + } + return constraintOR(encoder->cnf, size, constraints); +} diff --git a/src/Backend/satfuncencoder.h b/src/Backend/satfuncencoder.h new file mode 100644 index 0000000..1246b0e --- /dev/null +++ b/src/Backend/satfuncencoder.h @@ -0,0 +1,10 @@ +#ifndef SATFUNCENCODER_H +#define SATFUNCENCODER_H + +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); + +#endif -- 2.34.1