mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-23 11:37:54 +00:00
Code Activity

mbqi

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-10-25 10:29:02 -07:00
parent 34e0e26e3d
commit 1ee2ba2a9b
17 changed files with 132 additions and 80 deletions
Download patch file Download diff file Expand all files Collapse all files

23
src/sat/smt/arith_axioms.cpp
View file

@ -296,21 +296,19 @@ namespace arith {
return lp::EQ;
}
void solver::mk_eq_axiom(theory_var v1, theory_var v2) {
void solver::mk_eq_axiom(bool is_eq, theory_var v1, theory_var v2) {
if (is_bool(v1))
return;
expr* e1 = var2expr(v1);
expr* e2 = var2expr(v2);
if (e1 == e2)
if (is_eq && m.are_equal(e1, e2))
return;
if (!is_eq && m.are_distinct(e1, e2))
return;
literal le, ge;
if (a.is_numeral(e1))
std::swap(e1, e2);
if (a.is_numeral(e1)) {
add_unit(~mk_literal(m.mk_eq(e1, e2)));
std::cout << "two numerals\n";
return;
}
SASSERT(!a.is_numeral(e1));
literal eq = eq_internalize(e1, e2);
if (a.is_numeral(e2)) {
le = mk_literal(a.mk_le(e1, e2));
@ -321,8 +319,11 @@ namespace arith {
expr_ref zero(a.mk_numeral(rational(0), a.is_int(e1)), m);
rewrite(diff);
if (a.is_numeral(diff)) {
std::cout << "diff " << diff << " " << mk_pp(e1, m) << " " << mk_pp(e2, m) << "\n";
if (zero == diff)
if (is_eq && a.is_zero(diff))
return;
if (!is_eq && !a.is_zero(diff))
return;
if (a.is_zero(diff))
add_unit(eq);
else
add_unit(~eq);
@ -331,8 +332,8 @@ namespace arith {
le = mk_literal(a.mk_le(diff, zero));
ge = mk_literal(a.mk_ge(diff, zero));
}
std::cout << mk_pp(e1, m) << " " << mk_pp(e2, m) << " ";
std::cout << le << " " << ge << "\n";
// std::cout << "eq " << mk_pp(e1, m) << " " << mk_pp(e2, m) << " ";
// std::cout << le << " " << ge << "\n";
add_clause(~eq, le);
add_clause(~eq, ge);
add_clause(~le, ~ge, eq);

2
src/sat/smt/arith_internalize.cpp
View file

@ -21,6 +21,7 @@ Author:
namespace arith {
sat::literal solver::internalize(expr* e, bool sign, bool root, bool learned) {
force_push();
flet<bool> _is_learned(m_is_redundant, learned);
internalize_atom(e);
literal lit = ctx.expr2literal(e);
@ -30,6 +31,7 @@ namespace arith {
}
void solver::internalize(expr* e, bool redundant) {
force_push();
flet<bool> _is_learned(m_is_redundant, redundant);
if (m.is_bool(e))
internalize_atom(e);

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

@ -583,7 +583,7 @@ namespace arith {
}
void solver::push_core() {
TRACE("arith", tout << "push\n";);
TRACE("arith_verbose", tout << "push\n";);
m_scopes.push_back(scope());
scope& sc = m_scopes.back();
sc.m_bounds_lim = m_bounds_trail.size();
@ -596,11 +596,11 @@ namespace arith {
if (m_nla)
m_nla->push();
th_euf_solver::push_core();
}
void solver::pop_core(unsigned num_scopes) {
TRACE("arith", tout << "pop " << num_scopes << "\n";);
th_euf_solver::pop_core(num_scopes);
unsigned old_size = m_scopes.size() - num_scopes;
del_bounds(m_scopes[old_size].m_bounds_lim);
m_idiv_terms.shrink(m_scopes[old_size].m_idiv_lim);
@ -613,7 +613,8 @@ namespace arith {
m_new_bounds.reset();
if (m_nla)
m_nla->pop(num_scopes);
TRACE("arith", tout << "num scopes: " << num_scopes << " new scope level: " << m_scopes.size() << "\n";);
TRACE("arith_verbose", tout << "num scopes: " << num_scopes << " new scope level: " << m_scopes.size() << "\n";);
th_euf_solver::pop_core(num_scopes);
}
void solver::del_bounds(unsigned old_size) {
@ -964,7 +965,7 @@ namespace arith {
return sat::check_result::CR_CONTINUE;
case l_undef:
TRACE("arith", tout << "check feasible is undef\n";);
return m.inc() ? sat::check_result::CR_CONTINUE : sat::check_result::CR_GIVEUP;
return sat::check_result::CR_CONTINUE;
case l_true:
break;
default:

6
src/sat/smt/arith_solver.h
View file

@ -303,7 +303,7 @@ namespace arith {
void refine_bound(theory_var v, const lp::implied_bound& be);
literal is_bound_implied(lp::lconstraint_kind k, rational const& value, api_bound const& b) const;
void assert_bound(bool is_true, api_bound& b);
void mk_eq_axiom(theory_var v1, theory_var v2);
void mk_eq_axiom(bool is_eq, theory_var v1, theory_var v2);
void assert_idiv_mod_axioms(theory_var u, theory_var v, theory_var w, rational const& r);
api_bound* mk_var_bound(sat::literal lit, theory_var v, lp_api::bound_kind bk, rational const& bound);
lp::lconstraint_kind bound2constraint_kind(bool is_int, lp_api::bound_kind bk, bool is_true);
@ -423,8 +423,8 @@ namespace arith {
void collect_statistics(statistics& st) const override;
euf::th_solver* clone(euf::solver& ctx) override;
bool use_diseqs() const override { return true; }
void new_eq_eh(euf::th_eq const& eq) override { mk_eq_axiom(eq.v1(), eq.v2()); }
void new_diseq_eh(euf::th_eq const& de) override { mk_eq_axiom(de.v1(), de.v2()); }
void new_eq_eh(euf::th_eq const& eq) override { mk_eq_axiom(true, eq.v1(), eq.v2()); }
void new_diseq_eh(euf::th_eq const& de) override { mk_eq_axiom(false, de.v1(), de.v2()); }
bool unit_propagate() override;
void init_model() override;
void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override;

5
src/sat/smt/euf_solver.cpp
View file

@ -402,12 +402,15 @@ namespace euf {
if (!init_relevancy())
give_up = true;
for (auto* e : m_solvers)
for (auto* e : m_solvers) {
if (!m.inc())
return sat::check_result::CR_GIVEUP;
switch (e->check()) {
case sat::check_result::CR_CONTINUE: cont = true; break;
case sat::check_result::CR_GIVEUP: give_up = true; break;
default: break;
}
}
if (cont)
return sat::check_result::CR_CONTINUE;
if (give_up)

5
src/sat/smt/q_mbi.cpp
View file

@ -39,6 +39,7 @@ namespace q {
{
auto* ap = alloc(mbp::arith_project_plugin, m);
ap->set_check_purified(false);
ap->set_apply_projection(true);
add_plugin(ap);
add_plugin(alloc(mbp::datatype_project_plugin, m));
add_plugin(alloc(mbp::array_project_plugin, m));
@ -186,11 +187,13 @@ namespace q {
expr_ref mbqi::solver_project(model& mdl, q_body& qb) {
for (app* v : qb.vars)
m_model->register_decl(v->get_decl(), mdl(v));
std::cout << "Project\n";
std::cout << *m_model << "\n";
std::cout << qb.vbody << "\n";
expr_ref_vector fmls(qb.vbody);
app_ref_vector vars(qb.vars);
mbp::project_plugin proj(m);
proj.purify(m_model_fixer, *m_model, vars, fmls);
std::cout << "fmls\n" << fmls << "\n";
for (unsigned i = 0; i < vars.size(); ++i) {
app* v = vars.get(i);
auto* p = get_plugin(v);

13
src/sat/smt/q_model_fixer.cpp
View file

@ -103,15 +103,17 @@ namespace q {
void model_fixer::add_projection_functions(model& mdl, ptr_vector<quantifier> const& qs) {
func_decl_set fns;
TRACE("q", tout << mdl << "\n";);
collect_partial_functions(qs, fns);
for (func_decl* f : fns)
add_projection_functions(mdl, f);
TRACE("q", tout << mdl << "\n";);
}
void model_fixer::add_projection_functions(model& mdl, func_decl* f) {
// update interpretation of f so that the graph of f is fully determined by the
// ground values of its arguments.
TRACE("q", tout << mdl << "\n";);
func_interp* fi = mdl.get_func_interp(f);
if (!fi)
return;
@ -120,8 +122,12 @@ namespace q {
expr_ref_vector args(m);
for (unsigned i = 0; i < f->get_arity(); ++i)
args.push_back(add_projection_function(mdl, f, i));
if (!fi->get_else() && fi->num_entries() > 0)
fi->set_else(fi->get_entry(ctx.s().rand()(fi->num_entries()))->get_result());
if (!fi->get_else() && fi->num_entries() > 0) {
unsigned idx = ctx.s().rand()(fi->num_entries());
func_entry const* e = fi->get_entry(idx);
fi->set_else(e->get_result());
fi->del_entry(idx);
}
bool has_projection = false;
for (expr* arg : args)
has_projection |= !is_var(arg);
@ -132,7 +138,6 @@ namespace q {
new_fi->set_else(m.mk_app(f_new, args));
mdl.update_func_interp(f, new_fi);
mdl.register_decl(f_new, fi);
TRACE("q", tout << mdl << "\n";);
}
expr_ref model_fixer::add_projection_function(model& mdl, func_decl* f, unsigned idx) {

4
src/sat/smt/sat_th.cpp
View file

@ -217,8 +217,8 @@ namespace euf {
return n;
}
unsigned th_propagation::get_obj_size(unsigned num_lits, unsigned num_eqs) {
return sizeof(th_propagation) + sizeof(sat::literal) * num_lits + sizeof(enode_pair) * num_eqs;
size_t th_propagation::get_obj_size(unsigned num_lits, unsigned num_eqs) {
return sat::constraint_base::obj_size(sizeof(th_propagation) + sizeof(sat::literal) * num_lits + sizeof(enode_pair) * num_eqs);
}
th_propagation::th_propagation(unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs) {

4
src/sat/smt/sat_th.h
View file

@ -161,7 +161,7 @@ namespace euf {
virtual void push_core();
virtual void pop_core(unsigned n);
void force_push() {
CTRACE("euf", m_num_scopes > 0, tout << "push-core " << m_num_scopes << "\n";);
CTRACE("euf_verbose", m_num_scopes > 0, tout << "push-core " << m_num_scopes << "\n";);
for (; m_num_scopes > 0; --m_num_scopes) push_core();
}
@ -194,7 +194,7 @@ namespace euf {
unsigned m_num_eqs;
sat::literal* m_literals;
enode_pair* m_eqs;
static unsigned get_obj_size(unsigned num_lits, unsigned num_eqs);
static size_t get_obj_size(unsigned num_lits, unsigned num_eqs);
th_propagation(unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs);
public:
static th_propagation* mk(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs);