Fixes and improvements in ezSAT library

libs/ezsat/.gitignore

@@ -0,0 +1,5 @@
+demo_bit
+demo_cmp
+demo_vec
+puzzle3d
+testbench

libs/ezsat/Makefile

@@ -5,10 +5,11 @@ CXXFLAGS = -MD -Wall -Wextra -ggdb
 CXXFLAGS += -std=c++11 -O0
 LDLIBS = -lminisat -lstdc++
 
-all: demo_vec demo_bit testbench puzzle3d
+all: demo_vec demo_bit demo_cmp testbench puzzle3d
 
 demo_vec: demo_vec.o ezsat.o ezminisat.o
 demo_bit: demo_bit.o ezsat.o ezminisat.o
+demo_cmp: demo_cmp.o ezsat.o ezminisat.o
 testbench: testbench.o ezsat.o ezminisat.o
 puzzle3d: puzzle3d.o ezsat.o ezminisat.o
 
@@ -16,6 +17,7 @@ test: all
 	./testbench
 	./demo_bit
 	./demo_vec
+	./demo_cmp
 
 clean:
 	rm -f demo_bit demo_vec testbench puzzle3d *.o *.d

libs/ezsat/demo_cmp.cc

@@ -0,0 +1,146 @@
+/*
+ *  ezSAT -- A simple and easy to use CNF generator for SAT solvers
+ *
+ *  Copyright (C) 2013  Clifford Wolf <clifford@clifford.at>
+ *  
+ *  Permission to use, copy, modify, and/or distribute this software for any
+ *  purpose with or without fee is hereby granted, provided that the above
+ *  copyright notice and this permission notice appear in all copies.
+ *  
+ *  THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+ *  WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+ *  MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+ *  ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+ *  WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+ *  ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+ *  OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+ *
+ */
+
+#include "ezminisat.h"
+#include <assert.h>
+
+#define INIT_X 123456789
+#define INIT_Y 362436069
+#define INIT_Z 521288629
+#define INIT_W  88675123
+
+uint32_t xorshift128() {
+	static uint32_t x = INIT_X;
+	static uint32_t y = INIT_Y;
+	static uint32_t z = INIT_Z;
+	static uint32_t w = INIT_W;
+	uint32_t t = x ^ (x << 11);
+	x = y; y = z; z = w;
+	w ^= (w >> 19) ^ t ^ (t >> 8);
+	return w;
+}
+
+void test_cmp(uint32_t a, uint32_t b)
+{
+	ezMiniSAT sat;
+
+	printf("A = %10u (%10d)\n", a, int32_t(a));
+	printf("B = %10u (%10d)\n", b, int32_t(b));
+	printf("\n");
+
+	std::vector<int> va = sat.vec_var("a", 32);
+	std::vector<int> vb = sat.vec_var("b", 32);
+
+	sat.vec_set_unsigned(va, a);
+	sat.vec_set_unsigned(vb, b);
+
+#define MONITOR_VARS \
+	X(carry) X(overflow) X(sign) X(zero) \
+	X(lt_signed) X(le_signed) X(ge_signed) X(gt_signed) \
+	X(lt_unsigned) X(le_unsigned) X(ge_unsigned) X(gt_unsigned)
+
+#define X(_n) int _n; bool _n ## _master;
+	MONITOR_VARS
+#undef X
+
+	carry_master = ((uint64_t(a) - uint64_t(b)) >> 32) & 1;
+	overflow_master = (int32_t(a) - int32_t(b)) != (int64_t(int32_t(a)) - int64_t(int32_t(b)));
+	sign_master = ((a - b) >> 31) & 1;
+	zero_master = a == b;
+
+	sat.vec_cmp(va, vb, carry, overflow, sign, zero);
+
+	lt_signed_master = int32_t(a) <  int32_t(b);
+	le_signed_master = int32_t(a) <= int32_t(b);
+	ge_signed_master = int32_t(a) >= int32_t(b);
+	gt_signed_master = int32_t(a) >  int32_t(b);
+
+	lt_unsigned_master = a <  b;
+	le_unsigned_master = a <= b;
+	ge_unsigned_master = a >= b;
+	gt_unsigned_master = a >  b;
+
+	lt_signed = sat.vec_lt_signed(va, vb);
+	le_signed = sat.vec_le_signed(va, vb);
+	ge_signed = sat.vec_ge_signed(va, vb);
+	gt_signed = sat.vec_gt_signed(va, vb);
+
+	lt_unsigned = sat.vec_lt_unsigned(va, vb);
+	le_unsigned = sat.vec_le_unsigned(va, vb);
+	ge_unsigned = sat.vec_ge_unsigned(va, vb);
+	gt_unsigned = sat.vec_gt_unsigned(va, vb);
+
+	std::vector<int> modelExpressions;
+	std::vector<bool> modelValues, modelMaster;
+	std::vector<std::string> modelNames;
+
+#define X(_n) modelExpressions.push_back(_n); modelNames.push_back(#_n); modelMaster.push_back(_n ## _master);
+	MONITOR_VARS
+#undef X
+
+	std::vector<int> add_ab = sat.vec_add(va, vb);
+	std::vector<int> sub_ab = sat.vec_sub(va, vb);
+	std::vector<int> sub_ba = sat.vec_sub(vb, va);
+
+	sat.vec_append(modelExpressions, add_ab);
+	sat.vec_append(modelExpressions, sub_ab);
+	sat.vec_append(modelExpressions, sub_ba);
+
+	if (!sat.solve(modelExpressions, modelValues)) {
+		fprintf(stderr, "SAT solver failed to find a model!\n");
+		abort();
+	}
+
+	bool found_error = false;
+
+	for (size_t i = 0; i < modelMaster.size(); i++) {
+		if (modelMaster.at(i) != int(modelValues.at(i)))
+			found_error = true;
+		printf("%-20s %d%s\n", modelNames.at(i).c_str(), int(modelValues.at(i)),
+				modelMaster.at(i) != modelValues.at(i) ? "   !!!" : "");
+	}
+	printf("\n");
+
+	uint32_t add_ab_value = sat.vec_model_get_unsigned(modelExpressions, modelValues, add_ab);
+	uint32_t sub_ab_value = sat.vec_model_get_unsigned(modelExpressions, modelValues, sub_ab);
+	uint32_t sub_ba_value = sat.vec_model_get_unsigned(modelExpressions, modelValues, sub_ba);
+
+	printf("%-20s %10u %10u%s\n", "result(a+b)", add_ab_value, a+b, add_ab_value != a+b ? "   !!!" : "");
+	printf("%-20s %10u %10u%s\n", "result(a-b)", sub_ab_value, a-b, sub_ab_value != a-b ? "   !!!" : "");
+	printf("%-20s %10u %10u%s\n", "result(b-a)", sub_ba_value, b-a, sub_ba_value != b-a ? "   !!!" : "");
+	printf("\n");
+
+	if (found_error || add_ab_value != a+b || sub_ab_value != a-b || sub_ba_value != b-a)
+		abort();
+}
+
+int main()
+{
+	printf("\n");
+	for (int i = 0; i < 1024; i++) {
+		printf("************** %d **************\n\n", i);
+		uint32_t a = xorshift128();
+		uint32_t b = xorshift128();
+		if (xorshift128() % 16 == 0)
+			a = b;
+		test_cmp(a, b);
+	}
+	return 0;
+}
+

