recfun

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

src/ast/array_decl_plugin.cpp

@@ -253,7 +253,10 @@ func_decl* array_decl_plugin::mk_select(unsigned arity, sort * const * domain) {
         if (!parameters[i].is_ast() || 
             !is_sort(parameters[i].get_ast()) || 
             !m_manager->compatible_sorts(domain[i+1], to_sort(parameters[i].get_ast()))) {
-            m_manager->raise_exception("domain sort and parameter do not match");
+            std::stringstream strm;
+            strm << "domain sort " << sort_ref(domain[i+1], *m_manager) << " and parameter ";
+            strm << parameter_pp(parameters[i], *m_manager) << " do not match";
+            m_manager->raise_exception(strm.str().c_str());
             UNREACHABLE();
             return nullptr;
         }
@@ -292,8 +295,12 @@ func_decl * array_decl_plugin::mk_store(unsigned arity, sort * const * domain) {
             m_manager->raise_exception("expecting sort parameter");
             return nullptr;
         }
-        if (!m_manager->compatible_sorts(to_sort(parameters[i].get_ast()), domain[i+1])) {
-            m_manager->raise_exception("domain sort and parameter do not match");
+        sort* srt1 = to_sort(parameters[i].get_ast());
+        sort* srt2 = domain[i+1];
+        if (!m_manager->compatible_sorts(srt1, srt2)) {
+            std::stringstream strm;
+            strm << "domain sort " << sort_ref(srt2, *m_manager) << " and parameter sort " << sort_ref(srt2, *m_manager) << " do not match";
+            m_manager->raise_exception(strm.str());
             UNREACHABLE();
             return nullptr;
         }
@@ -326,13 +333,13 @@ bool array_decl_plugin::check_set_arguments(unsigned arity, sort * const * domai
         if (domain[i] != domain[0]) {
             std::ostringstream buffer;
             buffer << "arguments " << 1 << " and " << (i+1) << " have different sorts";
-            m_manager->raise_exception(buffer.str().c_str());
+            m_manager->raise_exception(buffer.str());
             return false;
         }
         if (domain[i]->get_family_id() != m_family_id) {
             std::ostringstream buffer;
             buffer << "argument " << (i+1) << " is not of array sort";
-            m_manager->raise_exception(buffer.str().c_str());
+            m_manager->raise_exception(buffer.str());
             return false;
         }
     }

src/ast/ast.cpp

@@ -16,8 +16,8 @@ Author:
 Revision History:
 
 --*/
-#include<sstream>
-#include<cstring>
+#include <sstream>
+#include <cstring>
 #include "ast/ast.h"
 #include "ast/ast_pp.h"
 #include "ast/ast_ll_pp.h"
@@ -1541,6 +1541,20 @@ void ast_manager::raise_exception(char const * msg) {
     throw ast_exception(msg);
 }
 
+void ast_manager::raise_exception(std::string const&  msg) {
+    throw ast_exception(msg.c_str());
+}
+
+std::ostream& ast_manager::display(std::ostream& out, parameter const& p) {
+    switch (p.get_kind()) {
+    case parameter::PARAM_AST:
+        return out << ast_ref(p.get_ast(), *this);
+    default:
+        return p.display(out);
+    }
+    return out;
+}
+
 
 void ast_manager::copy_families_plugins(ast_manager const & from) {
     TRACE("copy_families_plugins",

src/ast/ast.h

@@ -1562,6 +1562,9 @@ public:
 
     // Equivalent to throw ast_exception(msg)
     Z3_NORETURN void raise_exception(char const * msg);
+    Z3_NORETURN void raise_exception(std::string const& s);
+
+    std::ostream& display(std::ostream& out, parameter const& p);
 
     bool is_format_manager() const { return m_format_manager == nullptr; }
 
@@ -2498,6 +2501,16 @@ public:
     void mark(ast * n, bool flag) { if (flag) mark(n); else reset_mark(n); }
 };
 
+struct parameter_pp {
+    parameter const& p;
+    ast_manager& m;
+    parameter_pp(parameter const& p, ast_manager& m): p(p), m(m) {}
+};
+
+inline std::ostream& operator<<(std::ostream& out, parameter_pp const& pp) {
+    return pp.m.display(out, pp.p);
+}
+
 typedef ast_ref_fast_mark<1> ast_ref_fast_mark1;
 typedef ast_ref_fast_mark<2> ast_ref_fast_mark2;
 typedef ast_ref_fast_mark1   expr_ref_fast_mark1;

src/parsers/smt2/smt2parser.cpp

@@ -2277,10 +2277,14 @@ namespace smt2 {
             parse_expr();
             if (m().get_sort(expr_stack().back()) != sort_stack().back())
                 throw parser_exception("invalid function/constant definition, sort mismatch");
-            if (is_fun) 
-                m_ctx.insert(id, num_vars, sort_stack().c_ptr() + sort_spos, expr_stack().back());
-            else 
-                m_ctx.model_add(id, num_vars, sort_stack().c_ptr() + sort_spos, expr_stack().back());
+            sort* const* sorts = sort_stack().c_ptr() + sort_spos;
+            expr* t = expr_stack().back();
+            if (is_fun) {
+                m_ctx.insert(id, num_vars, sorts, t);
+            }
+            else {
+                m_ctx.model_add(id, num_vars, sorts, t);
+            }
             check_rparen("invalid function/constant definition, ')' expected");
             // restore stacks & env
             symbol_stack().shrink(sym_spos);

src/smt/params/smt_params_helper.pyg

@@ -96,5 +96,6 @@ def_module_params(module_name='smt',
                           ('core.extend_nonlocal_patterns', BOOL, False, 'extend unsat cores with literals that have quantifiers with patterns that contain symbols which are not in the quantifier\'s body'),
                           ('lemma_gc_strategy', UINT, 0, 'lemma garbage collection strategy: 0 - fixed, 1 - geometric, 2 - at restart, 3 - none'),
                           ('dt_lazy_splits', UINT, 1, 'How lazy datatype splits are performed: 0- eager, 1- lazy for infinite types, 2- lazy'),
-                          ('recfun.native', BOOL, False, 'use native rec-fun solver')
+                          ('recfun.native', BOOL, False, 'use native rec-fun solver'),
+                          ('recfun.depth', UINT, 2, 'initial depth for maxrec expansion')
                           ))

src/smt/smt_context.cpp

@@ -1384,7 +1384,10 @@ namespace smt {
                 SASSERT(m_manager.is_eq(n));
                 expr * lhs = n->get_arg(0);
                 expr * rhs = n->get_arg(1);
-                if (val == l_true) {
+                if (m_manager.is_bool(lhs)) {
+                    // no-op
+                }
+                else if (val == l_true) {
                     add_eq(get_enode(lhs), get_enode(rhs), eq_justification(l));
                 }
                 else {

src/smt/smt_context_inv.cpp

@@ -303,7 +303,7 @@ namespace smt {
         for (bool_var v = 0; v < num; v++) {
             if (has_enode(v)) {
                 enode * n = bool_var2enode(v);
-                if (n->is_eq() && is_relevant(n) && get_assignment(v) == l_false) {
+                if (n->is_eq() && is_relevant(n) && get_assignment(v) == l_false && !m_manager.is_iff(n->get_owner())) {
                     TRACE("check_th_diseq_propagation", tout << "checking: #" << n->get_owner_id() << " " << mk_bounded_pp(n->get_owner(), m_manager) << "\n";);
                     enode * lhs = n->get_arg(0)->get_root();
                     enode * rhs = n->get_arg(1)->get_root();

src/smt/theory_recfun.cpp

@@ -50,7 +50,14 @@ namespace smt {
         return alloc(theory_recfun, new_ctx->get_manager());
     }
 
+    void theory_recfun::init_search_eh() {
+        smt_params_helper p(ctx().get_params());
+        m_max_depth = p.recfun_depth();
+    }
+
+
     bool theory_recfun::internalize_atom(app * atom, bool gate_ctx) {
+        TRACEFN(mk_pp(atom, m));
         for (expr * arg : *atom) {
             ctx().internalize(arg, false);
         }
@@ -76,7 +83,13 @@ namespace smt {
     }
 
     void theory_recfun::reset_queues() {
+        for (auto* e : m_q_case_expand) {
+            dealloc(e);
+        }
         m_q_case_expand.reset();
+        for (auto* e : m_q_body_expand) {
+            dealloc(e);
+        }
         m_q_body_expand.reset();
         m_q_clauses.clear();
     }
@@ -96,8 +109,7 @@ namespace smt {
         SASSERT(ctx().relevancy());
         if (u().is_defined(n)) {
             TRACEFN("relevant_eh: (defined) " <<  mk_pp(n, m));        
-            case_expansion e(u(), n);
-            push_case_expand(std::move(e));
+            push_case_expand(alloc(case_expansion, u(), n));
         }
     }
 
@@ -114,11 +126,13 @@ namespace smt {
         
         // restore depth book-keeping
         unsigned new_lim = m_preds_lim.size()-num_scopes;
+#if 0
         unsigned start = m_preds_lim[new_lim];
         for (unsigned i = start; i < m_preds.size(); ++i) {
             m_pred_depth.remove(m_preds.get(i));
         }
         m_preds.resize(start);
+#endif
         m_preds_lim.shrink(new_lim);
     }
     
@@ -141,25 +155,31 @@ namespace smt {
             ctx().mk_th_axiom(get_id(), c);
         }
         m_q_clauses.clear();
-
+		
         for (unsigned i = 0; i < m_q_case_expand.size(); ++i) {
-            case_expansion & e = m_q_case_expand[i];
-            if (e.m_def->is_fun_macro()) {
+            case_expansion* e = m_q_case_expand[i];
+            if (e->m_def->is_fun_macro()) {
                 // body expand immediately
-                assert_macro_axiom(e);
+                assert_macro_axiom(*e);
             }
             else {
                 // case expand
-                SASSERT(e.m_def->is_fun_defined());
-                assert_case_axioms(e);                
+                SASSERT(e->m_def->is_fun_defined());
+                assert_case_axioms(*e);                
             }
+            dealloc(e);
+            m_q_case_expand[i] = nullptr;
         }
-        m_q_case_expand.clear();
+        m_stats.m_case_expansions += m_q_case_expand.size();
+        m_q_case_expand.reset();
 
         for (unsigned i = 0; i < m_q_body_expand.size(); ++i) {
-            assert_body_axiom(m_q_body_expand[i]);
+            assert_body_axiom(*m_q_body_expand[i]);
+            dealloc(m_q_body_expand[i]);
+            m_q_body_expand[i] = nullptr;
         }
-        m_q_body_expand.clear();
+        m_stats.m_body_expansions += m_q_body_expand.size();
+        m_q_body_expand.reset();
     }
 
     /**
@@ -167,7 +187,6 @@ namespace smt {
      * the guard appears at a depth below the current cutoff.
      */
     void theory_recfun::assert_max_depth_limit(expr* guard) {
-        TRACEFN("max-depth limit");
         literal_vector c;
         app_ref dlimit = m_util.mk_depth_limit_pred(m_max_depth);
         c.push_back(~mk_literal(dlimit));
@@ -216,8 +235,7 @@ namespace smt {
         if (is_true && u().is_case_pred(e)) {
             TRACEFN("assign_case_pred_true " << mk_pp(e, m));
             // body-expand
-            body_expansion b_e(u(), to_app(e));
-            push_body_expand(std::move(b_e));            
+            push_body_expand(alloc(body_expansion, u(), to_app(e)));          
         }
     }
 
@@ -268,6 +286,7 @@ namespace smt {
      * 2. add unit clause `f(args) = rhs`
      */
     void theory_recfun::assert_macro_axiom(case_expansion & e) {
+        m_stats.m_macro_expansions++;
         TRACEFN("case expansion         " << pp_case_expansion(e, m) << "\n");
         SASSERT(e.m_def->is_fun_macro());
         auto & vars = e.m_def->get_vars();
@@ -381,6 +400,7 @@ namespace smt {
         for (auto & e : unsat_core) {
             if (u().is_depth_limit(e)) {
                 m_max_depth = (3 * m_max_depth) / 2;
+                IF_VERBOSE(1, verbose_stream() << "(smt.recfun :increase-depth " << m_max_depth << ")\n");
                 return true;
             }
         }

src/smt/theory_recfun.h

@@ -101,8 +101,8 @@ namespace smt {
         unsigned_vector          m_preds_lim;
         unsigned                 m_max_depth; // for fairness and termination
 
-        vector<case_expansion> m_q_case_expand;
-        vector<body_expansion> m_q_body_expand;
+        ptr_vector<case_expansion> m_q_case_expand;
+        ptr_vector<body_expansion> m_q_body_expand;
         vector<literal_vector> m_q_clauses;
 
         recfun_util & u() const { return m_util; }
@@ -128,8 +128,8 @@ namespace smt {
             return vars.size() == 0 || vars[vars.size()-1]->get_idx() == 0; 
         }
     protected:
-        void push_case_expand(case_expansion&& e) { m_q_case_expand.push_back(e); }
-        void push_body_expand(body_expansion&& e) { m_q_body_expand.push_back(e); }
+        void push_case_expand(case_expansion* e) { m_q_case_expand.push_back(e); }
+        void push_body_expand(body_expansion* e) { m_q_body_expand.push_back(e); }
 
         bool internalize_atom(app * atom, bool gate_ctx) override;
         bool internalize_term(app * term) override;
@@ -153,7 +153,7 @@ namespace smt {
         theory_recfun(ast_manager & m);
         ~theory_recfun() override;
         theory * mk_fresh(context * new_ctx) override;
-        void init_search_eh() override { m_max_depth = 2; }
+        void init_search_eh() override;
         void display(std::ostream & out) const override;
         void collect_statistics(::statistics & st) const override;
     };