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

@@ -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"))

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):

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