diff --git a/src/qe/nlarith_util.cpp b/src/qe/nlarith_util.cpp index 879000d25..7bccba885 100644 --- a/src/qe/nlarith_util.cpp +++ b/src/qe/nlarith_util.cpp @@ -555,8 +555,16 @@ namespace nlarith { tout << " 0 [-oo] --> " << mk_pp(t1.get(), m()) << "\n";); } TRACE(nlarith, tout << "inf-branch\n";); - // TODO: non-deterministic parameter evaluation - bc.add_branch(mk_and(es.size(), es.data()), m().mk_true(), subst, mk_inf(bc), z(), z(), z()); + expr_ref branch_expr(m()); + branch_expr = mk_and(es.size(), es.data()); + expr_ref true_expr(m()); + true_expr = m().mk_true(); + expr_ref inf_branch_expr(m()); + inf_branch_expr = mk_inf(bc); + expr* z1 = z(); + expr* z2 = z(); + expr* z3 = z(); + bc.add_branch(branch_expr, true_expr, subst, inf_branch_expr, z1, z2, z3); } void create_branch_l(unsigned j, unsigned i, polys const& polys, comps const& comps, @@ -588,8 +596,13 @@ namespace nlarith { es.push_back(m().mk_implies(bc.preds(k), t2)); subst.push_back(t1); } - // TODO: non-deterministic parameter evaluation - bc.add_branch(mk_and(es.size(), es.data()), cond, subst, mk_def(cmp, abc_poly(*this, z(), b, c), e0), a, b, c); + expr_ref branch_expr(m()); + branch_expr = mk_and(es.size(), es.data()); + app* z_val = z(); + abc_poly abc1(*this, z_val, b, c); + expr_ref def_expr(m()); + def_expr = mk_def(cmp, abc1, e0); + bc.add_branch(branch_expr, cond, subst, def_expr, a, b, c); } if (i == j && a != z()) { @@ -608,8 +621,13 @@ namespace nlarith { es.push_back(m().mk_implies(bc.preds(k), t1)); subst.push_back(t1); } - // TODO: non-deterministic parameter evaluation - bc.add_branch(mk_and(es.size(), es.data()), cond, subst, mk_def(cmp, abc_poly(*this, a2, b, z()),e1), a, b, c); + expr_ref branch_expr2(m()); + branch_expr2 = mk_and(es.size(), es.data()); + app* z_val2 = z(); + abc_poly abc2(*this, a2, b, z_val2); + expr_ref def_expr2(m()); + def_expr2 = mk_def(cmp, abc2, e1); + bc.add_branch(branch_expr2, cond, subst, def_expr2, a, b, c); } } diff --git a/src/tactic/ufbv/ufbv_tactic.cpp b/src/tactic/ufbv/ufbv_tactic.cpp index e1154f043..6998b3a22 100644 --- a/src/tactic/ufbv/ufbv_tactic.cpp +++ b/src/tactic/ufbv/ufbv_tactic.cpp @@ -32,43 +32,92 @@ Notes: static tactic * mk_der_fp_tactic(ast_manager & m, params_ref const & p) { - // TODO: non-deterministic parameter evaluation - return repeat(and_then(mk_der_tactic(m), mk_simplify_tactic(m, p)), 5); + tactic * der = mk_der_tactic(m); + tactic * simplify = mk_simplify_tactic(m, p); + tactic * seq = and_then(der, simplify); + tactic * result = repeat(seq, 5); + return result; } static tactic * mk_ufbv_preprocessor_tactic(ast_manager & m, params_ref const & p) { params_ref no_elim_and(p); no_elim_and.set_bool("elim_and", false); - // TODO: non-deterministic parameter evaluation - return and_then( - mk_trace_tactic("ufbv_pre"), - // TODO: non-deterministic parameter evaluation - and_then(mk_simplify_tactic(m, p), - mk_propagate_values_tactic(m, p), - and_then(if_no_proofs(if_no_unsat_cores(using_params(mk_macro_finder_tactic(m, no_elim_and), no_elim_and))), - mk_simplify_tactic(m, p)), - // TODO: non-deterministic parameter evaluation - and_then(mk_snf_tactic(m, p), mk_simplify_tactic(m, p)), - mk_elim_and_tactic(m, p), - mk_solve_eqs_tactic(m, p), - // TODO: non-deterministic parameter evaluation - and_then(mk_der_fp_tactic(m, p), mk_simplify_tactic(m, p)), - // TODO: non-deterministic parameter evaluation - and_then(mk_distribute_forall_tactic(m, p), mk_simplify_tactic(m, p))), - if_no_unsat_cores( - // TODO: non-deterministic parameter evaluation - and_then(and_then(mk_reduce_args_tactic(m, p), mk_simplify_tactic(m, p)), - // TODO: non-deterministic parameter evaluation - and_then(mk_macro_finder_tactic(m, p), mk_simplify_tactic(m, p)), - // TODO: non-deterministic parameter evaluation - and_then(mk_ufbv_rewriter_tactic(m, p), mk_simplify_tactic(m, p)), - // TODO: non-deterministic parameter evaluation - and_then(mk_quasi_macros_tactic(m, p), mk_simplify_tactic(m, p)))), - // TODO: non-deterministic parameter evaluation - and_then(mk_der_fp_tactic(m, p), mk_simplify_tactic(m, p)), - mk_simplify_tactic(m, p), - mk_trace_tactic("ufbv_post")); + tactic * trace_pre = mk_trace_tactic("ufbv_pre"); + + tactic * simplify1 = mk_simplify_tactic(m, p); + tactic * propagate_values = mk_propagate_values_tactic(m, p); + + tactic * macro_no_elim = mk_macro_finder_tactic(m, no_elim_and); + tactic * macro_with_params = using_params(macro_no_elim, no_elim_and); + tactic * unsat_guard = if_no_unsat_cores(macro_with_params); + tactic * proofs_guard = if_no_proofs(unsat_guard); + tactic * simplify_after_guard = mk_simplify_tactic(m, p); + tactic * guard_chain = and_then(proofs_guard, simplify_after_guard); + + tactic * snf_tac = mk_snf_tactic(m, p); + tactic * simplify_after_snf = mk_simplify_tactic(m, p); + tactic * snf_chain = and_then(snf_tac, simplify_after_snf); + + tactic * elim_and_tac = mk_elim_and_tactic(m, p); + tactic * solve_eqs_tac = mk_solve_eqs_tactic(m, p); + + tactic * der_fp_tac = mk_der_fp_tactic(m, p); + tactic * simplify_after_der = mk_simplify_tactic(m, p); + tactic * der_chain = and_then(der_fp_tac, simplify_after_der); + + tactic * distribute_forall = mk_distribute_forall_tactic(m, p); + tactic * simplify_after_distribute = mk_simplify_tactic(m, p); + tactic * distribute_chain = and_then(distribute_forall, simplify_after_distribute); + + tactic * preprocess_seq = and_then( + simplify1, + propagate_values, + guard_chain, + snf_chain, + elim_and_tac, + solve_eqs_tac, + der_chain, + distribute_chain); + + tactic * reduce_args_tac = mk_reduce_args_tactic(m, p); + tactic * simplify_after_reduce = mk_simplify_tactic(m, p); + tactic * reduce_chain = and_then(reduce_args_tac, simplify_after_reduce); + + tactic * macro_finder_tac = mk_macro_finder_tactic(m, p); + tactic * simplify_after_macro = mk_simplify_tactic(m, p); + tactic * macro_chain = and_then(macro_finder_tac, simplify_after_macro); + + tactic * ufbv_rewriter_tac = mk_ufbv_rewriter_tactic(m, p); + tactic * simplify_after_ufbv = mk_simplify_tactic(m, p); + tactic * ufbv_chain = and_then(ufbv_rewriter_tac, simplify_after_ufbv); + + tactic * quasi_macros_tac = mk_quasi_macros_tactic(m, p); + tactic * simplify_after_quasi = mk_simplify_tactic(m, p); + tactic * quasi_chain = and_then(quasi_macros_tac, simplify_after_quasi); + + tactic * post_simplify_seq = and_then( + reduce_chain, + macro_chain, + ufbv_chain, + quasi_chain); + tactic * guarded_post_simplify = if_no_unsat_cores(post_simplify_seq); + + tactic * der_fp_tac2 = mk_der_fp_tactic(m, p); + tactic * simplify_after_der2 = mk_simplify_tactic(m, p); + tactic * der_chain2 = and_then(der_fp_tac2, simplify_after_der2); + + tactic * simplify_final = mk_simplify_tactic(m, p); + tactic * trace_post = mk_trace_tactic("ufbv_post"); + + tactic * result = and_then( + trace_pre, + preprocess_seq, + guarded_post_simplify, + der_chain2, + simplify_final, + trace_post); + return result; } tactic * mk_ufbv_tactic(ast_manager & m, params_ref const & p) {