Merge remote-tracking branch 'upstream/master' into lackr

README.md

@@ -66,31 +66,6 @@ make
 make install
 ```
 
-Note the above will typically disable the installation of the Python bindings
-because the Python ``site-packages``  directory (e.g.
-``/usr/lib/python3.5/site-packages/``) is not rooted in the install prefix and
-installing outside of the install prefix is dangerous and misleading.
-
-To avoid this issue you can use the ``DESTDIR`` makefile variable and leave the
-install prefix as the default. The ``DESTDIR`` variable is prepended to the
-install locations during ``make install`` and ``make uninstall`` and is intended
-to allow ["staged installs"](https://www.gnu.org/prep/standards/html_node/DESTDIR.html).
-Therefore it must always contain a trailing slash.
-
-For example:
-
-```bash
-python scripts/mk_make.py
-cd build
-make
-make install DESTDIR=/home/leo/
-```
-
-In this example, the Z3 Python bindings will be stored at
-``/home/leo/lib/pythonX.Y/site-packages``
-(``/home/leo/lib/pythonX.Y/dist-packages`` on Debian based Linux
-distributions) where X.Y corresponds to the python version in your system.
-
 To uninstall Z3, use
 
 ```bash
@@ -105,17 +80,16 @@ Z3 has bindings for various programming languages.
 
 ### ``.NET``
 
