From e43383b6a8fa70afde7a205e3cd6ec27c71ecf13 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 18 Aug 2013 21:11:14 -0700
Subject: [PATCH] filter query predicates from models

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz_qe/clp_context.cpp       | 10 +++++++---
 src/muz_qe/dl_mk_array_blast.cpp |  2 +-
 src/muz_qe/dl_rule.cpp           |  9 ++++++++-
 src/muz_qe/horn_tactic.cpp       | 12 +++++++++++-
 4 files changed, 27 insertions(+), 6 deletions(-)

diff --git a/src/muz_qe/clp_context.cpp b/src/muz_qe/clp_context.cpp
index 3a3908f59..01299a2b7 100644
--- a/src/muz_qe/clp_context.cpp
+++ b/src/muz_qe/clp_context.cpp
@@ -68,9 +68,13 @@ namespace datalog {
             m_goals.reset();
             rm.mk_query(query, m_ctx.get_rules());
             m_ctx.apply_default_transformation();
-            func_decl *head_decl = m_ctx.get_rules().get_output_predicate();
-
-            expr_ref head(m_ctx.get_rules().get_predicate_rules(head_decl)[0]->get_head(), m);
+            func_decl* head_decl = m_ctx.get_rules().get_output_predicate();
+            rule_set& rules = m_ctx.get_rules();
+            rule_vector const& rv = rules.get_predicate_rules(head_decl);
+            if (rv.empty()) {
+                return l_false;
+            }
+            expr_ref head(rv[0]->get_head(), m);
             ground(head);
             m_goals.push_back(to_app(head));
             return search(20, 0);
diff --git a/src/muz_qe/dl_mk_array_blast.cpp b/src/muz_qe/dl_mk_array_blast.cpp
index 9f057a148..2bfb6807a 100644
--- a/src/muz_qe/dl_mk_array_blast.cpp
+++ b/src/muz_qe/dl_mk_array_blast.cpp
@@ -250,11 +250,11 @@ namespace datalog {
         rule_set new_rules(m_ctx);
         rm.mk_rule(fml2, p, new_rules, r.name());
 
-        TRACE("dl", new_rules.last()->display(m_ctx, tout << "new rule\n"););
         rule_ref new_rule(rm);
         if (m_simplifier.transform_rule(new_rules.last(), new_rule)) {
             rules.add_rule(new_rule.get());
             rm.mk_rule_rewrite_proof(r, *new_rule.get());
+            TRACE("dl", new_rule->display(m_ctx, tout << "new rule\n"););
         }
         return true;
     }
diff --git a/src/muz_qe/dl_rule.cpp b/src/muz_qe/dl_rule.cpp
index ac683eca9..70da4ed4b 100644
--- a/src/muz_qe/dl_rule.cpp
+++ b/src/muz_qe/dl_rule.cpp
@@ -41,6 +41,7 @@ Revision History:
 #include"expr_replacer.h"
 #include"bool_rewriter.h"
 #include"expr_safe_replace.h"
+#include"filter_model_converter.h"
 
 namespace datalog {
 
@@ -335,8 +336,14 @@ namespace datalog {
         vars.reverse();
         names.reverse();
         func_decl* qpred = m_ctx.mk_fresh_head_predicate(symbol("query"), symbol(), vars.size(), vars.c_ptr(), body_pred);
-        m_ctx.register_predicate(qpred, false);
+        m_ctx.register_predicate(qpred, false);        
         rules.set_output_predicate(qpred);
+        
+        if (m_ctx.get_model_converter()) {
+            filter_model_converter* mc = alloc(filter_model_converter, m);
+            mc->insert(qpred);
+            m_ctx.add_model_converter(mc);
+        }
 
         expr_ref_vector qhead_args(m);
         for (unsigned i = 0; i < vars.size(); i++) {
diff --git a/src/muz_qe/horn_tactic.cpp b/src/muz_qe/horn_tactic.cpp
index 9d331cbfa..1916839f4 100644
--- a/src/muz_qe/horn_tactic.cpp
+++ b/src/muz_qe/horn_tactic.cpp
@@ -24,6 +24,7 @@ Revision History:
 #include"expr_replacer.h"
 #include"dl_rule_transformer.h"
 #include"dl_mk_slice.h"
+#include"filter_model_converter.h"
 
 class horn_tactic : public tactic {
     struct imp {
@@ -226,6 +227,9 @@ class horn_tactic : public tactic {
                 }
                 queries.reset();
                 queries.push_back(q);
+                filter_model_converter* mc1 = alloc(filter_model_converter, m);
+                mc1->insert(to_app(q)->get_decl());
+                mc = mc1;
             }
             SASSERT(queries.size() == 1);
             q = queries[0].get();
@@ -276,7 +280,13 @@ class horn_tactic : public tactic {
                 g->reset();
                 if (produce_models) {
                     model_ref md = m_ctx.get_model();
-                    mc = model2model_converter(&*md);
+                    model_converter_ref mc2 = model2model_converter(&*md);
+                    if (mc) {
+                        mc = concat(mc.get(), mc2.get());
+                    }
+                    else {
+                        mc = mc2;
+                    }
                 }
                 break;    
             }