From: Clifford Wolf Date: Sat, 8 Jun 2013 10:14:20 +0000 (+0200) Subject: Fixes and improvements in ezSAT library X-Git-Tag: yosys-0.2.0~608 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=25ae2d4df0cf9fcd4069e66d260c207300415af9;p=yosys.git Fixes and improvements in ezSAT library --- 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 + * + * 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 + +#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 va = sat.vec_var("a", 32); + std::vector 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 modelExpressions; + std::vector modelValues, modelMaster; + std::vector modelNames; + +#define X(_n) modelExpressions.push_back(_n); modelNames.push_back(#_n); modelMaster.push_back(_n ## _master); + MONITOR_VARS +#undef X + + std::vector add_ab = sat.vec_add(va, vb); + std::vector sub_ab = sat.vec_sub(va, vb); + std::vector 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 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 &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 &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 args; + lookup_expression(id, op, args); + + if (op == OpNot) { + int idx = bind(args[0]); + cnfClauses.push_back(std::vector(1, -idx)); + cnfClausesCount++; + return; + } + if (op == OpOr) { + std::vector 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(1, bind(arg))); + cnfClausesCount++; + } + return; + } + } + } + int idx = bind(id); cnfClauses.push_back(std::vector(1, idx)); - cnfAssumptions.insert(id); cnfClausesCount++; }