Adding pring option for AST

diff --git a/src/AST/element.cc b/src/AST/element.cc
index ed0a7416853453316d44d2bb565fa991d8326389..fb5b8222badb2f4064215bfe74202d8c25e02532 100644 (file)
--- a/src/AST/element.cc
+++ b/src/AST/element.cc
@@ -77,6 +77,12 @@ void ElementSet::serialize(Serializer* serializer){
        serializer->mywrite(&set, sizeof(Set*));
 }
 
+void ElementSet::print(){
+       model_println("{ElementSet:");
+       set->print();
+       model_println("}\n");
+}
+
 void ElementConst::serialize(Serializer* serializer){
        if(serializer->isSerialized(this))
                return;
@@ -92,6 +98,10 @@ void ElementConst::serialize(Serializer* serializer){
        serializer->mywrite(&value, sizeof(uint64_t));
 }
 
+void ElementConst::print(){
+       model_println("{ElementConst: %lu}", value);    
+}
+
 void ElementFunction::serialize(Serializer* serializer){
        if(serializer->isSerialized(this))
                return;
@@ -118,3 +128,14 @@ void ElementFunction::serialize(Serializer* serializer){
        serializer->mywrite(&overflowstat, sizeof(Boolean*));
 }
 
+void ElementFunction::print(){
+        model_println("{ElementFunction:");
+       function->print();
+        model_println("Elements:");
+       uint size = inputs.getSize();
+       for(uint i=0; i<size; i++){
+               Element *input = inputs.get(i);
+               input->print();
+       }
+       model_println("}\n");
+}

diff --git a/src/AST/function.cc b/src/AST/function.cc
index 96b0797452aacfb744d418ceaa3170f9604838f1..26decd093b1d1354d778427419db991b3407f898 100644 (file)
--- a/src/AST/function.cc
+++ b/src/AST/function.cc
@@ -82,6 +82,13 @@ void FunctionTable::serialize(Serializer* serializer){
        
 }
 
+void FunctionTable::print(){
+       model_println("{FunctionTable:");
+        table->print();
+        model_println("}\n");
+       
+}
+
 void FunctionOperator::serialize(Serializer* serializer){
        if(serializer->isSerialized(this))
                return;
@@ -106,4 +113,8 @@ void FunctionOperator::serialize(Serializer* serializer){
        }
        serializer->mywrite(&range, sizeof(Set *));
        serializer->mywrite(&overflowbehavior, sizeof(OverFlowBehavior));
+}
+
+void FunctionOperator::print(){
+       model_println("{FunctionOperator: %s}", op == SATC_ADD? "ADD": "SUB" );
 }
\ No newline at end of file

diff --git a/src/AST/order.cc b/src/AST/order.cc
index 3920d3b88b7ac1cfc91e815407bb2c2f9d3a21ae..96e7be5f619ca7f28d971027babc5e8d2b191496 100644 (file)
--- a/src/AST/order.cc
+++ b/src/AST/order.cc
@@ -58,3 +58,9 @@ void Order::serialize(Serializer* serializer){
        serializer->mywrite(&type, sizeof(OrderType));
        serializer->mywrite(&set, sizeof(Set *));
 }
+
+void Order::print(){
+       model_println("{Order on Set:");
+        set->print();
+       model_println("}\n");
+}

diff --git a/src/AST/order.h b/src/AST/order.h
index b8ca724b3c33d2747ea9cb505d3ce34203e67256..e2e0b4310f9304da4bc592983d14567be2a4ef1f 100644 (file)
--- a/src/AST/order.h
+++ b/src/AST/order.h
@@ -17,6 +17,7 @@ public:
        OrderGraph *graph;
        Order *clone(CSolver *solver, CloneMap *map);
        void serialize(Serializer *serializer );
+       void print();
        Vector<BooleanOrder *> constraints;
        OrderEncoding encoding;
        void setOrderResolver(OrderResolver *_resolver) { ASSERT(encoding.resolver == NULL); encoding.resolver = _resolver;};

diff --git a/src/AST/predicate.cc b/src/AST/predicate.cc
index e3ae1db970280646bd4c30c17689c7374f415522..659a3e336a97d58b2d6c5f454bcb7a2e320944fd 100644 (file)
--- a/src/AST/predicate.cc
+++ b/src/AST/predicate.cc
@@ -66,6 +66,12 @@ void PredicateTable::serialize(Serializer* serializer){
        serializer->mywrite(&undefinedbehavior, sizeof(UndefinedBehavior));
 }
 
+void PredicateTable::print(){  
+       model_println("{PredicateTable:");
+        table->print();
+        model_println("}\n");
+}
+
 void PredicateOperator::serialize(Serializer* serializer){     
        if(serializer->isSerialized(this))
                return;

diff --git a/src/AST/predicate.h b/src/AST/predicate.h
index beaebc9b09989122f45d64573a0e7868c499f0b2..94a7e2e5e25a792dcf6e20a9967b2552066da14c 100644 (file)
--- a/src/AST/predicate.h
+++ b/src/AST/predicate.h
@@ -13,6 +13,7 @@ public:
        virtual ~Predicate() {}
        virtual Predicate *clone(CSolver *solver, CloneMap *map) {ASSERT(0); return NULL;}
        virtual void serialize(Serializer* serializer) = 0;
+        virtual void print() =0;
        PredicateType type;
        CMEMALLOC;
 };
@@ -23,6 +24,7 @@ public:
        bool evalPredicateOperator(uint64_t *inputs);
        Predicate *clone(CSolver *solver, CloneMap *map);
        virtual void serialize(Serializer* serializer);
+        virtual void print();
        Array<Set *> domains;
        CompOp getOp() {return op;}
        CMEMALLOC;
@@ -35,6 +37,7 @@ public:
        PredicateTable(Table *table, UndefinedBehavior undefBehavior);
        Predicate *clone(CSolver *solver, CloneMap *map);
        virtual void serialize(Serializer* serializer);
+        virtual void print();
        Table *table;
        UndefinedBehavior undefinedbehavior;
        CMEMALLOC;

diff --git a/src/AST/set.cc b/src/AST/set.cc
index d3801f8d498eb98e3a55440a4ac7faf243a195f3..25ccd05e67d6d9e480d45346735ea40ef4d1ed6f 100644 (file)
--- a/src/AST/set.cc
+++ b/src/AST/set.cc
@@ -142,3 +142,18 @@ void Set::serialize(Serializer* serializer){
                serializer->mywrite(&mem, sizeof(uint64_t));
        }
 }
+
+void Set::print(){
+       model_print("{Set:");
+        if(isRange){
+                model_print("Range: low=%lu, high=%lu}\n\n", low, high);
+        } else {
+                uint size = members->getSize();
+                model_print("Members: ");
+                for(uint i=0; i<size; i++){
+                        uint64_t mem = members->get(i);
+                        model_print("%lu, ", mem);
+                }
+                model_println("}\n");
+        }
+}

diff --git a/src/AST/set.h b/src/AST/set.h
index ad89504db94e76170464d1eb5c29c943dd1106c3..a0bd449e5b831535e432eb6bca85634ea132ea48 100644 (file)
--- a/src/AST/set.h
+++ b/src/AST/set.h
@@ -28,6 +28,7 @@ public:
        virtual bool isMutableSet() {return false;}
        virtual Set *clone(CSolver *solver, CloneMap *map);
        virtual void serialize(Serializer* serializer);
+       virtual void print();
        CMEMALLOC;
 protected:
        VarType type;

diff --git a/src/AST/table.cc b/src/AST/table.cc
index 838a53a2e641f6a64e98f003f4336f477ad4c432..f6494f479c17880e8b16d71979d0041d1c60c325 100644 (file)
--- a/src/AST/table.cc
+++ b/src/AST/table.cc
@@ -97,3 +97,17 @@ void Table::serialize(Serializer* serializer){
 }
 
 
+void Table::print(){
+        model_println("{Table:");
+       SetIteratorTableEntry* iterator = getEntries();
+       while(iterator->hasNext()){
+               TableEntry* entry = iterator->next();
+                model_print("<");
+                for(uint i=0; i<entry->inputSize; i++){
+                        model_print("%lu, ", entry->inputs[i]);
+                }
+                model_print(" == %lu>", entry->output);
+       }
+        model_println("}\n");
+       delete iterator;
+}

diff --git a/src/AST/table.h b/src/AST/table.h
index db8d188f9669476b1cce78698f7e80076c497ca8..d8c7829b86eb8e4dd60b9732d6fc7968485f5a44 100644 (file)
--- a/src/AST/table.h
+++ b/src/AST/table.h
@@ -11,6 +11,7 @@ public:
        TableEntry *getTableEntry(uint64_t *inputs, uint inputSize);
        Table *clone(CSolver *solver, CloneMap *map);
        void serialize(Serializer *serializer);
+        void print();
        ~Table();
        Set * getRange() {return range;}
        

diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc
index fdeee9ee8816faf0c812a7696bde8e69b6ba95eb..3a303628616a4ba4bb0dbba2922e4a536733208c 100644 (file)
--- a/src/Backend/satencoder.cc
+++ b/src/Backend/satencoder.cc
@@ -29,6 +29,7 @@ void SATEncoder::encodeAllSATEncoder(CSolver *csolver) {
        SetIteratorBooleanEdge *iterator = csolver->getConstraints();
        while (iterator->hasNext()) {
                BooleanEdge constraint = iterator->next();
+                constraint.getBoolean()->print();
                Edge c = encodeConstraintSATEncoder(constraint);
                addConstraintCNF(cnf, c);
        }

diff --git a/src/common.h b/src/common.h
index 4ebd816df11c9b900f705b580e730880b585a3cf..d52924c2d91e95904baae0e9fb7bb4d758778b96 100644 (file)
--- a/src/common.h
+++ b/src/common.h
@@ -18,7 +18,7 @@
 #include "config.h"
 #include "time.h"
 
-/*
+
    extern int model_out;
    extern int model_err;
    extern int switch_alloc;
@@ -26,12 +26,12 @@
  #define model_dprintf(fd, fmt, ...) do { switch_alloc = 1; dprintf(fd, fmt, ## __VA_ARGS__); switch_alloc = 0; } while (0)
 
  #define model_print(fmt, ...) do { model_dprintf(model_out, fmt, ## __VA_ARGS__); } while (0)
-
+#define model_println(fmt, ...) do { model_print(fmt, ## __VA_ARGS__); model_print("\n");} while(0)
  #define model_print_err(fmt, ...) do { model_dprintf(model_err, fmt, ## __VA_ARGS__); } while (0)
 
- */
 
-#define model_print printf
+
+//#define model_print printf
 
 #define NEXTPOW2(x) ((x == 1) ? 1 : (1 << (sizeof(uint) * 8 - __builtin_clz(x - 1))))
 #define NUMBITS(x) ((x == 0) ? 0 : 8 * sizeof(x) - __builtin_clz(x))