Merge branch 'master' of https://github.com/Z3Prover/z3

src/ast/array_decl_plugin.cpp

@@ -40,6 +40,15 @@ array_decl_plugin::array_decl_plugin():
 #define ARRAY_SORT_STR "Array"
 
 sort * array_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) {
+
+    if (k == _SET_SORT) {
+        if (num_parameters != 1) {
+            m_manager->raise_exception("invalid array sort definition, invalid number of parameters");
+            return 0;
+        }
+        parameter params[2] = { parameters[0], parameter(m_manager->mk_bool_sort()) };
+        return mk_sort(ARRAY_SORT, 2, params);
+    }
     SASSERT(k == ARRAY_SORT);
     if (num_parameters < 2) {
         m_manager->raise_exception("invalid array sort definition, invalid number of parameters");
@@ -506,6 +515,8 @@ func_decl * array_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
 
 void array_decl_plugin::get_sort_names(svector<builtin_name>& sort_names, symbol const & logic) {
     sort_names.push_back(builtin_name(ARRAY_SORT_STR, ARRAY_SORT));
+    // TBD: this could easily break users even though it is already used in CVC4: 
+    // sort_names.push_back(builtin_name("Set", _SET_SORT));
 }
 
 void array_decl_plugin::get_op_names(svector<builtin_name>& op_names, symbol const & logic) {

src/ast/array_decl_plugin.h

@@ -35,7 +35,8 @@ inline sort* get_array_domain(sort const * s, unsigned idx) {
 }
 
 enum array_sort_kind {
-    ARRAY_SORT
+    ARRAY_SORT,
+    _SET_SORT
 };
 
 enum array_op_kind {

src/ast/ast.cpp

@@ -1308,7 +1308,8 @@ ast_manager::ast_manager(proof_gen_mode m, char const * trace_file, bool is_form
     m_expr_dependency_array_manager(*this, m_alloc),
     m_proof_mode(m),
     m_trace_stream(0),
-    m_trace_stream_owner(false) {
+    m_trace_stream_owner(false),
+    m_rec_fun(":rec-fun") {
 
     if (trace_file) {
         m_trace_stream       = alloc(std::fstream, trace_file, std::ios_base::out);
@@ -1329,7 +1330,8 @@ ast_manager::ast_manager(proof_gen_mode m, std::fstream * trace_stream, bool is_
     m_expr_dependency_array_manager(*this, m_alloc),
     m_proof_mode(m),
     m_trace_stream(trace_stream),
-    m_trace_stream_owner(false) {
+    m_trace_stream_owner(false),
+    m_rec_fun(":rec-fun") {
 
     if (!is_format_manager)
         m_format_manager = alloc(ast_manager, PGM_DISABLED, trace_stream, true);
@@ -1345,7 +1347,8 @@ ast_manager::ast_manager(ast_manager const & src, bool disable_proofs):
     m_expr_dependency_array_manager(*this, m_alloc),
     m_proof_mode(disable_proofs ? PGM_DISABLED : src.m_proof_mode),
     m_trace_stream(src.m_trace_stream),
-    m_trace_stream_owner(false) {
+    m_trace_stream_owner(false),
+    m_rec_fun(":rec-fun") {
     SASSERT(!src.is_format_manager());
     m_format_manager = alloc(ast_manager, PGM_DISABLED, m_trace_stream, true);
     init();

src/ast/ast.h

@@ -1455,6 +1455,7 @@ protected:
     bool slow_not_contains(ast const * n);
 #endif
     ast_manager *             m_format_manager; // hack for isolating format objects in a different manager.
+    symbol                    m_rec_fun;
 
     void init();
 
@@ -1561,6 +1562,10 @@ public:
 
     bool contains(ast * a) const { return m_ast_table.contains(a); }
 
+    bool is_rec_fun_def(quantifier* q) const { return q->get_qid() == m_rec_fun; }
+    
+    symbol const& rec_fun_qid() const { return m_rec_fun; }
+
     unsigned get_num_asts() const { return m_ast_table.size(); }
 
     void debug_ref_count() { m_debug_ref_count = true; }

src/cmd_context/cmd_context.cpp

@@ -837,10 +837,16 @@ void cmd_context::insert_rec_fun(func_decl* f, expr_ref_vector const& binding, s
     eq  = m().mk_eq(lhs, e);
     if (!ids.empty()) {
         expr* pat = m().mk_pattern(lhs);
-        eq  = m().mk_forall(ids.size(), f->get_domain(), ids.c_ptr(), eq, 0, symbol(":rec-fun"), symbol::null, 1, &pat);
+        eq  = m().mk_forall(ids.size(), f->get_domain(), ids.c_ptr(), eq, 0, m().rec_fun_qid(), symbol::null, 1, &pat);
     }
-    if (!ids.empty() && !m_rec_fun_declared) {
+
-        warning_msg("recursive functions are currently only partially supported: they are translated into recursive equations without special handling");
+    //
+    // disable warning given the current way they are used 
+    // (Z3 will here silently assume and not check the definitions to be well founded, 
+    // and please use HSF for everything else).
+    //
+    if (false && !ids.empty() && !m_rec_fun_declared) {        
+        warning_msg("recursive function definitions are assumed well-founded");
         m_rec_fun_declared = true;
     }
     assert_expr(eq);

src/model/model.cpp

@@ -30,20 +30,6 @@ model::model(ast_manager & m):
 }
 
 model::~model() {
-    decl2expr::iterator it1  = m_interp.begin();
-    decl2expr::iterator end1 = m_interp.end();
-    for (; it1 != end1; ++it1) {
-        m_manager.dec_ref(it1->m_key);
-        m_manager.dec_ref(it1->m_value);
-    }
-
-    decl2finterp::iterator it2  = m_finterp.begin();
-    decl2finterp::iterator end2 = m_finterp.end();
-    for (; it2 != end2; ++it2) {
-        m_manager.dec_ref(it2->m_key);
-        dealloc(it2->m_value);
-    }
-    
     sort2universe::iterator it3  = m_usort2universe.begin();
     sort2universe::iterator end3 = m_usort2universe.end();
     for (; it3 != end3; ++it3) {
@@ -53,43 +39,6 @@ model::~model() {
     }
 }
 
-void model::register_decl(func_decl * d, expr * v) {
-    SASSERT(d->get_arity() == 0);
-    decl2expr::obj_map_entry * entry = m_interp.insert_if_not_there2(d, 0);
-    if (entry->get_data().m_value == 0) {
-        // new entry
-        m_decls.push_back(d);
-        m_const_decls.push_back(d);
-        m_manager.inc_ref(d);
-        m_manager.inc_ref(v);
-        entry->get_data().m_value = v;
-    }
-    else {
-        // replacing entry
-        m_manager.inc_ref(v);
-        m_manager.dec_ref(entry->get_data().m_value);
-        entry->get_data().m_value = v;
-    }
-}
-
-void model::register_decl(func_decl * d, func_interp * fi) {
-    SASSERT(d->get_arity() > 0);
-    SASSERT(&fi->m() == &m_manager);
-    decl2finterp::obj_map_entry * entry = m_finterp.insert_if_not_there2(d, 0);
-    if (entry->get_data().m_value == 0) {
-        // new entry
-        m_decls.push_back(d);
-        m_func_decls.push_back(d);
-        m_manager.inc_ref(d);
-        entry->get_data().m_value = fi;
-    }
-    else {
-        // replacing entry
-        if (fi != entry->get_data().m_value)
-            dealloc(entry->get_data().m_value);
-        entry->get_data().m_value = fi;
-    }
-}
 
 
 void model::copy_const_interps(model const & source) {

src/model/model.h

@@ -44,8 +44,7 @@ public:
     bool eval(func_decl * f, expr_ref & r) const { return model_core::eval(f, r); }
     bool eval(expr * e, expr_ref & result, bool model_completion = false);
     
-    expr * get_some_value(sort * s);
+    virtual expr * get_some_value(sort * s);
-
     virtual ptr_vector<expr> const & get_universe(sort * s) const;
     virtual unsigned get_num_uninterpreted_sorts() const;
     virtual sort * get_uninterpreted_sort(unsigned idx) const;
@@ -54,8 +53,6 @@ public:
     //
     // Primitives for building models
     //
-    void register_decl(func_decl * d, expr * v);
-    void register_decl(func_decl * f, func_interp * fi);
     void register_usort(sort * s, unsigned usize, expr * const * universe);
 
     // Model translation

src/model/model_core.cpp

@@ -18,6 +18,23 @@ Revision History:
 --*/
 #include"model_core.h"
 
+model_core::~model_core() {
+    decl2expr::iterator it1  = m_interp.begin();
+    decl2expr::iterator end1 = m_interp.end();
+    for (; it1 != end1; ++it1) {
+        m_manager.dec_ref(it1->m_key);
+        m_manager.dec_ref(it1->m_value);
+    }
+
+    decl2finterp::iterator it2  = m_finterp.begin();
+    decl2finterp::iterator end2 = m_finterp.end();
+    for (; it2 != end2; ++it2) {
+        func_decl* d = it2->m_key;
+        m_manager.dec_ref(it2->m_key);
+        dealloc(it2->m_value);
+    }   
+}
+
 bool model_core::eval(func_decl* f, expr_ref & r) const {
     if (f->get_arity() == 0) {
         r = get_const_interp(f);
@@ -32,3 +49,42 @@ bool model_core::eval(func_decl* f, expr_ref & r) const {
         return false;
     }
 }
+
+void model_core::register_decl(func_decl * d, expr * v) {
+    SASSERT(d->get_arity() == 0);
+    decl2expr::obj_map_entry * entry = m_interp.insert_if_not_there2(d, 0);
+    if (entry->get_data().m_value == 0) {
+        // new entry
+        m_decls.push_back(d);
+        m_const_decls.push_back(d);
+        m_manager.inc_ref(d);
+        m_manager.inc_ref(v);
+        entry->get_data().m_value = v;
+    }
+    else {
+        // replacing entry
+        m_manager.inc_ref(v);
+        m_manager.dec_ref(entry->get_data().m_value);
+        entry->get_data().m_value = v;
+    }
+}
+
+void model_core::register_decl(func_decl * d, func_interp * fi) {
+    SASSERT(d->get_arity() > 0);
+    SASSERT(&fi->m() == &m_manager);
+    decl2finterp::obj_map_entry * entry = m_finterp.insert_if_not_there2(d, 0);
+    if (entry->get_data().m_value == 0) {
+        // new entry
+        m_decls.push_back(d);
+        m_func_decls.push_back(d);
+        m_manager.inc_ref(d);
+        entry->get_data().m_value = fi;
+    }
+    else {
+        // replacing entry
+        if (fi != entry->get_data().m_value)
+            dealloc(entry->get_data().m_value);
+        entry->get_data().m_value = fi;
+    }
+}
+

src/model/model_core.h

@@ -36,8 +36,8 @@ protected:
     ptr_vector<func_decl>         m_func_decls;  
     
 public:
-    model_core(ast_manager & m):m_manager(m), m_ref_count(0) {}
+    model_core(ast_manager & m):m_manager(m), m_ref_count(0) { }
-    virtual ~model_core() {}
+    virtual ~model_core();
 
     ast_manager & get_manager() const { return m_manager; }
 
@@ -58,6 +58,11 @@ public:
     virtual unsigned get_num_uninterpreted_sorts() const = 0;
     virtual sort * get_uninterpreted_sort(unsigned idx) const = 0;
 
+    void register_decl(func_decl * d, expr * v);
+    void register_decl(func_decl * f, func_interp * fi);
+
+    virtual expr * get_some_value(sort * s) = 0;
+
     //
     // Reference counting
     //
@@ -68,6 +73,7 @@ public:
             dealloc(this);
         }
     }
+
 };
 
 #endif

src/model/model_evaluator.cpp

@@ -32,7 +32,7 @@ Revision History:
 #include"cooperate.h"
 
 struct evaluator_cfg : public default_rewriter_cfg {
-    model &                         m_model;
+    model_core &                         m_model;
     bool_rewriter                   m_b_rw;
     arith_rewriter                  m_a_rw;
     bv_rewriter                     m_bv_rw;
@@ -46,7 +46,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
     bool                            m_model_completion;
     bool                            m_cache;
 
-    evaluator_cfg(ast_manager & m, model & md, params_ref const & p):
+    evaluator_cfg(ast_manager & m, model_core & md, params_ref const & p):
         m_model(md),
         m_b_rw(m),
         // We must allow customers to set parameters for arithmetic rewriter/evaluator.
@@ -231,7 +231,7 @@ template class rewriter_tpl<evaluator_cfg>;
 
 struct model_evaluator::imp : public rewriter_tpl<evaluator_cfg> {
     evaluator_cfg m_cfg;
-    imp(model & md, params_ref const & p):
+    imp(model_core & md, params_ref const & p):
         rewriter_tpl<evaluator_cfg>(md.get_manager(),
                                     false, // no proofs for evaluator
                                     m_cfg),
@@ -239,7 +239,7 @@ struct model_evaluator::imp : public rewriter_tpl<evaluator_cfg> {
     }
 };
 
-model_evaluator::model_evaluator(model & md, params_ref const & p) {
+model_evaluator::model_evaluator(model_core & md, params_ref const & p) {
     m_imp = alloc(imp, md, p);
 }
 
@@ -269,7 +269,7 @@ unsigned model_evaluator::get_num_steps() const {
 
 
 void model_evaluator::cleanup(params_ref const & p) {
-    model & md = m_imp->cfg().m_model;
+    model_core & md = m_imp->cfg().m_model;
     #pragma omp critical (model_evaluator)
     {
         dealloc(m_imp);

src/model/model_evaluator.h

@@ -30,7 +30,7 @@ class model_evaluator {
     struct imp;
     imp *  m_imp;
 public:
-    model_evaluator(model & m, params_ref const & p = params_ref());
+    model_evaluator(model_core & m, params_ref const & p = params_ref());
     ~model_evaluator();
 
     ast_manager & m () const;

src/smt/proto_model/proto_model.cpp

@@ -29,7 +29,6 @@ Revision History:
 
 proto_model::proto_model(ast_manager & m, simplifier & s, params_ref const & p):
     model_core(m),
-    m_asts(m),
     m_simplifier(s),
     m_afid(m.mk_family_id(symbol("array"))) {
     register_factory(alloc(basic_factory, m));
@@ -39,45 +38,11 @@ proto_model::proto_model(ast_manager & m, simplifier & s, params_ref const & p):
     m_model_partial = model_params(p).partial();
 }
 
-void proto_model::reset_finterp() {
-     decl2finterp::iterator it  = m_finterp.begin();
-     decl2finterp::iterator end = m_finterp.end();
-     for (; it != end; ++it) {
-         dealloc(it->m_value);
-     }
-}
 
-proto_model::~proto_model() {
-    reset_finterp();
-}
 
-void proto_model::register_decl(func_decl * d, expr * v) {
+void proto_model::register_aux_decl(func_decl * d, func_interp * fi) {
-    SASSERT(d->get_arity() == 0);
+    model_core::register_decl(d, fi);
-    if (m_interp.contains(d)) {
+    m_aux_decls.insert(d);
-        DEBUG_CODE({
-            expr * old_v = 0;
-            m_interp.find(d, old_v);
-            SASSERT(old_v == v);
-        });
-        return;
-    }
-    SASSERT(!m_interp.contains(d));
-    m_decls.push_back(d);
-    m_asts.push_back(d);
-    m_asts.push_back(v);
-    m_interp.insert(d, v);
-    m_const_decls.push_back(d);
-}
-
-void proto_model::register_decl(func_decl * d, func_interp * fi, bool aux) {
-    SASSERT(d->get_arity() > 0);
-    SASSERT(!m_finterp.contains(d));
-    m_decls.push_back(d);
-    m_asts.push_back(d);
-    m_finterp.insert(d, fi);
-    m_func_decls.push_back(d);
-    if (aux)
-        m_aux_decls.insert(d);
 }
 
 /**
@@ -486,6 +451,7 @@ void proto_model::cleanup() {
                 m_finterp.find(faux, fi);
                 SASSERT(fi != 0);
                 m_finterp.erase(faux);
+                m_manager.dec_ref(faux);
                 dealloc(fi);
             }
         }
@@ -666,20 +632,16 @@ model * proto_model::mk_model() {
     decl2finterp::iterator end2 = m_finterp.end();
     for (; it2 != end2; ++it2) {
         m->register_decl(it2->m_key, it2->m_value);
+        m_manager.dec_ref(it2->m_key);
     }
+    
     m_finterp.reset(); // m took the ownership of the func_interp's
 
     unsigned sz = get_num_uninterpreted_sorts();
     for (unsigned i = 0; i < sz; i++) {
         sort * s = get_uninterpreted_sort(i);
         TRACE("proto_model", tout << "copying uninterpreted sorts...\n" << mk_pp(s, m_manager) << "\n";);
-        ptr_buffer<expr> buf;
+        ptr_vector<expr> const& buf = get_universe(s);
-        obj_hashtable<expr> const & u = get_known_universe(s);
-        obj_hashtable<expr>::iterator it  = u.begin();
-        obj_hashtable<expr>::iterator end = u.end();
-        for (; it != end; ++it) {
-            buf.push_back(*it);
-        }
         m->register_usort(s, buf.size(), buf.c_ptr());
     }
 

src/smt/proto_model/proto_model.h

@@ -38,7 +38,6 @@ Revision History:
 #include"params.h"
 
 class proto_model : public model_core {
-    ast_ref_vector                m_asts;
     plugin_manager<value_factory> m_factories;
     user_sort_factory *           m_user_sort_factory;
     simplifier &                  m_simplifier;
@@ -48,8 +47,6 @@ class proto_model : public model_core {
 
     bool                          m_model_partial;
 
-    void reset_finterp();
-
     expr * mk_some_interp_for(func_decl * d);
 
     // Invariant: m_decls subset m_func_decls union m_const_decls union union m_value_decls
@@ -63,7 +60,7 @@ class proto_model : public model_core {
 
 public:
     proto_model(ast_manager & m, simplifier & s, params_ref const & p = params_ref());
-    virtual ~proto_model(); 
+    virtual ~proto_model() {}
 
     void register_factory(value_factory * f) { m_factories.register_plugin(f); }
 
@@ -73,7 +70,7 @@ public:
     
     value_factory * get_factory(family_id fid);
 
-    expr * get_some_value(sort * s);
+    virtual expr * get_some_value(sort * s);
 
     bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2);
 
@@ -84,8 +81,7 @@ public:
     //
     // Primitives for building models
     //
-    void register_decl(func_decl * d, expr * v);
+    void register_aux_decl(func_decl * f, func_interp * fi);
-    void register_decl(func_decl * f, func_interp * fi, bool aux = false);
     void reregister_decl(func_decl * f, func_interp * new_fi, func_decl * f_aux);
     void compress();
     void cleanup();

src/smt/smt_model_checker.cpp

@@ -322,20 +322,18 @@ namespace smt {
         for (; it != end; ++it) {
             if (m_context->is_relevant(*it)) {
                 app* e = (*it)->get_owner();
-                for (unsigned i = 0; i < e->get_num_args(); ++i) {
+                SASSERT(e->get_num_args() == num_decls);
-                    args[num_decls - i - 1] = e->get_arg(i);
+                for (unsigned i = 0; i < num_decls; ++i) {
+                    args[i] = e->get_arg(i);
                 }
                 sub(q->get_expr(), num_decls, args.c_ptr(), tmp);
                 m_curr_model->eval(tmp, result, true);
-                if (m.is_true(result)) {
-                    continue;
-                }
                 if (m.is_false(result)) {
                     add_instance(q, args, 0);
                     return false;
                 }
-                TRACE("model_checker", tout << tmp << "evaluates to undetermined " << result << "\n";);
+                TRACE("model_checker", tout << tmp << "\nevaluates to:\n" << result << "\n";);
-                is_undef = true;
+                // if (!m.is_true(result)) is_undef = true;
             }
         }
         return !is_undef;
@@ -395,7 +393,7 @@ namespace smt {
                     verbose_stream() << "(smt.mbqi :checking " << q->get_qid() << ")\n";
                 }
                 found_relevant = true;
-                if (q->get_qid() == symbol(":rec-fun")) {
+                if (m.is_rec_fun_def(q)) {
                     if (!check_rec_fun(q)) {
                         num_failures++;
                     }

src/smt/smt_model_finder.cpp

@@ -915,7 +915,7 @@ namespace smt {
                 }
                 func_interp * rpi = alloc(func_interp, m_manager, 1);
                 rpi->set_else(pi);
-                m_model->register_decl(p, rpi, true);
+                m_model->register_aux_decl(p, rpi);
                 n->set_proj(p);
             }
 
@@ -928,7 +928,7 @@ namespace smt {
                 func_decl *   p  = m_manager.mk_fresh_func_decl(1, &s, s);
                 func_interp * pi = alloc(func_interp, m_manager, 1);
                 pi->set_else(else_val);
-                m_model->register_decl(p, pi, true);
+                m_model->register_aux_decl(p, pi);
                 ptr_buffer<expr>::const_iterator it  = values.begin();
                 ptr_buffer<expr>::const_iterator end = values.end();
                 for (; it != end; ++it) {

src/smt/smt_model_generator.cpp

@@ -516,43 +516,6 @@ namespace smt {
         }
     }
 
-    /**
-       \brief Auxiliary functor for method register_indirect_elim_decls.
-    */
-    class mk_interp_proc {
-        context &       m_context;
-        proto_model &   m_model;
-    public:
-        mk_interp_proc(context & ctx, proto_model & m):
-            m_context(ctx), 
-            m_model(m) {
-        }
-
-        void operator()(var * n) { 
-        }
-
-        void operator()(app * n) { 
-            if (!is_uninterp(n))
-                return; // n is interpreted
-            func_decl * d  = n->get_decl();
-            if (m_model.has_interpretation(d))
-                return; // declaration already has an interpretation.
-            if (n->get_num_args() == 0) {
-                sort * r = d->get_range();
-                expr * v = m_model.get_some_value(r);
-                m_model.register_decl(d, v);
-            }
-            else {
-                func_interp * fi = alloc(func_interp, m_context.get_manager(), d->get_arity());            
-                m_model.register_decl(d, fi);
-            }
-        }
-        
-        void operator()(quantifier * n) { 
-        }
-        
-    };
-
     proto_model * model_generator::mk_model() {
         SASSERT(!m_model);
         TRACE("func_interp_bug", m_context->display(tout););

src/smt/smt_quantifier.cpp

@@ -40,7 +40,6 @@ namespace smt {
         ptr_vector<quantifier>                 m_quantifiers;
         scoped_ptr<quantifier_manager_plugin>  m_plugin;
         unsigned                               m_num_instances;
-        symbol                                 m_rec_fun;
         
         imp(quantifier_manager & wrapper, context & ctx, smt_params & p, quantifier_manager_plugin * plugin):
             m_wrapper(wrapper),
@@ -48,8 +47,7 @@ namespace smt {
             m_params(p),
             m_qi_queue(m_wrapper, ctx, p),
             m_qstat_gen(ctx.get_manager(), ctx.get_region()),
-            m_plugin(plugin),
+            m_plugin(plugin) {
-            m_rec_fun(":rec-fun") {
             m_num_instances = 0;
             m_qi_queue.setup();
         }
@@ -187,7 +185,7 @@ namespace smt {
         }
         
         bool check_quantifier(quantifier* q) {
-            return m_context.is_relevant(q) && m_context.get_assignment(q) == l_true; // TBD: && q->get_qid() != m_rec_fun;
+            return m_context.is_relevant(q) && m_context.get_assignment(q) == l_true; // TBD: && !m_context->get_manager().is_rec_fun_def(q);
         }
 
         bool quick_check_quantifiers() {

src/smt/theory_datatype.cpp

@@ -547,6 +547,10 @@ namespace smt {
         out << "\n";
     }
 
+    bool theory_datatype::include_func_interp(func_decl* f) {
+        return false; // return m_util.is_accessor(f);
+    }
+
     void theory_datatype::init_model(model_generator & m) {
         m_factory = alloc(datatype_factory, get_manager(), m.get_model());
         m.register_factory(m_factory);

src/smt/theory_datatype.h

@@ -111,6 +111,8 @@ namespace smt {
         static void after_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) {}
         void unmerge_eh(theory_var v1, theory_var v2);
         virtual char const * get_name() const { return "datatype"; }
+        virtual bool include_func_interp(func_decl* f);
+
     };
 
 };