Bug fix for serializer + adding more debug info inr printing functions

diff --git a/src/AST/boolean.cc b/src/AST/boolean.cc
index 939f937d37fa4b02e516cb6f75920cf7a110b0e2..c576268058f3b5203687a2d6cef9e496a90bcf2e 100644 (file)
--- a/src/AST/boolean.cc
+++ b/src/AST/boolean.cc
@@ -115,11 +115,11 @@ void BooleanVar::serialize(Serializer *serializer) {
 }
 
 void BooleanVar::print() {
 }
 
 void BooleanVar::print() {

-       model_print("BooleanVar:%lu\n", (uintptr_t)this);
+       model_print("BooleanVar<%p>\n", this);

 }
 
 void BooleanConst::print() {
 }
 
 void BooleanConst::print() {

-       model_print("BooleanConst:%s\n", istrue ? "TRUE" : "FALSE");
+       model_print("BooleanConst<%p>:%s\n", this, istrue ? "TRUE" : "FALSE");

 }
 
 void BooleanOrder::serialize(Serializer *serializer) {
 }
 
 void BooleanOrder::serialize(Serializer *serializer) {


@@ -137,7 +137,7 @@ void BooleanOrder::serialize(Serializer *serializer) {
 }
 
 void BooleanOrder::print() {
 }
 
 void BooleanOrder::print() {

-       model_print("{BooleanOrder: First= %lu, Second = %lu on Order:\n", first, second);
+       model_print("{BooleanOrder<%p>: First= %lu, Second = %lu on Order:\n", this, first, second);

        order->print();
        model_print("}\n");
 }
        order->print();
        model_print("}\n");
 }


