diff --git a/src/ast/euf/euf_ac_plugin.cpp b/src/ast/euf/euf_ac_plugin.cpp index 04ee7afeb..a97d9f63e 100644 --- a/src/ast/euf/euf_ac_plugin.cpp +++ b/src/ast/euf/euf_ac_plugin.cpp @@ -1411,8 +1411,10 @@ namespace euf { m_monomial_table.insert(s1.m, s1); else if (s2.n->get_root() != s1.n->get_root()) { TRACE(plugin, tout << "merge shared " << g.bpp(s1.n->get_root()) << " and " << g.bpp(s2.n->get_root()) << "\n"); - // TODO: non-deterministic parameter evaluation - push_merge(s1.n, s2.n, justification::dependent(m_dep_manager.mk_join(m_dep_manager.mk_leaf(s1.j), m_dep_manager.mk_leaf(s2.j)))); + auto dep1 = m_dep_manager.mk_leaf(s1.j); + auto dep2 = m_dep_manager.mk_leaf(s2.j); + auto joined = m_dep_manager.mk_join(dep1, dep2); + push_merge(s1.n, s2.n, justification::dependent(joined)); } } } @@ -1464,8 +1466,10 @@ namespace euf { } justification ac_plugin::join(justification j, eq const& eq) { - // TODO: non-deterministic parameter evaluation - return justification::dependent(m_dep_manager.mk_join(m_dep_manager.mk_leaf(j), m_dep_manager.mk_leaf(eq.j))); + auto* dep1 = m_dep_manager.mk_leaf(j); + auto* dep2 = m_dep_manager.mk_leaf(eq.j); + auto* joined = m_dep_manager.mk_join(dep1, dep2); + return justification::dependent(joined); } } diff --git a/src/ast/euf/euf_bv_plugin.cpp b/src/ast/euf/euf_bv_plugin.cpp index 0ae215faa..b5755a2c4 100644 --- a/src/ast/euf/euf_bv_plugin.cpp +++ b/src/ast/euf/euf_bv_plugin.cpp @@ -167,8 +167,11 @@ namespace euf { unsigned lo, hi; for (enode* p : enode_parents(x)) { if (is_concat(p, a, b) && is_value(a) && is_value(b)) - // TODO: non-deterministic parameter evaluation - push_merge(mk_concat(a->get_interpreted(), b->get_interpreted()), mk_value_concat(a, b)); + { + enode* concat_interp = mk_concat(a->get_interpreted(), b->get_interpreted()); + enode* concat_value = mk_value_concat(a, b); + push_merge(concat_interp, concat_value); + } if (is_extract(p, lo, hi)) { auto val_p = mod2k(machine_div2k(val_x, lo), hi - lo + 1); @@ -182,8 +185,8 @@ namespace euf { if (is_concat(sib, a, b)) { auto val_a = machine_div2k(val_x, width(b)); auto val_b = mod2k(val_x, width(b)); - // TODO: non-deterministic parameter evaluation - push_merge(mk_concat(mk_value(val_a, width(a)), mk_value(val_b, width(b))), x->get_interpreted()); + enode* concat_value = mk_concat(mk_value(val_a, width(a)), mk_value(val_b, width(b))); + push_merge(concat_value, x->get_interpreted()); } } } @@ -216,9 +219,11 @@ namespace euf { if (is_extract(p1, lo_, hi_) && lo_ == lo && hi_ == hi && p1->get_arg(0)->get_root() == arg_r) return; // add the axiom instead of merge(p, mk_extract(arg, lo, hi)), which would require tracking justifications - // TODO: non-deterministic parameter evaluation - // TODO: non-deterministic parameter evaluation - push_merge(mk_concat(mk_extract(arg, mid + 1, hi), mk_extract(arg, lo, mid)), mk_extract(arg, lo, hi)); + enode* high = mk_extract(arg, mid + 1, hi); + enode* low = mk_extract(arg, lo, mid); + enode* concat = mk_concat(high, low); + enode* whole = mk_extract(arg, lo, hi); + push_merge(concat, whole); }; auto propagate_above = [&](enode* b) { diff --git a/src/smt/dyn_ack.cpp b/src/smt/dyn_ack.cpp index 83c73e070..542b9ae91 100644 --- a/src/smt/dyn_ack.cpp +++ b/src/smt/dyn_ack.cpp @@ -482,11 +482,13 @@ namespace smt { clause_del_eh * del_eh = alloc(dyn_ack_clause_del_eh, *this); justification * js = nullptr; if (m.proofs_enabled()) { - // TODO: non-deterministic parameter evaluation + app_ref eq_n1_r(m.mk_eq(n1, r), m); + app_ref eq_n2_r(m.mk_eq(n2, r), m); + app_ref eq_n1_n2(m.mk_eq(n1, n2), m); js = alloc(dyn_ack_eq_justification, n1, n2, r, - m.mk_eq(n1, r), - m.mk_eq(n2, r), - m.mk_eq(n1, n2)); + eq_n1_r.get(), + eq_n2_r.get(), + eq_n1_n2.get()); } ctx.mark_as_relevant(eq1); ctx.mark_as_relevant(eq2); diff --git a/src/tactic/smtlogics/qfauflia_tactic.cpp b/src/tactic/smtlogics/qfauflia_tactic.cpp index 51aa95a73..594f4c38b 100644 --- a/src/tactic/smtlogics/qfauflia_tactic.cpp +++ b/src/tactic/smtlogics/qfauflia_tactic.cpp @@ -29,16 +29,20 @@ tactic * mk_qfauflia_tactic(ast_manager & m, params_ref const & p) { main_p.set_bool("elim_and", true); main_p.set_bool("som", true); main_p.set_bool("sort_store", true); - + params_ref solver_p; solver_p.set_bool("array.simplify", false); // disable array simplifications at old_simplify module - // TODO: non-deterministic parameter evaluation - tactic * preamble_st = and_then(mk_simplify_tactic(m), - mk_propagate_values_tactic(m), - mk_solve_eqs_tactic(m), - mk_elim_uncnstr_tactic(m), - mk_simplify_tactic(m) + tactic* simplify1 = mk_simplify_tactic(m); + tactic* propagate = mk_propagate_values_tactic(m); + tactic* solve_eqs = mk_solve_eqs_tactic(m); + tactic* elim_unc = mk_elim_uncnstr_tactic(m); + tactic* simplify2 = mk_simplify_tactic(m); + tactic * preamble_st = and_then(simplify1, + propagate, + solve_eqs, + elim_unc, + simplify2 ); tactic * st = and_then(using_params(preamble_st, main_p), diff --git a/src/tactic/smtlogics/qfbv_tactic.cpp b/src/tactic/smtlogics/qfbv_tactic.cpp index 32a5de2a3..df1b92bc2 100644 --- a/src/tactic/smtlogics/qfbv_tactic.cpp +++ b/src/tactic/smtlogics/qfbv_tactic.cpp @@ -57,26 +57,40 @@ static tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p) { hoist_p.set_bool("som", false); hoist_p.set_bool("flat_and_or", false); - return - // TODO: non-deterministic parameter evaluation - and_then( - using_params(mk_simplify_tactic(m), flat_and_or_p), - using_params(mk_propagate_values_tactic(m), flat_and_or_p), - using_params(mk_solve_eqs_tactic(m), solve_eq_p), - mk_elim_uncnstr_tactic(m), - if_no_proofs(if_no_unsat_cores(mk_bv_size_reduction_tactic(m))), - using_params(mk_simplify_tactic(m), simp2_p), + tactic* simplify1 = mk_simplify_tactic(m); + tactic* simplify1_param = using_params(simplify1, flat_and_or_p); + tactic* propagate = mk_propagate_values_tactic(m); + tactic* propagate_param = using_params(propagate, flat_and_or_p); + tactic* solve_eqs = mk_solve_eqs_tactic(m); + tactic* solve_eqs_param = using_params(solve_eqs, solve_eq_p); + tactic* elim_unc = mk_elim_uncnstr_tactic(m); + tactic* size_reduction = mk_bv_size_reduction_tactic(m); + tactic* guarded_size = if_no_proofs(if_no_unsat_cores(size_reduction)); + tactic* simplify2 = mk_simplify_tactic(m); + tactic* simplify2_param = using_params(simplify2, simp2_p); + tactic* simplify3 = mk_simplify_tactic(m); + tactic* simplify3_param = using_params(simplify3, hoist_p); + tactic* max_sharing = mk_max_bv_sharing_tactic(m); + tactic* ackermann = mk_ackermannize_bv_tactic(m,p); + tactic* guarded_ackermann = if_no_proofs(if_no_unsat_cores(ackermann)); - // - // Z3 can solve a couple of extra benchmarks by using hoist_mul - // but the timeout in SMT-COMP is too small. - // Moreover, it impacted negatively some easy benchmarks. - // We should decide later, if we keep it or not. - // - using_params(mk_simplify_tactic(m), hoist_p), - mk_max_bv_sharing_tactic(m), - if_no_proofs(if_no_unsat_cores(mk_ackermannize_bv_tactic(m,p))) - ); + // + // Z3 can solve a couple of extra benchmarks by using hoist_mul + // but the timeout in SMT-COMP is too small. + // Moreover, it impacted negatively some easy benchmarks. + // We should decide later, if we keep it or not. + // + return and_then( + simplify1_param, + propagate_param, + solve_eqs_param, + elim_unc, + guarded_size, + simplify2_param, + simplify3_param, + max_sharing, + guarded_ackermann + ); } static tactic * main_p(tactic* t) { @@ -99,24 +113,32 @@ static tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat solver_p.set_bool("preprocess", false); // preprocessor of smt::context is not needed. tactic* preamble_st = mk_qfbv_preamble(m, p); - tactic * st = main_p(and_then(preamble_st, - // If the user sets HI_DIV0=false, then the formula may contain uninterpreted function - // symbols. In this case, we should not use the `sat', but instead `smt'. Alternatively, - // the UFs can be eliminated by eager ackermannization in the preamble. - cond(mk_is_qfbv_eq_probe(), - and_then(mk_bv1_blaster_tactic(m), - using_params(smt, solver_p)), - cond(mk_is_qfbv_probe(), - and_then(mk_bit_blaster_tactic(m), - // TODO: non-deterministic parameter evaluation - when(mk_lt(mk_memory_probe(), mk_const_probe(MEMLIMIT)), - // TODO: non-deterministic parameter evaluation - and_then(using_params(and_then(mk_simplify_tactic(m), - mk_solve_eqs_tactic(m)), - local_ctx_p), - if_no_proofs(mk_aig_tactic()))), - sat), - smt)))); + tactic* bv1_blaster = mk_bv1_blaster_tactic(m); + tactic* smt_with_solver = using_params(smt, solver_p); + tactic* eq_branch = and_then(bv1_blaster, smt_with_solver); + + tactic* bit_blaster = mk_bit_blaster_tactic(m); + probe* memory_probe = mk_memory_probe(); + probe* mem_limit = mk_const_probe(MEMLIMIT); + probe* memory_ok = mk_lt(memory_probe, mem_limit); + + tactic* simplify4 = mk_simplify_tactic(m); + tactic* solve_eqs4 = mk_solve_eqs_tactic(m); + tactic* simplify_and_solve = and_then(simplify4, solve_eqs4); + tactic* simplify_and_solve_with_params = using_params(simplify_and_solve, local_ctx_p); + tactic* aig = mk_aig_tactic(); + tactic* guarded_aig = if_no_proofs(aig); + tactic* memory_branch = and_then(simplify_and_solve_with_params, guarded_aig); + tactic* when_memory = when(memory_ok, memory_branch); + + tactic* bit_branch = and_then(bit_blaster, when_memory, sat); + tactic* standard_branch = cond(mk_is_qfbv_probe(), bit_branch, smt); + + tactic* combined = cond(mk_is_qfbv_eq_probe(), + eq_branch, + standard_branch); + + tactic * st = main_p(and_then(preamble_st, combined)); st->updt_params(p); return st; @@ -125,11 +147,14 @@ static tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) { - // TODO: non-deterministic parameter evaluation - tactic * new_sat = cond(mk_produce_proofs_probe(), - // TODO: non-deterministic parameter evaluation - and_then(mk_simplify_tactic(m), mk_smt_tactic(m, p)), - mk_psat_tactic(m, p)); + tactic* simplify = mk_simplify_tactic(m); + tactic* smt = mk_smt_tactic(m, p); + tactic* simplify_then_smt = and_then(simplify, smt); + probe* produce_proofs = mk_produce_proofs_probe(); + tactic* psat = mk_psat_tactic(m, p); + tactic * new_sat = cond(produce_proofs, + simplify_then_smt, + psat); return mk_qfbv_tactic(m, p, new_sat, mk_smt_tactic(m, p)); }