From 64e452e086ac0ba91ab2e37ec8688bdfd8e6432a Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Wed, 29 Mar 2023 15:30:05 +0200 Subject: [PATCH] Add some clause names --- src/math/polysat/constraint_manager.cpp | 10 +++++----- src/math/polysat/op_constraint.cpp | 5 +++-- src/math/polysat/op_constraint.h | 12 ++++++------ src/math/polysat/solver.cpp | 12 ++++++++++-- src/math/polysat/solver.h | 2 ++ 5 files changed, 26 insertions(+), 15 deletions(-) diff --git a/src/math/polysat/constraint_manager.cpp b/src/math/polysat/constraint_manager.cpp index 46cf0738f..c55935c33 100644 --- a/src/math/polysat/constraint_manager.cpp +++ b/src/math/polysat/constraint_manager.cpp @@ -397,12 +397,12 @@ namespace polysat { // b = 0 ==> q = -1 // TODO: when a,b become evaluable, can we actually propagate q,r? doesn't seem like it. // Maybe we need something like an op_constraint for better propagation. - s.add_clause(eq(b * q + r - a), false); - s.add_clause(~umul_ovfl(b, q), false); + s.add_clause("[axiom] quot_rem 1", { eq(b * q + r - a) }, false); + s.add_clause("[axiom] quot_rem 2", { ~umul_ovfl(b, q) }, false); // r <= b*q+r // { apply equivalence: p <= q <=> q-p <= -p-1 } // b*q <= -r-1 - s.add_clause(ule(b*q, -r-1), false); + s.add_clause("[axiom] quot_rem 3", { ule(b*q, -r-1) }, false); #if 0 // b*q <= b*q+r // { apply equivalence: p <= q <=> q-p <= -p-1 } @@ -411,8 +411,8 @@ namespace polysat { #endif auto c_eq = eq(b); - s.add_clause(c_eq, ult(r, b), false); - s.add_clause(~c_eq, eq(q + 1), false); + s.add_clause("[axiom] quot_rem 4", { c_eq, ult(r, b) }, false); + s.add_clause("[axiom] quot_rem 5", { ~c_eq, eq(q + 1) }, false); return {std::move(q), std::move(r)}; } diff --git a/src/math/polysat/op_constraint.cpp b/src/math/polysat/op_constraint.cpp index 621b7ebfd..f0c2e6dd7 100644 --- a/src/math/polysat/op_constraint.cpp +++ b/src/math/polysat/op_constraint.cpp @@ -45,6 +45,7 @@ namespace polysat { default: break; } + VERIFY(r.is_var()); } lbool op_constraint::eval() const { @@ -342,12 +343,12 @@ namespace polysat { rational const& q_val = qv.val(); if (q_val >= N) // q >= N ==> r = 0 - return s.mk_clause(~shl, ~s.ule(N, q()), s.eq(r()), true); + return s.mk_clause("shl forward 1", {~shl, ~s.ule(N, q()), s.eq(r())}, true); if (pv.is_val()) { SASSERT(q_val.is_unsigned()); // p = p_val & q = q_val ==> r = p_val * 2^q_val rational const r_val = pv.val() * rational::power_of_two(q_val.get_unsigned()); - return s.mk_clause(~shl, ~s.eq(p(), pv), ~s.eq(q(), qv), s.eq(r(), r_val), true); + return s.mk_clause("shl forward 2", {~shl, ~s.eq(p(), pv), ~s.eq(q(), qv), s.eq(r(), r_val)}, true); } } } diff --git a/src/math/polysat/op_constraint.h b/src/math/polysat/op_constraint.h index 2a205aab7..5258c890c 100644 --- a/src/math/polysat/op_constraint.h +++ b/src/math/polysat/op_constraint.h @@ -27,21 +27,21 @@ namespace polysat { class op_constraint final : public constraint { public: enum class code { - /// r is the logical right shift of p by q + /// r is the logical right shift of p by q. lshr_op, - /// r is the arithmetic right shift of p by q + /// r is the arithmetic right shift of p by q. ashr_op, - /// r is the left shift of p by q + /// r is the left shift of p by q. shl_op, - /// r is the bit-wise 'and' of p and q + /// r is the bit-wise 'and' of p and q. and_op, /// r is the smallest multiplicative pseudo-inverse of p; /// by definition we set r == 0 when p == 0. /// Note that in general, there are 2^parity(p) many pseudo-inverses of p. inv_op, - // r is the quotient of dividing p by q + // r is the quotient of unsigned division of p by q. udiv_op, - // r is the remainder of dividing p by q + // r is the remainder of unsigned division of p by q. urem_op, }; protected: diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index b51862b18..89d09d45a 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -1395,12 +1395,20 @@ namespace polysat { enqueue_pwatch(lit2cnstr(lit).get()); } - void solver::add_clause(unsigned n, signed_constraint const* cs, bool is_redundant) { - clause_ref clause = mk_clause(n, cs, is_redundant); + void solver::add_clause(char const* name, unsigned n, signed_constraint const* cs, bool is_redundant) { + clause_ref clause = mk_clause(name, n, cs, is_redundant); if (clause) add_clause(*clause); } + void solver::add_clause(char const* name, std::initializer_list cs, bool is_redundant) { + add_clause(name, static_cast(cs.size()), std::data(cs), is_redundant); + } + + void solver::add_clause(unsigned n, signed_constraint const* cs, bool is_redundant) { + add_clause("", n, cs, is_redundant); + } + void solver::add_clause(std::initializer_list cs, bool is_redundant) { add_clause(static_cast(cs.size()), std::data(cs), is_redundant); } diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index 4dd49a945..83975ad01 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -327,6 +327,8 @@ namespace polysat { void add_clause(signed_constraint c1, signed_constraint c2, signed_constraint c3, signed_constraint c4, bool is_redundant); void add_clause(std::initializer_list cs, bool is_redundant); void add_clause(unsigned n, signed_constraint const* cs, bool is_redundant); + void add_clause(char const* name, std::initializer_list cs, bool is_redundant); + void add_clause(char const* name, unsigned n, signed_constraint const* cs, bool is_redundant); // Create a clause without adding it to the solver. clause_ref mk_clause(signed_constraint c1, bool is_redundant);