Edits

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

-       model_print("{ElementConst: %lu}\n", value);
+       model_print("{ElementConst: %" PRIu64 "}\n", value);

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

diff --git a/src/common.h b/src/common.h
index 52c0b5f7ebd85b9e0830bafee33367b18bc19123..fb4d7bacb1028c752f58dc62e947e214f4c05793 100644 (file)
--- a/src/common.h
+++ b/src/common.h
@@ -18,21 +18,18 @@
 #include "config.h"
 #include "time.h"
 
 #include "config.h"
 #include "time.h"
 

-/*
-   extern int model_out;
-   extern int model_err;
-   extern int switch_alloc;

 
 

- #define model_dprintf(fd, fmt, ...) do { switch_alloc = 1; dprintf(fd, fmt, ## __VA_ARGS__); switch_alloc = 0; } while (0)
- #define model_print(fmt, ...) do { printf(fmt, ## __VA_ARGS__); } while (0)
- #define model_println(fmt, ...) do { model_print(fmt, ## __VA_ARGS__); model_print("\n");} while(0)
-
- #define model_print(fmt, ...) do { model_dprintf(model_out, fmt, ## __VA_ARGS__); } while (0)
-
- #define model_print_err(fmt, ...) do { model_dprintf(model_err, fmt, ## __VA_ARGS__); } while (0)
- */
+#if 1
+extern int model_out;
+extern int model_err;
+extern int switch_alloc;

 
 

+#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_print_err(fmt, ...) do { model_dprintf(model_err, fmt, ## __VA_ARGS__); } while (0)
+#else

 #define model_print printf
 #define model_print printf

+#endif

 
 #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))
 
 #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))

diff --git a/src/csolver.cc b/src/csolver.cc
index 756798b6297b510884c5fc6d2e6a93c40aa57c23..be4a3a88063882cc05f5cfafca9218724b870f72 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -386,7 +386,10 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint
 }
 
 BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t second) {
 }
 
 BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t second) {

-       ASSERT(first != second);
+       //      ASSERT(first != second);
+       if (first == second)
+               return getBooleanFalse();
+       

        bool negate = false;
        if (order->type == SATC_TOTAL) {
                if (first > second) {
        bool negate = false;
        if (order->type == SATC_TOTAL) {
                if (first > second) {


@@ -470,13 +473,13 @@ int CSolver::solve() {
        DecomposeOrderTransform dot(this);
        dot.doTransform();
 
        DecomposeOrderTransform dot(this);
        dot.doTransform();
 

-       IntegerEncodingTransform iet(this);
-       iet.doTransform();
+       //IntegerEncodingTransform iet(this);
+       //iet.doTransform();

 
 

-       EncodingGraph eg(this);
-       eg.buildGraph();
-       eg.encode();
-       printConstraints();
+       //EncodingGraph eg(this);
+       //eg.buildGraph();
+       //eg.encode();
+       //printConstraints();

        naiveEncodingDecision(this);
        satEncoder->encodeAllSATEncoder(this);
        model_print("Is problem UNSAT after encoding: %d\n", unsat);
        naiveEncodingDecision(this);
        satEncoder->encodeAllSATEncoder(this);
        model_print("Is problem UNSAT after encoding: %d\n", unsat);


@@ -504,6 +507,13 @@ void CSolver::printConstraints() {
 
 }
 
 
 }
 

+void CSolver::printConstraint(BooleanEdge b) {
+       if (b.isNegated())
+               model_print("!");
+       b->print();
+       model_print("\n");
+}
+

 uint64_t CSolver::getElementValue(Element *element) {
        switch (element->type) {
        case ELEMSET:
 uint64_t CSolver::getElementValue(Element *element) {
        switch (element->type) {
        case ELEMSET:

diff --git a/src/csolver.h b/src/csolver.h
index 15d5b453c8b697505ac40e22b4efe7b65cd03996..2730a934164a7d267bdf26d47f78576671c8c52a 100644 (file)
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -134,6 +134,7 @@ public:
        void setUnSAT() { model_print("Setting UNSAT %%%%%%\n"); unsat = true; }
        bool isUnSAT() { return unsat; }
 
        void setUnSAT() { model_print("Setting UNSAT %%%%%%\n"); unsat = true; }
        bool isUnSAT() { return unsat; }
 

+       void printConstraint(BooleanEdge boolean);

        void printConstraints();
 
        Vector<Order *> *getOrders() { return &allOrders;}
        void printConstraints();
 
        Vector<Order *> *getOrders() { return &allOrders;}

diff --git a/src/mymemory.h b/src/mymemory.h
index 9708936e9d829934fd2176053ce37361a8edf6cb..92fb0fed609057c3fd40132bcf507986489133cd 100644 (file)
--- a/src/mymemory.h
+++ b/src/mymemory.h
@@ -26,7 +26,7 @@
    void * ourrealloc(void *ptr, size_t size);
  */
 
    void * ourrealloc(void *ptr, size_t size);
  */
 

-#if 0
+#if 1

 void *model_malloc(size_t size);
 void model_free(void *ptr);
 void *model_calloc(size_t count, size_t size);
 void *model_malloc(size_t size);
 void model_free(void *ptr);
 void *model_calloc(size_t count, size_t size);