From 02290e8736d936812d41b9569d89f0f04f0b8d16 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 30 Oct 2025 07:16:18 -0700 Subject: [PATCH] fix param evaluation non-determinism Signed-off-by: Lev Nachmanson --- src/smt/old_interval.cpp | 6 +- src/smt/theory_arith_nl.h | 42 ++++++--- src/tactic/portfolio/default_tactic.cpp | 91 ++++++++++++------- src/tactic/portfolio/smt_strategic_solver.cpp | 9 +- 4 files changed, 92 insertions(+), 56 deletions(-) diff --git a/src/smt/old_interval.cpp b/src/smt/old_interval.cpp index 142561788..45f471091 100644 --- a/src/smt/old_interval.cpp +++ b/src/smt/old_interval.cpp @@ -274,8 +274,9 @@ interval & interval::operator-=(interval const & other) { } v_dependency * interval::join(v_dependency * d1, v_dependency * d2, v_dependency * d3, v_dependency * d4) { - // TODO: non-deterministic parameter evaluation - return m_manager.mk_join(m_manager.mk_join(d1, d2), m_manager.mk_join(d3,d4)); + v_dependency* first = m_manager.mk_join(d1, d2); + v_dependency* second = m_manager.mk_join(d3, d4); + return m_manager.mk_join(first, second); } /** @@ -665,4 +666,3 @@ void interval::display_with_dependencies(std::ostream & out) const { - diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index 2345fbc18..0c76bd093 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -213,18 +213,25 @@ interval theory_arith::mk_interval_for(theory_var v) { bound * l = lower(v); bound * u = upper(v); if (l && u) { + auto const& l_val = l->get_value(); + auto const& u_val = u->get_value(); // optimization may introduce non-standard bounds. - if (l->get_value() == u->get_value() && !l->get_value().get_infinitesimal().to_rational().is_zero()) { + if (l_val == u_val && !l_val.get_infinitesimal().to_rational().is_zero()) { return interval(m_dep_manager); } - // TODO: non-deterministic parameter evaluation + rational l_rat = l_val.get_rational().to_rational(); + bool l_open = l_val.get_infinitesimal().to_rational().is_pos(); + v_dependency* l_dep = m_dep_manager.mk_leaf(l); + rational u_rat = u_val.get_rational().to_rational(); + bool u_open = u_val.get_infinitesimal().to_rational().is_neg(); + v_dependency* u_dep = m_dep_manager.mk_leaf(u); return interval(m_dep_manager, - l->get_value().get_rational().to_rational(), - l->get_value().get_infinitesimal().to_rational().is_pos(), - m_dep_manager.mk_leaf(l), - u->get_value().get_rational().to_rational(), - u->get_value().get_infinitesimal().to_rational().is_neg(), - m_dep_manager.mk_leaf(u)); + l_rat, + l_open, + l_dep, + u_rat, + u_open, + u_dep); } else if (l) { return interval(m_dep_manager, @@ -1712,8 +1719,12 @@ grobner::monomial * theory_arith::mk_gb_monomial(rational const & _coeff, e if (is_fixed(_var)) { if (!already_found.contains(_var)) { already_found.insert(_var); - // TODO: non-deterministic parameter evaluation - dep = m_dep_manager.mk_join(dep, m_dep_manager.mk_join(m_dep_manager.mk_leaf(lower(_var)), m_dep_manager.mk_leaf(upper(_var)))); + bound* lower_b = lower(_var); + bound* upper_b = upper(_var); + v_dependency* lower_dep = m_dep_manager.mk_leaf(lower_b); + v_dependency* upper_dep = m_dep_manager.mk_leaf(upper_b); + v_dependency* joined_bounds = m_dep_manager.mk_join(lower_dep, upper_dep); + dep = m_dep_manager.mk_join(dep, joined_bounds); } coeff *= lower_bound(_var).get_rational().to_rational(); } @@ -1779,8 +1790,12 @@ void theory_arith::add_monomial_def_to_gb(theory_var v, grobner & gb) { monomials.push_back(new_m); rational coeff(-1); if (is_fixed(v)) { - // TODO: non-deterministic parameter evaluation - dep = m_dep_manager.mk_join(dep, m_dep_manager.mk_join(m_dep_manager.mk_leaf(lower(v)), m_dep_manager.mk_leaf(upper(v)))); + bound* lower_b = lower(v); + bound* upper_b = upper(v); + v_dependency* lower_dep = m_dep_manager.mk_leaf(lower_b); + v_dependency* upper_dep = m_dep_manager.mk_leaf(upper_b); + v_dependency* joined_bounds = m_dep_manager.mk_join(lower_dep, upper_dep); + dep = m_dep_manager.mk_join(dep, joined_bounds); coeff *= lower_bound(v).get_rational().to_rational(); if (!coeff.is_zero()) monomials.push_back(gb.mk_monomial(coeff, 0, nullptr)); @@ -2414,6 +2429,3 @@ final_check_status theory_arith::process_non_linear() { }; - - - diff --git a/src/tactic/portfolio/default_tactic.cpp b/src/tactic/portfolio/default_tactic.cpp index b43515d2f..98f44e848 100644 --- a/src/tactic/portfolio/default_tactic.cpp +++ b/src/tactic/portfolio/default_tactic.cpp @@ -34,37 +34,64 @@ Notes: #include "tactic/smtlogics/smt_tactic.h" tactic * mk_default_tactic(ast_manager & m, params_ref const & p) { - tactic * st = using_params(and_then(mk_simplify_tactic(m, p), - // TODO: non-deterministic parameter evaluation - // TODO: non-deterministic parameter evaluation - cond(mk_and(mk_is_propositional_probe(), mk_not(mk_produce_proofs_probe())), - mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_fd_tactic(m, p); }), - // TODO: non-deterministic parameter evaluation - cond(mk_is_qfbv_probe(), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_qfbv_tactic(m, p); }), - // TODO: non-deterministic parameter evaluation - cond(mk_is_qfaufbv_probe(), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_qfaufbv_tactic(m, p); }), - // TODO: non-deterministic parameter evaluation - cond(mk_is_qflia_probe(), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_qflia_tactic(m, p); }), - // TODO: non-deterministic parameter evaluation - cond(mk_is_qfauflia_probe(), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_qfauflia_tactic(m, p); }), - // TODO: non-deterministic parameter evaluation - cond(mk_is_qflra_probe(), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_qflra_tactic(m, p); }), - // TODO: non-deterministic parameter evaluation - cond(mk_is_qfnra_probe(), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_qfnra_tactic(m, p); }), - // TODO: non-deterministic parameter evaluation - cond(mk_is_qfnia_probe(), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_qfnia_tactic(m, p); }), - // TODO: non-deterministic parameter evaluation - cond(mk_is_lira_probe(), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_lira_tactic(m, p); }), - // TODO: non-deterministic parameter evaluation - cond(mk_is_nra_probe(), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_nra_tactic(m, p); }), - // TODO: non-deterministic parameter evaluation - cond(mk_is_qffp_probe(), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_qffp_tactic(m, p); }), - // TODO: non-deterministic parameter evaluation - cond(mk_is_qffplra_probe(), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_qffplra_tactic(m, p); }), - //cond(mk_is_qfufnra_probe(), mk_qfufnra_tactic(m, p), - // TODO: non-deterministic parameter evaluation - and_then(mk_preamble_tactic(m), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_smt_tactic(m, p);}))))))))))))))), - p); + tactic* simplify = mk_simplify_tactic(m, p); + + tactic* preamble = mk_preamble_tactic(m); + tactic* lazy_smt = mk_lazy_tactic(m, p, [&](auto& m_ref, auto const& p_ref) { return mk_smt_tactic(m_ref, p_ref); }); + tactic* branch = and_then(preamble, lazy_smt); + + tactic* lazy_qffplra = mk_lazy_tactic(m, p, [&](auto& m_ref, auto const& p_ref) { return mk_qffplra_tactic(m_ref, p_ref); }); + probe* qffplra_probe = mk_is_qffplra_probe(); + branch = cond(qffplra_probe, lazy_qffplra, branch); + + tactic* lazy_qffp = mk_lazy_tactic(m, p, [&](auto& m_ref, auto const& p_ref) { return mk_qffp_tactic(m_ref, p_ref); }); + probe* qffp_probe = mk_is_qffp_probe(); + branch = cond(qffp_probe, lazy_qffp, branch); + + tactic* lazy_nra = mk_lazy_tactic(m, p, [&](auto& m_ref, auto const& p_ref) { return mk_nra_tactic(m_ref, p_ref); }); + probe* nra_probe = mk_is_nra_probe(); + branch = cond(nra_probe, lazy_nra, branch); + + tactic* lazy_lira = mk_lazy_tactic(m, p, [&](auto& m_ref, auto const& p_ref) { return mk_lira_tactic(m_ref, p_ref); }); + probe* lira_probe = mk_is_lira_probe(); + branch = cond(lira_probe, lazy_lira, branch); + + tactic* lazy_qfnia = mk_lazy_tactic(m, p, [&](auto& m_ref, auto const& p_ref) { return mk_qfnia_tactic(m_ref, p_ref); }); + probe* qfnia_probe = mk_is_qfnia_probe(); + branch = cond(qfnia_probe, lazy_qfnia, branch); + + tactic* lazy_qfnra = mk_lazy_tactic(m, p, [&](auto& m_ref, auto const& p_ref) { return mk_qfnra_tactic(m_ref, p_ref); }); + probe* qfnra_probe = mk_is_qfnra_probe(); + branch = cond(qfnra_probe, lazy_qfnra, branch); + + tactic* lazy_qflra = mk_lazy_tactic(m, p, [&](auto& m_ref, auto const& p_ref) { return mk_qflra_tactic(m_ref, p_ref); }); + probe* qflra_probe = mk_is_qflra_probe(); + branch = cond(qflra_probe, lazy_qflra, branch); + + tactic* lazy_qfauflia = mk_lazy_tactic(m, p, [&](auto& m_ref, auto const& p_ref) { return mk_qfauflia_tactic(m_ref, p_ref); }); + probe* qfauflia_probe = mk_is_qfauflia_probe(); + branch = cond(qfauflia_probe, lazy_qfauflia, branch); + + tactic* lazy_qflia = mk_lazy_tactic(m, p, [&](auto& m_ref, auto const& p_ref) { return mk_qflia_tactic(m_ref, p_ref); }); + probe* qflia_probe = mk_is_qflia_probe(); + branch = cond(qflia_probe, lazy_qflia, branch); + + tactic* lazy_qfaufbv = mk_lazy_tactic(m, p, [&](auto& m_ref, auto const& p_ref) { return mk_qfaufbv_tactic(m_ref, p_ref); }); + probe* qfaufbv_probe = mk_is_qfaufbv_probe(); + branch = cond(qfaufbv_probe, lazy_qfaufbv, branch); + + tactic* lazy_qfbv = mk_lazy_tactic(m, p, [&](auto& m_ref, auto const& p_ref) { return mk_qfbv_tactic(m_ref, p_ref); }); + probe* qfbv_probe = mk_is_qfbv_probe(); + branch = cond(qfbv_probe, lazy_qfbv, branch); + + tactic* lazy_fd = mk_lazy_tactic(m, p, [&](auto& m_ref, auto const& p_ref) { return mk_fd_tactic(m_ref, p_ref); }); + probe* propositional_probe = mk_is_propositional_probe(); + probe* produce_proofs_probe = mk_produce_proofs_probe(); + probe* no_proofs_probe = mk_not(produce_proofs_probe); + probe* propositional_no_proofs = mk_and(propositional_probe, no_proofs_probe); + branch = cond(propositional_no_proofs, lazy_fd, branch); + + tactic* combined = and_then(simplify, branch); + tactic * st = using_params(combined, p); return st; } - diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp index 3b089d6fd..4450ef520 100644 --- a/src/tactic/portfolio/smt_strategic_solver.cpp +++ b/src/tactic/portfolio/smt_strategic_solver.cpp @@ -185,10 +185,9 @@ public: if (!t) { t = mk_tactic_for_logic(m, p, l); } - // TODO: non-deterministic parameter evaluation - return mk_combined_solver(mk_tactic2solver(m, t.get(), p, proofs_enabled, models_enabled, unsat_core_enabled, l), - mk_solver_for_logic(m, p, l), - p); + solver* tactic_solver = mk_tactic2solver(m, t.get(), p, proofs_enabled, models_enabled, unsat_core_enabled, l); + solver* logic_solver = mk_solver_for_logic(m, p, l); + return mk_combined_solver(tactic_solver, logic_solver, p); } solver_factory* translate(ast_manager& m) override { @@ -199,5 +198,3 @@ public: solver_factory * mk_smt_strategic_solver_factory(symbol const & logic) { return alloc(smt_strategic_solver_factory, logic); } - -