From f49e65172873082ebf1e38ce5be00ad05776526f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Pierre=20Cr=C3=A9gut?= <pierre.cregut@orange.com>
Date: Fri, 27 Jul 2018 12:38:12 +0200
Subject: [PATCH] Do not activate Z3 relaxed cycle detection if no Z3

Method name renamed to be more explicit on its purpose.

Change-Id: I02ed664d5a2ca03020a126758937d5f933cb2af5
---
 congress/policy_engines/agnostic.py | 7 ++++---
 congress/tests/z3/test_z3theory.py  | 6 +++---
 congress/z3/z3theory.py             | 2 +-
 3 files changed, 8 insertions(+), 7 deletions(-)

diff --git a/congress/policy_engines/agnostic.py b/congress/policy_engines/agnostic.py
index 69ef1b0b0..4d69f7f06 100644
--- a/congress/policy_engines/agnostic.py
+++ b/congress/policy_engines/agnostic.py
@@ -1229,9 +1229,10 @@ class Runtime (object):
             events, include_atoms=False)
         if graph_changes:
             if (self.global_dependency_graph.has_cycle() and
-                z3theory.irreducible_cycle(
-                    self.theory,
-                    self.global_dependency_graph.cycles())):
+                (not z3types.Z3_AVAILABLE or
+                 z3theory.cycle_not_contained_in_z3(
+                     self.theory,
+                     self.global_dependency_graph.cycles()))):
                 # TODO(thinrichs): include path
                 errors.append(exception.PolicyException(
                     "Rules are recursive"))
diff --git a/congress/tests/z3/test_z3theory.py b/congress/tests/z3/test_z3theory.py
index d8bdc119e..bcb006375 100644
--- a/congress/tests/z3/test_z3theory.py
+++ b/congress/tests/z3/test_z3theory.py
@@ -35,7 +35,7 @@ def mockz3(f):
 
 class TestZ3Utilities(base.TestCase):
 
-    def test_irreducible_cycle(self):
+    def test_cycle_not_contained_in_z3(self):
         t1 = mock.MagicMock(spec=z3theory.Z3Theory)
         t2 = mock.MagicMock(spec=z3theory.Z3Theory)
         t3 = mock.MagicMock(spec=topdown.TopDownTheory)
@@ -43,10 +43,10 @@ class TestZ3Utilities(base.TestCase):
         for name, th in six.iteritems(theories):
             th.name = name
         cycles = [['t1:p', 't2:q', 't1:r'], ['t1:p1', 't2:q2']]
-        r = z3theory.irreducible_cycle(theories, cycles)
+        r = z3theory.cycle_not_contained_in_z3(theories, cycles)
         self.assertIs(False, r)
         cycles = [['t1:p', 't2:q', 't1:r'], ['t3:p1', 't2:q2']]
-        r = z3theory.irreducible_cycle(theories, cycles)
+        r = z3theory.cycle_not_contained_in_z3(theories, cycles)
         self.assertIs(True, r)
 
     def test_congress_constant(self):
diff --git a/congress/z3/z3theory.py b/congress/z3/z3theory.py
index 8481f55c7..d0db79d43 100644
--- a/congress/z3/z3theory.py
+++ b/congress/z3/z3theory.py
@@ -52,7 +52,7 @@ Z3OPT = z3types.z3
 INTER_COMPILE_DELAY = 60.0
 
 
-def irreducible_cycle(theories, cycles):
+def cycle_not_contained_in_z3(theories, cycles):
     # type: (Dict[str, base.Theory], List[List[str]]) -> bool
     """Check that there is a true cycle not through Z3 theory