mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
euf solver updates
This commit is contained in:
parent
7bf691e1f9
commit
60ef60dff8
|
@ -142,4 +142,13 @@ namespace euf {
|
|||
return false;
|
||||
return true;
|
||||
}
|
||||
|
||||
unsigned enode::class_generation() {
|
||||
unsigned gen = m_generation;
|
||||
|
||||
for (enode* n : enode_class(this))
|
||||
gen = std::min(n->generation(), gen);
|
||||
return gen;
|
||||
}
|
||||
|
||||
}
|
||||
|
|
|
@ -149,6 +149,7 @@ namespace euf {
|
|||
void set_table_id(unsigned t) { m_table_id = t; }
|
||||
|
||||
unsigned generation() const { return m_generation; }
|
||||
unsigned class_generation();
|
||||
|
||||
void mark1() { m_mark1 = true; }
|
||||
void unmark1() { m_mark1 = false; }
|
||||
|
|
|
@ -215,6 +215,10 @@ namespace euf {
|
|||
return m_values2root;
|
||||
}
|
||||
|
||||
expr* solver::node2value(enode* n) const {
|
||||
return m_values.get(n->get_root_id(), nullptr);
|
||||
}
|
||||
|
||||
void solver::validate_model(model& mdl) {
|
||||
for (enode* n : m_egraph.nodes()) {
|
||||
expr* e = n->get_expr();
|
||||
|
|
|
@ -306,6 +306,7 @@ namespace euf {
|
|||
bool check_model(sat::model const& m) const override;
|
||||
unsigned max_var(unsigned w) const override;
|
||||
|
||||
// proof
|
||||
bool use_drat() { return s().get_config().m_drat && (init_drat(), true); }
|
||||
sat::drat& get_drat() { return s().get_drat(); }
|
||||
void drat_bool_def(sat::bool_var v, expr* n);
|
||||
|
@ -345,6 +346,7 @@ namespace euf {
|
|||
// model construction
|
||||
void update_model(model_ref& mdl);
|
||||
obj_map<expr, enode*> const& values2root();
|
||||
expr* node2value(enode* n) const;
|
||||
|
||||
// diagnostics
|
||||
func_decl_ref_vector const& unhandled_functions() { return m_unhandled_functions; }
|
||||
|
|
|
@ -183,4 +183,25 @@ namespace q {
|
|||
ctx.push(insert_ref2_map<euf::solver, ast_manager, sort, expr>(m, m_unit_table, s, val));
|
||||
return val;
|
||||
}
|
||||
|
||||
unsigned solver::get_max_generation(expr* e) const {
|
||||
unsigned g = 0;
|
||||
expr_fast_mark1 mark;
|
||||
m_todo.push_back(e);
|
||||
while (!m_todo.empty()) {
|
||||
e = m_todo.back();
|
||||
m_todo.pop_back();
|
||||
if (mark.is_marked(e))
|
||||
continue;
|
||||
mark.mark(e);
|
||||
euf::enode* n = ctx.get_egraph().find(e);
|
||||
if (n)
|
||||
g = std::max(g, n->generation());
|
||||
else if (is_app(e))
|
||||
for (expr* arg : *to_app(e))
|
||||
m_todo.push_back(arg);
|
||||
}
|
||||
return g;
|
||||
}
|
||||
|
||||
}
|
||||
|
|
|
@ -44,6 +44,7 @@ namespace q {
|
|||
flat_table m_flat;
|
||||
sat::literal_vector m_universal;
|
||||
obj_map<sort, expr*> m_unit_table;
|
||||
mutable ptr_vector<expr> m_todo;
|
||||
|
||||
sat::literal instantiate(quantifier* q, bool negate, std::function<expr* (quantifier*, unsigned)>& mk_var);
|
||||
sat::literal skolemize(quantifier* q);
|
||||
|
@ -75,5 +76,7 @@ namespace q {
|
|||
ast_manager& get_manager() { return m; }
|
||||
sat::literal_vector const& universal() const { return m_universal; }
|
||||
quantifier* flatten(quantifier* q);
|
||||
|
||||
unsigned get_max_generation(expr* e) const;
|
||||
};
|
||||
}
|
||||
|
|
|
@ -221,6 +221,10 @@ namespace euf {
|
|||
return n;
|
||||
}
|
||||
|
||||
unsigned th_euf_solver::random() {
|
||||
return ctx.s().rand()();
|
||||
}
|
||||
|
||||
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);
|
||||
}
|
||||
|
|
|
@ -187,6 +187,8 @@ namespace euf {
|
|||
bool is_root(theory_var v) const { return var2enode(v)->is_root(); }
|
||||
void push() override { m_num_scopes++; }
|
||||
void pop(unsigned n) override;
|
||||
|
||||
unsigned random();
|
||||
};
|
||||
|
||||
|
||||
|
|
Loading…
Reference in a new issue