-These bindings are enabled by default on Windows and are enabled on other
+Use the ``--dotnet`` command line flag with ``mk_make.py`` to enable building these.
-platforms if [mono](http://www.mono-project.com/) is detected. On these
+
+On non-windows platforms [mono](http://www.mono-project.com/) is required. On these
 platforms the location of the C# compiler and gac utility need to be known. You
 can set these as follows if they aren't detected automatically. For example:
 
 ```bash
-CSC=/usr/bin/csc GACUTIL=/usr/bin/gacutil python scripts/mk_make.py
+CSC=/usr/bin/csc GACUTIL=/usr/bin/gacutil python scripts/mk_make.py --dotnet
 ```
 
-To disable building these bindings pass ``--nodotnet`` to ``mk_make.py``.
-
 Note for very old versions of Mono (e.g. ``2.10``) you may need to set ``CSC``
 to ``/usr/bin/dmcs``.
 
@@ -156,6 +130,34 @@ See [``examples/ml``](examples/ml) for examples.
 
 ### ``Python``
 
-These bindings are always enabled.
+Use the ``--python`` command line flag with ``mk_make.py`` to enable building these.
+
+Note that is required on certain platforms that the Python package directory
+(``site-packages`` on most distributions and ``dist-packages`` on Debian based
+distributions) live under the install prefix. If you use a non standard prefix
+you can use the ``--pypkgdir`` option to change the Python package directory
+used for installation. For example:
+
+```bash
+python scripts/mk_make.py --prefix=/home/leo --python --pypkgdir=/home/leo/lib/python-2.7/site-packages
+```
+
+If you do need to install to a non standard prefix a better approach is to use
+a [Python virtual environment](https://virtualenv.readthedocs.org/en/latest/)
+and install Z3 there.
+
+```bash
+virtualenv venv
+source venv/bin/activate
+python scripts/mk_make.py --python
+cd build
+make
+make install
+# You will find Z3 and the Python bindings installed in the virtual environment
+venv/bin/z3 -h
+...
+python -c 'import z3; print(z3.get_version_string())'
+...
+```
 
 See [``examples/python``](examples/python) for examples.

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:
+        return body
     _vs = (Ast * num_vars)()
     for i in range(num_vars):
         ## TODO: Check if is constant

src/ast/ast.cpp

@@ -2866,22 +2866,24 @@ proof * ast_manager::mk_unit_resolution(unsigned num_proofs, proof * const * pro
         svector<bool> found;
 #endif
         for (unsigned i = 0; i < num_args; i++) {
+            bool found_complement = false;
             expr * lit = cls->get_arg(i);
-            unsigned j = 1;
+            for (unsigned j = 1; j < num_proofs; j++) {
-            for (; j < num_proofs; j++) {
                 expr const * _fact = get_fact(proofs[j]);
                 if (is_complement(lit, _fact)) {
-                    DEBUG_CODE(found.setx(j, true, false););
+                    found_complement = true;
+                    DEBUG_CODE(found.setx(j, true, false); continue;);                    
                     break;
                 }
             }
-            if (j == num_proofs)
+            if (!found_complement)
                 new_lits.push_back(lit);
         }
         DEBUG_CODE({
             for (unsigned i = 1; m_proof_mode == PGM_FINE && i < num_proofs; i++) {
                 CTRACE("mk_unit_resolution_bug", !found.get(i, false), 
                        for (unsigned j = 0; j < num_proofs; j++) {
+                           if (j == i) tout << "Index " << i << " was not found:\n";                       
                            tout << mk_ll_pp(get_fact(proofs[j]), *this);
                        });
                 SASSERT(found.get(i, false));

src/muz/base/dl_context.cpp

@@ -891,6 +891,7 @@ namespace datalog {
     }
 
     lbool context::rel_query(unsigned num_rels, func_decl * const* rels) {        
+        m_last_answer = 0;
         ensure_engine();
         return m_engine->query(num_rels, rels);
     }

src/muz/base/dl_rule.cpp

@@ -282,6 +282,8 @@ namespace datalog {
 
 
     func_decl* rule_manager::mk_query(expr* query, rule_set& rules) {
+        TRACE("dl", tout << mk_pp(query, m) << "\n";);
+            
         ptr_vector<sort> vars;
         svector<symbol> names;
         app_ref_vector body(m);
@@ -290,6 +292,7 @@ namespace datalog {
         // Add implicit variables.
         // Remove existential prefix.
         bind_variables(query, false, q);
+
         quantifier_hoister qh(m);
         qh.pull_quantifier(false, q, 0, &names);
         // retrieve free variables.
@@ -358,6 +361,7 @@ namespace datalog {
         if (!vars.empty()) {
             rule_expr = m.mk_forall(vars.size(), vars.c_ptr(), names.c_ptr(), impl);
         }
+        TRACE("dl", tout << rule_expr << "\n";);
 
         scoped_proof_mode _sc(m, m_ctx.generate_proof_trace()?PGM_FINE:PGM_DISABLED);
         proof_ref pr(m);

src/muz/base/hnf.cpp

@@ -325,9 +325,10 @@ private:
 
     void eliminate_disjunctions(expr_ref_vector::element_ref& body, proof_ref_vector& proofs) {
         expr* b = body.get(); 
-        expr* e1;
+        expr* e1, *e2;
         bool negate_args = false;
         bool is_disj = false;
+        expr_ref_vector _body(m);
         unsigned num_disj = 0;
         expr* const* disjs = 0;
         if (!contains_predicate(b)) {
@@ -346,6 +347,14 @@ private:
             num_disj = to_app(e1)->get_num_args();
             disjs = to_app(e1)->get_args();
         }
+        if (m.is_implies(b, e1, e2)) {
+            is_disj = true;
+            _body.push_back(mk_not(m, e1));
+            _body.push_back(e2);
+            disjs = _body.c_ptr();
+            num_disj = 2;
+            negate_args = false;
+        }
         if (is_disj) {
             app* old_head = 0;
             if (m_memoize_disj.find(b, old_head)) {

src/muz/fp/dl_cmds.cpp

@@ -114,9 +114,16 @@ struct dl_context {
         }
     }    
 
-    bool collect_query(expr* q) {
+    bool collect_query(func_decl* q) {
         if (m_collected_cmds) {
-            expr_ref qr = m_context->bind_vars(q, false);
+            ast_manager& m = m_cmd.m();
+            expr_ref qr(m);
+            expr_ref_vector args(m);
+            for (unsigned i = 0; i < q->get_arity(); ++i) {
+                args.push_back(m.mk_var(i, q->get_domain(i)));
+            }
+            qr = m.mk_app(q, args.size(), args.c_ptr());
+            qr = m_context->bind_vars(qr, false);
             m_collected_cmds->m_queries.push_back(qr);
             m_trail.push(push_back_vector<dl_context, expr_ref_vector>(m_collected_cmds->m_queries));
             return true;
@@ -187,30 +194,30 @@ public:
     virtual void finalize(cmd_context & ctx) { 
     }
     virtual void execute(cmd_context & ctx) {
-      m_dl_ctx->add_rule(m_t, m_name, m_bound);
+        m_dl_ctx->add_rule(m_t, m_name, m_bound);
     }
 };
 
 class dl_query_cmd : public parametric_cmd {
     ref<dl_context> m_dl_ctx;
-    expr* m_target;
+    func_decl* m_target;
 public:
     dl_query_cmd(dl_context * dl_ctx):
         parametric_cmd("query"),
         m_dl_ctx(dl_ctx),
         m_target(0) {
     }
-    virtual char const * get_usage() const { return "(exists (q) (and body))"; }
+    virtual char const * get_usage() const { return "predicate"; }
     virtual char const * get_main_descr() const { 
-        return "pose a query based on the Horn rules."; 
+        return "pose a query to a predicate based on the Horn rules."; 
     }
 
     virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { 
-        if (m_target == 0) return CPK_EXPR;
+        if (m_target == 0) return CPK_FUNC_DECL;
         return parametric_cmd::next_arg_kind(ctx);
     }
 
-    virtual void set_next_arg(cmd_context & ctx, expr * t) {
+    virtual void set_next_arg(cmd_context & ctx, func_decl* t) {
         m_target = t;
     }
 
@@ -239,7 +246,7 @@ public:
             scoped_timer timer(timeout, &eh);
             cmd_context::scoped_watch sw(ctx);
             try {
-                status = dlctx.query(m_target);
+                status = dlctx.rel_query(1, &m_target);
             }
             catch (z3_error & ex) {
                 ctx.regular_stream() << "(error \"query failed: " << ex.msg() << "\")" << std::endl;

src/parsers/smt2/smt2parser.cpp

@@ -719,9 +719,9 @@ namespace smt2 {
             SASSERT(sort_stack().size() == stack_pos + 1);
         }
 
-        unsigned parse_sorts() {
+        unsigned parse_sorts(char const* context) {
-            unsigned sz = 0;
+            unsigned sz = 0;            
-            check_lparen_next("invalid list of sorts, '(' expected");
+            check_lparen_next(context);
             while (!curr_is_rparen()) {
                 parse_sort();
                 sz++;
@@ -2019,7 +2019,7 @@ namespace smt2 {
             symbol id = curr_id();
             next();
             unsigned spos = sort_stack().size();
-            unsigned num_params = parse_sorts();
+            unsigned num_params = parse_sorts("Parsing function declaration. Expecting sort list '('");
             parse_sort();
             func_decl_ref f(m());
             f = m().mk_func_decl(id, num_params, sort_stack().c_ptr() + spos, sort_stack().back());
@@ -2300,7 +2300,7 @@ namespace smt2 {
                     next();
                 }
                 unsigned spos = sort_stack().size();
-                parse_sorts();
+                parse_sorts("Parsing function name. Expecting sort list startig with '(' to disambiguate function name");
                 unsigned domain_size = sort_stack().size() - spos;
                 parse_sort();
                 func_decl * d = m_ctx.find_func_decl(id, indices.size(), indices.c_ptr(), domain_size, sort_stack().c_ptr() + spos, sort_stack().back());
@@ -2380,7 +2380,7 @@ namespace smt2 {
                 return;
             case CPK_SORT_LIST: {
                 unsigned spos = sort_stack().size();
-                unsigned num = parse_sorts();
+                unsigned num = parse_sorts("expecting sort list starting with '('");
                 m_curr_cmd->set_next_arg(m_ctx, num, sort_stack().c_ptr() + spos);
                 break;
             }

src/smt/proto_model/proto_model.cpp

@@ -174,6 +174,13 @@ bool eval(func_interp & fi, simplifier & s, expr * const * args, expr_ref & resu
     return true;
 }
 
+bool proto_model::is_select_of_model_value(expr* e) const {
+    return 
+        is_app_of(e, m_afid, OP_SELECT) && 
+        is_as_array(to_app(e)->get_arg(0)) &&
+        has_interpretation(array_util(m_manager).get_as_array_func_decl(to_app(to_app(e)->get_arg(0))));
+}
+
 /**
    \brief Evaluate the expression e in the current model, and store the result in \c result.
    It returns \c true if succeeded, and false otherwise. If the evaluation fails,
@@ -257,7 +264,7 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
                         m_simplifier.mk_app(f, num_args, args.c_ptr(), new_t);
                         TRACE("model_eval", tout << mk_pp(t, m_manager) << " -> " << new_t << "\n";);
                         trail.push_back(new_t);
-                        if (!is_app(new_t) || to_app(new_t)->get_decl() != f) {
+                        if (!is_app(new_t) || to_app(new_t)->get_decl() != f || is_select_of_model_value(new_t)) {
                             // if the result is not of the form (f ...), then assume we must simplify it.
                             expr * new_new_t = 0;
                             if (!eval_cache.find(new_t.get(), new_new_t)) {
@@ -588,7 +595,7 @@ void proto_model::register_value(expr * n) {
     }
 }
 
-bool proto_model::is_array_value(expr * v) const {
+bool proto_model::is_as_array(expr * v) const {
     return is_app_of(v, m_afid, OP_AS_ARRAY);
 }
 

src/smt/proto_model/proto_model.h

@@ -59,6 +59,7 @@ class proto_model : public model_core {
     void remove_aux_decls_not_in_set(ptr_vector<func_decl> & decls, func_decl_set const & s);
     void cleanup_func_interp(func_interp * fi, func_decl_set & found_aux_fs);
 
+    bool is_select_of_model_value(expr* e) const;
 
 public:
     proto_model(ast_manager & m, simplifier & s, params_ref const & p = params_ref());
@@ -68,7 +69,7 @@ public:
 
     bool eval(expr * e, expr_ref & result, bool model_completion = false);
 
-    bool is_array_value(expr * v) const;
+    bool is_as_array(expr * v) const;
     
     value_factory * get_factory(family_id fid);
 

src/smt/smt_context.cpp

@@ -4126,6 +4126,7 @@ namespace smt {
             if (m_fparams.m_model_compact)
                 m_proto_model->compress();
             TRACE("mbqi_bug", tout << "after cleanup:\n"; model_pp(tout, *m_proto_model););
+            //SASSERT(validate_model());
         }
     }
 

src/smt/smt_context.h

@@ -1415,6 +1415,8 @@ namespace smt {
         bool update_model(bool refinalize);
 
         void get_proto_model(proto_model_ref & m) const;
+
+        bool validate_model();
         
         unsigned get_num_asserted_formulas() const { return m_asserted_formulas.get_num_formulas(); }
 

src/smt/smt_context_inv.cpp

@@ -399,6 +399,45 @@ namespace smt {
 
 #endif
 
+    bool context::validate_model() {
+        if (!m_proto_model) {
+            return true;
+        }
+        ast_manager& m = m_manager;
+        literal_vector::const_iterator it  = m_assigned_literals.begin();
+        literal_vector::const_iterator end = m_assigned_literals.end();
+        for (; it != end; ++it) {
+            literal lit = *it;
+            if (!is_relevant(lit)) {
+                continue;
+            }
+            expr_ref n(m), res(m);
+            literal2expr(lit, n);
+            if (!is_ground(n)) {
+                continue;
+            }
+            switch (get_assignment(*it)) {
+            case l_undef:
+                break;
+            case l_true:
+                m_proto_model->eval(n, res, false);
+                CTRACE("mbqi_bug", !m.is_true(res), tout << n << " evaluates to " << res << "\n";); 
+                if (m.is_false(res)) {
+                    return false;
+                }
+                break;
+            case l_false:
+                m_proto_model->eval(n, res, false);
+                CTRACE("mbqi_bug", !m.is_false(res), tout << n << " evaluates to " << res << "\n";); 
+                if (m.is_true(res)) {
+                    return false;
+                }
+                break;
+            }
+        }
+        return true;
+    }
+
     /**
        \brief validate unsat core returned by 
      */

src/smt/smt_context_pp.cpp

@@ -239,6 +239,7 @@ namespace smt {
                     first = false;
                 }
                 out << "#" << n->get_id() << " -> #" << r->get_id() << "\n";
+                out << mk_pp(n, m_manager) << " -> " << mk_pp(r, m_manager) << "\n";
             }
         }
     }

src/smt/smt_internalizer.cpp

@@ -291,18 +291,18 @@ namespace smt {
             return;
         }
         sort * s = m_manager.get_sort(n->get_arg(0));
-        sort * u = m_manager.mk_fresh_sort("distinct-elems");
+        sort_ref u(m_manager.mk_fresh_sort("distinct-elems"), m_manager);
-        func_decl * f = m_manager.mk_fresh_func_decl("distinct-aux-f", "", 1, &s, u);
+        func_decl_ref f(m_manager.mk_fresh_func_decl("distinct-aux-f", "", 1, &s, u), m_manager);
         for (unsigned i = 0; i < num_args; i++) {
             expr * arg  = n->get_arg(i);
-            app * fapp  = m_manager.mk_app(f, arg);
+            app_ref fapp(m_manager.mk_app(f, arg), m_manager);
-            app * val   = m_manager.mk_fresh_const("unique-value", u);
+            app_ref val(m_manager.mk_fresh_const("unique-value", u), m_manager);
             enode * e   = mk_enode(val, false, false, true);
             e->mark_as_interpreted();
-            app * eq    = m_manager.mk_eq(fapp, val);
+            app_ref eq(m_manager.mk_eq(fapp, val), m_manager);
             TRACE("assert_distinct", tout << "eq: " << mk_pp(eq, m_manager) << "\n";);
             assert_default(eq, 0);
-            mark_as_relevant(eq);
+            mark_as_relevant(eq.get());
             // TODO: we may want to hide the auxiliary values val and the function f from the model.
         }
     }
@@ -322,6 +322,9 @@ namespace smt {
         TRACE("internalize", tout << "internalizing:\n" << mk_pp(n, m_manager) << "\n";);
         TRACE("internalize_bug", tout << "internalizing:\n" << mk_bounded_pp(n, m_manager) << "\n";);
         if (m_manager.is_bool(n)) {
+            if (is_var(n)) {
+                throw default_exception("Formulas should not contain unbound variables");
+            }
             SASSERT(is_quantifier(n) || is_app(n));
             internalize_formula(n, gate_ctx);
         }
@@ -432,7 +435,7 @@ namespace smt {
         TRACE("distinct", tout << "internalizing distinct: " << mk_pp(n, m_manager) << "\n";);
         SASSERT(!b_internalized(n));
         SASSERT(m_manager.is_distinct(n));
-        expr * def  = m_manager.mk_distinct_expanded(n->get_num_args(), n->get_args());
+        expr_ref def(m_manager.mk_distinct_expanded(n->get_num_args(), n->get_args()), m_manager);
         internalize(def, true);
         bool_var v    = mk_bool_var(n);
         literal l(v);
@@ -750,8 +753,8 @@ namespace smt {
         expr * c  = n->get_arg(0);
         expr * t  = n->get_arg(1);
         expr * e  = n->get_arg(2);
-        app * eq1 = mk_eq_atom(n, t);
+        app_ref eq1(mk_eq_atom(n, t), m_manager);
-        app * eq2 = mk_eq_atom(n, e);
+        app_ref eq2(mk_eq_atom(n, e), m_manager);
         mk_enode(n, 
                  true /* supress arguments, I don't want to apply CC on ite terms */, 
                  false /* it is a term, so it should not be merged with true/false */,

src/smt/smt_model_checker.cpp

@@ -346,6 +346,10 @@ namespace smt {
         for (; it != end; ++it) {
             quantifier * q = *it;
 	    if(!m_qm->mbqi_enabled(q)) continue;
+            TRACE("model_checker", 
+                  tout << "Check: " << mk_pp(q, m_manager) << "\n";
+                  tout << m_context->get_assignment(q) << "\n";);
+
             if (m_context->is_relevant(q) && m_context->get_assignment(q) == l_true) {
                 if (m_params.m_mbqi_trace && q->get_qid() != symbol::null) {
                     verbose_stream() << "(smt.mbqi :checking " << q->get_qid() << ")\n";
@@ -364,8 +368,12 @@ namespace smt {
             m_iteration_idx++;
 
         TRACE("model_checker", tout << "model after check:\n"; model_pp(tout, *md););
-        TRACE("model_checker", tout << "model checker result: " << (num_failures == 0) << "\n";);
+        TRACE("model_checker", tout << "model checker result: " << (num_failures == 0) << "\n";);        
         m_max_cexs += m_params.m_mbqi_max_cexs;
+
+        if (num_failures == 0 && !m_context->validate_model()) {
+            num_failures = 1;
+        }
         if (num_failures == 0)
             m_curr_model->cleanup();
         if (m_params.m_mbqi_trace) {

src/smt/smt_model_finder.cpp

@@ -1418,7 +1418,7 @@ namespace smt {
 
             func_decl * get_array_func_decl(app * ground_array, auf_solver & s) {
                 expr * ground_array_interp = s.eval(ground_array, false);
-                if (ground_array_interp != 0 && s.get_model()->is_array_value(ground_array_interp))
+                if (ground_array_interp != 0 && s.get_model()->is_as_array(ground_array_interp))
                     return to_func_decl(to_app(ground_array_interp)->get_decl()->get_parameter(0).get_ast());
                 return 0;
             }

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

src/smt/theory_array.cpp

@@ -44,7 +44,9 @@ namespace smt {
 
     void theory_array::merge_eh(theory_var v1, theory_var v2, theory_var, theory_var) {
         // v1 is the new root
-        TRACE("array", tout << "merging v" << v1 << " v" << v2 << "\n"; display_var(tout, v1););
+        TRACE("array", 
+              tout << "merging v" << v1 << " v" << v2 << "\n"; display_var(tout, v1);
+              tout << mk_pp(get_enode(v1)->get_owner(), get_manager()) << " <- " << mk_pp(get_enode(v2)->get_owner(), get_manager()) << "\n";);
         SASSERT(v1 == find(v1));
         var_data * d1 = m_var_data[v1];
         var_data * d2 = m_var_data[v2];
@@ -70,21 +72,23 @@ namespace smt {
     }
 
     theory_var theory_array::mk_var(enode * n) {
+        ast_manager& m = get_manager();
+        context& ctx = get_context();
         theory_var r  = theory_array_base::mk_var(n);
         theory_var r2 = m_find.mk_var();
         SASSERT(r == r2);
         SASSERT(r == static_cast<int>(m_var_data.size()));
         m_var_data.push_back(alloc(var_data));
         var_data * d  = m_var_data[r];
-        TRACE("array", tout << mk_bounded_pp(n->get_owner(), get_manager()) << "\nis_array: " << is_array_sort(n) << ", is_select: " << is_select(n) <<
+        TRACE("array", tout << mk_bounded_pp(n->get_owner(), m) << "\nis_array: " << is_array_sort(n) << ", is_select: " << is_select(n) <<
               ", is_store: " << is_store(n) << "\n";);
         d->m_is_array  = is_array_sort(n);
         if (d->m_is_array) 
-            register_sort(get_manager().get_sort(n->get_owner()));
+            register_sort(m.get_sort(n->get_owner()));
-        d->m_is_select = is_select(n);
+        d->m_is_select = is_select(n);        
         if (is_store(n))
             d->m_stores.push_back(n);
-        get_context().attach_th_var(n, this, r);
+        ctx.attach_th_var(n, this, r);
         if (m_params.m_array_laziness <= 1 && is_store(n))
             instantiate_axiom1(n);
         return r;
@@ -97,6 +101,7 @@ namespace smt {
         v                = find(v);
         var_data * d     = m_var_data[v];
         d->m_parent_selects.push_back(s);
+        TRACE("array", tout << mk_pp(s->get_owner(), get_manager()) << " " << mk_pp(get_enode(v)->get_owner(), get_manager()) << "\n";);
         m_trail_stack.push(push_back_trail<theory_array, enode *, false>(d->m_parent_selects));
         ptr_vector<enode>::iterator it  = d->m_stores.begin();
         ptr_vector<enode>::iterator end = d->m_stores.end();
@@ -109,8 +114,9 @@ namespace smt {
             for (; it != end; ++it) {
                 enode * store = *it;
                 SASSERT(is_store(store));
-                if (!m_params.m_array_cg || store->is_cgr())
+                if (!m_params.m_array_cg || store->is_cgr()) {
                     instantiate_axiom2b(s, store);
+                }
             }
         }
     }
@@ -331,6 +337,9 @@ namespace smt {
     void theory_array::relevant_eh(app * n) {
         if (m_params.m_array_laziness == 0)
             return;
+        if (get_manager().is_ite(n)) {
+            TRACE("array", tout << "relevant ite " << mk_pp(n, get_manager()) << "\n";);
+        }
         if (!is_store(n) && !is_select(n))
             return;
         context & ctx    = get_context();

src/smt/theory_array.h

@@ -49,7 +49,7 @@ namespace smt {
             var_data():m_prop_upward(false), m_is_array(false), m_is_select(false) {}
         };
         ptr_vector<var_data>            m_var_data;
-        theory_array_params &           m_params;
+        theory_array_params&            m_params;
         theory_array_stats              m_stats;
         th_union_find                   m_find;
         th_trail_stack                  m_trail_stack;
@@ -98,7 +98,7 @@ namespace smt {
         theory_array(ast_manager & m, theory_array_params & params);
         virtual ~theory_array();
 
-        virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_array, new_ctx->get_manager(), m_params); }
+        virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_array, new_ctx->get_manager(), new_ctx->get_fparams()); }
 
         virtual char const * get_name() const { return "array"; }
 

src/smt/theory_array_base.cpp

@@ -943,6 +943,18 @@ namespace smt {
                 result->add_entry(args.size(), args.c_ptr(), select);
             }
         }
+        TRACE("array", 
+              tout << mk_pp(n->get_root()->get_owner(), get_manager()) << "\n";
+              if (sel_set) {
+                  select_set::iterator it  = sel_set->begin();
+                  select_set::iterator end = sel_set->end();
+                  for (; it != end; ++it) {
+                      tout << "#" << (*it)->get_root()->get_owner()->get_id() << " " << mk_pp((*it)->get_owner(), get_manager()) << "\n";
+                  }
+              }
+              if (else_val_n) {
+                  tout << "else: " << mk_pp(else_val_n->get_owner(), get_manager()) << "\n";
+              });
         return result;
     }
 

src/smt/theory_seq.cpp

@@ -551,9 +551,6 @@ bool theory_seq::is_solved() {
         IF_VERBOSE(10, verbose_stream() << "(seq.giveup " << m_eqs[0].ls() << " = " << m_eqs[0].rs() << " is unsolved)\n";);
         return false;
     }
-    if (!m_nqs.empty()) {
-        return false;
-    }
     for (unsigned i = 0; i < m_automata.size(); ++i) {
         if (!m_automata[i]) {
             IF_VERBOSE(10, verbose_stream() << "(seq.giveup regular expression did not compile to automaton)\n";);
@@ -1252,9 +1249,28 @@ void theory_seq::collect_statistics(::statistics & st) const {
     st.update("seq add axiom", m_stats.m_add_axiom);
 }
 
+void theory_seq::init_model(expr_ref_vector const& es) {
+    expr_ref new_s(m);
+    for (unsigned i = 0; i < es.size(); ++i) {
+        dependency* eqs = 0;
+        expr_ref s = canonize(es[i], eqs);
+        if (is_var(s)) {
+            new_s = m_factory->get_fresh_value(m.get_sort(s));
+            m_rep.update(s, new_s, eqs);
+        }
+    }
+}
+
 void theory_seq::init_model(model_generator & mg) {
     m_factory = alloc(seq_factory, get_manager(), get_family_id(), mg.get_model());
     mg.register_factory(m_factory);
+    for (unsigned j = 0; j < m_nqs.size(); ++j) {
+        ne const& n = m_nqs[j];
+        for (unsigned i = 0; i < n.ls().size(); ++i) {
+            init_model(n.ls(i));
+            init_model(n.rs(i));
+        }
+    }
 }
 
 
@@ -2182,7 +2198,7 @@ void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) {
     m_rewrite(eq);
     if (!m.is_false(eq)) {
         literal lit = ~mk_eq(e1, e2, false);
-        SASSERT(get_context().get_assignment(lit) == l_true);
+        //SASSERT(get_context().get_assignment(lit) == l_true);
         dependency* dep = m_dm.mk_leaf(assumption(lit));
         m_nqs.push_back(ne(e1, e2, dep));
         solve_nqs(m_nqs.size() - 1);

src/smt/theory_seq.h

@@ -301,6 +301,7 @@ namespace smt {
         virtual model_value_proc * mk_value(enode * n, model_generator & mg);
         virtual void init_model(model_generator & mg);
 
+        void init_model(expr_ref_vector const& es);
         // final check 
         bool simplify_and_solve_eqs();   // solve unitary equalities
         bool branch_variable();          // branch on a variable

src/smt/theory_seq_empty.h

@@ -31,7 +31,7 @@ namespace smt {
         symbol_set   m_strings;
         unsigned     m_next;
         char         m_char;
-        std::string  m_unique_prefix;
+        std::string  m_unique_delim;
         obj_map<sort, expr*> m_unique_sequences;
         expr_ref_vector m_trail;
     public:
@@ -43,7 +43,7 @@ namespace smt {
             u(m),
             m_next(0),
             m_char(0),
-            m_unique_prefix("#B"),
+            m_unique_delim("!"),
             m_trail(m)
         {
             m_strings.insert(symbol(""));
@@ -56,7 +56,7 @@ namespace smt {
         }
 
         void set_prefix(char const* p) {
-            m_unique_prefix = p;
+            m_unique_delim = p;
         }
 
         // generic method for setting unique sequences
@@ -89,7 +89,7 @@ namespace smt {
             if (u.is_string(s)) {
                 while (true) {
                     std::ostringstream strm;
-                    strm << m_unique_prefix << m_next++;
+                    strm << m_unique_delim << std::hex << m_next++ << std::dec << m_unique_delim;
                     symbol sym(strm.str().c_str());
                     if (m_strings.contains(sym)) continue;
                     m_strings.insert(sym);

src/util/mpf.cpp

@@ -244,32 +244,35 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode
         m_mpq_manager.abs(sig);
         m_mpz_manager.set(exp, exponent);
 
-        // Normalize
+        // Normalize such that 1.0 <= sig < 2.0
-        while (m_mpq_manager.ge(sig, 2)) {
+        if (m_mpq_manager.ge(sig, mpq(2))) {
-            m_mpq_manager.div(sig, mpq(2), sig);
+            unsigned int pp = m_mpq_manager.prev_power_of_two(sig);
-            m_mpz_manager.inc(exp);
+            scoped_mpz p2(m_mpz_manager);
+            m_mpq_manager.power(2, pp, p2);
+            m_mpq_manager.div(sig, p2, sig);
+            m_mpz_manager.add(exp, mpz(pp), exp);
         }
+        SASSERT(m_mpq_manager.lt(sig, mpq(2)));
 
         while (m_mpq_manager.lt(sig, 1)) {
             m_mpq_manager.mul(sig, 2, sig);
             m_mpz_manager.dec(exp);
         }
 
-        // 1.0 <= sig < 2.0
+        // Check that 1.0 <= sig < 2.0
         SASSERT((m_mpq_manager.le(1, sig) && m_mpq_manager.lt(sig, 2)));
 
-        TRACE("mpf_dbg", tout << "sig = " << m_mpq_manager.to_string(sig) <<
+        TRACE("mpf_dbg", tout << "Normalized: sig = " << m_mpq_manager.to_string(sig) <<
                                  " exp = " << m_mpz_manager.to_string(exp) << std::endl;);
 
-        m_mpz_manager.set(o.significand, 0);
+        scoped_mpz p(m_mpq_manager);
-        for (unsigned i = 0; i < (sbits+3); i++) {
+        scoped_mpq t(m_mpq_manager), sq(m_mpq_manager);
-            m_mpz_manager.mul2k(o.significand, 1);
+        m_mpz_manager.power(2, sbits + 3 - 1, p);
-            if (m_mpq_manager.ge(sig, 1)) {
+        m_mpq_manager.mul(p, sig, t);
-                m_mpz_manager.inc(o.significand);
+        m_mpq_manager.floor(t, o.significand);
-                m_mpq_manager.dec(sig);
+        m_mpq_manager.set(sq, o.significand);
-            }
+        m_mpq_manager.div(sq, p, t);
-            m_mpq_manager.mul(sig, mpq(2), sig);
+        m_mpq_manager.sub(sig, t, sig);
-        }
 
         // sticky
         if (!m_mpq_manager.is_zero(sig) && m_mpz_manager.is_even(o.significand))