Added bitwuzla to pysmt frontend (#325)

stanford-centaur · Mar 14, 2023 · f2d7d3d · f2d7d3d
1 parent 68f82c5
commit f2d7d3d
Showing 1 changed file with 16 additions and 0 deletions.
diff --git a/python/smt_switch/pysmt_frontend/pysmt_solver.py b/python/smt_switch/pysmt_frontend/pysmt_solver.py
@@ -199,6 +199,22 @@ def _reset_assertions(self):
     SWITCH_SOLVERS['btor'] = SwitchBtor
 
 
+if 'bitwuzla' in  ss.solvers:
+    logics_params = dict(
+        quantifier_free=[True],
+        arrays=[True, False],
+        bit_vectors=[True],
+        uninterpreted=[True, False],
+        floating_point=[True, False],
+    )
+
+    class SwitchBitwuzla(_SwitchSolver):
+        LOGICS = _build_logics(logics_params)
+        _create_solver = ft.partial(ss.create_bitwuzla_solver, False)
+
+    SWITCH_SOLVERS['bitwuzla'] = SwitchBitwuzla
+
+
 if 'msat' in ss.solvers:
     logics_params = dict(
         quantifier_free=[True],