update display method for datalog to use predicates, throttle use of extensionality

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

src/muz/base/dl_context.cpp

@@ -1069,14 +1069,7 @@ namespace datalog {
         func_decl_set::iterator it = rels.begin(), end = rels.end();
         for (; it != end; ++it) {
             func_decl* f = *it;
-            out << "(declare-rel " << f->get_name() << " (";
+            display_rel_decl(out, f);
-            for (unsigned i = 0; i < f->get_arity(); ++i) {                
-                ast_smt2_pp(out, f->get_domain(i), env);
-                if (i + 1 < f->get_arity()) {
-                    out << " ";
-                }
-            }
-            out << "))\n";
         }
 
         if (use_fixedpoint_extensions && do_declare_vars) {
@@ -1120,10 +1113,30 @@ namespace datalog {
         }
         if (use_fixedpoint_extensions) {
             for (unsigned i = 0; i < queries.size(); ++i) {
-                out << "(query ";
+                expr* q = queries[i].get();
-                PP(queries[i].get());                
+                func_decl_ref fn(m);
+                if (is_query(q)) {
+                    fn = to_app(q)->get_decl();
+                }
+                else {
+                    m_free_vars(q);
+                    m_free_vars.set_default_sort(m.mk_bool_sort());
+                    sort* const* domain = m_free_vars.c_ptr();
+                    expr_ref qfn(m);
+                    expr_ref_vector args(m);
+                    fn = m.mk_fresh_func_decl(symbol("q"), symbol(""), m_free_vars.size(), domain, m.mk_bool_sort());
+                    display_rel_decl(out, fn);
+                    for (unsigned j = 0; j < m_free_vars.size(); ++j) {
+                        args.push_back(m.mk_var(j, m_free_vars[j]));
+                    }
+                    qfn = m.mk_implies(q, m.mk_app(fn, args.size(), args.c_ptr()));
+                    
+                    out << "(assert ";
+                    PP(qfn);
                     out << ")\n";
                 }
+                out << "(query " << fn->get_name() << ")\n";
+            }
         }
         else {
             for (unsigned i = 0; i < queries.size(); ++i) {
@@ -1139,6 +1152,35 @@ namespace datalog {
         }
     }
 
+    void context::display_rel_decl(std::ostream& out, func_decl* f) {
+        smt2_pp_environment_dbg env(m);
+        out << "(declare-rel " << f->get_name() << " (";
+        for (unsigned i = 0; i < f->get_arity(); ++i) {                
+            ast_smt2_pp(out, f->get_domain(i), env);
+            if (i + 1 < f->get_arity()) {
+                out << " ";
+            }
+        }
+        out << "))\n";
+    }
+
+    bool context::is_query(expr* q) {
+        if (!is_app(q) || !is_predicate(to_app(q)->get_decl())) {
+            return false;
+        }
+        app* a = to_app(q);
+        for (unsigned i = 0; i < a->get_num_args(); ++i) {
+            if (!is_var(a->get_arg(i))) {
+                return false;
+            }
+            var* v = to_var(a->get_arg(i));
+            if (v->get_idx() != i) {
+                return false;
+            }
+        }
+        return true;
+    }
+
 
     void context::declare_vars(expr_ref_vector& rules, mk_fresh_name& fresh_names, std::ostream& out) {
         //

src/muz/base/dl_context.h

@@ -581,6 +581,9 @@ namespace datalog {
         //undefined and private copy constructor and operator=
         context(const context&);
         context& operator=(const context&);
+
+        bool is_query(expr* e);
+        void display_rel_decl(std::ostream& out, func_decl* f);
     };
 
 };

src/smt/theory_seq.cpp

@@ -573,12 +573,12 @@ bool theory_seq::check_extensionality() {
     unsigned sz = get_num_vars();
     unsigned_vector seqs;
     for (unsigned v = 0; v < sz; ++v) {
-        enode* n = get_enode(v);
+        enode* n1 = get_enode(v);
-        expr* o1 = n->get_owner();
+        expr* o1 = n1->get_owner();
-        if (n != n->get_root()) {
+        if (n1 != n1->get_root()) {
             continue;
         }
-        if (!seqs.empty() && ctx.is_relevant(n) && m_util.is_seq(o1) && ctx.is_shared(n)) {
+        if (!seqs.empty() && ctx.is_relevant(n1) && m_util.is_seq(o1) && ctx.is_shared(n1)) {
             dependency* dep = 0;
             expr_ref e1 = canonize(o1, dep);
             for (unsigned i = 0; i < seqs.size(); ++i) {
@@ -587,7 +587,7 @@ bool theory_seq::check_extensionality() {
                 if (m.get_sort(o1) != m.get_sort(o2)) {
                     continue;
                 }
-                if (m_exclude.contains(o1, o2)) {
+                if (ctx.is_diseq(n1, n2) || m_exclude.contains(o1, o2)) {
                     continue;
                 }
                 expr_ref e2 = canonize(n2->get_owner(), dep);
@@ -597,8 +597,17 @@ bool theory_seq::check_extensionality() {
                     m_exclude.update(o1, o2);
                     continue;
                 }
+                bool excluded = false;
+                for (unsigned j = 0; !excluded && j < m_lhs.size(); ++j) {
+                    if (m_exclude.contains(m_lhs[j].get(), m_rhs[j].get())) {
+                        excluded = true;
+                    }
+                }
+                if (excluded) {
+                    continue;
+                }
                 TRACE("seq", tout << mk_pp(o1, m) << " = " << mk_pp(o2, m) << "\n";);
-                ctx.assume_eq(n, n2);                
+                ctx.assume_eq(n1, n2);                
                 return false;
             }
         }