From 082dcda7f7e2e5850fc6b7a9b4452c493b280a05 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 10 Jan 2016 19:16:59 -0800
Subject: [PATCH] Fix Issue #405: Horn normal form ignores implication

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz/base/dl_rule.cpp |  4 ++++
 src/muz/base/hnf.cpp     | 11 ++++++++++-
 src/smt/smt_context.cpp  |  2 +-
 3 files changed, 15 insertions(+), 2 deletions(-)

diff --git a/src/muz/base/dl_rule.cpp b/src/muz/base/dl_rule.cpp
index aa010ab5a..693391bef 100644
--- a/src/muz/base/dl_rule.cpp
+++ b/src/muz/base/dl_rule.cpp
@@ -282,6 +282,8 @@ namespace datalog {
 
 
     func_decl* rule_manager::mk_query(expr* query, rule_set& rules) {
+        TRACE("dl", tout << mk_pp(query, m) << "\n";);
+            
         ptr_vector<sort> vars;
         svector<symbol> names;
         app_ref_vector body(m);
@@ -290,6 +292,7 @@ namespace datalog {
         // Add implicit variables.
         // Remove existential prefix.
         bind_variables(query, false, q);
+
         quantifier_hoister qh(m);
         qh.pull_quantifier(false, q, 0, &names);
         // retrieve free variables.
@@ -358,6 +361,7 @@ namespace datalog {
         if (!vars.empty()) {
             rule_expr = m.mk_forall(vars.size(), vars.c_ptr(), names.c_ptr(), impl);
         }
+        TRACE("dl", tout << rule_expr << "\n";);
 
         scoped_proof_mode _sc(m, m_ctx.generate_proof_trace()?PGM_FINE:PGM_DISABLED);
         proof_ref pr(m);
diff --git a/src/muz/base/hnf.cpp b/src/muz/base/hnf.cpp
index 6c1e917c3..6d1c19a13 100644
--- a/src/muz/base/hnf.cpp
+++ b/src/muz/base/hnf.cpp
@@ -325,9 +325,10 @@ private:
 
     void eliminate_disjunctions(expr_ref_vector::element_ref& body, proof_ref_vector& proofs) {
         expr* b = body.get(); 
-        expr* e1;
+        expr* e1, *e2;
         bool negate_args = false;
         bool is_disj = false;
+        expr_ref_vector _body(m);
         unsigned num_disj = 0;
         expr* const* disjs = 0;
         if (!contains_predicate(b)) {
@@ -346,6 +347,14 @@ private:
             num_disj = to_app(e1)->get_num_args();
             disjs = to_app(e1)->get_args();
         }
+        if (m.is_implies(b, e1, e2)) {
+            is_disj = true;
+            _body.push_back(mk_not(m, e1));
+            _body.push_back(e2);
+            disjs = _body.c_ptr();
+            num_disj = 2;
+            negate_args = false;
+        }
         if (is_disj) {
             app* old_head = 0;
             if (m_memoize_disj.find(b, old_head)) {
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 9b9fdf841..f12708150 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -4126,7 +4126,7 @@ namespace smt {
             if (m_fparams.m_model_compact)
                 m_proto_model->compress();
             TRACE("mbqi_bug", tout << "after cleanup:\n"; model_pp(tout, *m_proto_model););
-            SASSERT(validate_model());
+            //SASSERT(validate_model());
         }
     }