stash

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

src/api/api_datalog.cpp

@@ -358,7 +358,7 @@ extern "C" {
             v->m_ast_vector.push_back(coll.m_queries[i].get());
         }
         for (unsigned i = 0; i < coll.m_rels.size(); ++i) {
-            to_fixedpoint_ref(d)->ctx().register_predicate(coll.m_rels[i].get());
+            to_fixedpoint_ref(d)->ctx().register_predicate(coll.m_rels[i].get(), true);
         }
         for (unsigned i = 0; i < coll.m_rules.size(); ++i) {
             to_fixedpoint_ref(d)->add_rule(coll.m_rules[i].get(), coll.m_names[i]);
@@ -415,7 +415,7 @@ extern "C" {
     void Z3_API Z3_fixedpoint_register_relation(Z3_context c,Z3_fixedpoint d, Z3_func_decl f) {
         Z3_TRY;
         LOG_Z3_fixedpoint_register_relation(c, d, f);
-        to_fixedpoint_ref(d)->ctx().register_predicate(to_func_decl(f));
+        to_fixedpoint_ref(d)->ctx().register_predicate(to_func_decl(f), true);
         Z3_CATCH;
     }
 

src/ast/rewriter/expr_safe_replace.cpp

@@ -100,3 +100,9 @@ void expr_safe_replace::operator()(expr* e, expr_ref& res) {
     }
     res = cache.find(e);
 }
+
+void expr_safe_replace::reset() {
+    m_src.reset();
+    m_dst.reset();
+    m_subst.reset();
+}

src/ast/rewriter/expr_safe_replace.h

@@ -38,6 +38,8 @@ public:
     void operator()(expr_ref& e) { (*this)(e.get(), e); }
 
     void operator()(expr* src, expr_ref& e);
+
+    void reset();
 };
 
 #endif /* __EXPR_SAFE_REPLACE_H__ */

src/muz_qe/dl_cmds.cpp

