diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp index fbec59e20..0b40eec77 100644 --- a/src/math/polynomial/polynomial.cpp +++ b/src/math/polynomial/polynomial.cpp @@ -2995,16 +2995,18 @@ namespace polynomial { polynomial * add(polynomial const * p1, polynomial const * p2) { numeral one(1); - // TODO: non-deterministic parameter evaluation - return addmul(one, mk_unit(), p1, one, mk_unit(), p2); + monomial* unit1 = mk_unit(); + monomial* unit2 = mk_unit(); + return addmul(one, unit1, p1, one, unit2, p2); } polynomial * sub(polynomial const * p1, polynomial const * p2) { numeral one(1); numeral minus_one; // It is incorrect to initialize with -1 when numeral_manager is GF_2 m_manager.set(minus_one, -1); - // TODO: non-deterministic parameter evaluation - return addmul(one, mk_unit(), p1, minus_one, mk_unit(), p2); + monomial* unit1 = mk_unit(); + monomial* unit2 = mk_unit(); + return addmul(one, unit1, p1, minus_one, unit2, p2); } diff --git a/src/model/model.cpp b/src/model/model.cpp index 1bdda5448..cb113839d 100644 --- a/src/model/model.cpp +++ b/src/model/model.cpp @@ -625,8 +625,10 @@ void model::add_rec_funs() { expr_safe_replace subst(m); unsigned arity = f->get_arity(); for (unsigned i = 0; i < arity; ++i) { - // TODO: non-deterministic parameter evaluation - subst.insert(m.mk_var(arity - i - 1, f->get_domain(i)), m.mk_var(i, f->get_domain(i))); + sort* dom = f->get_domain(i); + expr* lhs = m.mk_var(arity - i - 1, dom); + expr* rhs = m.mk_var(i, dom); + subst.insert(lhs, rhs); } expr_ref bodyr(m); subst(rhs, bodyr); diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index 337dd3a91..55218e8e5 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -457,8 +457,12 @@ struct evaluator_cfg : public default_rewriter_cfg { if (interp) { var_subst vs(m, false); result = vs(fi->get_interp(), num, args); - // TODO: non-deterministic parameter evaluation - result = m.mk_ite(m.mk_eq(m_au.mk_numeral(rational(0), args[1]->get_sort()), args[1]), result, m.mk_app(f, num, args)); + expr_ref zero(m_au.mk_numeral(rational(0), args[1]->get_sort()), m); + expr_ref is_zero(m); + is_zero = m.mk_eq(zero, args[1]); + expr_ref app_expr(m); + app_expr = m.mk_app(f, num, args); + result = m.mk_ite(is_zero, result, app_expr); return BR_DONE; } } diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index c6306f12a..de4838ee2 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -891,12 +891,14 @@ namespace opt { g->assert_expr(fml); for (expr * a : asms) g->assert_expr(a, a); - tactic_ref tac0 = - // TODO: non-deterministic parameter evaluation - and_then(mk_simplify_tactic(m, m_params), - mk_propagate_values_tactic(m), - m_incremental ? mk_skip_tactic() : mk_solve_eqs_tactic(m), - mk_simplify_tactic(m)); + tactic* simplify_with_params = mk_simplify_tactic(m, m_params); + tactic* propagate_values = mk_propagate_values_tactic(m); + tactic* solve_or_skip = m_incremental ? mk_skip_tactic() : mk_solve_eqs_tactic(m); + tactic* simplify_plain = mk_simplify_tactic(m); + tactic_ref tac0 = and_then(simplify_with_params, + propagate_values, + solve_or_skip, + simplify_plain); opt_params optp(m_params); tactic_ref tac1, tac2, tac3, tac4; bool has_dep = false; diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index c444f2ebf..24c2ecdd7 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -653,22 +653,29 @@ public: simp2_p.set_bool("flat", false); sat_params sp(m_params); - if (sp.euf()) - m_preprocess = - // TODO: non-deterministic parameter evaluation - and_then(mk_simplify_tactic(m), - mk_propagate_values_tactic(m)); - else - m_preprocess = - // TODO: non-deterministic parameter evaluation - and_then(mk_simplify_tactic(m), - mk_propagate_values_tactic(m), - mk_card2bv_tactic(m, m_params), // updates model converter - using_params(mk_simplify_tactic(m), simp1_p), - mk_max_bv_sharing_tactic(m), - mk_bit_blaster_tactic(m, m_bb_rewriter.get()), - using_params(mk_simplify_tactic(m), simp2_p) - ); + if (sp.euf()) { + tactic* simplify = mk_simplify_tactic(m); + tactic* propagate = mk_propagate_values_tactic(m); + m_preprocess = and_then(simplify, propagate); + } + else { + tactic* simplify1 = mk_simplify_tactic(m); + tactic* propagate = mk_propagate_values_tactic(m); + tactic* card2bv = mk_card2bv_tactic(m, m_params); // updates model converter + tactic* simplify_param1 = mk_simplify_tactic(m); + tactic* simplify_with_params1 = using_params(simplify_param1, simp1_p); + tactic* max_sharing = mk_max_bv_sharing_tactic(m); + tactic* bit_blaster = mk_bit_blaster_tactic(m, m_bb_rewriter.get()); + tactic* simplify_param2 = mk_simplify_tactic(m); + tactic* simplify_with_params2 = using_params(simplify_param2, simp2_p); + m_preprocess = and_then(simplify1, + propagate, + card2bv, + simplify_with_params1, + max_sharing, + bit_blaster, + simplify_with_params2); + } while (m_bb_rewriter->get_num_scopes() < m_num_scopes) { m_bb_rewriter->push(); } diff --git a/src/tactic/fpa/qffp_tactic.cpp b/src/tactic/fpa/qffp_tactic.cpp index 98a1b0a39..c92089f8a 100644 --- a/src/tactic/fpa/qffp_tactic.cpp +++ b/src/tactic/fpa/qffp_tactic.cpp @@ -82,26 +82,39 @@ tactic * mk_qffp_tactic(ast_manager & m, params_ref const & p) { simp_p.set_bool("arith_lhs", true); simp_p.set_bool("elim_and", true); - // TODO: non-deterministic parameter evaluation - tactic * preamble = and_then(mk_simplify_tactic(m, simp_p), - mk_propagate_values_tactic(m, p), - mk_fpa2bv_tactic(m, p), - mk_propagate_values_tactic(m, p), - using_params(mk_simplify_tactic(m, p), simp_p), - if_no_proofs(if_no_unsat_cores(mk_ackermannize_bv_tactic(m, p)))); + tactic* simplify_simp = mk_simplify_tactic(m, simp_p); + tactic* propagate1 = mk_propagate_values_tactic(m, p); + tactic* fpa2bv = mk_fpa2bv_tactic(m, p); + tactic* propagate2 = mk_propagate_values_tactic(m, p); + tactic* simplify_for_params = mk_simplify_tactic(m, p); + tactic* simplify_with_params = using_params(simplify_for_params, simp_p); + tactic* ackermann = mk_ackermannize_bv_tactic(m, p); + tactic* ackermann_guard = if_no_proofs(if_no_unsat_cores(ackermann)); + tactic * preamble = and_then(simplify_simp, + propagate1, + fpa2bv, + propagate2, + simplify_with_params, + ackermann_guard); + + tactic* bit_blaster = mk_bit_blaster_tactic(m, p); + tactic* simplify_post_bb = mk_simplify_tactic(m, p); + tactic* simplify_post_bb_params = using_params(simplify_post_bb, simp_p); + probe* propositional_probe = mk_is_propositional_probe(); + probe* produce_proofs_probe = mk_produce_proofs_probe(); + tactic* smt_with_proofs = mk_smt_tactic(m, p); // `sat' does not support proofs. + tactic* psat = mk_psat_tactic(m, p); + tactic* proofs_branch = cond(produce_proofs_probe, smt_with_proofs, psat); + probe* fp_qfnra_probe = mk_is_fp_qfnra_probe(); + tactic* qfnra = mk_qfnra_tactic(m, p); + tactic* smt_default = mk_smt_tactic(m, p); + tactic* fp_branch = cond(fp_qfnra_probe, qfnra, smt_default); + tactic* top_branch = cond(propositional_probe, proofs_branch, fp_branch); tactic * st = and_then(preamble, - mk_bit_blaster_tactic(m, p), - using_params(mk_simplify_tactic(m, p), simp_p), - cond(mk_is_propositional_probe(), - // TODO: non-deterministic parameter evaluation - cond(mk_produce_proofs_probe(), - mk_smt_tactic(m, p), // `sat' does not support proofs. - mk_psat_tactic(m, p)), - // TODO: non-deterministic parameter evaluation - cond(mk_is_fp_qfnra_probe(), - mk_qfnra_tactic(m, p), - mk_smt_tactic(m, p)))); + bit_blaster, + simplify_post_bb_params, + top_branch); st->updt_params(p); return st;