From 9ebb6d4db4562fe6beab403b362267393add29dc Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Mon, 13 Sep 2021 18:33:59 -0400 Subject: [PATCH] remove Solver offline method, fix mypy for test_smt.py --- cryptol-remote-api/python/cryptol/solver.py | 11 ----------- cryptol-remote-api/python/tests/cryptol/test_smt.py | 9 ++++++--- 2 files changed, 6 insertions(+), 14 deletions(-) diff --git a/cryptol-remote-api/python/cryptol/solver.py b/cryptol-remote-api/python/cryptol/solver.py index d2279460..b6bfab9c 100644 --- a/cryptol-remote-api/python/cryptol/solver.py +++ b/cryptol-remote-api/python/cryptol/solver.py @@ -32,27 +32,16 @@ class Solver(metaclass=ABCMeta): """Returns whether hash consing is enabled (if applicable).""" return self.__hash_consing - @abstractmethod - def offline(self) -> bool: - """Returns true iff this solver generates offline queries.""" - pass - @abstractmethod def without_hash_consing(self) -> 'Solver': """Returns an identical solver but with hash consing disabled (if applicable).""" pass class OnlineSolver(Solver): - def offline(self) -> bool: - return False - def without_hash_consing(self) -> 'OnlineSolver': return OnlineSolver(name=self.__name, hash_consing=False) class OfflineSolver(Solver): - def offline(self) -> bool: - return True - def without_hash_consing(self) -> 'OfflineSolver': return OfflineSolver(name=self.__name, hash_consing=False) diff --git a/cryptol-remote-api/python/tests/cryptol/test_smt.py b/cryptol-remote-api/python/tests/cryptol/test_smt.py index f7055f62..84a31921 100644 --- a/cryptol-remote-api/python/tests/cryptol/test_smt.py +++ b/cryptol-remote-api/python/tests/cryptol/test_smt.py @@ -29,7 +29,8 @@ class TestSMT(unittest.TestCase): ex_false_prove = c.prove(ex_false) self.assertFalse(ex_false_prove) self.assertIsInstance(ex_false_prove, cryptol.Counterexample) - self.assertEqual(ex_false_prove.type, "predicate falsified") + if isinstance(ex_false_prove, cryptol.Counterexample): + self.assertEqual(ex_false_prove.type, "predicate falsified") ex_false_sat = c.sat(ex_false) self.assertFalse(ex_false_sat) self.assertIsInstance(ex_false_sat, cryptol.Unsatisfiable) @@ -38,11 +39,13 @@ class TestSMT(unittest.TestCase): ex_partial_safe = c.safe(ex_partial) self.assertFalse(ex_partial_safe) self.assertIsInstance(ex_partial_safe, cryptol.Counterexample) - self.assertEqual(ex_partial_safe.type, "safety violation") + if isinstance(ex_partial_safe, cryptol.Counterexample): + self.assertEqual(ex_partial_safe.type, "safety violation") ex_partial_prove = c.prove(ex_partial) self.assertFalse(ex_partial_prove) self.assertIsInstance(ex_partial_prove, cryptol.Counterexample) - self.assertEqual(ex_partial_prove.type, "safety violation") + if isinstance(ex_partial_prove, cryptol.Counterexample): + self.assertEqual(ex_partial_prove.type, "safety violation") ex_partial_sat = c.sat(ex_partial) self.assertTrue(ex_partial_sat) self.assertIsInstance(ex_partial_sat, cryptol.Satisfiable)