@@ -229,6 +229,7 @@ public:
                 status = dlctx.query(m_target);
             }
             catch (z3_error & ex) {
+                ctx.regular_stream() << "(error \"query failed: " << ex.msg() << "\")" << std::endl;
                 throw ex;
             }
             catch (z3_exception& ex) {

src/muz_qe/dl_context.cpp

@@ -46,6 +46,8 @@ Revision History:
 #include"dl_mk_bit_blast.h"
 #include"dl_mk_array_blast.h"
 #include"dl_mk_karr_invariants.h"
+#include"dl_mk_quantifier_abstraction.h"
+#include"dl_mk_quantifier_instantiation.h"
 #include"datatype_decl_plugin.h"
 #include"expr_abstract.h"
 
@@ -300,14 +302,6 @@ namespace datalog {
         return m_preds.contains(pred);
     }
 
-    func_decl * context::try_get_predicate_decl(symbol pred_name) const {
-        func_decl * res;
-        if (!m_preds_by_name.find(pred_name, res)) {
-            return 0;
-        }
-        return res;
-    }
-
     void context::register_variable(func_decl* var) {
         m_vars.push_back(m.mk_const(var));
     }
@@ -359,7 +353,6 @@ namespace datalog {
         m_pinned.push_back(decl);
         m_preds.insert(decl);
         if (named) {
-            SASSERT(!m_preds_by_name.contains(decl->get_name()));
             m_preds_by_name.insert(decl->get_name(), decl);
         }
     }
@@ -446,7 +439,7 @@ namespace datalog {
         func_decl* new_pred = 
             m.mk_fresh_func_decl(prefix, suffix, arity, domain, m.mk_bool_sort());
 
-        register_predicate(new_pred);
+        register_predicate(new_pred, true);
 
         if (m_rel.get()) {
             m_rel->inherit_predicate_kind(new_pred, orig_pred);
@@ -905,6 +898,13 @@ namespace datalog {
         m_transf.register_plugin(alloc(datalog::mk_rule_inliner, *this, 34890));
         m_transf.register_plugin(alloc(datalog::mk_subsumption_checker, *this, 34880));
 
+
+        if (get_params().quantify_arrays()) {
+            m_transf.register_plugin(alloc(datalog::mk_quantifier_abstraction, *this, 33000));
+            m_transf.register_plugin(alloc(datalog::mk_array_blast, *this, 32500));
+        }
+        m_transf.register_plugin(alloc(datalog::mk_quantifier_instantiation, *this, 32000));
+
         m_transf.register_plugin(alloc(datalog::mk_bit_blast, *this, 35000));
         m_transf.register_plugin(alloc(datalog::mk_array_blast, *this, 36000));
         m_transf.register_plugin(alloc(datalog::mk_karr_invariants, *this, 36010));

src/muz_qe/dl_context.h

@@ -183,18 +183,22 @@ namespace datalog {
            retrieved by the try_get_predicate_decl() function. Auxiliary predicates introduced
            e.g. by rule transformations do not need to be named.
          */
-        void register_predicate(func_decl * pred, bool named = true);
+        void register_predicate(func_decl * pred, bool named);
 
         bool is_predicate(func_decl * pred) const;
-        
+
         /**
            \brief If a predicate name has a \c func_decl object assigned, return pointer to it;
            otherwise return 0.
-
+           
            Not all \c func_decl object used as relation identifiers need to be assigned to their
            names. Generally, the names coming from the parses are registered here.
-         */
+        */
-        func_decl * try_get_predicate_decl(symbol pred_name) const;
+        func_decl * try_get_predicate_decl(symbol const& pred_name) const {
+            func_decl * res = 0;
+            m_preds_by_name.find(pred_name, res);
+            return res;
+        }        
 
         /**
            \brief Create a fresh head predicate declaration.

src/muz_qe/dl_mk_karr_invariants.cpp

@@ -206,7 +206,7 @@ namespace datalog {
         for (; it != end; ++it) {
             rule_ref r(*it, m_inner_ctx.get_rule_manager());
             m_inner_ctx.add_rule(r);
-            m_inner_ctx.register_predicate(r->get_decl());
+            m_inner_ctx.register_predicate(r->get_decl(), false);
         }
         m_inner_ctx.close();
         rule_set::decl2rules::iterator dit  = source.begin_grouped_rules();

src/muz_qe/dl_mk_loop_counter.cpp

@@ -72,14 +72,14 @@ namespace datalog {
             for (unsigned j = 0; j < utsz; ++j, ++cnt) {
                 tail.push_back(add_arg(r.get_tail(j), cnt));                
                 neg.push_back(r.is_neg_tail(j));
-                ctx.register_predicate(tail.back()->get_decl());
+                ctx.register_predicate(tail.back()->get_decl(), false);
             }
             for (unsigned j = utsz; j < tsz; ++j) {
                 tail.push_back(r.get_tail(j));
                 neg.push_back(false);
             }
             head = add_arg(r.get_head(), cnt);
-            ctx.register_predicate(head->get_decl());
+            ctx.register_predicate(head->get_decl(), false);
             // set the loop counter to be an increment of the previous 
             bool found = false;
             unsigned last = head->get_num_args()-1;

src/muz_qe/dl_rule.cpp

@@ -135,7 +135,7 @@ namespace datalog {
         h.set_name(name);
         h(fml, p, fmls, prs);
         for (unsigned i = 0; i < h.get_fresh_predicates().size(); ++i) {
-            m_ctx.register_predicate(h.get_fresh_predicates()[i]);
+            m_ctx.register_predicate(h.get_fresh_predicates()[i], false);
         }
         for (unsigned i = 0; i < fmls.size(); ++i) {
             mk_rule_core2(fmls[i].get(), prs[i].get(), rules, name);

src/muz_qe/dl_rule_set.h

@@ -20,7 +20,6 @@ Revision History:
 #define _DL_RULE_SET_H_
 
 #include"obj_hashtable.h"
-
 #include"dl_rule.h"
 
 namespace datalog {

src/muz_qe/fixedpoint_params.pyg

@@ -42,6 +42,8 @@ def_module_params('fixedpoint',
                           ('simplify_formulas_post', BOOL, False, "PDR: simplify derived formulas after inductive propagation"),
                           ('slice', BOOL, True, "PDR: simplify clause set using slicing"),
 	                  ('karr',  BOOL, False, "Add linear invariants to clauses using Karr's method"),
+	                  ('quantify_arrays', BOOL, False, "create quantified Horn clauses from clauses with arrays"),
+	                  ('instantiate_quantifiers', BOOL, False, "instantiate quantified Horn clauses using E-matching heuristic"),
                           ('coalesce_rules', BOOL, False, "BMC: coalesce rules"),
                           ('use_multicore_generalizer', BOOL, False, "PDR: extract multiple cores for blocking states"),
                           ('use_inductive_generalizer', BOOL, True, "PDR: generalize lemmas using induction strengthening"),

src/muz_qe/horn_tactic.cpp

@@ -92,7 +92,7 @@ class horn_tactic : public tactic {
 
         void register_predicate(expr* a) {
             SASSERT(is_predicate(a));
-            m_ctx.register_predicate(to_app(a)->get_decl(), true);
+            m_ctx.register_predicate(to_app(a)->get_decl(), false);
         }
 
         void check_predicate(ast_mark& mark, expr* a) {