From a79799d1c357cde4563996ce89caf5086bcf1faa Mon Sep 17 00:00:00 2001 From: bdemsky Date: Tue, 11 Jul 2017 15:43:50 -0700 Subject: [PATCH] Split encoder into more files --- src/Backend/satelemencoder.c | 44 ++++++++++++ src/Backend/satelemencoder.h | 7 ++ src/Backend/satencoder.c | 129 ---------------------------------- src/Backend/satencoder.h | 13 +--- src/Backend/satorderencoder.c | 97 +++++++++++++++++++++++++ src/Backend/satorderencoder.h | 11 +++ 6 files changed, 162 insertions(+), 139 deletions(-) create mode 100644 src/Backend/satelemencoder.c create mode 100644 src/Backend/satelemencoder.h create mode 100644 src/Backend/satorderencoder.c create mode 100644 src/Backend/satorderencoder.h diff --git a/src/Backend/satelemencoder.c b/src/Backend/satelemencoder.c new file mode 100644 index 0000000..1644a6b --- /dev/null +++ b/src/Backend/satelemencoder.c @@ -0,0 +1,44 @@ +#include "satencoder.h" +#include "structs.h" +#include "common.h" +#include "ops.h" +#include "element.h" + +Edge getElementValueConstraint(SATEncoder* This, Element* elem, uint64_t value) { + generateElementEncodingVariables(This, getElementEncoding(elem)); + switch(getElementEncoding(elem)->type){ + case ONEHOT: + //FIXME + ASSERT(0); + break; + case UNARY: + ASSERT(0); + break; + case BINARYINDEX: + return getElementValueBinaryIndexConstraint(This, elem, value); + break; + case ONEHOTBINARY: + ASSERT(0); + break; + case BINARYVAL: + ASSERT(0); + break; + default: + ASSERT(0); + break; + } + return E_BOGUS; +} + +Edge getElementValueBinaryIndexConstraint(SATEncoder * This, Element* elem, uint64_t value) { + ASTNodeType type = GETELEMENTTYPE(elem); + ASSERT(type == ELEMSET || type == ELEMFUNCRETURN); + ElementEncoding* elemEnc = getElementEncoding(elem); + for(uint i=0; iencArraySize; i++){ + if( isinUseElement(elemEnc, i) && elemEnc->encodingArray[i]==value){ + return generateBinaryConstraint(This->cnf, elemEnc->numVars, elemEnc->variables, i); + } + } + return E_BOGUS; +} + diff --git a/src/Backend/satelemencoder.h b/src/Backend/satelemencoder.h new file mode 100644 index 0000000..28d50b0 --- /dev/null +++ b/src/Backend/satelemencoder.h @@ -0,0 +1,7 @@ +#ifndef SATELEMENTENCODER_H +#define SATELEMENTENCODER_H + +Edge getElementValueBinaryIndexConstraint(SATEncoder * This, Element* element, uint64_t value); +Edge getElementValueConstraint(SATEncoder* encoder, Element* This, uint64_t value); + +#endif diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c index e68226f..5809a59 100644 --- a/src/Backend/satencoder.c +++ b/src/Backend/satencoder.c @@ -10,7 +10,6 @@ #include "table.h" #include "order.h" #include "predicate.h" -#include "orderpair.h" #include "set.h" SATEncoder * allocSATEncoder() { @@ -25,44 +24,6 @@ void deleteSATEncoder(SATEncoder *This) { ourfree(This); } -Edge getElementValueConstraint(SATEncoder* This, Element* elem, uint64_t value) { - generateElementEncodingVariables(This, getElementEncoding(elem)); - switch(getElementEncoding(elem)->type){ - case ONEHOT: - //FIXME - ASSERT(0); - break; - case UNARY: - ASSERT(0); - break; - case BINARYINDEX: - return getElementValueBinaryIndexConstraint(This, elem, value); - break; - case ONEHOTBINARY: - ASSERT(0); - break; - case BINARYVAL: - ASSERT(0); - break; - default: - ASSERT(0); - break; - } - return E_BOGUS; -} - -Edge getElementValueBinaryIndexConstraint(SATEncoder * This, Element* elem, uint64_t value) { - ASTNodeType type = GETELEMENTTYPE(elem); - ASSERT(type == ELEMSET || type == ELEMFUNCRETURN); - ElementEncoding* elemEnc = getElementEncoding(elem); - for(uint i=0; iencArraySize; i++){ - if( isinUseElement(elemEnc, i) && elemEnc->encodingArray[i]==value){ - return generateBinaryConstraint(This->cnf, elemEnc->numVars, elemEnc->variables, i); - } - } - return E_BOGUS; -} - void encodeAllSATEncoder(CSolver *csolver, SATEncoder * This) { VectorBoolean *constraints=csolver->constraints; uint size=getSizeVectorBoolean(constraints); @@ -132,96 +93,6 @@ Edge encodeLogicSATEncoder(SATEncoder *This, BooleanLogic * constraint) { } } -Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint) { - switch( constraint->order->type){ - case PARTIAL: - return encodePartialOrderSATEncoder(This, constraint); - case TOTAL: - return encodeTotalOrderSATEncoder(This, constraint); - default: - ASSERT(0); - } - return E_BOGUS; -} - -Edge getPairConstraint(SATEncoder *This, HashTableOrderPair * table, OrderPair * pair) { - bool negate = false; - OrderPair flipped; - if (pair->first > pair->second) { - negate=true; - flipped.first=pair->second; - flipped.second=pair->first; - pair = &flipped; - } - Edge constraint; - if (!containsOrderPair(table, pair)) { - constraint = getNewVarSATEncoder(This); - OrderPair * paircopy = allocOrderPair(pair->first, pair->second, constraint); - putOrderPair(table, paircopy, paircopy); - } else - constraint = getOrderPair(table, pair)->constraint; - - return negate ? constraintNegate(constraint) : constraint; -} - -Edge encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder * boolOrder) { - ASSERT(boolOrder->order->type == TOTAL); - if(boolOrder->order->orderPairTable == NULL) { - initializeOrderHashTable(boolOrder->order); - createAllTotalOrderConstraintsSATEncoder(This, boolOrder->order); - } - HashTableOrderPair* orderPairTable = boolOrder->order->orderPairTable; - OrderPair pair={boolOrder->first, boolOrder->second, E_NULL}; - Edge constraint = getPairConstraint(This, orderPairTable, & pair); - return constraint; -} - -void createAllTotalOrderConstraintsSATEncoder(SATEncoder* This, Order* order){ - ASSERT(order->type == TOTAL); - VectorInt* mems = order->set->members; - HashTableOrderPair* table = order->orderPairTable; - uint size = getSizeVectorInt(mems); - uint csize =0; - for(uint i=0; icnf, generateTransOrderConstraintSATEncoder(This, constIJ, constJK, constIK)); - } - } - } -} - -Edge getOrderConstraint(HashTableOrderPair *table, OrderPair *pair){ - ASSERT(pair->first!= pair->second); - Edge constraint = getOrderPair(table, pair)->constraint; - if(pair->first > pair->second) - return constraint; - else - return constraintNegate(constraint); -} - -Edge generateTransOrderConstraintSATEncoder(SATEncoder *This, Edge constIJ,Edge constJK,Edge constIK){ - Edge carray[] = {constIJ, constJK, constraintNegate(constIK)}; - Edge loop1= constraintOR(This->cnf, 3, carray); - Edge carray2[] = {constraintNegate(constIJ), constraintNegate(constJK), constIK}; - Edge loop2= constraintOR(This->cnf, 3, carray2 ); - return constraintAND2(This->cnf, loop1, loop2); -} - -Edge encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint){ - ASSERT(constraint->order->type == PARTIAL); - return E_BOGUS; -} - Edge encodePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) { switch(GETPREDICATETYPE(constraint->predicate) ){ case TABLEPRED: diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h index dfcb886..1f059b7 100644 --- a/src/Backend/satencoder.h +++ b/src/Backend/satencoder.h @@ -11,18 +11,15 @@ struct SATEncoder { CNF * cnf; }; +#include "satelemencoder.h" +#include "satorderencoder.h" + SATEncoder * allocSATEncoder(); void deleteSATEncoder(SATEncoder *This); void encodeAllSATEncoder(CSolver *csolver, SATEncoder *This); Edge getNewVarSATEncoder(SATEncoder *This); void getArrayNewVarsSATEncoder(SATEncoder* encoder, uint num, Edge*carray); Edge encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint); -Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint); -void createAllTotalOrderConstraintsSATEncoder(SATEncoder* This, Order* order); -Edge getOrderConstraint(HashTableOrderPair *table, OrderPair *pair); -Edge generateTransOrderConstraintSATEncoder(SATEncoder *This, Edge constIJ, Edge constJK, Edge constIK); -Edge encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint); -Edge encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint); Edge encodeVarSATEncoder(SATEncoder *This, BooleanVar * constraint); Edge encodeLogicSATEncoder(SATEncoder *This, BooleanLogic * constraint); Edge encodePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint); @@ -30,10 +27,6 @@ Edge encodeTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constr Edge encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint); Edge encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint); Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint); - -Edge getElementValueBinaryIndexConstraint(SATEncoder * This, Element* element, uint64_t value); -Edge getElementValueConstraint(SATEncoder* encoder, Element* This, uint64_t value); - void encodeElementSATEncoder(SATEncoder* encoder, Element *This); Edge encodeElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction *This); Edge encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This); diff --git a/src/Backend/satorderencoder.c b/src/Backend/satorderencoder.c new file mode 100644 index 0000000..f04b86e --- /dev/null +++ b/src/Backend/satorderencoder.c @@ -0,0 +1,97 @@ +#include "satencoder.h" +#include "structs.h" +#include "common.h" +#include "order.h" +#include "orderpair.h" +#include "set.h" + +Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint) { + switch( constraint->order->type){ + case PARTIAL: + return encodePartialOrderSATEncoder(This, constraint); + case TOTAL: + return encodeTotalOrderSATEncoder(This, constraint); + default: + ASSERT(0); + } + return E_BOGUS; +} + +Edge getPairConstraint(SATEncoder *This, HashTableOrderPair * table, OrderPair * pair) { + bool negate = false; + OrderPair flipped; + if (pair->first > pair->second) { + negate=true; + flipped.first=pair->second; + flipped.second=pair->first; + pair = &flipped; + } + Edge constraint; + if (!containsOrderPair(table, pair)) { + constraint = getNewVarSATEncoder(This); + OrderPair * paircopy = allocOrderPair(pair->first, pair->second, constraint); + putOrderPair(table, paircopy, paircopy); + } else + constraint = getOrderPair(table, pair)->constraint; + + return negate ? constraintNegate(constraint) : constraint; +} + +Edge encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder * boolOrder) { + ASSERT(boolOrder->order->type == TOTAL); + if(boolOrder->order->orderPairTable == NULL) { + initializeOrderHashTable(boolOrder->order); + createAllTotalOrderConstraintsSATEncoder(This, boolOrder->order); + } + HashTableOrderPair* orderPairTable = boolOrder->order->orderPairTable; + OrderPair pair={boolOrder->first, boolOrder->second, E_NULL}; + Edge constraint = getPairConstraint(This, orderPairTable, & pair); + return constraint; +} + + +void createAllTotalOrderConstraintsSATEncoder(SATEncoder* This, Order* order){ + ASSERT(order->type == TOTAL); + VectorInt* mems = order->set->members; + HashTableOrderPair* table = order->orderPairTable; + uint size = getSizeVectorInt(mems); + uint csize =0; + for(uint i=0; icnf, generateTransOrderConstraintSATEncoder(This, constIJ, constJK, constIK)); + } + } + } +} + +Edge getOrderConstraint(HashTableOrderPair *table, OrderPair *pair){ + ASSERT(pair->first!= pair->second); + Edge constraint = getOrderPair(table, pair)->constraint; + if(pair->first > pair->second) + return constraint; + else + return constraintNegate(constraint); +} + +Edge generateTransOrderConstraintSATEncoder(SATEncoder *This, Edge constIJ,Edge constJK,Edge constIK){ + Edge carray[] = {constIJ, constJK, constraintNegate(constIK)}; + Edge loop1= constraintOR(This->cnf, 3, carray); + Edge carray2[] = {constraintNegate(constIJ), constraintNegate(constJK), constIK}; + Edge loop2= constraintOR(This->cnf, 3, carray2 ); + return constraintAND2(This->cnf, loop1, loop2); +} + +Edge encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint){ + ASSERT(constraint->order->type == PARTIAL); + return E_BOGUS; +} diff --git a/src/Backend/satorderencoder.h b/src/Backend/satorderencoder.h new file mode 100644 index 0000000..c26e668 --- /dev/null +++ b/src/Backend/satorderencoder.h @@ -0,0 +1,11 @@ +#ifndef SATORDERENCODER_H +#define SATORDERENCODER_H + +Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint); +Edge getPairConstraint(SATEncoder *This, HashTableOrderPair *table, OrderPair *pair); +Edge encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint); +Edge encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint); +void createAllTotalOrderConstraintsSATEncoder(SATEncoder* This, Order* order); +Edge getOrderConstraint(HashTableOrderPair *table, OrderPair *pair); +Edge generateTransOrderConstraintSATEncoder(SATEncoder *This, Edge constIJ, Edge constJK, Edge constIK); +#endif -- 2.34.1