mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-07 03:31:23 +00:00
Code Activity

add comments

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-08-09 16:31:44 -07:00
parent 52182098d0
commit 75c6d7b5a8
1 changed files with 5 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -156,11 +156,15 @@ namespace synth {
} }
} }
if (m_blockers.size() > m_blockers_qhead)
return;
for (app* e : m_synth) { for (app* e : m_synth) {
// TODO: actually wait to call compute_solution until unit propagation!
euf::enode* n = expr2enode(e->get_arg(0)); euf::enode* n = expr2enode(e->get_arg(0));
if (is_computable(n)) { if (is_computable(n)) {
expr_ref sol = compute_solution(e); expr_ref sol = compute_solution(e);
verbose_stream() << "solution " << sol << "\n"; IF_VERBOSE(0, verbose_stream() << "solution " << sol << "\n");
ctx.push_vec(m_blockers, ~eq_internalize(sol, n->get_expr())); ctx.push_vec(m_blockers, ~eq_internalize(sol, n->get_expr()));
} }
} }