Split encoder into more files

[satune.git] / src / Backend / satencoder.c

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: