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

fixup model generation for theory_intblast

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-10-27 14:08:22 -07:00
parent 7e2acad030
commit 98bc3d392d
4 changed files with 56 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/ast/rewriter/bv2int_translator.cpp
View file

@ -317,7 +317,6 @@ void bv2int_translator::translate_bv(app* e) {
else {
expr* x = arg(0), * y = umod(e, 1);
r = a.mk_int(0);
IF_VERBOSE(2, verbose_stream() << "shl " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n");
for (unsigned i = 0; i < bv.get_bv_size(e); ++i)
r = if_eq(y, i, mul(x, a.mk_int(rational::power_of_two(i))), r);
}
@ -332,7 +331,7 @@ void bv2int_translator::translate_bv(app* e) {
else {
expr* x = arg(0), * y = umod(e, 1);
r = a.mk_int(0);
IF_VERBOSE(2, verbose_stream() << "lshr " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n");
IF_VERBOSE(4, verbose_stream() << "lshr " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n");
for (unsigned i = 0; i < bv.get_bv_size(e); ++i)
r = if_eq(y, i, a.mk_idiv(x, a.mk_int(rational::power_of_two(i))), r);
}
@ -352,7 +351,7 @@ void bv2int_translator::translate_bv(app* e) {
expr* x = umod(e, 0), * y = umod(e, 1);
expr* signx = a.mk_ge(x, a.mk_int(N / 2));
r = m.mk_ite(signx, a.mk_int(-1), a.mk_int(0));
IF_VERBOSE(1, verbose_stream() << "ashr " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n");
IF_VERBOSE(4, verbose_stream() << "ashr " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n");
for (unsigned i = 0; i < sz; ++i) {
expr* d = a.mk_idiv(x, a.mk_int(rational::power_of_two(i)));
r = if_eq(y, i,
@ -363,7 +362,7 @@ void bv2int_translator::translate_bv(app* e) {
break;
case OP_BOR:
// p | q := (p + q) - band(p, q)
IF_VERBOSE(2, verbose_stream() << "bor " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n");
IF_VERBOSE(4, verbose_stream() << "bor " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n");
r = arg(0);
for (unsigned i = 1; i < args.size(); ++i)
r = a.mk_sub(add(r, arg(i)), a.mk_band(bv.get_bv_size(e), r, arg(i)));
@ -372,14 +371,14 @@ void bv2int_translator::translate_bv(app* e) {
r = bnot(band(args));
break;
case OP_BAND:
IF_VERBOSE(2, verbose_stream() << "band " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n");
IF_VERBOSE(4, verbose_stream() << "band " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n");
r = band(args);
break;
case OP_BXNOR:
case OP_BXOR: {
// p ^ q := (p + q) - 2*band(p, q);
unsigned sz = bv.get_bv_size(e);
IF_VERBOSE(2, verbose_stream() << "bxor " << bv.get_bv_size(e) << "\n");
IF_VERBOSE(4, verbose_stream() << "bxor " << bv.get_bv_size(e) << "\n");
r = arg(0);
for (unsigned i = 1; i < args.size(); ++i) {
expr* q = arg(i);

1
src/smt/smt_setup.cpp
View file

@ -699,6 +699,7 @@ namespace smt {
switch (m_params.m_bv_solver) {
case 2:
m_context.register_plugin(alloc(smt::theory_intblast, m_context));
setup_lra_arith();
return;
default:
break;

45
src/smt/theory_intblast.cpp
View file

@ -13,6 +13,7 @@ Author:
#include "smt/smt_context.h"
#include "smt/theory_intblast.h"
#include "smt/smt_model_generator.h"
namespace smt {
@ -134,9 +135,34 @@ namespace smt {
bool theory_intblast::internalize_atom(app * atom, bool gate_ctx) {
return internalize_term(atom);
}
void theory_intblast::apply_sort_cnstr(enode* n, sort* s) {
SASSERT(bv.is_bv_sort(s));
if (!is_attached_to_var(n)) {
m_translator.internalize_bv(n->get_expr());
auto v = mk_var(n);
ctx.attach_th_var(n, this, v);
}
}
bool theory_intblast::internalize_term(app* term) {
ctx.internalize(term->get_args(), term->get_num_args(), false);
m_translator.internalize_bv(term);
enode* n;
if (!ctx.e_internalized(term))
n = ctx.mk_enode(term, false, false, false);
else
n = ctx.get_enode(term);
if (!is_attached_to_var(n)) {
auto v = mk_var(n);
ctx.attach_th_var(n, this, v);
}
if (m.is_bool(term)) {
literal l(ctx.mk_bool_var(term));
ctx.set_var_theory(l.var(), get_id());
}
return true;
}
@ -144,5 +170,24 @@ namespace smt {
m_translator.translate_eq(atom);
}
void theory_intblast::init_model(model_generator& mg) {
m_factory = alloc(bv_factory, m);
mg.register_factory(m_factory);
}
model_value_proc* theory_intblast::mk_value(enode* n, model_generator& mg) {
expr* e = n->get_expr();
SASSERT(bv.is_bv(e));
auto ie = m_translator.translated(e);
expr_ref val(m);
rational r;
if (bv.is_numeral(e, r))
;
else {
VERIFY(ctx.get_value(ctx.get_enode(ie), val));
VERIFY(a.is_numeral(val, r));
}
return alloc(expr_wrapper_proc, m_factory->mk_num_value(r, bv.get_bv_size(e)));
}
}

5
src/smt/theory_intblast.h
View file

@ -21,6 +21,7 @@ Author:
#include "ast/sls/sat_ddfw.h"
#include "smt/smt_theory.h"
#include "model/model.h"
#include "model/numeral_factory.h"
#include "ast/rewriter/bv2int_translator.h"
@ -42,6 +43,7 @@ namespace smt {
bv_util bv;
arith_util a;
unsigned m_vars_qhead = 0, m_preds_qhead = 0;
bv_factory * m_factory = nullptr;
bool add_bound_axioms();
bool add_predicate_axioms();
@ -60,6 +62,9 @@ namespace smt {
bool internalize_atom(app * atom, bool gate_ctx) override;
bool internalize_term(app* term) override;
void internalize_eq_eh(app * atom, bool_var v) override;
void apply_sort_cnstr(enode* n, sort* s) override;
void init_model(model_generator& m) override;
model_value_proc* mk_value(enode* n, model_generator& m) override;
void new_eq_eh(theory_var v1, theory_var v2) override {}
void new_diseq_eh(theory_var v1, theory_var v2) override {}