mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-05 13:56:03 +00:00
Code Activity

fix param evaluation non-determinism

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-10-30 07:16:18 -07:00
parent 3c5cb7c044
commit 02290e8736
4 changed files with 92 additions and 56 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/smt/old_interval.cpp
View file

@ -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) { v_dependency * interval::join(v_dependency * d1, v_dependency * d2, v_dependency * d3, v_dependency * d4) {
// TODO: non-deterministic parameter evaluation v_dependency* first = m_manager.mk_join(d1, d2);
return m_manager.mk_join(m_manager.mk_join(d1, d2), m_manager.mk_join(d3,d4)); 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 {

42
src/smt/theory_arith_nl.h
View file

@ -213,18 +213,25 @@ interval theory_arith<Ext>::mk_interval_for(theory_var v) {
bound * l = lower(v); bound * l = lower(v);
bound * u = upper(v); bound * u = upper(v);
if (l && u) { if (l && u) {
auto const& l_val = l->get_value();
auto const& u_val = u->get_value();
// optimization may introduce non-standard bounds. // 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); 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, return interval(m_dep_manager,
l->get_value().get_rational().to_rational(), l_rat,
l->get_value().get_infinitesimal().to_rational().is_pos(), l_open,
m_dep_manager.mk_leaf(l), l_dep,
u->get_value().get_rational().to_rational(), u_rat,
u->get_value().get_infinitesimal().to_rational().is_neg(), u_open,
m_dep_manager.mk_leaf(u)); u_dep);
} }
else if (l) { else if (l) {
return interval(m_dep_manager, return interval(m_dep_manager,
@ -1712,8 +1719,12 @@ grobner::monomial * theory_arith<Ext>::mk_gb_monomial(rational const & _coeff, e
if (is_fixed(_var)) { if (is_fixed(_var)) {
if (!already_found.contains(_var)) { if (!already_found.contains(_var)) {
already_found.insert(_var); already_found.insert(_var);
// TODO: non-deterministic parameter evaluation bound* lower_b = lower(_var);
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* 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(); coeff *= lower_bound(_var).get_rational().to_rational();
} }
@ -1779,8 +1790,12 @@ void theory_arith<Ext>::add_monomial_def_to_gb(theory_var v, grobner & gb) {
monomials.push_back(new_m); monomials.push_back(new_m);
rational coeff(-1); rational coeff(-1);
if (is_fixed(v)) { if (is_fixed(v)) {
// TODO: non-deterministic parameter evaluation bound* lower_b = lower(v);
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* 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(); coeff *= lower_bound(v).get_rational().to_rational();
if (!coeff.is_zero()) if (!coeff.is_zero())
monomials.push_back(gb.mk_monomial(coeff, 0, nullptr)); monomials.push_back(gb.mk_monomial(coeff, 0, nullptr));
@ -2414,6 +2429,3 @@ final_check_status theory_arith<Ext>::process_non_linear() {
}; };

91
src/tactic/portfolio/default_tactic.cpp
View file

@ -34,37 +34,64 @@ Notes:
#include "tactic/smtlogics/smt_tactic.h" #include "tactic/smtlogics/smt_tactic.h"
tactic * mk_default_tactic(ast_manager & m, params_ref const & p) { tactic * mk_default_tactic(ast_manager & m, params_ref const & p) {
tactic * st = using_params(and_then(mk_simplify_tactic(m, p), tactic* simplify = mk_simplify_tactic(m, p);
// TODO: non-deterministic parameter evaluation
// TODO: non-deterministic parameter evaluation tactic* preamble = mk_preamble_tactic(m);
cond(mk_and(mk_is_propositional_probe(), mk_not(mk_produce_proofs_probe())), tactic* lazy_smt = mk_lazy_tactic(m, p, [&](auto& m_ref, auto const& p_ref) { return mk_smt_tactic(m_ref, p_ref); });
mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_fd_tactic(m, p); }), tactic* branch = and_then(preamble, lazy_smt);
// 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); }), tactic* lazy_qffplra = mk_lazy_tactic(m, p, [&](auto& m_ref, auto const& p_ref) { return mk_qffplra_tactic(m_ref, p_ref); });
// TODO: non-deterministic parameter evaluation probe* qffplra_probe = mk_is_qffplra_probe();
cond(mk_is_qfaufbv_probe(), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_qfaufbv_tactic(m, p); }), branch = cond(qffplra_probe, lazy_qffplra, branch);
// 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); }), tactic* lazy_qffp = mk_lazy_tactic(m, p, [&](auto& m_ref, auto const& p_ref) { return mk_qffp_tactic(m_ref, p_ref); });
// TODO: non-deterministic parameter evaluation probe* qffp_probe = mk_is_qffp_probe();
cond(mk_is_qfauflia_probe(), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_qfauflia_tactic(m, p); }), branch = cond(qffp_probe, lazy_qffp, branch);
// 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); }), tactic* lazy_nra = mk_lazy_tactic(m, p, [&](auto& m_ref, auto const& p_ref) { return mk_nra_tactic(m_ref, p_ref); });
// TODO: non-deterministic parameter evaluation probe* nra_probe = mk_is_nra_probe();
cond(mk_is_qfnra_probe(), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_qfnra_tactic(m, p); }), branch = cond(nra_probe, lazy_nra, branch);
// 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); }), tactic* lazy_lira = mk_lazy_tactic(m, p, [&](auto& m_ref, auto const& p_ref) { return mk_lira_tactic(m_ref, p_ref); });
// TODO: non-deterministic parameter evaluation probe* lira_probe = mk_is_lira_probe();
cond(mk_is_lira_probe(), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_lira_tactic(m, p); }), branch = cond(lira_probe, lazy_lira, branch);
// 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); }), tactic* lazy_qfnia = mk_lazy_tactic(m, p, [&](auto& m_ref, auto const& p_ref) { return mk_qfnia_tactic(m_ref, p_ref); });
// TODO: non-deterministic parameter evaluation probe* qfnia_probe = mk_is_qfnia_probe();
cond(mk_is_qffp_probe(), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_qffp_tactic(m, p); }), branch = cond(qfnia_probe, lazy_qfnia, branch);
// 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); }), tactic* lazy_qfnra = mk_lazy_tactic(m, p, [&](auto& m_ref, auto const& p_ref) { return mk_qfnra_tactic(m_ref, p_ref); });
//cond(mk_is_qfufnra_probe(), mk_qfufnra_tactic(m, p), probe* qfnra_probe = mk_is_qfnra_probe();
// TODO: non-deterministic parameter evaluation branch = cond(qfnra_probe, lazy_qfnra, branch);
and_then(mk_preamble_tactic(m), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_smt_tactic(m, p);}))))))))))))))),
p); 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; return st;
} }

9
src/tactic/portfolio/smt_strategic_solver.cpp
View file

@ -185,10 +185,9 @@ public:
if (!t) { if (!t) {
t = mk_tactic_for_logic(m, p, l); t = mk_tactic_for_logic(m, p, l);
} }
// TODO: non-deterministic parameter evaluation solver* tactic_solver = mk_tactic2solver(m, t.get(), p, proofs_enabled, models_enabled, unsat_core_enabled, l);
return mk_combined_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);
mk_solver_for_logic(m, p, l), return mk_combined_solver(tactic_solver, logic_solver, p);
p);
} }
solver_factory* translate(ast_manager& m) override { solver_factory* translate(ast_manager& m) override {
@ -199,5 +198,3 @@ public:
solver_factory * mk_smt_strategic_solver_factory(symbol const & logic) { solver_factory * mk_smt_strategic_solver_factory(symbol const & logic) {
return alloc(smt_strategic_solver_factory, logic); return alloc(smt_strategic_solver_factory, logic);
} }