fix what4-abc solver in python client, add more SMT tests

cryptol-remote-api/python/CHANGELOG.md

@@ -5,6 +5,8 @@
 * Add an interface for Cryptol quasiquotation using an f-string-like syntax,
   see `tests/cryptol/test_quoting` for some examples.
 
+* Fixed a bug with the client's `W4_ABC` solver, added a `W4_ANY` solver.
+
 ## 2.12.0 -- 2021-11-19
 
 * v2.12 release in tandem with Cryptol 2.12 release. See Cryptol release 2.12

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

@@ -67,9 +67,10 @@ def without_hash_consing(self) -> 'OfflineSolver':
 SBV_ABC: OnlineSolver       = OnlineSolver("sbv-abc")
 SBV_OFFLINE: OfflineSolver  = OfflineSolver("sbv-offline")
 SBV_ANY: OnlineSolver       = OnlineSolver("sbv-any")
-W4_CVC4: OnlineSolver      = OnlineSolver("w4-cvc4")
-W4_YICES: OnlineSolver     = OnlineSolver("w4-yices")
-W4_Z3: OnlineSolver        = OnlineSolver("w4-z3")
-W4_BOOLECTOR: OnlineSolver = OnlineSolver("w4-boolector")
-W4_OFFLINE: OfflineSolver  = OfflineSolver("w4-offline")
-W4_ABC: OnlineSolver       = OnlineSolver("w4-any")
+W4_CVC4: OnlineSolver       = OnlineSolver("w4-cvc4")
+W4_YICES: OnlineSolver      = OnlineSolver("w4-yices")
+W4_Z3: OnlineSolver         = OnlineSolver("w4-z3")
+W4_BOOLECTOR: OnlineSolver  = OnlineSolver("w4-boolector")
+W4_OFFLINE: OfflineSolver   = OfflineSolver("w4-offline")
+W4_ABC: OnlineSolver        = OnlineSolver("w4-abc")
+W4_ANY: OnlineSolver        = OnlineSolver("w4-any")

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

@@ -2,6 +2,7 @@
 from pathlib import Path
 import unittest
 import cryptol
+import cryptol.solver as solver
 from cryptol.single_connection import *
 from cryptol.bitvector import BV
 
@@ -22,7 +23,7 @@ def test_SMT(self):
         self.assertTrue(ex_true_sat)
         self.assertIsInstance(ex_true_sat, cryptol.Satisfiable)
 
-        ex_false = '\(x : [8]) -> x+2*x+1 == x'        
+        ex_false = '\(x : [8]) -> x+2*x+1 == x'
         ex_false_safe = safe(ex_false)
         self.assertTrue(ex_false_safe)
         self.assertIsInstance(ex_false_safe, cryptol.Safe)
@@ -47,6 +48,39 @@ def test_SMT(self):
         self.assertTrue(ex_partial_sat)
         self.assertIsInstance(ex_partial_sat, cryptol.Satisfiable)
 
+    def test_each_online_solver(self):
+        # We test each solver that is packaged for use with what4
+        # via https://github.com/GaloisInc/what4-solvers - the others
+        # are commented out for now.
+        ex_true  = '\(x : [128]) -> negate (complement x + 1) == complement (negate x) + 1'
+        solvers = \
+            [solver.CVC4,
+             solver.YICES,
+             solver.Z3,
+             #solver.BOOLECTOR,
+             #solver.MATHSAT,
+             solver.ABC,
+             #solver.OFFLINE,
+             solver.ANY,
+             solver.SBV_CVC4,
+             solver.SBV_YICES,
+             solver.SBV_Z3,
+             #solver.SBV_BOOLECTOR,
+             #solver.SBV_MATHSAT,
+             solver.SBV_ABC,
+             #solver.SBV_OFFLINE,
+             solver.SBV_ANY,
+             solver.W4_CVC4,
+             solver.W4_YICES,
+             solver.W4_Z3,
+             #solver.W4_BOOLECTOR,
+             #solver.W4_OFFLINE,
+             solver.W4_ABC,
+             solver.W4_ANY]
+
+        for s in solvers:
+            self.assertTrue(prove(ex_true, s))
+
 
 if __name__ == "__main__":
     unittest.main()