From 132f984d5142bdc676da614796bd59da2a06caa1 Mon Sep 17 00:00:00 2001
From: Alex Horn <t-alexh@microsoft.com>
Date: Wed, 10 Jun 2015 20:19:14 +0100
Subject: [PATCH] Add syntactical min checker

The purpose of this patch is to find out more about the "shape" of
the constraints in our benchmarks. In particular, we would like to
determine whether aggregation and negation, together, appear in
recursive rules.

Signed-off-by: Alex Horn <t-alexh@microsoft.com>
---
 src/muz/base/dl_rule_set.cpp | 45 +++++++++++++++++++++++++++++++++++-
 src/muz/base/dl_rule_set.h   |  2 +-
 2 files changed, 45 insertions(+), 2 deletions(-)

diff --git a/src/muz/base/dl_rule_set.cpp b/src/muz/base/dl_rule_set.cpp
index ad3b512a3..555b592ef 100644
--- a/src/muz/base/dl_rule_set.cpp
+++ b/src/muz/base/dl_rule_set.cpp
@@ -400,7 +400,7 @@ namespace datalog {
         SASSERT(!is_closed()); //the rule_set is not already closed        
         m_deps.populate(*this);
         m_stratifier = alloc(rule_stratifier, m_deps);
-        if (!stratified_negation()) {
+        if (!stratified_negation() || !check_min()) {
             m_stratifier = 0;
             m_deps.reset();
             return false;
@@ -441,6 +441,49 @@ namespace datalog {
         return true;
     }
 
+    bool rule_set::check_min() {
+        // For now, we check the following:
+        //
+        // if a min aggregation function occurs in an SCC, is this SCC
+        // free of any other non-monotonic functions, e.g. negation?
+        const unsigned NEG_BIT = 1U << 0;
+        const unsigned MIN_BIT = 1U << 1;
+
+        ptr_vector<rule>::const_iterator it = m_rules.c_ptr();
+        ptr_vector<rule>::const_iterator end = m_rules.c_ptr() + m_rules.size();
+        unsigned_vector component_status(m_stratifier->get_strats().size());
+
+        for (; it != end; it++) {
+            rule * r = *it;
+            app * head = r->get_head();
+            func_decl * head_decl = head->get_decl();
+            unsigned head_strat = get_predicate_strat(head_decl);
+            unsigned n = r->get_tail_size();
+            for (unsigned i = 0; i < n; i++) {
+                func_decl * tail_decl = r->get_tail(i)->get_decl();
+                unsigned strat = get_predicate_strat(tail_decl);
+
+                if (r->is_neg_tail(i)) {
+                    SASSERT(strat < component_status.size());
+                    component_status[strat] |= NEG_BIT;
+                }
+
+                if (r->is_min_tail(i)) {
+                    SASSERT(strat < component_status.size());
+                    component_status[strat] |= MIN_BIT;
+                }
+            }
+        }
+
+        const unsigned CONFLICT = NEG_BIT | MIN_BIT;
+        for (unsigned k = 0; k < component_status.size(); ++k) {
+            if (component_status[k] == CONFLICT)
+                return false;
+        }
+
+        return true;
+    }
+
     void rule_set::replace_rules(const rule_set & src) {
         if (this != &src) {
             reset();
diff --git a/src/muz/base/dl_rule_set.h b/src/muz/base/dl_rule_set.h
index 5201d9257..a7d09b099 100644
--- a/src/muz/base/dl_rule_set.h
+++ b/src/muz/base/dl_rule_set.h
@@ -179,7 +179,7 @@ namespace datalog {
         void compute_deps();
         void compute_tc_deps();
         bool stratified_negation();
-
+        bool check_min();
     public:
         rule_set(context & ctx);
         rule_set(const rule_set & rs);