Added rule body reordering for safety

Previously, we assumed the user would order rule bodies to ensure
that negative literals always occurred after all their vars were
bound.

This change moves all the negative literals to the end of each rule.
It is not even smart enough to check whether there is a need to
change the ordering.  Will need to be revised once performance becomes
an issue.

Change-Id: Idae20e23abc70307fcfba5d11b1a5958d4ab05bc

congress/policy/runtime.py

@@ -1233,6 +1233,7 @@ class DeltaRuleTheory (Theory):
             return False
         self.log(rule.tablename(), "Insert 2: {}".format(str(rule)))
         for delta in self.compute_delta_rules([rule]):
+            self.reorder(delta)
             self.insert_delta(delta)
         self.originals.add(rule)
         return True
@@ -1254,6 +1255,8 @@ class DeltaRuleTheory (Theory):
                 self.all_tables[table] = 1
 
         # contents
+        # TODO(thinrichs): eliminate dups, maybe including
+        #     case where bodies are reorderings of each other
         if delta.trigger.table not in self.contents:
             self.contents[delta.trigger.table] = [delta]
         else:
@@ -1395,6 +1398,17 @@ class DeltaRuleTheory (Theory):
                     DeltaRule(literal, rule.head, newbody, rule))
         return delta_rules
 
+    @classmethod
+    def reorder(cls, delta):
+        """Given a delta rule DELTA, re-order its body for efficient
+        and correct computation.
+        """
+        # ensure negatives come after positives
+        positives = [lit for lit in delta.body if not lit.is_negated()]
+        negatives = [lit for lit in delta.body if lit.is_negated()]
+        positives.extend(negatives)
+        delta.body = positives
+
 
 class MaterializedViewTheory(TopDownTheory):
     """A theory that stores the table contents of views explicitly.
@@ -1561,6 +1575,7 @@ class MaterializedViewTheory(TopDownTheory):
             # need to eliminate self-joins here so that we fill all
             #   the tables introduced by self-join elimination.
             for rule in DeltaRuleTheory.eliminate_self_joins([formula]):
+                DeltaRuleTheory.reorder(rule)
                 bindings = self.top_down_evaluation(
                     rule.variables(), rule.body)
                 self.log(rule.tablename(),

congress/policy/tests/test_runtime.py

@@ -378,7 +378,7 @@ class TestRuntime(unittest.TestCase):
                 'q(2,6) q(2,7)')
         self.check_class(run, code, "Delete: larger self join")
 
-        # actual bug: insert data first, then
+        # was actual bug: insert data first, then
         #   insert rule with self-join
         code = ('s(1)'
                 'q(1,1)'
@@ -532,6 +532,16 @@ class TestRuntime(unittest.TestCase):
             run, 'q(1,2) r(2,3) r(2,4) u(3,5) u(4,6) s(1,3) s(1,4)',
             'Insert into non-unary with different propagation')
 
+        # Negation ordering
+        code = ("p(x) :- not q(x), r(x)")
+        run = self.prep_runtime(code, "Negation ordering")
+        self.insert(run, ['r', 1])
+        self.insert(run, ['r', 2])
+        self.insert(run, ['q', 1])
+        self.check_class(
+            run, 'r(1) r(2) q(1) p(2)',
+            'Reordering negation')
+
     def test_materialized_select(self):
         """Materialized Theory: test the SELECT event handler."""
         code = ("p(x, y) :- q(x), r(y)")