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

nits, add local functions

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-08-08 16:12:36 -07:00
parent b7d2ba471e
commit 3df12a641f
2 changed files with 33 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -12,7 +12,7 @@ Author:
--*/
#include "ast/synth_decl_plugin.h"
#include "sat/smt/synth_solver.h"
#include "sat/smt/euf_solver.h"
@ -30,44 +30,54 @@ namespace synth {
}
void solver::synthesize(app* e) {
bool solver::synthesize(app* e) {
if (e->get_num_args() == 0)
return false;
auto * n = expr2enode(e->get_arg(0));
expr_ref_vector repr(m);
euf::enode_vector todo;
auto has_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); };
for (unsigned i = 1; i < e->get_num_args(); ++i) {
expr * arg = e->get_arg(i);
auto * narg = expr2enode(arg);
todo.push_back(narg);
repr.setx(narg->get_root_id(), arg);
}
for (unsigned i = 0; i < todo.size() && !repr.get(n->get_root_id(), nullptr); ++i) {
for (unsigned i = 0; i < todo.size() && !has_rep(n); ++i) {
auto * nn = todo[i];
for (auto * p : euf::enode_parents(nn)) {
if (repr.get(p->get_root_id(), nullptr)) continue;
if (all_of(euf::enode_args(p), [&](auto * ch) { return repr.get(ch->get_root_id(), nullptr); })) {
ptr_buffer<expr> args;
for (auto * ch : euf::enode_args(p)) args.push_back(repr.get(ch->get_root_id()));
app * papp = m.mk_app(p->get_decl(), args);
if (has_rep(p))
continue;
if (all_of(euf::enode_args(p), [&](auto * ch) { return has_rep(ch); })) {
ptr_buffer<expr> args;
for (auto * ch : euf::enode_args(p))
args.push_back(get_rep(ch));
app * papp = m.mk_app(p->get_decl(), args);
repr.setx(p->get_root_id(), papp);
todo.push_back(p);
}
}
}
expr * sol = repr.get(n->get_root_id(), nullptr);
if (sol != nullptr) {
sat::literal lit = eq_internalize(n->get_expr(), sol);
add_unit(~lit);
IF_VERBOSE(0, verbose_stream() << mk_pp(sol, m) << "\n");
}
expr * sol = get_rep(n);
if (!sol)
return false;
sat::literal lit = eq_internalize(n->get_expr(), sol);
add_unit(~lit);
IF_VERBOSE(0, verbose_stream() << mk_pp(sol, m) << "\n");
return true;
}
// block current model using realizer by E-graph (and arithmetic)
//
sat::check_result solver::check() {
for (app* e : m_synth) {
synthesize(e);
}
return sat::check_result::CR_CONTINUE;
for (app* e : m_synth)
if (synthesize(e))
sat::check_result::CR_CONTINUE;
return sat::check_result::CR_DONE;
}
// nothing particular to do
@ -103,10 +113,12 @@ namespace synth {
// recognize synthesis objectives here and above
void solver::internalize(expr* e) {
SASSERT(is_app(e));
sat::bool_var bv =ctx.get_si().add_bool_var(e);
sat::bool_var bv = ctx.get_si().add_bool_var(e);
sat::literal lit(bv, false);
ctx.attach_lit(lit, e);
ctx.push_vec(m_synth, to_app(e));
synth::util util(m);
if (util.is_synthesiz3(e))
ctx.push_vec(m_synth, to_app(e));
}
// display current state (eg. current set of realizers)

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

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