restricting the use of Solver(): no specification of logic (#95)

Solves #93 in order to be compatible with z3.

Author: yoni206

cvc5_pythonic_api/cvc5_pythonic.py

@@ -6011,16 +6011,16 @@ class Solver(object):
     * get-model,
     * etc."""
 
-    def __init__(self, logic=None, ctx=None, logFile=None):
-        # save logic so that we can re-build the solver if needed.
-        self.logic = logic
+    def __init__(self, ctx=None, logFile=None):
         # ignore ctx (the paramter is kept for z3 compatibility)
         self.solver = None
+        self.logic = None
         self.initFromLogic()
         self.scopes = 0
         self.assertions_ = [[]]
         self.last_result = None
         self.resetAssertions()
+        assert ctx is None or type(ctx) == Context
 
     def initFromLogic(self):
         """Create the base-API solver from the logic"""
@@ -6426,7 +6426,10 @@ def SolverFor(logic, ctx=None, logFile=None):
     # sat
     # >>> s.model()
     # [x = 1]
-    return Solver(logic=logic, ctx=ctx, logFile=logFile)
+    s = Solver(ctx=ctx, logFile=logFile)
+    s.logic = logic
+    s.initFromLogic()
+    return s
 
 
 def SimpleSolver(ctx=None, logFile=None):

test/pgm_outputs/multiple_solvers.py.out

@@ -5,6 +5,7 @@ The logic was specified as QF_BV, which doesn't include THEORY_ARITH, but got a
 The atom:
 (= x (* 2 y))
 Can't solve integer problems with QF_BV solver
+got an exception, which is good
 unsat
 unsat
 Can't eagerly BB with models and ALL

test/pgms/multiple_solvers.py

@@ -21,6 +21,12 @@
     print(e)
     print("Can't solve integer problems with QF_BV solver")
 
+# Can't specify logic unless using `SolverFor`
+try:
+    s = Solver("QF_BV")
+except Exception as e:
+    print("got an exception, which is good")
+
 
 # QF_NIA
 s = SolverFor("QF_BV")