Do not activate Z3 relaxed cycle detection if no Z3
Method name renamed to be more explicit on its purpose. Change-Id: I02ed664d5a2ca03020a126758937d5f933cb2af5
This commit is contained in:
parent
c86a2f5d0c
commit
f49e651728
|
@ -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"))
|
||||
|
|
|
@ -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):
|
||||
|
|
|
@ -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
|
||||
|
||||
|
|
Loading…
Reference in New Issue