From 6e7e53e25c0bb1f42a6062d21963894e97888437 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 7 Apr 2020 19:14:01 -0700
Subject: [PATCH] block selected configurations from HORN tactic

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz/fp/horn_tactic.cpp  | 27 +++++++++++++++++++++++----
 src/muz/rel/dl_compiler.cpp | 25 +++++++++++++------------
 2 files changed, 36 insertions(+), 16 deletions(-)

diff --git a/src/muz/fp/horn_tactic.cpp b/src/muz/fp/horn_tactic.cpp
index dd63b81ae..6cc2636a6 100644
--- a/src/muz/fp/horn_tactic.cpp
+++ b/src/muz/fp/horn_tactic.cpp
@@ -16,20 +16,20 @@ Author:
 Revision History:
 
 --*/
+#include "ast/ast_util.h"
+#include "ast/rewriter/var_subst.h"
+#include "ast/rewriter/expr_replacer.h"
 #include "tactic/tactical.h"
 #include "tactic/model_converter.h"
 #include "tactic/proof_converter.h"
+#include "tactic/generic_model_converter.h"
 #include "muz/fp/horn_tactic.h"
 #include "muz/base/dl_context.h"
 #include "muz/fp/dl_register_engine.h"
-#include "ast/rewriter/expr_replacer.h"
 #include "muz/base/dl_rule_transformer.h"
 #include "muz/transforms/dl_mk_slice.h"
-#include "tactic/generic_model_converter.h"
 #include "muz/transforms/dl_transforms.h"
 #include "muz/base/fp_params.hpp"
-#include "ast/ast_util.h"
-#include "ast/rewriter/var_subst.h"
 
 class horn_tactic : public tactic {
     struct imp {
@@ -193,6 +193,8 @@ class horn_tactic : public tactic {
             expr_ref q(m), f(m);
             expr_ref_vector queries(m);
             std::stringstream msg;
+            
+            check_parameters();
 
             m_ctx.reset();
             m_ctx.ensure_opened();
@@ -228,6 +230,7 @@ class horn_tactic : public tactic {
                 mc1->hide(q);
                 g->add(mc1);
             }
+            
             SASSERT(queries.size() == 1);
             q = queries[0].get();
             proof_converter_ref pc = g->pc();
@@ -343,8 +346,24 @@ class horn_tactic : public tactic {
             g->set_prec(goal::UNDER_OVER);
         }
 
+        void check_parameters() {
+            fp_params const& p = m_ctx.get_params();
+            if (p.engine() == symbol("datalog"))
+                not_supported();
+            if (p.datalog_generate_explanations())
+                not_supported(); 
+            if (p.datalog_magic_sets_for_queries())
+                not_supported();
+        }
+
+        void not_supported() {
+            throw default_exception("unsupported parameter combination passed to HORN tactic");
+        }
+
     };
 
+
+
     bool       m_is_simplify;
     params_ref m_params;
     statistics m_stats;
diff --git a/src/muz/rel/dl_compiler.cpp b/src/muz/rel/dl_compiler.cpp
index b0a5ca9ee..b6f69873b 100644
--- a/src/muz/rel/dl_compiler.cpp
+++ b/src/muz/rel/dl_compiler.cpp
@@ -819,15 +819,15 @@ namespace datalog {
                 aci.domain=head_sig[i];
 
                 expr * exp = h->get_arg(i);
-                if(is_var(exp)) {
-                    unsigned var_num=to_var(exp)->get_idx();
-                    int2ints::entry * e = var_indexes.find_core(var_num);
-                    if(e) {
-                        unsigned_vector & binding_indexes = e->get_data().m_value;
-                        aci.kind=ACK_BOUND_VAR;
-                        aci.source_column=binding_indexes.back();
-                        SASSERT(aci.source_column<single_res_expr.size()); //we bind only to existing columns
-                        if(binding_indexes.size()>1) {
+                if (is_var(exp)) {
+                    unsigned var_num = to_var(exp)->get_idx();
+                    int2ints::entry* e = var_indexes.find_core(var_num);
+                    if (e) {
+                        unsigned_vector& binding_indexes = e->get_data().m_value;
+                        aci.kind = ACK_BOUND_VAR;
+                        aci.source_column = binding_indexes.back();
+                        SASSERT(aci.source_column < single_res_expr.size()); //we bind only to existing columns
+                        if (binding_indexes.size() > 1) {
                             //if possible, we do not want multiple head columns
                             //point to a single column in the intermediate table,
                             //since then we would have to duplicate the column
@@ -836,13 +836,14 @@ namespace datalog {
                         }
                     }
                     else {
-                        aci.kind=ACK_UNBOUND_VAR;
-                        aci.var_index=var_num;
+                        aci.kind = ACK_UNBOUND_VAR;
+                        aci.var_index = var_num;
                     }
                 }
                 else {
                     SASSERT(is_app(exp));
-                    SASSERT(m_context.get_decl_util().is_numeral_ext(exp));
+                    if (!m_context.get_decl_util().is_numeral_ext(exp))
+                        throw default_exception("could not process non-numeral in Datalog engine");
                     aci.kind=ACK_CONSTANT;
                     aci.constant=to_app(exp);
                 }