libs/ezsat/ezminisat.cc

@@ -86,9 +86,9 @@ contradiction:
 		Minisat::vec<Minisat::Lit> ps;
 		for (auto idx : clause)
 			if (idx > 0)
-				ps.push(Minisat::mkLit(minisatVars[idx-1]));
+				ps.push(Minisat::mkLit(minisatVars.at(idx-1)));
 			else
-				ps.push(Minisat::mkLit(minisatVars[-idx-1], true));
+				ps.push(Minisat::mkLit(minisatVars.at(-idx-1), true));
 		if (!minisatSolver->addClause(ps))
 			goto contradiction;
 	}
@@ -100,9 +100,9 @@ contradiction:
 
 	for (auto idx : extraClauses)
 		if (idx > 0)
-			assumps.push(Minisat::mkLit(minisatVars[idx-1]));
+			assumps.push(Minisat::mkLit(minisatVars.at(idx-1)));
 		else
-			assumps.push(Minisat::mkLit(minisatVars[-idx-1], true));
+			assumps.push(Minisat::mkLit(minisatVars.at(-idx-1), true));
 
 	if (!minisatSolver->solve(assumps))
 		return false;
@@ -110,9 +110,12 @@ contradiction:
 	modelValues.clear();
 	modelValues.reserve(modelIdx.size());
 	for (auto idx : modelIdx) {
-		auto value = minisatSolver->modelValue(minisatVars[idx-1]);
+		bool refvalue = true;
+		if (idx < 0)
+			idx = -idx, refvalue = false;
+		auto value = minisatSolver->modelValue(minisatVars.at(idx-1));
 		// FIXME: Undef values
-		modelValues.push_back(value == Minisat::lbool(true));
+		modelValues.push_back(value == Minisat::lbool(refvalue));
 	}
 
 	return true;

libs/ezsat/ezsat.cc

@@ -129,7 +129,7 @@ int ezSAT::expression(OpId op, const std::vector<int> &args)
 		if (myArgs.size() == 0)
 			return xorRemovedOddTrues ? TRUE : FALSE;
 		if (myArgs.size() == 1)
-			return myArgs[0];
+			return xorRemovedOddTrues ? NOT(myArgs[0]) : myArgs[0];
 		break;
 
 	case OpIFF:
@@ -162,7 +162,7 @@ int ezSAT::expression(OpId op, const std::vector<int> &args)
 		expressions.push_back(myExpr);
 	}
 
-	return xorRemovedOddTrues ? expression(OpNot, id) : id;
+	return xorRemovedOddTrues ? NOT(id) : id;
 }
 
 void ezSAT::lookup_literal(int id, std::string &name) const
@@ -341,9 +341,45 @@ void ezSAT::clear()
 
 void ezSAT::assume(int id)
 {
+	cnfAssumptions.insert(id);
+
+	if (id < 0)
+	{
+		assert(0 < -id && -id <= int(expressions.size()));
+		cnfExpressionVariables.resize(expressions.size());
+
+		if (cnfExpressionVariables[-id-1] == 0)
+		{
+			OpId op;
+			std::vector<int> args;
+			lookup_expression(id, op, args);
+
+			if (op == OpNot) {
+				int idx = bind(args[0]);
+				cnfClauses.push_back(std::vector<int>(1, -idx));
+				cnfClausesCount++;
+				return;
+			}
+			if (op == OpOr) {
+				std::vector<int> clause;
+				for (int arg : args)
+					clause.push_back(bind(arg));
+				cnfClauses.push_back(clause);
+				cnfClausesCount++;
+				return;
+			}
+			if (op == OpAnd) {
+				for (int arg : args) {
+					cnfClauses.push_back(std::vector<int>(1, bind(arg)));
+					cnfClausesCount++;
+				}
+				return;
+			}
+		}
+	}
+
 	int idx = bind(id);
 	cnfClauses.push_back(std::vector<int>(1, idx));
-	cnfAssumptions.insert(id);
 	cnfClausesCount++;
 }