mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

better equality solver for bit-vectors

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-07-29 21:02:57 -07:00
parent 16fb86b636
commit fd66d2f26c
7 changed files with 123 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/ast/rewriter/bv_rewriter.cpp
View file

@ -2108,6 +2108,7 @@ br_status bv_rewriter::mk_bv_not(expr * arg, expr_ref & result) {
}
br_status bv_rewriter::mk_bv_and(unsigned num, expr * const * args, expr_ref & result) {
return BR_FAILED;
ptr_buffer<expr> new_args;
for (unsigned i = 0; i < num; i++) {
new_args.push_back(m_util.mk_bv_not(args[i]));

74
src/ast/simplifiers/extract_eqs.cpp
View file

@ -20,6 +20,7 @@ Author:
#include "ast/for_each_expr.h"
#include "ast/ast_pp.h"
#include "ast/arith_decl_plugin.h"
#include "ast/bv_decl_plugin.h"
#include "ast/simplifiers/extract_eqs.h"
#include "ast/simplifiers/bound_manager.h"
#include "params/tactic_params.hpp"
@ -81,6 +82,76 @@ namespace euf {
}
};
class bv_extract_eq : public extract_eq {
ast_manager& m;
bv_util bv;
bool m_enabled = true;
void solve_add(expr* orig, expr* x, expr* y, expr_dependency* d, dep_eq_vector& eqs) {
if (!bv.is_bv_add(x))
return;
rational r, r_inverse;
unsigned i = 0;
expr_ref term(m);
expr* u, *z;
auto mk_term = [&](unsigned i) {
term = y;
unsigned j = 0;
for (expr* arg2 : *to_app(x)) {
if (i != j)
term = bv.mk_bv_sub(term, arg2);
++j;
}
};
unsigned sz;
for (expr* arg : *to_app(x)) {
if (is_uninterp_const(arg)) {
mk_term(i);
eqs.push_back(dependent_eq(orig, to_app(arg), term, d));
}
else if (bv.is_bv_mul(arg, u, z) && bv.is_numeral(u, r, sz) && is_uninterp_const(z) && r.is_odd()) {
r.mult_inverse(sz, r_inverse);
mk_term(i);
term = bv.mk_bv_mul(bv.mk_numeral(r_inverse, sz), term);
eqs.push_back(dependent_eq(orig, to_app(z), term, d));
}
++i;
}
}
void solve_eq(expr* orig, expr* x, expr* y, expr_dependency* d, dep_eq_vector& eqs) {
solve_add(orig, x, y, d, eqs);
}
public:
bv_extract_eq(ast_manager& m): m(m), bv(m) {}
void get_eqs(dependent_expr const& e, dep_eq_vector& eqs) override {
if (!m_enabled)
return;
auto [f, p, d] = e();
expr* x, * y;
if (m.is_eq(f, x, y) && bv.is_bv(x)) {
solve_eq(f, x, y, d, eqs);
solve_eq(f, y, x, d, eqs);
}
}
void pre_process(dependent_expr_state& fmls) override {
}
void updt_params(params_ref const& p) override {
tactic_params tp(p);
m_enabled = p.get_bool("theory_solver", tp.solve_eqs_ite_solver());
}
};
class arith_extract_eq : public extract_eq {
ast_manager& m;
arith_util a;
@ -254,7 +325,7 @@ break;
}
}
void solve_eq(expr* orig, expr* x, expr* y, expr_dependency* d, dep_eq_vector& eqs) {
void solve_eq(expr* orig, expr* x, expr* y, expr_dependency* d, dep_eq_vector& eqs) {
solve_add(orig, x, y, d, eqs);
solve_mod(orig, x, y, d, eqs);
solve_mul(orig, x, y, d, eqs);
@ -311,5 +382,6 @@ break;
void register_extract_eqs(ast_manager& m, scoped_ptr_vector<extract_eq>& ex) {
ex.push_back(alloc(arith_extract_eq, m));
ex.push_back(alloc(basic_extract_eq, m));
ex.push_back(alloc(bv_extract_eq, m));
}
}

7
src/sat/smt/polysat/core.cpp
View file

@ -212,9 +212,11 @@ namespace polysat {
sat::check_result core::check() {
lbool r = l_true;
verbose_stream() << "check-propagate\n";
if (propagate())
return sat::check_result::CR_CONTINUE;
verbose_stream() << "check-assign-variable\n";
switch (assign_variable()) {
case l_true:
break;
@ -228,6 +230,7 @@ namespace polysat {
break;
}
verbose_stream() << "check-saturate\n";
saturation saturate(*this);
switch (saturate()) {
case l_true:
@ -240,7 +243,8 @@ namespace polysat {
r = l_undef;
break;
}
verbose_stream() << "check-refine\n";
switch (m_monomials.refine()) {
case l_true:
break;
@ -253,6 +257,7 @@ namespace polysat {
break;
}
verbose_stream() << "check-blast\n";
switch (m_monomials.bit_blast()) {
case l_true:
break;

2
src/sat/smt/polysat/op_constraint.cpp
View file

@ -456,6 +456,8 @@ namespace polysat {
auto rv = c.subst(r);
auto& C = c.cs();
verbose_stream() << "saturate and: " << p << " & " << q << " = " << r << "\n";
if (!pv.is_val() || !qv.is_val() || !rv.is_val())
return false;

2
src/sat/smt/polysat/saturation.cpp
View file

@ -359,7 +359,9 @@ namespace polysat {
if (a.degree(v) < r.degree(v))
return;
verbose_stream() << "resolve: " << a << " = " << b << " => " << r << "\n";
add_clause("ax + b = 0 & cx + d = 0 ==> cb - da = 0", { i.dep(), j.dep(), C.eq(r) }, true);
exit(0);
}

2
src/sat/smt/polysat/viable.cpp
View file

@ -868,7 +868,7 @@ v0[19] := 0 v0 [-131062 ; 0[ := [-131062;0[ src ~4 <= 43691*v0;
}
}
IF_VERBOSE(1, {
IF_VERBOSE(3, {
for (auto const& e : m_explain)
if (e.mark)
display_explain(verbose_stream() << "redundant: ", e) << "\n";

40
src/sat/smt/polysat_internalize.cpp
View file

@ -18,6 +18,7 @@ Author:
#include "params/bv_rewriter_params.hpp"
#include "sat/smt/polysat_solver.h"
#include "sat/smt/euf_solver.h"
#include "ast/rewriter/bit_blaster/bit_blaster.h"
namespace polysat {
@ -159,7 +160,9 @@ namespace polysat {
m_delayed_axioms.push_back(a);
ctx.push(push_back_vector(m_delayed_axioms));
break;
case OP_BIT2BOOL:
internalize_bit2bool(a);
break;
default:
IF_VERBOSE(0, verbose_stream() << mk_pp(a, m) << "\n");
NOT_IMPLEMENTED_YET();
@ -286,6 +289,16 @@ namespace polysat {
m_core.shl(expr2pdd(x), expr2pdd(y), expr2pdd(n));
}
void solver::internalize_bit2bool(app* n) {
expr* b = nullptr;
unsigned idx;
VERIFY(bv.is_bit2bool(n, b, idx));
pdd p = expr2pdd(b);
auto sc = m_core.bit(p, idx);
add_axiom("bit2bool", { eq_internalize(n, constraint2expr(sc)) });
}
bool solver::propagate_delayed_axioms() {
if (m_delayed_axioms_qhead == m_delayed_axioms.size())
return false;
@ -687,7 +700,7 @@ namespace polysat {
void solver::internalize_mul(app* a) {
vector<dd::pdd> args;
for (expr* arg : *to_app(a))
for (expr* arg : *a)
args.push_back(expr2pdd(arg));
if (args.size() == 1) {
internalize_set(a, args[0]);
@ -701,6 +714,29 @@ namespace polysat {
internalize_set(a, args[0] * args[1]);
return;
}
#if 0
// experiment with eagerly bit-blasting multiplication.
if (args.size() == 2) {
unsigned sz = bv.get_bv_size(a);
expr_ref_vector xs(m), ys(m), zs(m);
for (unsigned i = 0; i < sz; ++i) {
xs.push_back(bv.mk_bit2bool(a->get_arg(0), i));
ys.push_back(bv.mk_bit2bool(a->get_arg(1), i));
}
bit_blaster_params p;
bit_blaster bb(m, p);
bb.mk_multiplier(xs.size(), xs.data(), ys.data(), zs);
pdd z = expr2pdd(a);
for (unsigned i = 0; i < sz; ++i) {
// sat::literal bit_i = ctx.internalize(zs.get(i), false, false);
auto sc = m_core.bit(z, i);
add_axiom("mul", { eq_internalize(constraint2expr(sc), zs.get(i)) });
}
return;
}
#endif
auto pv = m_core.mul(args.size(), args.data());
m_pddvar2var.setx(pv, get_th_var(a), UINT_MAX);
internalize_set(a, m_core.var(pv));