mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-22 19:41:22 +03:00
remove Solver offline method, fix mypy for test_smt.py
This commit is contained in:
parent
2ef2a35118
commit
9ebb6d4db4
@ -32,27 +32,16 @@ class Solver(metaclass=ABCMeta):
|
|||||||
"""Returns whether hash consing is enabled (if applicable)."""
|
"""Returns whether hash consing is enabled (if applicable)."""
|
||||||
return self.__hash_consing
|
return self.__hash_consing
|
||||||
|
|
||||||
@abstractmethod
|
|
||||||
def offline(self) -> bool:
|
|
||||||
"""Returns true iff this solver generates offline queries."""
|
|
||||||
pass
|
|
||||||
|
|
||||||
@abstractmethod
|
@abstractmethod
|
||||||
def without_hash_consing(self) -> 'Solver':
|
def without_hash_consing(self) -> 'Solver':
|
||||||
"""Returns an identical solver but with hash consing disabled (if applicable)."""
|
"""Returns an identical solver but with hash consing disabled (if applicable)."""
|
||||||
pass
|
pass
|
||||||
|
|
||||||
class OnlineSolver(Solver):
|
class OnlineSolver(Solver):
|
||||||
def offline(self) -> bool:
|
|
||||||
return False
|
|
||||||
|
|
||||||
def without_hash_consing(self) -> 'OnlineSolver':
|
def without_hash_consing(self) -> 'OnlineSolver':
|
||||||
return OnlineSolver(name=self.__name, hash_consing=False)
|
return OnlineSolver(name=self.__name, hash_consing=False)
|
||||||
|
|
||||||
class OfflineSolver(Solver):
|
class OfflineSolver(Solver):
|
||||||
def offline(self) -> bool:
|
|
||||||
return True
|
|
||||||
|
|
||||||
def without_hash_consing(self) -> 'OfflineSolver':
|
def without_hash_consing(self) -> 'OfflineSolver':
|
||||||
return OfflineSolver(name=self.__name, hash_consing=False)
|
return OfflineSolver(name=self.__name, hash_consing=False)
|
||||||
|
|
||||||
|
@ -29,7 +29,8 @@ class TestSMT(unittest.TestCase):
|
|||||||
ex_false_prove = c.prove(ex_false)
|
ex_false_prove = c.prove(ex_false)
|
||||||
self.assertFalse(ex_false_prove)
|
self.assertFalse(ex_false_prove)
|
||||||
self.assertIsInstance(ex_false_prove, cryptol.Counterexample)
|
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)
|
ex_false_sat = c.sat(ex_false)
|
||||||
self.assertFalse(ex_false_sat)
|
self.assertFalse(ex_false_sat)
|
||||||
self.assertIsInstance(ex_false_sat, cryptol.Unsatisfiable)
|
self.assertIsInstance(ex_false_sat, cryptol.Unsatisfiable)
|
||||||
@ -38,11 +39,13 @@ class TestSMT(unittest.TestCase):
|
|||||||
ex_partial_safe = c.safe(ex_partial)
|
ex_partial_safe = c.safe(ex_partial)
|
||||||
self.assertFalse(ex_partial_safe)
|
self.assertFalse(ex_partial_safe)
|
||||||
self.assertIsInstance(ex_partial_safe, cryptol.Counterexample)
|
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)
|
ex_partial_prove = c.prove(ex_partial)
|
||||||
self.assertFalse(ex_partial_prove)
|
self.assertFalse(ex_partial_prove)
|
||||||
self.assertIsInstance(ex_partial_prove, cryptol.Counterexample)
|
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)
|
ex_partial_sat = c.sat(ex_partial)
|
||||||
self.assertTrue(ex_partial_sat)
|
self.assertTrue(ex_partial_sat)
|
||||||
self.assertIsInstance(ex_partial_sat, cryptol.Satisfiable)
|
self.assertIsInstance(ex_partial_sat, cryptol.Satisfiable)
|
||||||
|
Loading…
Reference in New Issue
Block a user