dealing with issues #402 #399 #258

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/api/api_quant.cpp

@@ -162,6 +162,11 @@ extern "C" {
         ptr_vector<expr> 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]);

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

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<expr> 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;

src/smt/theory_arith_aux.h

@@ -838,8 +838,9 @@ namespace smt {
     
     template<typename Ext>
     typename theory_arith<Ext>::inf_numeral theory_arith<Ext>::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);

src/smt/theory_arith_core.h

@@ -64,12 +64,44 @@ namespace smt {
         return f >= adaptive_assertion_threshold();
     }
 
+    template<typename Ext>
+    bool theory_arith<Ext>::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<typename Ext>
     theory_var theory_arith<Ext>::mk_var(enode * n) {
         theory_var r = theory::mk_var(n);
         SASSERT(r == static_cast<int>(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<Ext>::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<atom> 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) {

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);