Split encoder into more files

diff --git a/src/Backend/satelemencoder.c b/src/Backend/satelemencoder.c
new file mode 100644 (file)
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; i<elemEnc->encArraySize; 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 (file)
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 e68226fc49dfee190715639a858bd6f9c794d06c..5809a599aeeb29603a13a32cf6af7810024a3835 100644 (file)
--- 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; i<elemEnc->encArraySize; 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; i<size; i++){
-               uint64_t valueI = getVectorInt(mems, i);
-               for(uint j=i+1; j<size;j++){
-                       uint64_t valueJ = getVectorInt(mems, j);
-                       OrderPair pairIJ = {valueI, valueJ};
-                       Edge constIJ=getPairConstraint(This, table, & pairIJ);
-                       for(uint k=j+1; k<size; k++){
-                               uint64_t valueK = getVectorInt(mems, k);
-                               OrderPair pairJK = {valueJ, valueK};
-                               OrderPair pairIK = {valueI, valueK};
-                               Edge constIK = getPairConstraint(This, table, & pairIK);
-                               Edge constJK = getPairConstraint(This, table, & pairJK);
-                               addConstraintCNF(This->cnf, 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 dfcb8868dbbedb0ad3db22de4a1f4937f6fc194c..1f059b73137d12fa55a864c9ad71c8df16891259 100644 (file)
--- 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 (file)
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; i<size; i++){
+               uint64_t valueI = getVectorInt(mems, i);
+               for(uint j=i+1; j<size;j++){
+                       uint64_t valueJ = getVectorInt(mems, j);
+                       OrderPair pairIJ = {valueI, valueJ};
+                       Edge constIJ=getPairConstraint(This, table, & pairIJ);
+                       for(uint k=j+1; k<size; k++){
+                               uint64_t valueK = getVectorInt(mems, k);
+                               OrderPair pairJK = {valueJ, valueK};
+                               OrderPair pairIK = {valueI, valueK};
+                               Edge constIK = getPairConstraint(This, table, & pairIK);
+                               Edge constJK = getPairConstraint(This, table, & pairJK);
+                               addConstraintCNF(This->cnf, 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 (file)
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