From 77683dd2de7fd732d855c5d190a46c26ba5e5db4 Mon Sep 17 00:00:00 2001 From: Hamed Date: Wed, 19 Jul 2017 19:19:26 -0700 Subject: [PATCH] breaking functionencoding to different files --- src/Backend/satencoder.c | 1 + src/Backend/satencoder.h | 2 +- .../{satfuncencoder.c => satfuncopencoder.c} | 232 ++---------------- .../{satfuncencoder.h => satfuncopencoder.h} | 8 +- src/Backend/satfunctableencoder.c | 194 +++++++++++++++ src/Backend/satfunctableencoder.h | 9 + 6 files changed, 232 insertions(+), 214 deletions(-) rename src/Backend/{satfuncencoder.c => satfuncopencoder.c} (52%) rename src/Backend/{satfuncencoder.h => satfuncopencoder.h} (51%) create mode 100644 src/Backend/satfunctableencoder.c create mode 100644 src/Backend/satfunctableencoder.h diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c index 6148074..885aab8 100644 --- a/src/Backend/satencoder.c +++ b/src/Backend/satencoder.c @@ -11,6 +11,7 @@ #include "order.h" #include "predicate.h" #include "set.h" +#include "satfuncopencoder.h" //TODO: Should handle sharing of AST Nodes without recoding them a second time diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h index 8241b93..aceb271 100644 --- a/src/Backend/satencoder.h +++ b/src/Backend/satencoder.h @@ -13,7 +13,7 @@ struct SATEncoder { #include "satelemencoder.h" #include "satorderencoder.h" -#include "satfuncencoder.h" +#include "satfunctableencoder.h" SATEncoder * allocSATEncoder(); void deleteSATEncoder(SATEncoder *This); diff --git a/src/Backend/satfuncencoder.c b/src/Backend/satfuncopencoder.c similarity index 52% rename from src/Backend/satfuncencoder.c rename to src/Backend/satfuncopencoder.c index 683336f..67441d5 100644 --- a/src/Backend/satfuncencoder.c +++ b/src/Backend/satfuncopencoder.c @@ -9,42 +9,7 @@ #include "set.h" #include "element.h" #include "common.h" - -Edge encodeEnumEntriesTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){ - Table* table = ((PredicateTable*)constraint->predicate)->table; - FunctionEncodingType encType = constraint->encoding.type; - ArrayElement* inputs = &constraint->inputs; - uint inputNum =getSizeArrayElement(inputs); - //Encode all the inputs first ... - for(uint i=0; ientrie); - bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE; - Edge constraints[size]; - HSIteratorTableEntry* iterator = iteratorTableEntry(table->entrie); - uint i=0; - while(hasNextTableEntry(iterator)){ - TableEntry* entry = nextTableEntry(iterator); - if(generateNegation == entry->output) { - //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 ? constraintNegate(result) : result; -} -Edge encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){ - //FIXME - return E_NULL; -} +#include "satfuncopencoder.h" Edge encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) { switch(constraint->encoding.type){ @@ -58,35 +23,6 @@ Edge encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * con exit(-1); } -Edge encodeCircuitOperatorPredicateEncoder(SATEncoder *This, BooleanPredicate * constraint) { - PredicateOperator * predicate = (PredicateOperator*) constraint->predicate; - - switch(predicate->op) { - case EQUALS: { - return encodeCircuitEquals(This, constraint); - } - default: - ASSERT(0); - } - exit(-1); -} - -Edge encodeCircuitEquals(SATEncoder * This, BooleanPredicate * constraint) { - PredicateOperator * predicate = (PredicateOperator*) constraint->predicate; - ASSERT(getSizeArraySet(&predicate->domains) == 2); - Element *elem0 = getArrayElement( &constraint->inputs, 0); - Element *elem1 = getArrayElement( &constraint->inputs, 1); - ElementEncoding *ee0=getElementEncoding(elem0); - ElementEncoding *ee1=getElementEncoding(elem1); - ASSERT(ee0->numVars==ee1->numVars); - uint numVars=ee0->numVars; - Edge carray[numVars]; - for (uint i=0; icnf, ee0->variables[i], ee1->variables[i]); - } - return constraintAND(This->cnf, numVars, carray); -} - Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) { PredicateOperator* predicate = (PredicateOperator*)constraint->predicate; uint numDomains=getSizeArraySet(&predicate->domains); @@ -254,149 +190,31 @@ void encodeOperatorElementFunctionSATEncoder(SATEncoder* This, ElementFunction* deleteVectorEdge(clauses); } -void encodeEnumEntriesTableElemFuncSATEncoder(SATEncoder* This, ElementFunction* func){ - UndefinedBehavior undefStatus = ((FunctionTable*) func->function)->undefBehavior; - ASSERT(undefStatus == IGNOREBEHAVIOR || undefStatus == FLAGFORCEUNDEFINED); - ArrayElement* elements= &func->inputs; - Table* table = ((FunctionTable*) (func->function))->table; - uint size = getSizeHashSetTableEntry(table->entrie); - Edge constraints[size]; - HSIteratorTableEntry* iterator = iteratorTableEntry(table->entrie); - uint i=0; - while(hasNextTableEntry(iterator)) { - TableEntry* entry = nextTableEntry(iterator); - ASSERT(entry!=NULL); - uint inputNum = getSizeArrayElement(elements); - Edge carray[inputNum]; - for(uint j=0; jinputs[j]); - } - Edge output = getElementValueConstraint(This, (Element*)func, entry->output); - Edge row; - switch(undefStatus ){ - case IGNOREBEHAVIOR: { - row=constraintIMPLIES(This->cnf,constraintAND(This->cnf, inputNum, carray), output); - break; - } - case FLAGFORCEUNDEFINED: { - Edge undefConst = ((BooleanVar*)func->overflowstatus)->var; - row=constraintIMPLIES(This->cnf,constraintAND(This->cnf, inputNum, carray), constraintAND2(This->cnf, output, constraintNegate(undefConst))); - break; - } - default: - ASSERT(0); - - } - constraints[i++]=row; - } - deleteIterTableEntry(iterator); - addConstraintCNF(This->cnf, constraintAND(This->cnf, size, constraints)); -} - -void encodeEnumTableElemFunctionSATEncoder(SATEncoder* This, ElementFunction* elemFunc){ -#ifdef TRACE_DEBUG - model_print("Enumeration Table functions ...\n"); -#endif - ASSERT(GETFUNCTIONTYPE(elemFunc->function)==TABLEFUNC); - //First encode children - ArrayElement* elements= &elemFunc->inputs; - for(uint i=0; iundefBehavior){ - case IGNOREBEHAVIOR: - case FLAGFORCEUNDEFINED: - return encodeEnumEntriesTableElemFuncSATEncoder(This, elemFunc); - default: - break; - } - - uint numDomains=getSizeArraySet(&function->table->domains); - - VectorEdge * clauses=allocDefVectorEdge(); // Setup array of clauses - - uint indices[numDomains]; //setup indices - bzero(indices, sizeof(uint)*numDomains); +Edge encodeCircuitOperatorPredicateEncoder(SATEncoder *This, BooleanPredicate * constraint) { + PredicateOperator * predicate = (PredicateOperator*) constraint->predicate; - uint64_t vals[numDomains]; //setup value array - for(uint i=0;itable->domains, i); - vals[i]=getSetElement(set, indices[i]); + switch(predicate->op) { + case EQUALS: { + return encodeCircuitEquals(This, constraint); } - - Edge undefConstraint = ((BooleanVar*) elemFunc->overflowstatus)->var; - - bool notfinished=true; - while(notfinished) { - Edge carray[numDomains+1]; - TableEntry* tableEntry = getTableEntryFromTable(function->table, vals, numDomains); - bool isInRange = tableEntry!=NULL; - bool needClause = isInRange; - if (function->undefBehavior == UNDEFINEDSETSFLAG || function->undefBehavior == FLAGIFFUNDEFINED) { - 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, (Element*)elemFunc, tableEntry->output); - } - - Edge clause; - switch(function->undefBehavior) { - case UNDEFINEDSETSFLAG: { - if (isInRange) { - clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]); - } else { - clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint); - } - break; - } - case FLAGIFFUNDEFINED: { - if (isInRange) { - clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintAND2(This->cnf, carray[numDomains], constraintNegate(undefConstraint))); - } else { - clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint); - } - break; - } - default: - ASSERT(0); - } -#ifdef TRACE_DEBUG - model_print("added clause in table enumeration ...\n"); - printCNF(clause); - model_print("\n"); -#endif - pushVectorEdge(clauses, clause); - } - - notfinished=false; - for(uint i=0;itable->domains, i); - - if (index < getSetSize(set)) { - vals[i]=getSetElement(set, index); - notfinished=true; - break; - } else { - indices[i]=0; - vals[i]=getSetElement(set, 0); - } - } + default: + ASSERT(0); } - - Edge cor=constraintAND(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses)); - addConstraintCNF(This->cnf, cor); - deleteVectorEdge(clauses); - + exit(-1); } + +Edge encodeCircuitEquals(SATEncoder * This, BooleanPredicate * constraint) { + PredicateOperator * predicate = (PredicateOperator*) constraint->predicate; + ASSERT(getSizeArraySet(&predicate->domains) == 2); + Element *elem0 = getArrayElement( &constraint->inputs, 0); + Element *elem1 = getArrayElement( &constraint->inputs, 1); + ElementEncoding *ee0=getElementEncoding(elem0); + ElementEncoding *ee1=getElementEncoding(elem1); + ASSERT(ee0->numVars==ee1->numVars); + uint numVars=ee0->numVars; + Edge carray[numVars]; + for (uint i=0; icnf, ee0->variables[i], ee1->variables[i]); + } + return constraintAND(This->cnf, numVars, carray); +} \ No newline at end of file diff --git a/src/Backend/satfuncencoder.h b/src/Backend/satfuncopencoder.h similarity index 51% rename from src/Backend/satfuncencoder.h rename to src/Backend/satfuncopencoder.h index 8b8a9a2..0bfca3d 100644 --- a/src/Backend/satfuncencoder.h +++ b/src/Backend/satfuncopencoder.h @@ -1,13 +1,9 @@ -#ifndef SATFUNCENCODER_H -#define SATFUNCENCODER_H +#ifndef SATFUNCOPENCODER_H +#define SATFUNCOPENCODER_H -Edge encodeEnumEntriesTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint); -Edge encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint); Edge encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint); Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint); void encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder,ElementFunction* This); -void encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This); -void encodeEnumEntriesTableElemFuncSATEncoder(SATEncoder* encoder, ElementFunction* This); Edge encodeCircuitOperatorPredicateEncoder(SATEncoder *This, BooleanPredicate * constraint); Edge encodeCircuitEquals(SATEncoder * This, BooleanPredicate * constraint); diff --git a/src/Backend/satfunctableencoder.c b/src/Backend/satfunctableencoder.c new file mode 100644 index 0000000..8ed9a2c --- /dev/null +++ b/src/Backend/satfunctableencoder.c @@ -0,0 +1,194 @@ +#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" +#include "common.h" + +Edge encodeEnumEntriesTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){ + Table* table = ((PredicateTable*)constraint->predicate)->table; + FunctionEncodingType encType = constraint->encoding.type; + ArrayElement* inputs = &constraint->inputs; + uint inputNum =getSizeArrayElement(inputs); + //Encode all the inputs first ... + for(uint i=0; ientrie); + bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE; + Edge constraints[size]; + HSIteratorTableEntry* iterator = iteratorTableEntry(table->entrie); + uint i=0; + while(hasNextTableEntry(iterator)){ + TableEntry* entry = nextTableEntry(iterator); + if(generateNegation == entry->output) { + //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 ? constraintNegate(result) : result; +} +Edge encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){ + //FIXME + return E_NULL; +} + +void encodeEnumEntriesTableElemFuncSATEncoder(SATEncoder* This, ElementFunction* func){ + UndefinedBehavior undefStatus = ((FunctionTable*) func->function)->undefBehavior; + ASSERT(undefStatus == IGNOREBEHAVIOR || undefStatus == FLAGFORCEUNDEFINED); + ArrayElement* elements= &func->inputs; + Table* table = ((FunctionTable*) (func->function))->table; + uint size = getSizeHashSetTableEntry(table->entrie); + Edge constraints[size]; + HSIteratorTableEntry* iterator = iteratorTableEntry(table->entrie); + uint i=0; + while(hasNextTableEntry(iterator)) { + TableEntry* entry = nextTableEntry(iterator); + ASSERT(entry!=NULL); + uint inputNum = getSizeArrayElement(elements); + Edge carray[inputNum]; + for(uint j=0; jinputs[j]); + } + Edge output = getElementValueConstraint(This, (Element*)func, entry->output); + Edge row; + switch(undefStatus ){ + case IGNOREBEHAVIOR: { + row=constraintIMPLIES(This->cnf,constraintAND(This->cnf, inputNum, carray), output); + break; + } + case FLAGFORCEUNDEFINED: { + Edge undefConst = ((BooleanVar*)func->overflowstatus)->var; + row=constraintIMPLIES(This->cnf,constraintAND(This->cnf, inputNum, carray), constraintAND2(This->cnf, output, constraintNegate(undefConst))); + break; + } + default: + ASSERT(0); + + } + constraints[i++]=row; + } + deleteIterTableEntry(iterator); + addConstraintCNF(This->cnf, constraintAND(This->cnf, size, constraints)); +} + +void encodeEnumTableElemFunctionSATEncoder(SATEncoder* This, ElementFunction* elemFunc){ +#ifdef TRACE_DEBUG + model_print("Enumeration Table functions ...\n"); +#endif + ASSERT(GETFUNCTIONTYPE(elemFunc->function)==TABLEFUNC); + //First encode children + ArrayElement* elements= &elemFunc->inputs; + for(uint i=0; iundefBehavior){ + case IGNOREBEHAVIOR: + case FLAGFORCEUNDEFINED: + return encodeEnumEntriesTableElemFuncSATEncoder(This, elemFunc); + default: + break; + } + + uint numDomains=getSizeArraySet(&function->table->domains); + + 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;itable->domains, i); + vals[i]=getSetElement(set, indices[i]); + } + + Edge undefConstraint = ((BooleanVar*) elemFunc->overflowstatus)->var; + + bool notfinished=true; + while(notfinished) { + Edge carray[numDomains+1]; + TableEntry* tableEntry = getTableEntryFromTable(function->table, vals, numDomains); + bool isInRange = tableEntry!=NULL; + bool needClause = isInRange; + if (function->undefBehavior == UNDEFINEDSETSFLAG || function->undefBehavior == FLAGIFFUNDEFINED) { + 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, (Element*)elemFunc, tableEntry->output); + } + + Edge clause; + switch(function->undefBehavior) { + case UNDEFINEDSETSFLAG: { + if (isInRange) { + clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]); + } else { + clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint); + } + break; + } + case FLAGIFFUNDEFINED: { + if (isInRange) { + clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintAND2(This->cnf, carray[numDomains], constraintNegate(undefConstraint))); + } else { + clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint); + } + break; + } + default: + ASSERT(0); + } +#ifdef TRACE_DEBUG + model_print("added clause in table enumeration ...\n"); + printCNF(clause); + model_print("\n"); +#endif + pushVectorEdge(clauses, clause); + } + + notfinished=false; + for(uint i=0;itable->domains, i); + + if (index < getSetSize(set)) { + vals[i]=getSetElement(set, index); + notfinished=true; + break; + } else { + indices[i]=0; + vals[i]=getSetElement(set, 0); + } + } + } + + Edge cor=constraintAND(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses)); + addConstraintCNF(This->cnf, cor); + deleteVectorEdge(clauses); + +} diff --git a/src/Backend/satfunctableencoder.h b/src/Backend/satfunctableencoder.h new file mode 100644 index 0000000..6ac111c --- /dev/null +++ b/src/Backend/satfunctableencoder.h @@ -0,0 +1,9 @@ +#ifndef SATFUNCTABLEENCODER_H +#define SATFUNCTABLEENCODER_H + +Edge encodeEnumEntriesTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint); +Edge encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint); +void encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This); +void encodeEnumEntriesTableElemFuncSATEncoder(SATEncoder* encoder, ElementFunction* This); + +#endif -- 2.34.1