feat: support for all solver backends for cryptol server/client

cryptol-remote-api/cryptol-remote-api.cabal

@@ -42,6 +42,7 @@ common deps
     bytestring           ^>= 0.10.8,
     containers           >=0.6.0.1 && <0.7,
     cryptol              >= 2.9.0,
+    directory,
     filepath             ^>= 1.4,
     lens                 >= 4.17 && < 4.20,
     mtl                  ^>= 2.2,

cryptol-remote-api/docs/Cryptol.rst

@@ -559,7 +559,7 @@ Parameter fields
 
 
 ``prover``
-  The SMT solver to use to check for satisfiability. I.e., one of the following: ``cvc4``, ``yices``, ``z3``, ``boolector``, ``mathsat``, ``abc``, ``offline``, ``any``, ``sbv-cvc4``, ``sbv-yices``, ``sbv-z3``, ``sbv-boolector``, ``sbv-mathsat``, ``sbv-abc``, ``sbv-offline``, ``sbv-any``, .
+  The SMT solver to use to check for satisfiability. I.e., one of the following: ``w4-cvc4``, ``w4-yices``, ``w4-z3``, ``w4-boolector``, ``w4-offline``, ``w4-any``, ``cvc4``, ``yices``, ``z3``, ``boolector``, ``mathsat``, ``abc``, ``offline``, ``any``, ``sbv-cvc4``, ``sbv-yices``, ``sbv-z3``, ``sbv-boolector``, ``sbv-mathsat``, ``sbv-abc``, ``sbv-offline``, ``sbv-any``.
 
 
 
@@ -578,27 +578,37 @@ Parameter fields
 
 
 
+``hash consing``
+  Whether or not to use hash consing of terms (if available).``true`` to enable or ``false`` to disable.
+
+
+
 Return fields
 +++++++++++++
 
 
 ``result``
-  A string (one of ``unsatisfiable``, ``invalid``, or ``satisfied``) indicating the result of checking for validity, satisfiability, or safety.
+  Either a string indicating the result of checking for validity, satisfiability, or safety---i.e., one of ``unsatisfiable``, ``invalid``, or ``satisfied``---or the string literal ``offline`` indicating an offline solver option was selected and the contents of the SMT query will be returned instead of a SAT result.
 
 
 
 ``counterexample type``
-  Only used if the ``result`` is ``invalid``.This describes the variety of counterexample that was produced. This can be either ``safety violation`` or ``predicate falsified``.
+  Only used if the ``result`` is ``invalid``. This describes the variety of counterexample that was produced. This can be either ``safety violation`` or ``predicate falsified``.
 
 
 
 ``counterexample``
-  Only used if the ``result`` is ``invalid``.A list of objects where each object has an ``expr``field, indicating a counterexample expression, and a ``type``field, indicating the type of the expression.
+  Only used if the ``result`` is ``invalid``. A list of objects where each object has an ``expr``field, indicating a counterexample expression, and a ``type``field, indicating the type of the expression.
 
 
 
 ``models``
-  Only used if the ``result`` is ``satisfied``.A list of list of objects where each object has an ``expr``field, indicating a expression in a model, and a ``type``field, indicating the type of the expression.
+  Only used if the ``result`` is ``satisfied``. A list of list of objects where each object has an ``expr``field, indicating a expression in a model, and a ``type``field, indicating the type of the expression.
+
+
+
+``query``
+  Only used if the ``result`` is ``offline``. The raw textual contents of the requested SMT query which can inspected or manually given to an SMT solver.
 
 
 

cryptol-remote-api/python/cryptol/commands.py

@@ -9,7 +9,7 @@
 
 import argo_client.interaction as argo
 from argo_client.interaction import HasProtocolState
-from . import solver
+from .solver import Solver, OfflineSmtQuery
 from .bitvector import BV
 from .opaque import OpaqueValue
 
@@ -167,12 +167,13 @@ class SmtQueryType(str, Enum):
     SAT   = 'sat'
 
 class CryptolProveSat(argo.Command):
-    def __init__(self, connection : HasProtocolState, qtype : SmtQueryType, expr : Any, solver : solver.Solver, count : Optional[int]) -> None:
+    def __init__(self, connection : HasProtocolState, qtype : SmtQueryType, expr : Any, solver : Solver, count : Optional[int]) -> None:
         super(CryptolProveSat, self).__init__(
             'prove or satisfy',
             {'query type': qtype,
              'expression': expr,
-             'prover': solver,
+             'prover': solver.name(),
+             'hash consing': "true" if solver.hash_consing() else "false",
              'result count': 'all' if count is None else count},
             connection
         )
@@ -193,19 +194,21 @@ def process_result(self, res : Any) -> Any:
             return [from_cryptol_arg(arg['expr'])
                     for m in res['models']
                     for arg in m]
+        elif res['result'] == 'offline':
+            return OfflineSmtQuery(content=res['query'])
         else:
             raise ValueError("Unknown SMT result: " + str(res))
 
 class CryptolProve(CryptolProveSat):
