From cb7c06ddd64db6313d3fb9859c649d4646d3ac59 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 30 Oct 2025 07:43:17 -0700 Subject: [PATCH] fix param evaluation non-determinism Signed-off-by: Lev Nachmanson --- src/tactic/smtlogics/qfidl_tactic.cpp | 92 +++++++++++++-------- src/tactic/smtlogics/qfnra_tactic.cpp | 114 +++++++++++++++++--------- src/tactic/smtlogics/qfuf_tactic.cpp | 21 +++-- 3 files changed, 147 insertions(+), 80 deletions(-) diff --git a/src/tactic/smtlogics/qfidl_tactic.cpp b/src/tactic/smtlogics/qfidl_tactic.cpp index 267c31947..9fc28b500 100644 --- a/src/tactic/smtlogics/qfidl_tactic.cpp +++ b/src/tactic/smtlogics/qfidl_tactic.cpp @@ -55,18 +55,28 @@ tactic * mk_qfidl_tactic(ast_manager & m, params_ref const & p) { pull_ite_p.set_bool("local_ctx", true); pull_ite_p.set_uint("local_ctx_limit", 10000000); - // TODO: non-deterministic parameter evaluation - tactic * preamble_st = and_then(and_then(mk_simplify_tactic(m), - mk_fix_dl_var_tactic(m), - mk_propagate_values_tactic(m), - mk_elim_uncnstr_tactic(m) - ), - // TODO: non-deterministic parameter evaluation - and_then(mk_solve_eqs_tactic(m), - using_params(mk_simplify_tactic(m), lhs_p), - mk_propagate_values_tactic(m), - mk_normalize_bounds_tactic(m), - mk_solve_eqs_tactic(m))); + tactic* simplify1 = mk_simplify_tactic(m); + tactic* fix_dl = mk_fix_dl_var_tactic(m); + tactic* propagate1 = mk_propagate_values_tactic(m); + tactic* elim_unc = mk_elim_uncnstr_tactic(m); + tactic* phase1 = and_then(simplify1, + fix_dl, + propagate1, + elim_unc); + + tactic* solve_eqs1 = mk_solve_eqs_tactic(m); + tactic* simplify2 = mk_simplify_tactic(m); + tactic* simplify_with_lhs = using_params(simplify2, lhs_p); + tactic* propagate2 = mk_propagate_values_tactic(m); + tactic* normalize_bounds = mk_normalize_bounds_tactic(m); + tactic* solve_eqs2 = mk_solve_eqs_tactic(m); + tactic* phase2 = and_then(solve_eqs1, + simplify_with_lhs, + propagate2, + normalize_bounds, + solve_eqs2); + + tactic * preamble_st = and_then(phase1, phase2); @@ -78,15 +88,21 @@ tactic * mk_qfidl_tactic(ast_manager & m, params_ref const & p) { // dynamic psm seems to work well. bv_solver_p.set_sym("gc", symbol("dyn_psm")); - // TODO: non-deterministic parameter evaluation - tactic * bv_solver = using_params(and_then(mk_simplify_tactic(m), - mk_propagate_values_tactic(m), - mk_solve_eqs_tactic(m), - mk_max_bv_sharing_tactic(m), - mk_bit_blaster_tactic(m), - mk_aig_tactic(), - mk_sat_tactic(m)), - bv_solver_p); + tactic* simplify3 = mk_simplify_tactic(m); + tactic* propagate3 = mk_propagate_values_tactic(m); + tactic* solve_eqs3 = mk_solve_eqs_tactic(m); + tactic* max_sharing = mk_max_bv_sharing_tactic(m); + tactic* bit_blaster = mk_bit_blaster_tactic(m); + tactic* aig = mk_aig_tactic(); + tactic* sat = mk_sat_tactic(m); + tactic* bv_solver_core = and_then(simplify3, + propagate3, + solve_eqs3, + max_sharing, + bit_blaster, + aig, + sat); + tactic * bv_solver = using_params(bv_solver_core, bv_solver_p); tactic * try2bv = and_then(using_params(mk_lia2pb_tactic(m), lia2pb_p), @@ -98,19 +114,27 @@ tactic * mk_qfidl_tactic(ast_manager & m, params_ref const & p) { params_ref diff_neq_p; diff_neq_p.set_uint("diff_neq_max_k", 25); - // TODO: non-deterministic parameter evaluation - // TODO: non-deterministic parameter evaluation - // TODO: non-deterministic parameter evaluation - tactic * st = cond(mk_and(mk_lt(mk_num_consts_probe(), mk_const_probe(static_cast(BIG_PROBLEM))), - // TODO: non-deterministic parameter evaluation - mk_and(mk_not(mk_produce_proofs_probe()), - mk_not(mk_produce_unsat_cores_probe()))), - using_params(and_then(preamble_st, - or_else(using_params(mk_diff_neq_tactic(m), diff_neq_p), - try2bv, - mk_smt_tactic(m))), - main_p), - mk_smt_tactic(m)); + probe* num_consts = mk_num_consts_probe(); + probe* const_limit = mk_const_probe(static_cast(BIG_PROBLEM)); + probe* few_consts = mk_lt(num_consts, const_limit); + probe* produce_proofs = mk_produce_proofs_probe(); + probe* produce_unsat = mk_produce_unsat_cores_probe(); + probe* no_proofs = mk_not(produce_proofs); + probe* no_unsat = mk_not(produce_unsat); + probe* no_proofs_or_unsat = mk_and(no_proofs, no_unsat); + probe* small_problem = mk_and(few_consts, no_proofs_or_unsat); + + tactic* diff_neq = mk_diff_neq_tactic(m); + tactic* diff_neq_with_params = using_params(diff_neq, diff_neq_p); + tactic* smt_default = mk_smt_tactic(m); + tactic* branch_solver = or_else(diff_neq_with_params, + try2bv, + smt_default); + tactic* main_branch = using_params(and_then(preamble_st, branch_solver), main_p); + + tactic * st = cond(small_problem, + main_branch, + smt_default); st->updt_params(p); diff --git a/src/tactic/smtlogics/qfnra_tactic.cpp b/src/tactic/smtlogics/qfnra_tactic.cpp index 94d8c328e..307440a75 100644 --- a/src/tactic/smtlogics/qfnra_tactic.cpp +++ b/src/tactic/smtlogics/qfnra_tactic.cpp @@ -39,8 +39,11 @@ tactic * mk_qfnra_very_small_solver(ast_manager& m, params_ref const& p) { params_ref p_sc = p; p_sc.set_bool("simple_check", true); // p_sc.set_uint("seed", 997); - // TODO: non-deterministic parameter evaluation - ts.push_back(try_for(and_then(mk_qfnra_nlsat_tactic(m, p_sc), mk_fail_if_undecided_tactic()), 10 * 1000)); + tactic* nlsat = mk_qfnra_nlsat_tactic(m, p_sc); + tactic* fail_if_undecided = mk_fail_if_undecided_tactic(); + tactic* seq = and_then(nlsat, fail_if_undecided); + tactic* limited = try_for(seq, 10 * 1000); + ts.push_back(limited); } { params_ref p_heuristic = p; @@ -74,7 +77,11 @@ tactic * mk_qfnra_very_small_solver(ast_manager& m, params_ref const& p) { { params_ref p_l = p; p_l.set_bool("arith.greatest_error_pivot", true); - ts.push_back(and_then(try_for(using_params(mk_smt_tactic(m), p_l), 300 * 1000), mk_fail_if_undecided_tactic())); + tactic* smt = mk_smt_tactic(m); + tactic* smt_with_params = using_params(smt, p_l); + tactic* smt_limited = try_for(smt_with_params, 300 * 1000); + tactic* fail_if_undecided = mk_fail_if_undecided_tactic(); + ts.push_back(and_then(smt_limited, fail_if_undecided)); } for (unsigned i = 0; i < 200; ++i) { // 3s * 200 = 600s params_ref p_i = p; @@ -96,8 +103,11 @@ tactic * mk_qfnra_small_solver(ast_manager& m, params_ref const& p) { params_ref p_sc = p; p_sc.set_bool("simple_check", true); // p_sc.set_uint("seed", 997); - // TODO: non-deterministic parameter evaluation - ts.push_back(try_for(and_then(mk_qfnra_nlsat_tactic(m, p_sc), mk_fail_if_undecided_tactic()), 20 * 1000)); + tactic* nlsat = mk_qfnra_nlsat_tactic(m, p_sc); + tactic* fail_if_undecided = mk_fail_if_undecided_tactic(); + tactic* seq = and_then(nlsat, fail_if_undecided); + tactic* limited = try_for(seq, 20 * 1000); + ts.push_back(limited); } { params_ref p_heuristic = p; @@ -133,7 +143,11 @@ tactic * mk_qfnra_small_solver(ast_manager& m, params_ref const& p) { { params_ref p_l = p; p_l.set_bool("arith.greatest_error_pivot", true); - ts.push_back(and_then(try_for(using_params(mk_smt_tactic(m), p_l), 350 * 1000), mk_fail_if_undecided_tactic())); + tactic* smt = mk_smt_tactic(m); + tactic* smt_with_params = using_params(smt, p_l); + tactic* smt_limited = try_for(smt_with_params, 350 * 1000); + tactic* fail_if_undecided = mk_fail_if_undecided_tactic(); + ts.push_back(and_then(smt_limited, fail_if_undecided)); } for (unsigned i = 0; i < 100; ++i) { // 5s * 100 = 500s params_ref p_i = p; @@ -154,8 +168,11 @@ tactic * mk_qfnra_middle_solver(ast_manager& m, params_ref const& p) { { params_ref p_sc = p; p_sc.set_bool("simple_check", true); - // TODO: non-deterministic parameter evaluation - ts.push_back(try_for(and_then(mk_qfnra_nlsat_tactic(m, p_sc), mk_fail_if_undecided_tactic()), 30 * 1000)); + tactic* nlsat = mk_qfnra_nlsat_tactic(m, p_sc); + tactic* fail_if_undecided = mk_fail_if_undecided_tactic(); + tactic* seq = and_then(nlsat, fail_if_undecided); + tactic* limited = try_for(seq, 30 * 1000); + ts.push_back(limited); } { params_ref p_heuristic = p; @@ -192,7 +209,11 @@ tactic * mk_qfnra_middle_solver(ast_manager& m, params_ref const& p) { { params_ref p_l = p; p_l.set_bool("arith.greatest_error_pivot", true); - ts.push_back(and_then(try_for(using_params(mk_smt_tactic(m), p_l), 375 * 1000), mk_fail_if_undecided_tactic())); + tactic* smt = mk_smt_tactic(m); + tactic* smt_with_params = using_params(smt, p_l); + tactic* smt_limited = try_for(smt_with_params, 375 * 1000); + tactic* fail_if_undecided = mk_fail_if_undecided_tactic(); + ts.push_back(and_then(smt_limited, fail_if_undecided)); } for (unsigned i = 0; i < 40; ++i) { // 10s * 40 = 400s params_ref p_i = p; @@ -213,8 +234,11 @@ tactic * mk_qfnra_large_solver(ast_manager& m, params_ref const& p) { { params_ref p_sc = p; p_sc.set_bool("simple_check", true); - // TODO: non-deterministic parameter evaluation - ts.push_back(try_for(and_then(mk_qfnra_nlsat_tactic(m, p_sc), mk_fail_if_undecided_tactic()), 50 * 1000)); + tactic* nlsat = mk_qfnra_nlsat_tactic(m, p_sc); + tactic* fail_if_undecided = mk_fail_if_undecided_tactic(); + tactic* seq = and_then(nlsat, fail_if_undecided); + tactic* limited = try_for(seq, 50 * 1000); + ts.push_back(limited); } { @@ -247,7 +271,11 @@ tactic * mk_qfnra_large_solver(ast_manager& m, params_ref const& p) { { params_ref p_l = p; p_l.set_bool("arith.greatest_error_pivot", true); - ts.push_back(and_then(try_for(using_params(mk_smt_tactic(m), p_l), 400 * 1000), mk_fail_if_undecided_tactic())); + tactic* smt = mk_smt_tactic(m); + tactic* smt_with_params = using_params(smt, p_l); + tactic* smt_limited = try_for(smt_with_params, 400 * 1000); + tactic* fail_if_undecided = mk_fail_if_undecided_tactic(); + ts.push_back(and_then(smt_limited, fail_if_undecided)); } for (unsigned i = 0; i < 10; ++i) { // 20s * 10 = 200s params_ref p_i = p; @@ -268,8 +296,11 @@ tactic * mk_qfnra_very_large_solver(ast_manager& m, params_ref const& p) { { params_ref p_sc = p; p_sc.set_bool("simple_check", true); - // TODO: non-deterministic parameter evaluation - ts.push_back(try_for(and_then(mk_qfnra_nlsat_tactic(m, p_sc), mk_fail_if_undecided_tactic()), 100 * 1000)); + tactic* nlsat = mk_qfnra_nlsat_tactic(m, p_sc); + tactic* fail_if_undecided = mk_fail_if_undecided_tactic(); + tactic* seq = and_then(nlsat, fail_if_undecided); + tactic* limited = try_for(seq, 100 * 1000); + ts.push_back(limited); } { params_ref p_order_1 = p; @@ -292,7 +323,11 @@ tactic * mk_qfnra_very_large_solver(ast_manager& m, params_ref const& p) { { params_ref p_l = p; p_l.set_bool("arith.greatest_error_pivot", true); - ts.push_back(and_then(try_for(using_params(mk_smt_tactic(m), p_l), 425 * 1000), mk_fail_if_undecided_tactic())); + tactic* smt = mk_smt_tactic(m); + tactic* smt_with_params = using_params(smt, p_l); + tactic* smt_limited = try_for(smt_with_params, 425 * 1000); + tactic* fail_if_undecided = mk_fail_if_undecided_tactic(); + ts.push_back(and_then(smt_limited, fail_if_undecided)); } { ts.push_back(mk_qfnra_nlsat_tactic(m, p)); @@ -307,33 +342,34 @@ const double LARGE_THRESHOLD = 600.0; tactic * mk_qfnra_mixed_solver(ast_manager& m, params_ref const& p) { auto very_small_t = mk_lazy_tactic(m, p, [&](ast_manager& m, params_ref const& p) {return mk_qfnra_very_small_solver(m, p); }); auto small_t = mk_lazy_tactic(m, p, [&](ast_manager& m, params_ref const& p) {return mk_qfnra_small_solver(m, p); }); - auto middle_t = mk_lazy_tactic(m, p, [&](ast_manager& m, params_ref const& p) {return mk_qfnra_middle_solver(m, p); }); - auto large_t = mk_lazy_tactic(m, p, [&](ast_manager& m, params_ref const& p) {return mk_qfnra_large_solver(m, p); }); - auto very_large_t = mk_lazy_tactic(m, p, [&](ast_manager& m, params_ref const& p) {return mk_qfnra_very_large_solver(m, p); }); - // TODO: non-deterministic parameter evaluation - return cond(mk_lt(mk_memory_probe(), mk_const_probe(VERY_SMALL_THRESHOLD)), - very_small_t, - // TODO: non-deterministic parameter evaluation - cond(mk_lt(mk_memory_probe(), mk_const_probe(SMALL_THRESHOLD)), - small_t, - // TODO: non-deterministic parameter evaluation - cond(mk_lt(mk_memory_probe(), mk_const_probe(MIDDLE_THRESHOLD)), - middle_t, - // TODO: non-deterministic parameter evaluation - cond(mk_lt(mk_memory_probe(), mk_const_probe(LARGE_THRESHOLD)), - large_t, - very_large_t - ) - ) - ) - ); + auto middle_t = mk_lazy_tactic(m, p, [&](ast_manager& m, params_ref const& p) {return mk_qfnra_middle_solver(m, p); }); + auto large_t = mk_lazy_tactic(m, p, [&](ast_manager& m, params_ref const& p) {return mk_qfnra_large_solver(m, p); }); + auto very_large_t = mk_lazy_tactic(m, p, [&](ast_manager& m, params_ref const& p) {return mk_qfnra_very_large_solver(m, p); }); + probe* memory_usage = mk_memory_probe(); + probe* very_small_limit = mk_const_probe(VERY_SMALL_THRESHOLD); + probe* small_limit = mk_const_probe(SMALL_THRESHOLD); + probe* middle_limit = mk_const_probe(MIDDLE_THRESHOLD); + probe* large_limit = mk_const_probe(LARGE_THRESHOLD); + + probe* very_small_check = mk_lt(memory_usage, very_small_limit); + probe* small_check = mk_lt(memory_usage, small_limit); + probe* middle_check = mk_lt(memory_usage, middle_limit); + probe* large_check = mk_lt(memory_usage, large_limit); + + tactic* large_branch = cond(large_check, large_t, very_large_t); + tactic* middle_branch = cond(middle_check, middle_t, large_branch); + tactic* small_branch = cond(small_check, small_t, middle_branch); + return cond(very_small_check, very_small_t, small_branch); } tactic * mk_qfnra_tactic(ast_manager & m, params_ref const& p) { - // TODO: non-deterministic parameter evaluation - return and_then(mk_simplify_tactic(m, p), - mk_propagate_values_tactic(m, p), - mk_qfnra_mixed_solver(m, p) + tactic* simplify = mk_simplify_tactic(m, p); + tactic* propagate = mk_propagate_values_tactic(m, p); + tactic* mixed_solver = mk_qfnra_mixed_solver(m, p); + + return and_then(simplify, + propagate, + mixed_solver ); } diff --git a/src/tactic/smtlogics/qfuf_tactic.cpp b/src/tactic/smtlogics/qfuf_tactic.cpp index b0ddaaf11..4d75d0893 100644 --- a/src/tactic/smtlogics/qfuf_tactic.cpp +++ b/src/tactic/smtlogics/qfuf_tactic.cpp @@ -29,13 +29,20 @@ tactic * mk_qfuf_tactic(ast_manager & m, params_ref const & p) { s2_p.set_bool("pull_cheap_ite", true); s2_p.set_bool("local_ctx", true); s2_p.set_uint("local_ctx_limit", 10000000); - // TODO: non-deterministic parameter evaluation - return and_then(mk_simplify_tactic(m, p), - mk_propagate_values_tactic(m, p), - mk_solve_eqs_tactic(m, p), - using_params(mk_simplify_tactic(m, p), s2_p), - if_no_proofs(if_no_unsat_cores(mk_symmetry_reduce_tactic(m, p))), - mk_smt_tactic(m, p)); + tactic* simplify = mk_simplify_tactic(m, p); + tactic* propagate = mk_propagate_values_tactic(m, p); + tactic* solve_eqs = mk_solve_eqs_tactic(m, p); + tactic* simplify2 = mk_simplify_tactic(m, p); + tactic* simplify_with_pull = using_params(simplify2, s2_p); + tactic* symmetry = mk_symmetry_reduce_tactic(m, p); + tactic* guarded_symmetry = if_no_proofs(if_no_unsat_cores(symmetry)); + tactic* smt = mk_smt_tactic(m, p); + return and_then(simplify, + propagate, + solve_eqs, + simplify_with_pull, + guarded_symmetry, + smt); }