From 77f32c79afdf12f29c040d511cd84f15d703ceb9 Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky@uci.edu>
Date: Mon, 23 Oct 2017 00:12:17 -0700
Subject: [PATCH 1/1] Edits

---
 src/AST/element.cc |  2 +-
 src/common.h       | 21 +++++++++------------
 src/csolver.cc     | 24 +++++++++++++++++-------
 src/csolver.h      |  1 +
 src/mymemory.h     |  2 +-
 5 files changed, 29 insertions(+), 21 deletions(-)

diff --git a/src/AST/element.cc b/src/AST/element.cc
index 62e0c4c..f575a90 100644
--- a/src/AST/element.cc
+++ b/src/AST/element.cc
@@ -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) {
diff --git a/src/common.h b/src/common.h
index 52c0b5f..fb4d7ba 100644
--- a/src/common.h
+++ b/src/common.h
@@ -18,21 +18,18 @@
 #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))
diff --git a/src/csolver.cc b/src/csolver.cc
index 756798b..be4a3a8 100644
--- 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) {
-	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:
diff --git a/src/csolver.h b/src/csolver.h
index 15d5b45..2730a93 100644
--- 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 printConstraint(BooleanEdge boolean);
 	void printConstraints();
 
 	Vector<Order *> *getOrders() { return &allOrders;}
diff --git a/src/mymemory.h b/src/mymemory.h
index 9708936..92fb0fe 100644
--- a/src/mymemory.h
+++ b/src/mymemory.h
@@ -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);
-- 
2.34.1