Edits
authorbdemsky <bdemsky@uci.edu>
Mon, 23 Oct 2017 07:12:17 +0000 (00:12 -0700)
committerbdemsky <bdemsky@uci.edu>
Mon, 23 Oct 2017 07:12:17 +0000 (00:12 -0700)
src/AST/element.cc
src/common.h
src/csolver.cc
src/csolver.h
src/mymemory.h

index 62e0c4c..f575a90 100644 (file)
@@ -101,7 +101,7 @@ void ElementConst::serialize(Serializer *serializer) {
 }
 
 void ElementConst::print() {
-       model_print("{ElementConst: %lu}\n", value);
+       model_print("{ElementConst: %" PRIu64 "}\n", value);
 }
 
 void ElementFunction::serialize(Serializer *serializer) {
index 52c0b5f..fb4d7ba 100644 (file)
 #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
+#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))
index 756798b..be4a3a8 100644 (file)
@@ -386,7 +386,10 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint
 }
 
 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) {
@@ -470,13 +473,13 @@ int CSolver::solve() {
        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);
@@ -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:
index 15d5b45..2730a93 100644 (file)
@@ -134,6 +134,7 @@ public:
        void setUnSAT() { model_print("Setting UNSAT %%%%%%\n"); unsat = true; }
        bool isUnSAT() { return unsat; }
 
+       void printConstraint(BooleanEdge boolean);
        void printConstraints();
 
        Vector<Order *> *getOrders() { return &allOrders;}
index 9708936..92fb0fe 100644 (file)
@@ -26,7 +26,7 @@
    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);