mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-21 05:13:39 +00:00
Code Activity

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

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-01-09 10:01:44 -08:00
parent aecab2b35b
commit fc4260e018
2 changed files with 6 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/muz/pdr/pdr_context.cpp
View file

@ -1705,6 +1705,7 @@ namespace pdr {
void context::validate_search() { void context::validate_search() {
expr_ref tr = m_search.get_trace(*this); expr_ref tr = m_search.get_trace(*this);
TRACE("pdr", tout << tr << "\n";);
smt::kernel solver(m, get_fparams()); smt::kernel solver(m, get_fparams());
solver.assert_expr(tr); solver.assert_expr(tr);
lbool res = solver.check(); lbool res = solver.check();

6
src/smt/theory_arith_nl.h
View file

@ -354,6 +354,7 @@ namespace smt {
*/ */
template<typename Ext> template<typename Ext>
interval theory_arith<Ext>::evaluate_as_interval(expr * n) { interval theory_arith<Ext>::evaluate_as_interval(expr * n) {
expr* arg;
TRACE("nl_evaluate", tout << "evaluating: " << mk_bounded_pp(n, get_manager(), 10) << "\n";); TRACE("nl_evaluate", tout << "evaluating: " << mk_bounded_pp(n, get_manager(), 10) << "\n";);
if (has_var(n)) { if (has_var(n)) {
TRACE("nl_evaluate", tout << "n has a variable associated with it\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";); TRACE("cross_nested_eval_bug", display_nested_form(tout, n); tout << "\ninterval: " << r << "\n";);
return r; return r;
} }
else if (m_util.is_to_real(n, arg)) {
return evaluate_as_interval(arg);
}
else { else {
rational val; rational val;
if (m_util.is_numeral(n, 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. 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 return true; // giving up... see comment above
TRACE("cross_nested", tout << "cheking problematic row...\n";); TRACE("cross_nested", tout << "cheking problematic row...\n";);