@@ -169,7 +169,7 @@ void BooleanPredicate::serialize(Serializer *serializer) {
 }
 
 void BooleanPredicate::print() {
 }
 
 void BooleanPredicate::print() {

-       model_print("{BooleanPredicate:\n");
+       model_print("{BooleanPredicate<%p>:\n", this);

        predicate->print();
        model_print("elements:\n");
        uint size = inputs.getSize();
        predicate->print();
        model_print("elements:\n");
        uint size = inputs.getSize();


@@ -201,7 +201,7 @@ void BooleanLogic::serialize(Serializer *serializer) {
 }
 
 void BooleanLogic::print() {
 }
 
 void BooleanLogic::print() {

-       model_print("{BooleanLogic: %s\n",
+       model_print("{BooleanLogic<%p>: %s\n", this,

                                                        op == SATC_AND ? "AND" : op == SATC_OR ? "OR" : op == SATC_NOT ? "NOT" :
                                                        op == SATC_XOR ? "XOR" : op == SATC_IFF ? "IFF" : "IMPLIES");
        uint size = inputs.getSize();
                                                        op == SATC_AND ? "AND" : op == SATC_OR ? "OR" : op == SATC_NOT ? "NOT" :
                                                        op == SATC_XOR ? "XOR" : op == SATC_IFF ? "IFF" : "IMPLIES");
        uint size = inputs.getSize();

diff --git a/src/AST/element.cc b/src/AST/element.cc
index f575a9034c2565695ac2f1696d0a5af2541c5e21..ffe7acc929bfa534e15596a037ae7b90ee5ee92a 100644 (file)
--- a/src/AST/element.cc
+++ b/src/AST/element.cc
@@ -78,7 +78,7 @@ void ElementSet::serialize(Serializer *serializer) {
 }
 
 void ElementSet::print() {
 }
 
 void ElementSet::print() {

-       model_print("{ElementSet:");
+       model_print("{ElementSet<%p>:", this);

        set->print();
        model_print(" %p ", this);
        getElementEncoding()->print();
        set->print();
        model_print(" %p ", this);
        getElementEncoding()->print();


@@ -101,7 +101,7 @@ void ElementConst::serialize(Serializer *serializer) {
 }
 
 void ElementConst::print() {
 }
 
 void ElementConst::print() {

-       model_print("{ElementConst: %" PRIu64 "}\n", value);
+       model_print("{ElementConst<%p>: %" PRIu64 "}\n", this, value);

 }
 
 void ElementFunction::serialize(Serializer *serializer) {
 }
 
 void ElementFunction::serialize(Serializer *serializer) {


@@ -131,7 +131,7 @@ void ElementFunction::serialize(Serializer *serializer) {
 }
 
 void ElementFunction::print() {
 }
 
 void ElementFunction::print() {

-       model_print("{ElementFunction:\n");
+       model_print("{ElementFunction<%p>:\n", this);

        function->print();
        model_print("Elements:\n");
        uint size = inputs.getSize();
        function->print();
        model_print("Elements:\n");
        uint size = inputs.getSize();

diff --git a/src/AST/function.cc b/src/AST/function.cc
index c38551246ef93a5e231624a7474e202268f63d1a..ccd89dd28c624d32714df88787715ef83dbc84e3 100644 (file)
--- a/src/AST/function.cc
+++ b/src/AST/function.cc
@@ -83,7 +83,7 @@ void FunctionTable::serialize(Serializer *serializer) {
 }
 
 void FunctionTable::print() {
 }
 
 void FunctionTable::print() {

-       model_print("{FunctionTable:\n");
+       model_print("{FunctionTable<%p>:\n", this);

        table->print();
        model_print("}\n");
 }
        table->print();
        model_print("}\n");
 }


@@ -115,5 +115,5 @@ void FunctionOperator::serialize(Serializer *serializer) {
 }
 
 void FunctionOperator::print() {
 }
 
 void FunctionOperator::print() {

-       model_print("{FunctionOperator: %s}\n", op == SATC_ADD ? "ADD" : "SUB" );
+       model_print("{FunctionOperator<%p>: %s}\n", this, op == SATC_ADD ? "ADD" : "SUB" );

 }
 }

diff --git a/src/AST/order.cc b/src/AST/order.cc
index f3ccde419dc9e07957a62229a913c855aca7fdd8..315b112d1c2aae07dec86b71dfb8a7db345e29a1 100644 (file)
--- a/src/AST/order.cc
+++ b/src/AST/order.cc
@@ -60,7 +60,7 @@ void Order::serialize(Serializer *serializer) {
 }
 
 void Order::print() {
 }
 
 void Order::print() {

-       model_print("{Order on Set:\n");
+       model_print("{Order<%p> on Set:\n", this);

        set->print();
        model_print("}\n");
 }
        set->print();
        model_print("}\n");
 }

diff --git a/src/AST/set.cc b/src/AST/set.cc
index 52494e393ca9ef682fbd5d20bce9e52041d31665..d45791aae1482f6882c4b6db463b4d348a697083 100644 (file)
--- a/src/AST/set.cc
+++ b/src/AST/set.cc
@@ -155,7 +155,7 @@ void Set::serialize(Serializer *serializer) {
 }
 
 void Set::print() {
 }
 
 void Set::print() {

-       model_print("{Set:");
+       model_print("{Set<%p>:", this);

        if (isRange) {
                model_print("Range: low=%lu, high=%lu}", low, high);
        } else {
        if (isRange) {
                model_print("Range: low=%lu, high=%lu}", low, high);
        } else {

diff --git a/src/AST/table.cc b/src/AST/table.cc
index 5786b173d2499ebe9dc499630343aeaf46723da0..513935dab5bd4bff7736ca5bf1d3128eba673224 100644 (file)
--- a/src/AST/table.cc
+++ b/src/AST/table.cc
@@ -98,7 +98,7 @@ void Table::serialize(Serializer *serializer) {
 
 
 void Table::print() {
 
 
 void Table::print() {

-       model_print("{Table:\n");
+       model_print("{Table<%p>:\n", this);

        SetIteratorTableEntry *iterator = getEntries();
        while (iterator->hasNext()) {
                TableEntry *entry = iterator->next();
        SetIteratorTableEntry *iterator = getEntries();
        while (iterator->hasNext()) {
                TableEntry *entry = iterator->next();

diff --git a/src/Serialize/serializer.cc b/src/Serialize/serializer.cc
index 4a970748e66470319550dde3a34fa4c49406c887..cfad4e8a29b52f3c2c390072f1ca6393d411bf6f 100644 (file)
--- a/src/Serialize/serializer.cc
+++ b/src/Serialize/serializer.cc
@@ -62,6 +62,7 @@ void Serializer::mywrite(const void *__buf, size_t __n) {
                        if (spacefree < __n) {
                                flushBuffer();
                                towrite += datatowrite;
                        if (spacefree < __n) {
                                flushBuffer();
                                towrite += datatowrite;

+                                __n-=datatowrite;

                        } else if (spacefree == __n) {
                                flushBuffer();
                                return;
                        } else if (spacefree == __n) {
                                flushBuffer();
                                return;

diff --git a/src/config.h b/src/config.h
index e34b82810f12e85049baa60ecf112985fbecaa43..5ce22b0f0fdf89a4f2e0e5c6690201aacddd6579 100644 (file)
--- a/src/config.h
+++ b/src/config.h
@@ -19,7 +19,6 @@
 //#define CONFIG_DEBUG
 #endif
 
 //#define CONFIG_DEBUG
 #endif
 

-#define SATCHECK_CONFIG

 
 #ifndef CONFIG_ASSERT
 #define CONFIG_ASSERT
 
 #ifndef CONFIG_ASSERT
 #define CONFIG_ASSERT

diff --git a/src/csolver.cc b/src/csolver.cc
index 160e6867f854c7abb42a646521782cd576a69d0f..e844e792eb305c4cc1c53cb59022326de8a71113 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -40,6 +40,7 @@ CSolver::CSolver() :
 /** This function tears down the solver and the entire AST */
 
 CSolver::~CSolver() {
 /** This function tears down the solver and the entire AST */
 
 CSolver::~CSolver() {

+       serialize();

        uint size = allBooleans.getSize();
        for (uint i = 0; i < size; i++) {
                delete allBooleans.get(i);
        uint size = allBooleans.getSize();
        for (uint i = 0; i < size; i++) {
                delete allBooleans.get(i);

diff --git a/src/mymemory.h b/src/mymemory.h
index 97e177ce07a626a24bbdbb73bb46c2e08d7992fc..92fb0fed609057c3fd40132bcf507986489133cd 100644 (file)
--- a/src/mymemory.h
+++ b/src/mymemory.h
@@ -19,8 +19,6 @@
 
 #include "config.h"
 
 
 #include "config.h"
 

-#define SATCHECK_CONFIG
-

 /*
    void * ourmalloc(size_t size);
    void ourfree(void *ptr);
 /*
    void * ourmalloc(size_t size);
    void ourfree(void *ptr);