mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-18 17:22:15 +00:00
Code Activity

synth

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-08-08 20:39:53 -07:00
parent 90780576f1
commit 0fb7055597
2 changed files with 28 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

46
src/sat/smt/synth_solver.cpp
View file

@ -23,16 +23,17 @@ namespace synth {
solver::~solver() {} solver::~solver() {}
bool solver::synthesize(app* e) { sat::literal solver::synthesize(app* e) {
if (e->get_num_args() == 0) if (e->get_num_args() == 0)
return false; return sat::null_literal;
auto * n = expr2enode(e->get_arg(0)); auto * n = expr2enode(e->get_arg(0));
expr_ref_vector repr(m); expr_ref_vector repr(m);
auto get_rep = [&](euf::enode* n) { return repr.get(n->get_root_id(), nullptr); }; auto get_rep = [&](euf::enode* n) { return repr.get(n->get_root_id(), nullptr); };
auto has_rep = [&](euf::enode* n) { return !!get_rep(n); }; auto has_rep = [&](euf::enode* n) { return !!get_rep(n); };
auto set_rep = [&](euf::enode* n, expr* e) { repr.setx(n->get_root_id(), e); }; auto set_rep = [&](euf::enode* n, expr* e) { repr.setx(n->get_root_id(), e); };
auto is_computable = [&](func_decl* f) { return true; };
euf::enode_vector todo; euf::enode_vector todo;
@ -47,33 +48,40 @@ namespace synth {
for (auto * p : euf::enode_parents(nn)) { for (auto * p : euf::enode_parents(nn)) {
if (has_rep(p)) if (has_rep(p))
continue; continue;
if (all_of(euf::enode_args(p), [&](auto * ch) { return has_rep(ch); })) { if (!is_computable(p->get_decl()))
ptr_buffer<expr> args; continue;
for (auto * ch : euf::enode_args(p)) if (!all_of(euf::enode_args(p), [&](auto * ch) { return has_rep(ch); }))
args.push_back(get_rep(ch)); continue;
app * papp = m.mk_app(p->get_decl(), args); ptr_buffer<expr> args;
set_rep(p, papp); for (auto * ch : euf::enode_args(p))
todo.push_back(p); args.push_back(get_rep(ch));
} app * papp = m.mk_app(p->get_decl(), args);
} set_rep(p, papp);
todo.push_back(p);
}
} }
expr * sol = get_rep(n); expr * sol = get_rep(n);
if (!sol) if (!sol)
return false; return sat::null_literal;
sat::literal lit = eq_internalize(n->get_expr(), sol);
add_unit(~lit);
IF_VERBOSE(0, verbose_stream() << mk_pp(sol, m) << "\n"); IF_VERBOSE(0, verbose_stream() << mk_pp(sol, m) << "\n");
return true; return eq_internalize(n->get_expr(), sol);
} }
// block current model using realizer by E-graph (and arithmetic) // block current model using realizer by E-graph (and arithmetic)
// //
sat::check_result solver::check() { sat::check_result solver::check() {
for (app* e : m_synth) sat::literal_vector clause;
if (synthesize(e)) for (app* e : m_synth) {
sat::check_result::CR_CONTINUE; auto lit = synthesize(e);
return sat::check_result::CR_DONE; if (lit == sat::null_literal)
return sat::check_result::CR_GIVEUP;
clause.push_back(~lit);
}
if (clause.empty())
return sat::check_result::CR_DONE;
add_clause(clause);
return sat::check_result::CR_CONTINUE;
} }
// recognize synthesis objectives here. // recognize synthesis objectives here.

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

@ -39,7 +39,7 @@ namespace synth {
euf::th_solver* clone(euf::solver& ctx) override; euf::th_solver* clone(euf::solver& ctx) override;
private: private:
bool synthesize(app* e); sat::literal synthesize(app* e);
ptr_vector<app> m_synth; ptr_vector<app> m_synth;