aboutsummaryrefslogtreecommitdiffstats
path: root/libs
diff options
context:
space:
mode:
Diffstat (limited to 'libs')
-rw-r--r--libs/ezsat/.gitignore5
-rw-r--r--libs/ezsat/Makefile4
-rw-r--r--libs/ezsat/demo_cmp.cc146
-rw-r--r--libs/ezsat/ezminisat.cc15
-rw-r--r--libs/ezsat/ezsat.cc42
5 files changed, 202 insertions, 10 deletions
diff --git a/libs/ezsat/.gitignore b/libs/ezsat/.gitignore
new file mode 100644
index 000000000..e079bd096
--- /dev/null
+++ b/libs/ezsat/.gitignore
@@ -0,0 +1,5 @@
+demo_bit
+demo_cmp
+demo_vec
+puzzle3d
+testbench
diff --git a/libs/ezsat/Makefile b/libs/ezsat/Makefile
index 7a5d5fae4..da2355a9b 100644
--- a/libs/ezsat/Makefile
+++ b/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
diff --git a/libs/ezsat/demo_cmp.cc b/libs/ezsat/demo_cmp.cc
new file mode 100644
index 000000000..b2df8a8d9
--- /dev/null
+++ b/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;
+}
+
diff --git a/libs/ezsat/ezminisat.cc b/libs/ezsat/ezminisat.cc
index fbc85c1ff..a5ceb9e56 100644
--- a/libs/ezsat/ezminisat.cc
+++ b/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;
diff --git a/libs/ezsat/ezsat.cc b/libs/ezsat/ezsat.cc
index cf9dd65b9..f21c8ee2a 100644
--- a/libs/ezsat/ezsat.cc
+++ b/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++;
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-17 21:01:07 +0000