From b3e8020c88ff3d74e5c895629254c797454fb97d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 1 Dec 2015 14:47:33 -0800
Subject: [PATCH] bind variables in queries generated from Horn tactic to
 enforce that rule formulas don't contain free variables. Issue #328

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz/base/bind_variables.h            |  2 +-
 src/muz/base/dl_context.cpp              |  3 +--
 src/muz/base/dl_context.h                |  2 +-
 src/muz/duality/duality_dl_interface.cpp |  2 +-
 src/muz/fp/horn_tactic.cpp               | 17 +++++++++++++++++
 5 files changed, 21 insertions(+), 5 deletions(-)

diff --git a/src/muz/base/bind_variables.h b/src/muz/base/bind_variables.h
index f2aa29224..18af319f8 100644
--- a/src/muz/base/bind_variables.h
+++ b/src/muz/base/bind_variables.h
@@ -7,7 +7,7 @@ Module Name:
 
 Abstract:
 
-    Utility to find constants that are declard as varaibles.
+    Utility to find constants that are declard as variables.
 
 Author:
 
diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp
index c2db15e3a..210173f8c 100644
--- a/src/muz/base/dl_context.cpp
+++ b/src/muz/base/dl_context.cpp
@@ -973,7 +973,7 @@ namespace datalog {
         }
     }
    
-    void context::get_raw_rule_formulas(expr_ref_vector& rules, svector<symbol>& names, vector<unsigned> &bounds) {
+    void context::get_raw_rule_formulas(expr_ref_vector& rules, svector<symbol>& names, unsigned_vector &bounds) {
         for (unsigned i = 0; i < m_rule_fmls.size(); ++i) {
             expr_ref r = bind_vars(m_rule_fmls[i].get(), true);
             rules.push_back(r.get());
@@ -988,7 +988,6 @@ namespace datalog {
         
         // ensure that rules are all using bound variables.
         for (unsigned i = m_rule_fmls_head; i < m_rule_fmls.size(); ++i) {
-            ptr_vector<sort> sorts;
             m_free_vars(m_rule_fmls[i].get());
             if (!m_free_vars.empty()) {
                 rm.mk_rule(m_rule_fmls[i].get(), 0, m_rule_set, m_rule_names[i]);
diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h
index 705758aca..3b8b9d067 100644
--- a/src/muz/base/dl_context.h
+++ b/src/muz/base/dl_context.h
@@ -377,7 +377,7 @@ namespace datalog {
         rule_set & get_rules() { flush_add_rules(); return m_rule_set; }
 
         void get_rules_as_formulas(expr_ref_vector& fmls, expr_ref_vector& qs, svector<symbol>& names);
-        void get_raw_rule_formulas(expr_ref_vector& fmls, svector<symbol>& names, vector<unsigned> &bounds);
+        void get_raw_rule_formulas(expr_ref_vector& fmls, svector<symbol>& names, unsigned_vector &bounds);
 
         void add_fact(app * head);
         void add_fact(func_decl * pred, const relation_fact & fact);
diff --git a/src/muz/duality/duality_dl_interface.cpp b/src/muz/duality/duality_dl_interface.cpp
index 4e173ca44..1f64236d9 100755
--- a/src/muz/duality/duality_dl_interface.cpp
+++ b/src/muz/duality/duality_dl_interface.cpp
@@ -156,7 +156,7 @@ namespace Duality {
 
         expr_ref_vector rules(m_ctx.get_manager());
         svector< ::symbol> names;  
-        vector<unsigned> bounds;
+        unsigned_vector bounds;
         // m_ctx.get_rules_as_formulas(rules, names);
 
 
diff --git a/src/muz/fp/horn_tactic.cpp b/src/muz/fp/horn_tactic.cpp
index 8e9e48f55..ee1b773cc 100644
--- a/src/muz/fp/horn_tactic.cpp
+++ b/src/muz/fp/horn_tactic.cpp
@@ -29,6 +29,7 @@ Revision History:
 #include"dl_transforms.h"
 #include"fixedpoint_params.hpp"
 #include"ast_util.h"
+#include"var_subst.h"
 
 class horn_tactic : public tactic {
     struct imp {
@@ -37,6 +38,7 @@ class horn_tactic : public tactic {
         datalog::register_engine m_register_engine;
         datalog::context         m_ctx;
         smt_params               m_fparams;
+        expr_free_vars           m_free_vars;
 
         imp(bool t, ast_manager & m, params_ref const & p):
             m(m),
@@ -228,6 +230,7 @@ class horn_tactic : public tactic {
                 register_predicate(q);
                 for (unsigned i = 0; i < queries.size(); ++i) {
                     f = mk_rule(queries[i].get(), q);
+                    bind_variables(f);
                     m_ctx.add_rule(f, symbol::null);
                 }
                 queries.reset();
@@ -303,6 +306,20 @@ class horn_tactic : public tactic {
             SASSERT(g->is_well_sorted());
         }
 
+        void bind_variables(expr_ref& f) {
+            m_free_vars.reset();
+            m_free_vars(f);
+            m_free_vars.set_default_sort(m.mk_bool_sort());
+            if (!m_free_vars.empty()) {
+                m_free_vars.reverse();
+                svector<symbol> names;
+                for (unsigned i = 0; i < m_free_vars.size(); ++i) {
+                    names.push_back(symbol(m_free_vars.size() - i - 1));
+                }
+                f = m.mk_forall(m_free_vars.size(), m_free_vars.c_ptr(), names.c_ptr(), f);
+            }
+        }
+
         void simplify(expr* q, 
                     goal_ref const& g,
                     goal_ref_buffer & result,