mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
remove lazy push from theory_lra
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
9b5dc0ca26
commit
727ea43b16
|
|
@ -666,7 +666,7 @@ private:
|
|||
return l_undef;
|
||||
}
|
||||
g = m_subgoals[0];
|
||||
expr_ref_vector atoms(m);
|
||||
func_decl_ref_vector funs(m);
|
||||
m_pc = g->pc();
|
||||
m_mcs.set(m_mcs.size()-1, concat(m_mcs.back(), g->mc()));
|
||||
TRACE("sat", g->display_with_dependencies(tout););
|
||||
|
|
@ -674,13 +674,13 @@ private:
|
|||
// ensure that if goal is already internalized, then import mc from m_solver.
|
||||
|
||||
m_goal2sat(*g, m_params, m_solver, m_map, m_dep2asm, is_incremental());
|
||||
m_goal2sat.get_interpreted_atoms(atoms);
|
||||
m_goal2sat.get_interpreted_funs(funs);
|
||||
if (!m_sat_mc) m_sat_mc = alloc(sat2goal::mc, m);
|
||||
m_sat_mc->flush_smc(m_solver, m_map);
|
||||
if (!atoms.empty()) {
|
||||
if (!funs.empty()) {
|
||||
m_has_uninterpreted = true;
|
||||
std::stringstream strm;
|
||||
strm << "(sat.giveup interpreted atoms sent to SAT solver " << atoms <<")";
|
||||
strm << "(sat.giveup interpreted functions sent to SAT solver " << funs <<")";
|
||||
TRACE("sat", tout << strm.str() << "\n";);
|
||||
IF_VERBOSE(1, verbose_stream() << strm.str() << "\n";);
|
||||
set_reason_unknown(strm.str());
|
||||
|
|
|
|||
|
|
@ -79,6 +79,7 @@ namespace euf {
|
|||
}
|
||||
|
||||
bool solver::propagate(literal l, ext_constraint_idx idx) {
|
||||
force_push();
|
||||
auto* ext = sat::constraint_base::to_extension(idx);
|
||||
SASSERT(ext != this);
|
||||
return ext->propagate(l, idx);
|
||||
|
|
@ -101,17 +102,17 @@ namespace euf {
|
|||
// init_ackerman();
|
||||
|
||||
switch (j.kind()) {
|
||||
case constraint::conflict:
|
||||
case constraint::kind_t::conflict:
|
||||
SASSERT(m_egraph.inconsistent());
|
||||
m_egraph.explain<unsigned>(m_explain);
|
||||
break;
|
||||
case constraint::eq:
|
||||
case constraint::kind_t::eq:
|
||||
n = m_var2node[l.var()].first;
|
||||
SASSERT(n);
|
||||
SASSERT(m_egraph.is_equality(n));
|
||||
m_egraph.explain_eq<unsigned>(m_explain, n->get_arg(0), n->get_arg(1), n->commutative());
|
||||
break;
|
||||
case constraint::lit:
|
||||
case constraint::kind_t::lit:
|
||||
p = m_var2node[l.var()];
|
||||
n = p.first;
|
||||
sign = l.sign() != p.second;
|
||||
|
|
@ -127,8 +128,10 @@ namespace euf {
|
|||
}
|
||||
|
||||
void solver::asserted(literal l) {
|
||||
|
||||
auto* ext = get_solver(l.var());
|
||||
if (ext) {
|
||||
force_push();
|
||||
ext->asserted(l);
|
||||
return;
|
||||
}
|
||||
|
|
@ -136,6 +139,7 @@ namespace euf {
|
|||
auto p = m_var2node.get(l.var(), enode_bool_pair(nullptr, false));
|
||||
if (!p.first)
|
||||
return;
|
||||
force_push();
|
||||
bool sign = p.second != l.sign();
|
||||
euf::enode* n = p.first;
|
||||
expr* e = n->get_owner();
|
||||
|
|
@ -152,7 +156,7 @@ namespace euf {
|
|||
propagate();
|
||||
}
|
||||
|
||||
void solver::propagate() {
|
||||
void solver::propagate() {
|
||||
m_egraph.propagate();
|
||||
if (m_egraph.inconsistent()) {
|
||||
s().set_conflict(sat::justification::mk_ext_justification(s().scope_lvl(), conflict_constraint().to_index()));
|
||||
|
|
@ -196,6 +200,7 @@ namespace euf {
|
|||
}
|
||||
|
||||
sat::check_result solver::check() {
|
||||
force_push();
|
||||
bool give_up = false;
|
||||
bool cont = false;
|
||||
for (auto* e : m_solvers)
|
||||
|
|
@ -212,27 +217,40 @@ namespace euf {
|
|||
}
|
||||
|
||||
void solver::push() {
|
||||
for (auto* e : m_solvers)
|
||||
e->push();
|
||||
m_egraph.push();
|
||||
++m_num_scopes;
|
||||
}
|
||||
|
||||
void solver::force_push() {
|
||||
for (; m_num_scopes > 0; --m_num_scopes) {
|
||||
scope s;
|
||||
s.m_bool_var_lim = m_bool_var_trail.size();
|
||||
s.m_trail_lim = m_trail.size();
|
||||
m_scopes.push_back(s);
|
||||
for (auto* e : m_solvers)
|
||||
e->push();
|
||||
m_egraph.push();
|
||||
}
|
||||
}
|
||||
|
||||
void solver::pop(unsigned n) {
|
||||
m_egraph.pop(n);
|
||||
for (auto* e : m_solvers)
|
||||
e->pop(n);
|
||||
if (n <= m_num_scopes) {
|
||||
m_num_scopes -= n;
|
||||
return;
|
||||
}
|
||||
n -= m_num_scopes;
|
||||
unsigned old_lim = m_bool_var_lim.size() - n;
|
||||
unsigned old_sz = m_bool_var_lim[old_lim];
|
||||
for (unsigned i = m_bool_var_trail.size(); i-- > old_sz; )
|
||||
m_egraph.pop(n);
|
||||
for (auto* e : m_solvers)
|
||||
e->pop(n);
|
||||
|
||||
scope & s = m_scopes[m_scopes.size() - n];
|
||||
|
||||
for (unsigned i = m_bool_var_trail.size(); i-- > s.m_bool_var_lim; )
|
||||
m_var2node[m_bool_var_trail[i]] = enode_bool_pair(nullptr, false);
|
||||
m_bool_var_trail.shrink(old_sz);
|
||||
m_bool_var_lim.shrink(old_lim);
|
||||
m_bool_var_trail.shrink(s.m_bool_var_lim);
|
||||
|
||||
undo_trail_stack(*this, m_trail, s.m_trail_lim);
|
||||
|
||||
m_scopes.shrink(m_scopes.size() - n);
|
||||
}
|
||||
|
||||
void solver::pre_simplify() {
|
||||
|
|
@ -312,6 +330,7 @@ namespace euf {
|
|||
}
|
||||
|
||||
void solver::pop_reinit() {
|
||||
force_push();
|
||||
for (auto* e : m_solvers)
|
||||
e->pop_reinit();
|
||||
}
|
||||
|
|
@ -390,6 +409,7 @@ namespace euf {
|
|||
}
|
||||
|
||||
sat::literal solver::internalize(expr* e, bool sign, bool root) {
|
||||
force_push();
|
||||
auto* ext = get_solver(e);
|
||||
if (ext)
|
||||
return ext->internalize(e, sign, root);
|
||||
|
|
@ -463,8 +483,6 @@ namespace euf {
|
|||
|
||||
void solver::attach_bool_var(sat::bool_var v, bool sign, euf::enode* n) {
|
||||
m_var2node.reserve(v + 1, enode_bool_pair(nullptr, false));
|
||||
for (; m_num_scopes > 0; --m_num_scopes)
|
||||
m_bool_var_lim.push_back(m_bool_var_trail.size());
|
||||
SASSERT(m_var2node[v].first == nullptr);
|
||||
m_var2node[v] = euf::enode_bool_pair(n, sign);
|
||||
m_bool_var_trail.push_back(v);
|
||||
|
|
|
|||
|
|
@ -17,6 +17,7 @@ Author:
|
|||
#pragma once
|
||||
|
||||
#include "util/scoped_ptr_vector.h"
|
||||
#include "util/trail.h"
|
||||
#include "ast/ast_translation.h"
|
||||
#include "ast/euf/euf_egraph.h"
|
||||
#include "smt/params/smt_params.h"
|
||||
|
|
@ -35,12 +36,12 @@ namespace euf {
|
|||
|
||||
class constraint {
|
||||
public:
|
||||
enum kind_t { conflict, eq, lit};
|
||||
enum class kind_t { conflict, eq, lit};
|
||||
private:
|
||||
kind_t m_kind;
|
||||
public:
|
||||
constraint(kind_t k) : m_kind(k) {}
|
||||
unsigned kind() const { return m_kind; }
|
||||
kind_t kind() const { return m_kind; }
|
||||
static constraint* from_idx(size_t z) { return reinterpret_cast<constraint*>(z); }
|
||||
size_t to_index() const { return sat::constraint_base::mem2base(this); }
|
||||
};
|
||||
|
|
@ -53,6 +54,11 @@ namespace euf {
|
|||
stats() { reset(); }
|
||||
void reset() { memset(this, 0, sizeof(*this)); }
|
||||
};
|
||||
struct scope {
|
||||
unsigned m_bool_var_lim;
|
||||
unsigned m_trail_lim;
|
||||
};
|
||||
typedef ptr_vector<trail<solver> > trail_stack;
|
||||
|
||||
ast_manager& m;
|
||||
atom2bool_var& m_expr2var;
|
||||
|
|
@ -60,8 +66,11 @@ namespace euf {
|
|||
smt_params m_config;
|
||||
euf::egraph m_egraph;
|
||||
stats m_stats;
|
||||
sat::solver* m_solver { nullptr };
|
||||
sat::lookahead* m_lookahead { nullptr };
|
||||
|
||||
trail_stack m_trail;
|
||||
|
||||
sat::solver* m_solver { nullptr };
|
||||
sat::lookahead* m_lookahead { nullptr };
|
||||
ast_manager* m_to_m;
|
||||
atom2bool_var* m_to_expr2var;
|
||||
sat::sat_internalizer* m_to_si;
|
||||
|
|
@ -73,7 +82,7 @@ namespace euf {
|
|||
svector<sat::frame> m_stack;
|
||||
unsigned m_num_scopes { 0 };
|
||||
unsigned_vector m_bool_var_trail;
|
||||
unsigned_vector m_bool_var_lim;
|
||||
svector<scope> m_scopes;
|
||||
scoped_ptr_vector<sat::th_solver> m_solvers;
|
||||
ptr_vector<sat::th_solver> m_id2solver;
|
||||
|
||||
|
|
@ -109,11 +118,12 @@ namespace euf {
|
|||
// solving
|
||||
void propagate();
|
||||
void get_antecedents(literal l, constraint& j, literal_vector& r);
|
||||
void force_push();
|
||||
|
||||
constraint& mk_constraint(constraint*& c, constraint::kind_t k);
|
||||
constraint& conflict_constraint() { return mk_constraint(m_conflict, constraint::conflict); }
|
||||
constraint& eq_constraint() { return mk_constraint(m_eq, constraint::eq); }
|
||||
constraint& lit_constraint() { return mk_constraint(m_lit, constraint::lit); }
|
||||
constraint& conflict_constraint() { return mk_constraint(m_conflict, constraint::kind_t::conflict); }
|
||||
constraint& eq_constraint() { return mk_constraint(m_eq, constraint::kind_t::eq); }
|
||||
constraint& lit_constraint() { return mk_constraint(m_lit, constraint::kind_t::lit); }
|
||||
|
||||
public:
|
||||
solver(ast_manager& m, atom2bool_var& expr2var, sat::sat_internalizer& si, params_ref const& p = params_ref()):
|
||||
|
|
|
|||
|
|
@ -66,11 +66,11 @@ struct goal2sat::imp : public sat::sat_internalizer {
|
|||
bool m_ite_extra;
|
||||
unsigned long long m_max_memory;
|
||||
expr_ref_vector m_trail;
|
||||
expr_ref_vector m_interpreted_atoms;
|
||||
func_decl_ref_vector m_interpreted_funs;
|
||||
bool m_default_external;
|
||||
bool m_xor_solver;
|
||||
bool m_euf;
|
||||
|
||||
sat::literal_vector aig_lits;
|
||||
|
||||
imp(ast_manager & _m, params_ref const & p, sat::solver_core & s, atom2bool_var & map, dep2asm_map& dep2asm, bool default_external):
|
||||
m(_m),
|
||||
|
|
@ -80,7 +80,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
|
|||
m_map(map),
|
||||
m_dep2asm(dep2asm),
|
||||
m_trail(m),
|
||||
m_interpreted_atoms(m),
|
||||
m_interpreted_funs(m),
|
||||
m_default_external(default_external) {
|
||||
updt_params(p);
|
||||
m_true = sat::null_literal;
|
||||
|
|
@ -174,7 +174,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
|
|||
return;
|
||||
}
|
||||
else
|
||||
m_interpreted_atoms.push_back(t);
|
||||
m_interpreted_funs.push_back(to_app(t)->get_decl());
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -257,8 +257,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
|
|||
}
|
||||
}
|
||||
|
||||
sat::literal_vector aig_lits;
|
||||
|
||||
void convert_or(app * t, bool root, bool sign) {
|
||||
TRACE("goal2sat", tout << "convert_or:\n" << mk_bounded_pp(t, m, 2) << "\n";);
|
||||
unsigned num = t->get_num_args();
|
||||
|
|
@ -775,8 +773,7 @@ bool goal2sat::has_unsupported_bool(goal const & g) {
|
|||
}
|
||||
|
||||
goal2sat::goal2sat():
|
||||
m_imp(nullptr),
|
||||
m_interpreted_atoms(nullptr) {
|
||||
m_imp(nullptr) {
|
||||
}
|
||||
|
||||
goal2sat::~goal2sat() {
|
||||
|
|
@ -795,23 +792,21 @@ void goal2sat::operator()(goal const & g, params_ref const & p, sat::solver_core
|
|||
|
||||
(*m_imp)(g);
|
||||
|
||||
m_interpreted_atoms = alloc(expr_ref_vector, g.m());
|
||||
m_interpreted_atoms->append(m_imp->m_interpreted_atoms);
|
||||
if (!t.get_extension()) {
|
||||
if (!t.get_extension() && m_imp->m_interpreted_funs.empty()) {
|
||||
dealloc(m_imp);
|
||||
m_imp = nullptr;
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
void goal2sat::get_interpreted_atoms(expr_ref_vector& atoms) {
|
||||
if (m_interpreted_atoms) {
|
||||
atoms.append(*m_interpreted_atoms);
|
||||
void goal2sat::get_interpreted_funs(func_decl_ref_vector& atoms) {
|
||||
if (m_imp) {
|
||||
atoms.append(m_imp->m_interpreted_funs);
|
||||
}
|
||||
}
|
||||
|
||||
bool goal2sat::has_interpreted_atoms() const {
|
||||
return m_interpreted_atoms && !m_interpreted_atoms->empty();
|
||||
bool goal2sat::has_interpreted_funs() const {
|
||||
return m_imp && !m_imp->m_interpreted_funs.empty();
|
||||
}
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -38,7 +38,6 @@ Notes:
|
|||
class goal2sat {
|
||||
struct imp;
|
||||
imp * m_imp;
|
||||
scoped_ptr<expr_ref_vector> m_interpreted_atoms;
|
||||
|
||||
public:
|
||||
goal2sat();
|
||||
|
|
@ -62,9 +61,9 @@ public:
|
|||
*/
|
||||
void operator()(goal const & g, params_ref const & p, sat::solver_core & t, atom2bool_var & m, dep2asm_map& dep2asm, bool default_external = false);
|
||||
|
||||
void get_interpreted_atoms(expr_ref_vector& atoms);
|
||||
void get_interpreted_funs(func_decl_ref_vector& atoms);
|
||||
|
||||
bool has_interpreted_atoms() const;
|
||||
bool has_interpreted_funs() const;
|
||||
|
||||
sat::sat_internalizer& si(ast_manager& m, params_ref const& p, sat::solver_core& t, atom2bool_var& a2b, dep2asm_map& dep2asm, bool default_external = false);
|
||||
|
||||
|
|
|
|||
|
|
@ -112,7 +112,7 @@ class sat_tactic : public tactic {
|
|||
ref<sat2goal::mc> mc;
|
||||
m_sat2goal(*m_solver, map, m_params, *(g.get()), mc);
|
||||
g->add(mc.get());
|
||||
if (produce_core || m_goal2sat.has_interpreted_atoms()) {
|
||||
if (produce_core || m_goal2sat.has_interpreted_funs()) {
|
||||
// sat2goal does not preseve assumptions or assignments to interpreted atoms
|
||||
g->updt_prec(goal::OVER);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -4072,19 +4072,15 @@ void theory_lra::init() {
|
|||
m_imp->init();
|
||||
}
|
||||
bool theory_lra::internalize_atom(app * atom, bool gate_ctx) {
|
||||
force_push();
|
||||
return m_imp->internalize_atom(atom, gate_ctx);
|
||||
}
|
||||
bool theory_lra::internalize_term(app * term) {
|
||||
force_push();
|
||||
return m_imp->internalize_term(term);
|
||||
}
|
||||
void theory_lra::internalize_eq_eh(app * atom, bool_var v) {
|
||||
force_push();
|
||||
m_imp->internalize_eq_eh(atom, v);
|
||||
}
|
||||
void theory_lra::assign_eh(bool_var v, bool is_true) {
|
||||
force_push();
|
||||
m_imp->assign_eh(v, is_true);
|
||||
}
|
||||
lbool theory_lra::get_phase(bool_var v) {
|
||||
|
|
@ -4097,22 +4093,16 @@ bool theory_lra::use_diseqs() const {
|
|||
return m_imp->use_diseqs();
|
||||
}
|
||||
void theory_lra::new_diseq_eh(theory_var v1, theory_var v2) {
|
||||
force_push();
|
||||
m_imp->new_diseq_eh(v1, v2);
|
||||
}
|
||||
void theory_lra::apply_sort_cnstr(enode* n, sort* s) {
|
||||
force_push();
|
||||
m_imp->apply_sort_cnstr(n, s);
|
||||
}
|
||||
void theory_lra::push_scope_eh() {
|
||||
if (lazy_push())
|
||||
return;
|
||||
theory::push_scope_eh();
|
||||
m_imp->push_scope_eh();
|
||||
}
|
||||
void theory_lra::pop_scope_eh(unsigned num_scopes) {
|
||||
if (lazy_pop(num_scopes))
|
||||
return;
|
||||
m_imp->pop_scope_eh(num_scopes);
|
||||
theory::pop_scope_eh(num_scopes);
|
||||
}
|
||||
|
|
@ -4126,7 +4116,6 @@ void theory_lra::init_search_eh() {
|
|||
m_imp->init_search_eh();
|
||||
}
|
||||
final_check_status theory_lra::final_check_eh() {
|
||||
force_push();
|
||||
return m_imp->final_check_eh();
|
||||
}
|
||||
bool theory_lra::is_shared(theory_var v) const {
|
||||
|
|
@ -4136,7 +4125,6 @@ bool theory_lra::can_propagate() {
|
|||
return m_imp->can_propagate();
|
||||
}
|
||||
void theory_lra::propagate() {
|
||||
force_push();
|
||||
m_imp->propagate();
|
||||
}
|
||||
justification * theory_lra::why_is_diseq(theory_var v1, theory_var v2) {
|
||||
|
|
|
|||
Loading…
Reference in a new issue