mirror of
https://github.com/Z3Prover/z3
synced 2026-06-11 11:25:36 +00:00
fix regression from nlsat integration
updates to nlsat polynomial simplification introduced checkpoints.
These can throw exceptions (if setting a timeout).
The code that uses this was not properly protected from exceptions to distinguish timeout based tactics from genuine exceptions that should terminate solving altogether.
see updates such as: 117da362f0
This commit is contained in:
Nikolaj Bjorner
parent
6420bff843
commit
b0956429fe
2 changed files with 73 additions and 65 deletions
|
|
@ -260,20 +260,9 @@ struct solver::imp {
|
||||||
out.close();
|
out.close();
|
||||||
}
|
}
|
||||||
|
|
||||||
lbool r = l_undef;
|
|
||||||
statistics& st = m_nla_core.lp_settings().stats().m_st;
|
statistics& st = m_nla_core.lp_settings().stats().m_st;
|
||||||
try {
|
lbool r = m_nlsat->check();
|
||||||
r = m_nlsat->check();
|
|
||||||
}
|
|
||||||
catch (z3_exception&) {
|
|
||||||
if (m_limit.is_canceled()) {
|
|
||||||
r = l_undef;
|
|
||||||
}
|
|
||||||
else {
|
|
||||||
m_nlsat->collect_statistics(st);
|
|
||||||
throw;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
m_nlsat->collect_statistics(st);
|
m_nlsat->collect_statistics(st);
|
||||||
TRACE(nra, tout << "nra result " << r << "\n");
|
TRACE(nra, tout << "nra result " << r << "\n");
|
||||||
CTRACE(nra, false,
|
CTRACE(nra, false,
|
||||||
|
|
@ -406,25 +395,15 @@ struct solver::imp {
|
||||||
setup_assignment_solver();
|
setup_assignment_solver();
|
||||||
lbool r = l_undef;
|
lbool r = l_undef;
|
||||||
statistics &st = m_nla_core.lp_settings().stats().m_st;
|
statistics &st = m_nla_core.lp_settings().stats().m_st;
|
||||||
nlsat::literal_vector clause;
|
nlsat::literal_vector clause;
|
||||||
try {
|
nlsat::assignment rvalues(m_nlsat->am());
|
||||||
nlsat::assignment rvalues(m_nlsat->am());
|
for (auto [j, x] : m_lp2nl) {
|
||||||
for (auto [j, x] : m_lp2nl) {
|
scoped_anum a(am());
|
||||||
scoped_anum a(am());
|
am().set(a, m_nla_core.val(j).to_mpq());
|
||||||
am().set(a, m_nla_core.val(j).to_mpq());
|
rvalues.set(x, a);
|
||||||
rvalues.set(x, a);
|
|
||||||
}
|
|
||||||
r = m_nlsat->check(rvalues, clause);
|
|
||||||
}
|
|
||||||
catch (z3_exception &) {
|
|
||||||
if (m_limit.is_canceled()) {
|
|
||||||
r = l_undef;
|
|
||||||
}
|
|
||||||
else {
|
|
||||||
m_nlsat->collect_statistics(st);
|
|
||||||
throw;
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
|
r = m_nlsat->check(rvalues, clause);
|
||||||
|
|
||||||
m_nlsat->collect_statistics(st);
|
m_nlsat->collect_statistics(st);
|
||||||
switch (r) {
|
switch (r) {
|
||||||
case l_true:
|
case l_true:
|
||||||
|
|
@ -657,20 +636,8 @@ struct solver::imp {
|
||||||
add_ub(lra.get_upper_bound(v), w, lra.get_column_upper_bound_witness(v));
|
add_ub(lra.get_upper_bound(v), w, lra.get_column_upper_bound_witness(v));
|
||||||
}
|
}
|
||||||
|
|
||||||
lbool r = l_undef;
|
lbool r = m_nlsat->check();
|
||||||
statistics& st = m_nla_core.lp_settings().stats().m_st;
|
statistics &st = m_nla_core.lp_settings().stats().m_st;
|
||||||
try {
|
|
||||||
r = m_nlsat->check();
|
|
||||||
}
|
|
||||||
catch (z3_exception&) {
|
|
||||||
if (m_limit.is_canceled()) {
|
|
||||||
r = l_undef;
|
|
||||||
}
|
|
||||||
else {
|
|
||||||
m_nlsat->collect_statistics(st);
|
|
||||||
throw;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
m_nlsat->collect_statistics(st);
|
m_nlsat->collect_statistics(st);
|
||||||
|
|
||||||
switch (r) {
|
switch (r) {
|
||||||
|
|
@ -719,18 +686,8 @@ struct solver::imp {
|
||||||
add_ub(lra.get_upper_bound(v), w);
|
add_ub(lra.get_upper_bound(v), w);
|
||||||
}
|
}
|
||||||
|
|
||||||
lbool r = l_undef;
|
|
||||||
try {
|
lbool r = m_nlsat->check();
|
||||||
r = m_nlsat->check();
|
|
||||||
}
|
|
||||||
catch (z3_exception&) {
|
|
||||||
if (m_limit.is_canceled()) {
|
|
||||||
r = l_undef;
|
|
||||||
}
|
|
||||||
else {
|
|
||||||
throw;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
if (r == l_true)
|
if (r == l_true)
|
||||||
return r;
|
return r;
|
||||||
|
|
@ -959,19 +916,68 @@ solver::~solver() {
|
||||||
|
|
||||||
|
|
||||||
lbool solver::check() {
|
lbool solver::check() {
|
||||||
return m_imp->check();
|
try {
|
||||||
|
return m_imp->check();
|
||||||
|
}
|
||||||
|
catch (z3_exception &) {
|
||||||
|
statistics &st = m_imp->m_nla_core.lp_settings().stats().m_st;
|
||||||
|
m_imp->m_nlsat->collect_statistics(st);
|
||||||
|
if (m_imp->m_limit.is_canceled()) {
|
||||||
|
return l_undef;
|
||||||
|
}
|
||||||
|
else {
|
||||||
|
throw;
|
||||||
|
}
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
lbool solver::check(vector<dd::pdd> const& eqs) {
|
lbool solver::check(vector<dd::pdd> const& eqs) {
|
||||||
return m_imp->check(eqs);
|
try {
|
||||||
|
return m_imp->check(eqs);
|
||||||
|
}
|
||||||
|
catch (z3_exception &) {
|
||||||
|
statistics &st = m_imp->m_nla_core.lp_settings().stats().m_st;
|
||||||
|
m_imp->m_nlsat->collect_statistics(st);
|
||||||
|
if (m_imp->m_limit.is_canceled()) {
|
||||||
|
return l_undef;
|
||||||
|
}
|
||||||
|
else {
|
||||||
|
throw;
|
||||||
|
}
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
lbool solver::check(dd::solver::equation_vector const& eqs) {
|
lbool solver::check(dd::solver::equation_vector const& eqs) {
|
||||||
return m_imp->check(eqs);
|
try {
|
||||||
|
return m_imp->check(eqs);
|
||||||
|
}
|
||||||
|
catch (z3_exception &) {
|
||||||
|
statistics &st = m_imp->m_nla_core.lp_settings().stats().m_st;
|
||||||
|
m_imp->m_nlsat->collect_statistics(st);
|
||||||
|
if (m_imp->m_limit.is_canceled()) {
|
||||||
|
return l_undef;
|
||||||
|
}
|
||||||
|
else {
|
||||||
|
throw;
|
||||||
|
}
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
lbool solver::check_assignment() {
|
lbool solver::check_assignment() {
|
||||||
return m_imp->check_assignment();
|
try {
|
||||||
|
return m_imp->check_assignment();
|
||||||
|
}
|
||||||
|
catch (z3_exception &) {
|
||||||
|
statistics &st = m_imp->m_nla_core.lp_settings().stats().m_st;
|
||||||
|
m_imp->m_nlsat->collect_statistics(st);
|
||||||
|
IF_VERBOSE(0, verbose_stream() << "check-assignment\n");
|
||||||
|
if (m_imp->m_limit.is_canceled()) {
|
||||||
|
return l_undef;
|
||||||
|
}
|
||||||
|
else {
|
||||||
|
throw;
|
||||||
|
}
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
bool solver::need_check() {
|
bool solver::need_check() {
|
||||||
|
|
|
||||||
|
|
@ -96,7 +96,8 @@ static tactic * mk_qfnia_sat_solver(ast_manager & m, params_ref const & p) {
|
||||||
params_ref simp_p = p;
|
params_ref simp_p = p;
|
||||||
simp_p.set_bool("hoist_mul", true); // hoist multipliers to create smaller circuits.
|
simp_p.set_bool("hoist_mul", true); // hoist multipliers to create smaller circuits.
|
||||||
|
|
||||||
return and_then(using_params(mk_simplify_tactic(m), simp_p),
|
return and_then(mk_report_verbose_tactic("(qfnia-sat)", 2),
|
||||||
|
using_params(mk_simplify_tactic(m), simp_p),
|
||||||
mk_nla2bv_tactic(m, nia2sat_p),
|
mk_nla2bv_tactic(m, nia2sat_p),
|
||||||
skip_if_failed(mk_qfnia_bv_solver(m, p)),
|
skip_if_failed(mk_qfnia_bv_solver(m, p)),
|
||||||
mk_fail_if_undecided_tactic());
|
mk_fail_if_undecided_tactic());
|
||||||
|
|
@ -107,7 +108,8 @@ static tactic * mk_qfnia_nlsat_solver(ast_manager & m, params_ref const & p) {
|
||||||
simp_p.set_bool("som", true); // expand into sums of monomials
|
simp_p.set_bool("som", true); // expand into sums of monomials
|
||||||
simp_p.set_bool("factor", false);
|
simp_p.set_bool("factor", false);
|
||||||
|
|
||||||
return and_then(using_params(mk_simplify_tactic(m), simp_p),
|
return and_then(mk_report_verbose_tactic("(qfnia-nlsat)", 2),
|
||||||
|
using_params(mk_simplify_tactic(m), simp_p),
|
||||||
try_for(mk_qfnra_nlsat_tactic(m, simp_p), 3000),
|
try_for(mk_qfnra_nlsat_tactic(m, simp_p), 3000),
|
||||||
mk_fail_if_undecided_tactic());
|
mk_fail_if_undecided_tactic());
|
||||||
}
|
}
|
||||||
|
|
@ -115,14 +117,14 @@ static tactic * mk_qfnia_nlsat_solver(ast_manager & m, params_ref const & p) {
|
||||||
static tactic * mk_qfnia_smt_solver(ast_manager& m, params_ref const& p) {
|
static tactic * mk_qfnia_smt_solver(ast_manager& m, params_ref const& p) {
|
||||||
params_ref simp_p = p;
|
params_ref simp_p = p;
|
||||||
simp_p.set_bool("som", true); // expand into sums of monomials
|
simp_p.set_bool("som", true); // expand into sums of monomials
|
||||||
return and_then(
|
return and_then(mk_report_verbose_tactic("(qfnia-smt)", 2),
|
||||||
using_params(mk_simplify_tactic(m), simp_p),
|
using_params(mk_simplify_tactic(m), simp_p),
|
||||||
mk_smt_tactic(m));
|
mk_smt_tactic(m));
|
||||||
}
|
}
|
||||||
|
|
||||||
tactic * mk_qfnia_tactic(ast_manager & m, params_ref const & p) {
|
tactic * mk_qfnia_tactic(ast_manager & m, params_ref const & p) {
|
||||||
return and_then(
|
return and_then(
|
||||||
mk_report_verbose_tactic("(qfnia-tactic)", 10),
|
mk_report_verbose_tactic("(qfnia-tactic)", 2),
|
||||||
mk_qfnia_preamble(m, p),
|
mk_qfnia_preamble(m, p),
|
||||||
or_else(mk_qfnia_sat_solver(m, p),
|
or_else(mk_qfnia_sat_solver(m, p),
|
||||||
try_for(mk_qfnia_smt_solver(m, p), 2000),
|
try_for(mk_qfnia_smt_solver(m, p), 2000),
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue