Fixing the testcase bug

diff --git a/src/Backend/constraint.c b/src/Backend/constraint.c
index e9f9aa0f35f1eecf72f5e42f60801fb7b145cc64..e8ef1db7d8278ed20eb31ace02721ba4f4ad2166 100644 (file)
--- a/src/Backend/constraint.c
+++ b/src/Backend/constraint.c
@@ -210,7 +210,7 @@ Edge constraintAND(CNF * cnf, uint numEdges, Edge * edges) {
                        edges[++lowindex]=edges[initindex];
        }
        lowindex++; //Make lowindex look like size
-       
+
        if (lowindex==1)
                return edges[0];
 
@@ -311,6 +311,9 @@ Edge constraintITE(CNF * cnf, Edge cond, Edge thenedge, Edge elseedge) {
 
 void addConstraintCNF(CNF *cnf, Edge constraint) {
        pushVectorEdge(&cnf->constraints, constraint);
+       printf("****ADDING NEW Constraint*****\n");
+       printCNF(constraint);
+       printf("\n******************************\n");
 }
 
 Edge constraintNewVar(CNF *cnf) {

diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c
index c34a04729d5038679d41d0504498d06b913e3422..5b2372b1cb626b2c6e969cc34e0a996b116c9d34 100644 (file)
--- a/src/Backend/satencoder.c
+++ b/src/Backend/satencoder.c
@@ -30,10 +30,10 @@ void encodeAllSATEncoder(CSolver *csolver, SATEncoder * This) {
        VectorBoolean *constraints=csolver->constraints;
        uint size=getSizeVectorBoolean(constraints);
        for(uint i=0;i<size;i++) {
+               model_print("Encoding All ...\n\n");
                Boolean *constraint=getVectorBoolean(constraints, i);
                Edge c= encodeConstraintSATEncoder(This, constraint);
-               printCNF(c);
-               printf("\n\n");
+               model_print("Returned Constraint in EncodingAll:\n");
                addConstraintCNF(This->cnf, c);
        }
 }
@@ -124,6 +124,7 @@ Edge encodeTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constr
 void encodeElementSATEncoder(SATEncoder* encoder, Element *This){
        switch( GETELEMENTTYPE(This) ){
                case ELEMFUNCRETURN:
+                       generateElementEncoding(encoder, This);
                        encodeElementFunctionSATEncoder(encoder, (ElementFunction*) This);
                        break;
                case ELEMSET:

diff --git a/src/Backend/satfuncencoder.c b/src/Backend/satfuncencoder.c
index d28d43d64d52efd5e835769413e143a721a04293..af7c8b3401f8809926d81d20c9623f90c0a927f0 100644 (file)
--- a/src/Backend/satfuncencoder.c
+++ b/src/Backend/satfuncencoder.c
@@ -8,7 +8,7 @@
 #include "tableentry.h"
 #include "set.h"
 #include "element.h"
-
+#include "common.h"
 Edge encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
        VectorTableEntry* entries = &(((PredicateTable*)constraint->predicate)->table->entries);
        FunctionEncodingType encType = constraint->encoding.type;
@@ -144,6 +144,9 @@ Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate *
 
 
 void encodeOperatorElementFunctionSATEncoder(SATEncoder* This, ElementFunction* func) {
+#ifdef TRACE_DEBUG
+       model_print("Operator Function ...\n");
+#endif
        FunctionOperator * function = (FunctionOperator *) func->function;
        uint numDomains=getSizeArrayElement(&func->inputs);
 
@@ -247,6 +250,9 @@ void encodeOperatorElementFunctionSATEncoder(SATEncoder* This, ElementFunction*
 }
 
 void encodeEnumTableElemFunctionSATEncoder(SATEncoder* This, ElementFunction* func){
+#ifdef TRACE_DEBUG
+       model_print("Enumeration Table functions ...\n");
+#endif
        //FIXME: HANDLE UNDEFINED BEHAVIORS
        ASSERT(GETFUNCTIONTYPE(func->function)==TABLEFUNC);
        ArrayElement* elements= &func->inputs;

diff --git a/src/Backend/satorderencoder.c b/src/Backend/satorderencoder.c
index f04b86edd5248844bd59506b9066dbade049f8aa..ff79d76a8536be3223dd4086f4de2b9174d309c0 100644 (file)
--- a/src/Backend/satorderencoder.c
+++ b/src/Backend/satorderencoder.c
@@ -51,6 +51,9 @@ Edge encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder * boolOrder) {
 
 
 void createAllTotalOrderConstraintsSATEncoder(SATEncoder* This, Order* order){
+#ifdef TRACE_DEBUG
+       model_print("in total order ...\n");
+#endif 
        ASSERT(order->type == TOTAL);
        VectorInt* mems = order->set->members;
        HashTableOrderPair* table = order->orderPairTable;

diff --git a/src/config.h b/src/config.h
index bd998c0a437fd69a3115897cbf06cfb2b2b60826..db02014b5f128ab4262b83f69f1ec7ae5a12dfc9 100644 (file)
--- a/src/config.h
+++ b/src/config.h
@@ -17,6 +17,7 @@
 /** Turn on debugging. */
 #ifndef CONFIG_DEBUG
 //#define CONFIG_DEBUG
+#define TRACE_DEBUG
 #endif
 
 #ifndef CONFIG_ASSERT