From 20cfbcd66b680bad0973c88963b1b19ed2264920 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 9 Jan 2016 13:29:44 -0800 Subject: [PATCH] dealing with issues #402 #399 #258 Signed-off-by: Nikolaj Bjorner --- src/api/api_quant.cpp | 5 +++++ src/api/python/z3.py | 2 ++ src/smt/theory_arith.h | 2 ++ src/smt/theory_arith_aux.h | 3 ++- src/smt/theory_arith_core.h | 41 +++++++++++++++++++++++++++++++++---- src/smt/theory_arith_eq.h | 3 +++ 6 files changed, 51 insertions(+), 5 deletions(-) diff --git a/src/api/api_quant.cpp b/src/api/api_quant.cpp index cfaf5b6df..73215580e 100644 --- a/src/api/api_quant.cpp +++ b/src/api/api_quant.cpp @@ -162,6 +162,11 @@ extern "C" { ptr_vector bound_asts; if (num_patterns > 0 && num_no_patterns > 0) { SET_ERROR_CODE(Z3_INVALID_USAGE); + RETURN_Z3(0); + } + if (num_bound == 0) { + SET_ERROR_CODE(Z3_INVALID_USAGE); + RETURN_Z3(0); } for (unsigned i = 0; i < num_bound; ++i) { app* a = to_app(bound[i]); diff --git a/src/api/python/z3.py b/src/api/python/z3.py index b8ec74d18..686d838b2 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -1815,6 +1815,8 @@ def _mk_quantifier(is_forall, vs, body, weight=1, qid="", skid="", patterns=[], if is_app(vs): vs = [vs] num_vars = len(vs) + if num_vars == 0: + raise Z3Exception("Quantification requires a non-empty list of variables.") _vs = (Ast * num_vars)() for i in range(num_vars): ## TODO: Check if is constant diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index 7b56f19e5..703e19f1d 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -544,6 +544,8 @@ namespace smt { void set_var_kind(theory_var v, var_kind k) { m_data[v].m_kind = k; } unsigned get_var_row(theory_var v) const { SASSERT(!is_non_base(v)); return m_data[v].m_row_id; } void set_var_row(theory_var v, unsigned r_id) { m_data[v].m_row_id = r_id; } + ptr_vector m_todo; + bool is_int_expr(expr* e); bool is_int(theory_var v) const { return m_data[v].m_is_int; } bool is_real(theory_var v) const { return !is_int(v); } bool get_implied_old_value(theory_var v, inf_numeral & r) const; diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index 4291590c6..72004f8b0 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -838,8 +838,9 @@ namespace smt { template typename theory_arith::inf_numeral theory_arith::normalize_bound(theory_var v, inf_numeral const & k, bound_kind kind) { - if (is_real(v)) + if (is_real(v)) { return k; + } if (kind == B_LOWER) return inf_numeral(ceil(k)); SASSERT(kind == B_UPPER); diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 4561e1ced..6f245d1c6 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -64,12 +64,44 @@ namespace smt { return f >= adaptive_assertion_threshold(); } + template + bool theory_arith::is_int_expr(expr* e) { + if (m_util.is_int(e)) return true; + if (is_uninterp(e)) return false; + m_todo.reset(); + m_todo.push_back(e); + rational r; + unsigned i = 0; + while (!m_todo.empty()) { + ++i; + if (i > 100) { + return false; + } + e = m_todo.back(); + m_todo.pop_back(); + if (m_util.is_to_real(e)) { + // pass + } + else if (m_util.is_numeral(e, r) && r.is_int()) { + // pass + } + else if (m_util.is_add(e) || m_util.is_mul(e)) { + m_todo.append(to_app(e)->get_num_args(), to_app(e)->get_args()); + } + else { + return false; + } + } + return true; + } + + template theory_var theory_arith::mk_var(enode * n) { theory_var r = theory::mk_var(n); SASSERT(r == static_cast(m_columns.size())); SASSERT(check_vector_sizes()); - bool is_int = m_util.is_int(n->get_owner()); + bool is_int = is_int_expr(n->get_owner()); TRACE("mk_arith_var", tout << mk_pp(n->get_owner(), get_manager()) << " is_int: " << is_int << "\n";); m_columns .push_back(column()); m_data .push_back(var_data(is_int)); @@ -835,7 +867,6 @@ namespace smt { void theory_arith::mk_bound_axioms(atom * a1) { theory_var v = a1->get_var(); atoms & occs = m_var_occs[v]; - //SASSERT(v != 15); TRACE("mk_bound_axioms", tout << "add bound axioms for v" << v << " " << a1 << "\n";); if (!get_context().is_searching()) { // @@ -974,9 +1005,9 @@ namespace smt { --i; } } - TRACE("arith", + CTRACE("arith", !atoms.empty(), for (unsigned i = 0; i < atoms.size(); ++i) { - atoms[i]->display(*this, tout); + atoms[i]->display(*this, tout); tout << "\n"; }); ptr_vector occs(m_var_occs[v]); @@ -1106,6 +1137,8 @@ namespace smt { kind = A_LOWER; app * lhs = to_app(n->get_arg(0)); app * rhs = to_app(n->get_arg(1)); + expr * rhs2; + if (m_util.is_to_real(rhs, rhs2) && is_app(rhs2)) { rhs = to_app(rhs2); } SASSERT(m_util.is_numeral(rhs)); theory_var v = internalize_term_core(lhs); if (v == null_theory_var) { diff --git a/src/smt/theory_arith_eq.h b/src/smt/theory_arith_eq.h index 7e61b968e..7ed6cfe50 100644 --- a/src/smt/theory_arith_eq.h +++ b/src/smt/theory_arith_eq.h @@ -328,6 +328,9 @@ namespace smt { // Ignore equality if variables are already known to be equal. if (is_equal(x, y)) return; + if (get_manager().get_sort(var2expr(x)) != get_manager().get_sort(var2expr(y))) { + return; + } context & ctx = get_context(); region & r = ctx.get_region(); enode * _x = get_enode(x);