From fc4260e0183dc35a6bad0e9fd124b18623f65c45 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 9 Jan 2016 10:01:44 -0800 Subject: [PATCH] enable Horner evaluation also for mixed-integer constraints now that ast-manger inserts coercions on the fly. Avoids loop for issue #399, but with this alone results in unknown status Signed-off-by: Nikolaj Bjorner --- src/muz/pdr/pdr_context.cpp | 1 + src/smt/theory_arith_nl.h | 6 +++++- 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp index b3648f38d..20bf183e0 100644 --- a/src/muz/pdr/pdr_context.cpp +++ b/src/muz/pdr/pdr_context.cpp @@ -1705,6 +1705,7 @@ namespace pdr { void context::validate_search() { expr_ref tr = m_search.get_trace(*this); + TRACE("pdr", tout << tr << "\n";); smt::kernel solver(m, get_fparams()); solver.assert_expr(tr); lbool res = solver.check(); diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index 982aa963f..311a62a38 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -354,6 +354,7 @@ namespace smt { */ template interval theory_arith::evaluate_as_interval(expr * n) { + expr* arg; TRACE("nl_evaluate", tout << "evaluating: " << mk_bounded_pp(n, get_manager(), 10) << "\n";); if (has_var(n)) { TRACE("nl_evaluate", tout << "n has a variable associated with it\n";); @@ -385,6 +386,9 @@ namespace smt { TRACE("cross_nested_eval_bug", display_nested_form(tout, n); tout << "\ninterval: " << r << "\n";); return r; } + else if (m_util.is_to_real(n, arg)) { + return evaluate_as_interval(arg); + } else { rational val; if (m_util.is_numeral(n, val)) { @@ -1660,7 +1664,7 @@ namespace smt { 3) (new non-int coeffs) This only happens in an optional step in the conversion. Now, for int rows, I only apply this optional step only if non-int coeffs are not created. */ - if (is_mixed_real_integer(r)) + if (!get_manager().int_real_coercions() && is_mixed_real_integer(r)) return true; // giving up... see comment above TRACE("cross_nested", tout << "cheking problematic row...\n";);