From a413783c1caa687e93127dc7c8c76049d5354ab7 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 30 Oct 2025 07:28:32 -0700 Subject: [PATCH] fix param evaluation non-determinism Signed-off-by: Lev Nachmanson --- src/tactic/smtlogics/qfaufbv_tactic.cpp | 41 +++++++---- src/tactic/smtlogics/qfnia_tactic.cpp | 94 ++++++++++++++++--------- src/tactic/smtlogics/qfufbv_tactic.cpp | 87 +++++++++++++++-------- 3 files changed, 144 insertions(+), 78 deletions(-) diff --git a/src/tactic/smtlogics/qfaufbv_tactic.cpp b/src/tactic/smtlogics/qfaufbv_tactic.cpp index f960ee09a..e97fd1aa6 100644 --- a/src/tactic/smtlogics/qfaufbv_tactic.cpp +++ b/src/tactic/smtlogics/qfaufbv_tactic.cpp @@ -38,17 +38,26 @@ static tactic * mk_qfaufbv_preamble(ast_manager & m, params_ref const & p) { simp2_p.set_uint("local_ctx_limit", 10000000); - // TODO: non-deterministic parameter evaluation - return and_then(mk_simplify_tactic(m), - mk_propagate_values_tactic(m), - mk_solve_eqs_tactic(m), - mk_elim_uncnstr_tactic(m), - // sound to use? if_no_proofs(if_no_unsat_cores(mk_reduce_args_tactic(m))), - if_no_proofs(if_no_unsat_cores(mk_bv_size_reduction_tactic(m))), - using_params(mk_simplify_tactic(m), simp2_p), - mk_max_bv_sharing_tactic(m), - if_no_proofs(if_no_unsat_cores(mk_ackermannize_bv_tactic(m, p))) - ); + 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* size_reduction = mk_bv_size_reduction_tactic(m); + tactic* guarded_size_reduction = if_no_proofs(if_no_unsat_cores(size_reduction)); + tactic* simplify2 = mk_simplify_tactic(m); + tactic* simplify_with_params = using_params(simplify2, simp2_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)); + + return and_then(simplify1, + propagate, + solve_eqs, + elim_unc, + guarded_size_reduction, + simplify_with_params, + max_sharing, + guarded_ackermann); } tactic * mk_qfaufbv_tactic(ast_manager & m, params_ref const & p) { @@ -58,10 +67,12 @@ tactic * mk_qfaufbv_tactic(ast_manager & m, params_ref const & p) { tactic * preamble_st = mk_qfaufbv_preamble(m, p); - tactic * st = using_params( - and_then(preamble_st, - // TODO: non-deterministic parameter evaluation - cond(mk_is_qfbv_probe(), mk_qfbv_tactic(m), mk_smt_tactic(m, p))), main_p); + tactic* qfbv = mk_qfbv_tactic(m); + tactic* smt = mk_smt_tactic(m, p); + probe* qfbv_probe = mk_is_qfbv_probe(); + tactic* branch = cond(qfbv_probe, qfbv, smt); + + tactic * st = using_params(and_then(preamble_st, branch), main_p); st->updt_params(p); return st; diff --git a/src/tactic/smtlogics/qfnia_tactic.cpp b/src/tactic/smtlogics/qfnia_tactic.cpp index 4f1cca0bb..da2ef5e83 100644 --- a/src/tactic/smtlogics/qfnia_tactic.cpp +++ b/src/tactic/smtlogics/qfnia_tactic.cpp @@ -48,13 +48,21 @@ static tactic * mk_qfnia_bv_solver(ast_manager & m, params_ref const & p_ref) { mem_p.set_uint("max_conflicts", 500); - // TODO: non-deterministic parameter evaluation - tactic * r = using_params(and_then(mk_simplify_tactic(m), - mk_propagate_values_tactic(m), - using_params(mk_simplify_tactic(m), simp2_p), - mk_max_bv_sharing_tactic(m), - using_params(mk_bit_blaster_tactic(m), mem_p), - mk_sat_tactic(m, mem_p)), + tactic* simplify1 = mk_simplify_tactic(m); + tactic* propagate = mk_propagate_values_tactic(m); + tactic* simplify2 = mk_simplify_tactic(m); + tactic* simplify_with_params = using_params(simplify2, simp2_p); + tactic* max_sharing = mk_max_bv_sharing_tactic(m); + tactic* bit_blaster = mk_bit_blaster_tactic(m); + tactic* bit_blaster_with_params = using_params(bit_blaster, mem_p); + tactic* sat = mk_sat_tactic(m, mem_p); + + tactic * r = using_params(and_then(simplify1, + propagate, + simplify_with_params, + max_sharing, + bit_blaster_with_params, + sat), p); return r; } @@ -73,16 +81,26 @@ static tactic * mk_qfnia_preamble(ast_manager & m, params_ref const & p_ref) { params_ref elim_p = p_ref; elim_p.set_uint("max_memory",20); - return - // TODO: non-deterministic parameter evaluation - and_then(mk_simplify_tactic(m), - mk_propagate_values_tactic(m), - using_params(mk_ctx_simplify_tactic(m), ctx_simp_p), - using_params(mk_simplify_tactic(m), pull_ite_p), - mk_elim_uncnstr_tactic(m), - mk_lia2card_tactic(m), - mk_card2bv_tactic(m, p_ref), - skip_if_failed(using_params(mk_cofactor_term_ite_tactic(m), elim_p))); + tactic* simplify1 = mk_simplify_tactic(m); + tactic* propagate = mk_propagate_values_tactic(m); + tactic* ctx_simplify = mk_ctx_simplify_tactic(m); + tactic* ctx_simplify_with_params = using_params(ctx_simplify, ctx_simp_p); + tactic* simplify2 = mk_simplify_tactic(m); + tactic* simplify_with_pull_ite = using_params(simplify2, pull_ite_p); + tactic* elim_unc = mk_elim_uncnstr_tactic(m); + tactic* lia2card = mk_lia2card_tactic(m); + tactic* card2bv = mk_card2bv_tactic(m, p_ref); + tactic* cofactor = mk_cofactor_term_ite_tactic(m); + tactic* cofactor_with_params = using_params(cofactor, elim_p); + + return and_then(simplify1, + propagate, + ctx_simplify_with_params, + simplify_with_pull_ite, + elim_unc, + lia2card, + card2bv, + skip_if_failed(cofactor_with_params)); } static tactic * mk_qfnia_sat_solver(ast_manager & m, params_ref const & p) { @@ -91,11 +109,17 @@ static tactic * mk_qfnia_sat_solver(ast_manager & m, params_ref const & p) { params_ref simp_p = p; simp_p.set_bool("hoist_mul", true); // hoist multipliers to create smaller circuits. - // TODO: non-deterministic parameter evaluation - return and_then(using_params(mk_simplify_tactic(m), simp_p), - mk_nla2bv_tactic(m, nia2sat_p), - skip_if_failed(mk_qfnia_bv_solver(m, p)), - mk_fail_if_undecided_tactic()); + tactic* simplify = mk_simplify_tactic(m); + tactic* simplify_with_params = using_params(simplify, simp_p); + tactic* nla2bv = mk_nla2bv_tactic(m, nia2sat_p); + tactic* bv_solver = mk_qfnia_bv_solver(m, p); + tactic* guarded_bv_solver = skip_if_failed(bv_solver); + tactic* fail_if_undecided = mk_fail_if_undecided_tactic(); + + return and_then(simplify_with_params, + nla2bv, + guarded_bv_solver, + fail_if_undecided); } static tactic * mk_qfnia_nlsat_solver(ast_manager & m, params_ref const & p) { @@ -117,14 +141,20 @@ static tactic * mk_qfnia_smt_solver(ast_manager& m, params_ref const& p) { } tactic * mk_qfnia_tactic(ast_manager & m, params_ref const & p) { - // TODO: non-deterministic parameter evaluation - return and_then( - mk_report_verbose_tactic("(qfnia-tactic)", 10), - mk_qfnia_preamble(m, p), - // TODO: non-deterministic parameter evaluation - or_else(mk_qfnia_sat_solver(m, p), - try_for(mk_qfnia_smt_solver(m, p), 2000), - mk_qfnia_nlsat_solver(m, p), - mk_qfnia_smt_solver(m, p))); -} + tactic* report = mk_report_verbose_tactic("(qfnia-tactic)", 10); + tactic* preamble = mk_qfnia_preamble(m, p); + tactic* sat_solver = mk_qfnia_sat_solver(m, p); + tactic* smt_solver1 = mk_qfnia_smt_solver(m, p); + tactic* smt_solver_try = try_for(mk_qfnia_smt_solver(m, p), 2000); + tactic* nlsat_solver = mk_qfnia_nlsat_solver(m, p); + + tactic* branch = or_else(sat_solver, + smt_solver_try, + nlsat_solver, + smt_solver1); + + return and_then(report, + preamble, + branch); +} diff --git a/src/tactic/smtlogics/qfufbv_tactic.cpp b/src/tactic/smtlogics/qfufbv_tactic.cpp index f816e348c..7891e6fa1 100644 --- a/src/tactic/smtlogics/qfufbv_tactic.cpp +++ b/src/tactic/smtlogics/qfufbv_tactic.cpp @@ -150,33 +150,56 @@ static tactic * mk_qfufbv_preamble1(ast_manager & m, params_ref const & p) { ctx_simp_p.set_uint("max_depth", 32); ctx_simp_p.set_uint("max_steps", 5000000); - // TODO: non-deterministic parameter evaluation + tactic* simplify = mk_simplify_tactic(m); + tactic* simplify_flat = using_params(simplify, flat_and_or_p); + tactic* propagate = mk_propagate_values_tactic(m); + tactic* propagate_flat = using_params(propagate, flat_and_or_p); + tactic* bv_bound = mk_bv_bound_chk_tactic(m); + tactic* guarded_bv_bound = if_no_proofs(if_no_unsat_cores(bv_bound)); + tactic* solve_eqs = mk_solve_eqs_tactic(m); + 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* max_sharing = mk_max_bv_sharing_tactic(m); + tactic* simplify2 = mk_simplify_tactic(m); + tactic* simplify_with_params = using_params(simplify2, simp2_p); + return and_then( - using_params(mk_simplify_tactic(m), flat_and_or_p), - using_params(mk_propagate_values_tactic(m), flat_and_or_p), - if_no_proofs(if_no_unsat_cores(mk_bv_bound_chk_tactic(m))), - //using_params(mk_ctx_simplify_tactic(m_m), ctx_simp_p), - mk_solve_eqs_tactic(m), - mk_elim_uncnstr_tactic(m), - if_no_proofs(if_no_unsat_cores(mk_bv_size_reduction_tactic(m))), - mk_max_bv_sharing_tactic(m), - using_params(mk_simplify_tactic(m), simp2_p) - ); + simplify_flat, + propagate_flat, + guarded_bv_bound, + solve_eqs, + elim_unc, + guarded_size, + max_sharing, + simplify_with_params); } static tactic * mk_qfufbv_preamble(ast_manager & m, params_ref const & p) { params_ref simp2_p = p, flat_and_or_p = p; flat_and_or_p.set_bool("flat_and_or", false); - // TODO: non-deterministic parameter evaluation - return and_then(using_params(mk_simplify_tactic(m), flat_and_or_p), - using_params(mk_propagate_values_tactic(m), flat_and_or_p), - mk_solve_eqs_tactic(m), - mk_elim_uncnstr_tactic(m), - if_no_proofs(if_no_unsat_cores(mk_reduce_args_tactic(m))), - if_no_proofs(if_no_unsat_cores(mk_bv_size_reduction_tactic(m))), - mk_max_bv_sharing_tactic(m), - if_no_proofs(if_no_unsat_cores(mk_ackermannize_bv_tactic(m,p))) - ); + tactic* simplify = mk_simplify_tactic(m); + tactic* simplify_flat = using_params(simplify, flat_and_or_p); + tactic* propagate = mk_propagate_values_tactic(m); + tactic* propagate_flat = using_params(propagate, flat_and_or_p); + tactic* solve_eqs = mk_solve_eqs_tactic(m); + tactic* elim_unc = mk_elim_uncnstr_tactic(m); + tactic* reduce_args = mk_reduce_args_tactic(m); + tactic* guarded_reduce_args = if_no_proofs(if_no_unsat_cores(reduce_args)); + tactic* size_reduction = mk_bv_size_reduction_tactic(m); + tactic* guarded_size_reduction = if_no_proofs(if_no_unsat_cores(size_reduction)); + 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)); + + return and_then(simplify_flat, + propagate_flat, + solve_eqs, + elim_unc, + guarded_reduce_args, + guarded_size_reduction, + max_sharing, + guarded_ackermann); } tactic * mk_qfufbv_tactic(ast_manager & m, params_ref const & p) { @@ -186,13 +209,14 @@ tactic * mk_qfufbv_tactic(ast_manager & m, params_ref const & p) { tactic * const preamble_st = mk_qfufbv_preamble(m, p); - tactic * st = using_params( - and_then(preamble_st, - // TODO: non-deterministic parameter evaluation - cond(mk_is_qfbv_probe(), - mk_qfbv_tactic(m), - mk_smt_tactic(m, p))), - main_p); + tactic* qfbv = mk_qfbv_tactic(m); + tactic* smt = mk_smt_tactic(m, p); + probe* qfbv_probe = mk_is_qfbv_probe(); + tactic* branch = cond(qfbv_probe, + qfbv, + smt); + + tactic * st = using_params(and_then(preamble_st, branch), main_p); st->updt_params(p); return st; @@ -202,7 +226,8 @@ tactic * mk_qfufbv_ackr_tactic(ast_manager & m, params_ref const & p) { tactic * const preamble_t = mk_qfufbv_preamble1(m, p); tactic * const actual_tactic = alloc(qfufbv_ackr_tactic, m, p); - return and_then(preamble_t, - // TODO: non-deterministic parameter evaluation - cond(mk_is_qfufbv_probe(), actual_tactic, mk_smt_tactic(m, p))); + tactic* smt = mk_smt_tactic(m, p); + probe* qfufbv_probe = mk_is_qfufbv_probe(); + tactic* branch = cond(qfufbv_probe, actual_tactic, smt); + return and_then(preamble_t, branch); }