From 3028ceb4199c2742a57ea027df88fb88ec5fea30 Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky@uci.edu>
Date: Tue, 17 Oct 2017 20:26:05 -0700
Subject: [PATCH 1/1] Minimize test case

---
 src/Test/bug_minimal.cc | 68 +++++++++++++++++++++++++++++++++++++++++
 1 file changed, 68 insertions(+)
 create mode 100644 src/Test/bug_minimal.cc

diff --git a/src/Test/bug_minimal.cc b/src/Test/bug_minimal.cc
new file mode 100644
index 0000000..8780b27
--- /dev/null
+++ b/src/Test/bug_minimal.cc
@@ -0,0 +1,68 @@
+
+#include "csolver.h"
+/**
+ * TotalOrder(0, 1, 2, 3, 4, 5, 6, 7, 8, 9)
+ * 0=>1
+ * 1=>2
+ * 2=>3
+ * 1=>4
+ * 4=>5
+ * 5=>6
+ * 1=>7
+ * 7=>8
+ * 8=>9
+ * 9=>2
+ * 6=>2
+ * 
+ * 
+ */
+int main(int numargs, char **argv) {
+	CSolver *solver = new CSolver();
+	uint64_t set1[] = {1, 2, 3, 4, 5, 6, 7, 8, 9};
+	Set *s = solver->createSet(0, set1, 9);
+	Order *order = solver->createOrder(SATC_TOTAL, s);
+	BooleanEdge b12 =  solver->orderConstraint(order, 1, 2);
+	solver->addConstraint(b12);
+	BooleanEdge b23 =  solver->orderConstraint(order, 2, 3);
+	solver->addConstraint(b23);
+	BooleanEdge b14 =  solver->orderConstraint(order, 1, 4);
+	solver->addConstraint(b14);
+	BooleanEdge b45 =  solver->orderConstraint(order, 4, 5);
+	solver->addConstraint(b45);
+	BooleanEdge b56 =  solver->orderConstraint(order, 5, 6);
+	solver->addConstraint(b56);
+	BooleanEdge b17 =  solver->orderConstraint(order, 1, 7);
+	solver->addConstraint(b17);
+	BooleanEdge b78 =  solver->orderConstraint(order, 7, 8);
+	solver->addConstraint(b78);
+	BooleanEdge b89 =  solver->orderConstraint(order, 8, 9);
+	solver->addConstraint(b89);
+	BooleanEdge b92 =  solver->orderConstraint(order, 9, 2);
+	solver->addConstraint(b92);
+	BooleanEdge b62 =  solver->orderConstraint(order, 6, 2);
+	solver->addConstraint(b62);
+
+	BooleanEdge v6 = solver->getBooleanVar(0);
+	BooleanEdge v7 = solver->getBooleanVar(0);
+	BooleanEdge v8 = solver->getBooleanVar(0);
+	solver->addConstraint(solver->applyLogicalOperation(SATC_OR, solver->applyLogicalOperation(SATC_IFF, v7, v8), v6));
+	solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v6));
+	solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v8));
+	BooleanEdge b48 =  solver->orderConstraint(order, 4, 8);
+	solver->addConstraint(b48);
+	BooleanEdge b57 =  solver->orderConstraint(order, 5, 7);
+	solver->addConstraint(b57);
+
+	
+	if (solver->solve() == 1){
+		printf("SAT\n");
+		printf("O(5,1)=%d O(1,4)=%d O(5,4)=%d O(1,5)=%d\n", 
+					 solver->getOrderConstraintValue(order, 5, 1), 
+					 solver->getOrderConstraintValue(order, 1, 4),
+					 solver->getOrderConstraintValue(order, 5, 4),
+					 solver->getOrderConstraintValue(order, 1, 5));
+	} else {
+		printf("UNSAT\n");
+	}
+	delete solver;
+}
-- 
2.34.1