-    def __init__(self, connection : HasProtocolState, expr : Any, solver : solver.Solver) -> None:
+    def __init__(self, connection : HasProtocolState, expr : Any, solver : Solver) -> None:
         super(CryptolProve, self).__init__(connection, SmtQueryType.PROVE, expr, solver, 1)
 
 class CryptolSat(CryptolProveSat):
-    def __init__(self, connection : HasProtocolState, expr : Any, solver : solver.Solver, count : int) -> None:
+    def __init__(self, connection : HasProtocolState, expr : Any, solver : Solver, count : int) -> None:
         super(CryptolSat, self).__init__(connection, SmtQueryType.SAT, expr, solver, count)
 
 class CryptolSafe(CryptolProveSat):
-    def __init__(self, connection : HasProtocolState, expr : Any, solver : solver.Solver) -> None:
+    def __init__(self, connection : HasProtocolState, expr : Any, solver : Solver) -> None:
         super(CryptolSafe, self).__init__(connection, SmtQueryType.SAFE, expr, solver, 1)
 
 class CryptolNames(argo.Command):

cryptol-remote-api/python/cryptol/solver.py

@@ -1,7 +1,35 @@
 """Cryptol solver-related definitions"""
 from typing import NewType
 
-Solver = NewType('Solver', str)
+from dataclasses import dataclass
+
+@dataclass
+class OfflineSmtQuery():
+  """An SMTLIB2 script -- produced when an `offline` prover is used."""
+  content: str
+
+class Solver():
+  """An SMT solver mode selectable for Cryptol. Compare with the `:set prover` options in
+  the Cryptol REPL."""
+  __name: str
+  __hash_consing: bool
+
+  def __init__(self, name:str, hash_consing:bool=True) -> None:
+    self.__name = name
+    self.__hash_consing = hash_consing
+
+  def name(self) -> str:
+    """Returns a string describing the solver setup which Cryptol will recognize -- i.e.,
+    see the options available via `:set prover = NAME`."""
+    return self.__name
+
+  def hash_consing(self) -> bool:
+    """Returns whether hash consing is enabled (if applicable)."""
+    return self.__hash_consing
+
+  def without_hash_consing(self) -> 'Solver':
+    """Returns an identical solver but with hash consing disabled (if applicable)."""
+    return Solver(name=self.__name, hash_consing=False)
 
 # Cryptol-supported SMT configurations/solvers
 # (see Cryptol.Symbolic.SBV Haskell module)
@@ -25,5 +53,5 @@
 W4_YICES: Solver     = Solver("w4-yices")
 W4_Z3: Solver        = Solver("w4-z3")
 W4_BOOLECTOR: Solver = Solver("w4-boolector")
-W4_MATHSAT: Solver   = Solver("w4-offline")
+W4_OFFLINE: Solver   = Solver("w4-offline")
 W4_ABC: Solver       = Solver("w4-any")

cryptol-remote-api/python/tests/cryptol/test_cryptol_api.py

@@ -54,7 +54,7 @@ def test_low_level(self):
     #     self.assertEqual(add(BV(8,1),   BV(8,2)), BV(8,3))
     #     self.assertEqual(add(BV(8,255), BV(8,1)), BV(8,0))
 
-    def test_sat(self):
+    def test_sat_and_prove(self):
         c = self.c
         # test a single sat model can be returned
         rootsOf9 = c.sat('isSqrtOf9').result()
@@ -81,6 +81,13 @@ def test_sat(self):
 
         # check for a valid condition
         self.assertTrue(c.prove('\\x -> isSqrtOf9 x ==> elem x [3,131,125,253]').result())
+        self.assertTrue(c.prove('\\x -> isSqrtOf9 x ==> elem x [3,131,125,253]', solver.Z3).result())
+        self.assertTrue(c.prove('\\x -> isSqrtOf9 x ==> elem x [3,131,125,253]', solver.W4_Z3).result())
+        self.assertTrue(c.prove('\\x -> isSqrtOf9 x ==> elem x [3,131,125,253]', solver.W4_Z3.without_hash_consing()).result())
+        self.assertTrue(c.prove('\\x -> isSqrtOf9 x ==> elem x [3,131,125,253]', solver.SBV_Z3).result())
+        self.assertIsInstance(c.prove('\\(x : [8]) -> x == reverse (reverse x)', solver.OFFLINE).result(), solver.OfflineSmtQuery)
+        self.assertIsInstance(c.prove('\\(x : [8]) -> x == reverse (reverse x)', solver.SBV_OFFLINE).result(), solver.OfflineSmtQuery)
+        self.assertIsInstance(c.prove('\\(x : [8]) -> x == reverse (reverse x)', solver.W4_OFFLINE).result(), solver.OfflineSmtQuery)
 
     def test_check(self):
         c = self.c
@@ -146,6 +153,12 @@ def test_safe(self):
         res = c.safe("\\x -> x / (x:[8])").result()
         self.assertEqual(res, [BV(size=8, value=0)])
 
+        res = c.safe("\\x -> x / (x:[8])", solver.Z3).result()
+        self.assertEqual(res, [BV(size=8, value=0)])
+
+        res = c.safe("\\x -> x / (x:[8])", solver.W4_Z3).result()
+        self.assertEqual(res, [BV(size=8, value=0)])
+
 
     def test_many_usages_one_connection(self):
         c = self.c