mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-31 16:33:18 +00:00
Code Activity

#5336

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-06-16 18:42:19 -05:00
parent 38fc97d18c
commit 6b5680f13e
2 changed files with 14 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/sat/smt/recfun_solver.cpp
View file

@ -328,5 +328,17 @@ namespace recfun {
} }
return found; return found;
} }
bool solver::add_dep(euf::enode* n, top_sort<euf::enode>& dep) {
if (n->num_args() == 0)
dep.insert(n, nullptr);
for (auto* k : euf::enode_args(n))
dep.add(n, k);
return true;
}
void solver::add_value(euf::enode* n, model& mdl, expr_ref_vector& values) {
values.set(n->get_root_id(), n->get_root()->get_expr());
}
} }

2
src/sat/smt/recfun_solver.h
View file

@ -103,6 +103,8 @@ namespace recfun {
bool unit_propagate() override; bool unit_propagate() override;
sat::literal internalize(expr* e, bool sign, bool root, bool learned) override; sat::literal internalize(expr* e, bool sign, bool root, bool learned) override;
void internalize(expr* e, bool redundant) override; void internalize(expr* e, bool redundant) override;
bool add_dep(euf::enode* n, top_sort<euf::enode>& dep) override;
void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override;
bool is_shared(euf::theory_var v) const override { return true; } bool is_shared(euf::theory_var v) const override { return true; }
void init_search() override {} void init_search() override {}
bool should_research(sat::literal_vector const& core) override; bool should_research(sat::literal_vector const& core) override;