mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

bugfixes in intblast solver

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-12-13 14:13:16 -08:00
parent 4de4618f5b
commit fde64365a3
3 changed files with 10 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/sat/smt/arith_solver.cpp
View file

@ -628,6 +628,9 @@ namespace arith {
}
else if (use_nra_model() && lp().external_to_local(v) != lp::null_lpvar) {
anum const& an = nl_value(v, m_nla->tmp1());
if (a.is_int(o) && !m_nla->am().is_int(an))
value = a.mk_numeral(rational::zero(), a.is_int(o));
else

1
src/sat/smt/intblast_solver.cpp
View file

@ -233,7 +233,6 @@ namespace intblast {
}
m_core.reset();
m_translate.reset();
m_is_plugin = false;
m_solver = mk_smt2_solver(m, s.params(), symbol::null);

11
src/sat/smt/intblast_solver.h
View file

@ -54,6 +54,7 @@ namespace intblast {
scoped_ptr<::solver> m_solver;
obj_map<func_decl, func_decl*> m_new_funs;
expr_ref_vector m_translate, m_args;
ast_ref_vector m_pinned;
sat::literal_vector m_core;
ptr_vector<app> m_bv2int, m_int2bv;
statistics m_stats;
@ -94,8 +95,9 @@ namespace intblast {
void add_value_plugin(euf::enode* n, model& mdl, expr_ref_vector& values);
void add_value_solver(euf::enode* n, model& mdl, expr_ref_vector& values);
bool is_translated(expr* e) const { return !!m_translate.get(e->get_id(), nullptr); }
expr* translated(expr* e) const { expr* r = m_translate.get(e->get_id(), nullptr); SASSERT(r); return r; }
void set_translated(expr* e, expr* r) { SASSERT(r); m_translate.setx(e->get_id(), r); }
void set_translated(expr* e, expr* r);
expr* arg(unsigned i) { return m_args.get(i); }
expr* umod(expr* bv_expr, unsigned i);
@ -112,9 +114,10 @@ namespace intblast {
void ensure_translated(expr* e);
void internalize_bv(app* e);
unsigned m_vars_qhead = 0;
ptr_vector<expr> m_vars;
void add_bound_axioms();
unsigned m_vars_qhead = 0, m_preds_qhead = 0;
ptr_vector<expr> m_vars, m_preds;
bool add_bound_axioms();
bool add_predicate_axioms();
euf::theory_var mk_var(euf::enode* n) override;