Fix Context/Solver interactions (#89)

We'd never really tested them before.

Author: alex-ozdemir

.github/workflows/ci.yml

@@ -18,7 +18,7 @@ jobs:
       with:
         options: "--check --verbose"
         src: "cvc5_pythonic_api"
-        version: "23.3.0"
+        version: "23.7.0"
 
     - uses: actions/checkout@v2
       with:

Makefile

@@ -7,10 +7,10 @@ check:
 	pyright ./cvc5_pythonic_api
 
 fmt:
-	black --required-version 23.3.0 ./cvc5_pythonic_api
+	black --required-version 23.7.0 ./cvc5_pythonic_api
 
 check-fmt:
-	black --check --verbose --required-version 23.3.0 ./cvc5_pythonic_api
+	black --check --verbose --required-version 23.7.0 ./cvc5_pythonic_api
 
 coverage:
 	coverage run test_unit.py && coverage report && coverage html

cvc5_pythonic_api/cvc5_pythonic.py

@@ -127,32 +127,32 @@ def _get_args(args):
 class Context(object):
     """A Context manages all terms, configurations, etc.
 
-    In cvc5's API, these are managed by a solver, but we keep the Context class
-    (which just wraps a solver) for compatiblity.
-
-    It's only responsibilities are:
+    In z3's API, a context owns terms, sorts, and solvers. It is used to create
+    them. Terms/sorts/solvers from one context cannot be implicitly used in
+    another. Items *can* be explicitly transfered between contexts. The result
+    is that essentially all functions have a context threaded through them.
+    There is a default "main" context.
+
+    In cvc5's API, terms and sorts are created using a solver, but stored
+    globally and are freely transferable.
+
+    Our compatibility solution is:
+    * a context wraps a solver, so that a context can be used to create terms
+    * also, a context does these things:
         * making fresh identifiers for a given sort
         * looking up previously defined constants
     """
 
-    def __init__(self, *args, **kws):
-        self.reset()
-
-    def __del__(self):
-        self.solver = None
-
-    def reset(self):
-        """Fully reset the context. This actually destroys the solver object and
-        recreates it. **This invalidates all objects created within this context
-        and using them will most likely crash.**
-        """
-        self.solver = pc.Solver()
-        self.solver.setOption("produce-models", "true")
+    def __init__(self, solver=None):
+        self.solver = solver.solver if solver is not None else SimpleSolver().solver
         # Map from (name, sort) pairs to constant terms
         self.vars = {}
         # An increasing identifier used to make fresh identifiers
         self.next_fresh_var = 0
 
+    def __del__(self):
+        self.solver = None
+
     def get_var(self, name, sort):
         """Get the variable identified by `name`.
 
@@ -633,7 +633,6 @@ def eq(self, other):
         True
         """
         instance_check(other, SortRef)
-        assert self.ctx == other.ctx
         return self.as_ast() == other.as_ast()
 
     def hash(self):
@@ -1754,6 +1753,16 @@ def is_string(self):
         """
         return isinstance(self, StringSortRef)
 
+    def elem_sort(self):
+        """Get the element sort for this sequence
+
+        >>> SeqSort(IntSort()).elem_sort()
+        Int
+        >>> SeqSort(SeqSort(IntSort())).elem_sort()
+        (Seq Int)
+        """
+        return _to_sort_ref(self.ast.getSequenceElementSort(), self.ctx)
+
 
 class SeqRef(ExprRef):
     """Sequence Expressions"""
@@ -1990,13 +1999,13 @@ def Empty(s):
     True
     >>> e3 = Empty(SeqSort(IntSort()))
     >>> print(e3)
-    (as seq.empty (Seq (Seq Int)))()
+    (as seq.empty (Seq Int))()
     """
     if isinstance(s, ReSortRef):
         return ReRef(s.ctx.solver.mkRegexpNone(), s.ctx)
     if isinstance(s, StringSortRef):
         return StringRef(s.ctx.solver.mkString(""), s.ctx)
-    return _to_expr_ref(s.ctx.solver.mkEmptySequence(s.ast), s.ctx)
+    return _to_expr_ref(s.ctx.solver.mkEmptySequence(s.elem_sort().ast), s.ctx)
 
 
 def is_seq(a):
@@ -5968,20 +5977,27 @@ class Solver(object):
     * get-model,
     * etc."""
 
-    def __init__(self, solver=None, ctx=None, logFile=None):
-        assert solver is None or ctx is not None
-        self.ctx = _get_ctx(ctx)
-        self.solver = self.ctx.solver
+    def __init__(self, logic=None, ctx=None, logFile=None):
+        # save logic so that we can re-build the solver if needed.
+        self.logic = logic
+        # ignore ctx (the paramter is kept for z3 compatibility)
+        self.solver = None
+        self.initFromLogic()
         self.scopes = 0
         self.assertions_ = [[]]
         self.last_result = None
         self.resetAssertions()
 
+    def initFromLogic(self):
+        """Create the base-API solver from the logic"""
+        self.solver = pc.Solver()
+        if self.logic is not None:
+            self.solver.setLogic(self.logic)
+        self.solver.setOption("produce-models", "true")
+
     def __del__(self):
         if self.solver is not None:
             self.solver = None
-        if self.ctx is not None:
-            self.ctx = None
 
     def push(self):
         """Create a backtracking point.
@@ -6081,9 +6097,7 @@ def reset(self):
         >>> s.reset()
         >>> s.setOption(incremental=True)
         """
-        self.ctx.reset()
-        self.solver = self.ctx.solver
-        self.resetAssertions()
+        self.initFromLogic()
 
     def assert_exprs(self, *args):
         """Assert constraints into the solver.
@@ -6095,7 +6109,7 @@ def assert_exprs(self, *args):
         [x > 0, x < 2]
         """
         args = _get_args(args)
-        s = BoolSort(self.ctx)
+        s = BoolSort()
         for arg in args:
             arg = s.cast(arg)
             self.assertions_[-1].append(arg)
@@ -6184,7 +6198,7 @@ def model(self):
         >>> s.model()
         [a = -2]
         """
-        return ModelRef(self, self.ctx)
+        return ModelRef(self)
 
     def assertions(self):
         """Return an AST vector containing all added constraints.
@@ -6229,7 +6243,6 @@ def sexpr(self):
     def set(self, *args, **kwargs):
         """Set an option on the solver. Wraps ``setOption()``.
 
-        >>> main_ctx().reset()
         >>> s = Solver()
         >>> s.set(incremental=True)
         >>> s.set('incremental', 'true')
@@ -6244,7 +6257,6 @@ def setOption(self, name=None, value=None, **kwargs):
         properly converted manually, all other types are convertes using
         ``str()``.
 
-        >>> main_ctx().reset()
         >>> s = Solver()
         >>> s.setOption('incremental', True)
         >>> s.setOption(incremental='true')
@@ -6263,7 +6275,6 @@ def getOption(self, name):
         """Get the current value of an option from the solver. The value is
         returned as a string. For type-safe querying use ``getOptionInfo()``.
 
-        >>> main_ctx().reset()
         >>> s = Solver()
         >>> s.setOption(incremental=True)
         >>> s.getOption("incremental")
@@ -6285,12 +6296,10 @@ def getOptionInfo(self, name):
         """Get the current value of an option from the solver. The value is
         returned as a string. For type-safe querying use ``getOptionInfo()``.
 
-        >>> main_ctx().reset()
         >>> s = Solver()
         >>> s.setOption(incremental=False)
         >>> s.getOptionInfo("incremental")
         {'name': 'incremental', 'aliases': [], 'setByUser': True, 'type': <class 'bool'>, 'current': False, 'default': True}
-        >>> main_ctx().reset()
         """
         return self.solver.getOptionInfo(name)
 
@@ -6305,7 +6314,7 @@ def statistics(self):
         sat
         >>> stats = s.statistics()
         >>> stats['cvc5::CONSTANT']
-        {'defaulted': False, 'internal': False, 'value': {'integer type': 1}}
+        {'defaulted': True, 'internal': False, 'value': {}}
         >>> len(stats.get()) < 10
         True
         >>> len(stats.get(True, True)) > 30
@@ -6331,11 +6340,7 @@ def SolverFor(logic, ctx=None, logFile=None):
     # sat
     # >>> s.model()
     # [x = 1]
-    # """
-    solver = pc.Solver()
-    solver.setLogic(logic)
-    ctx = _get_ctx(ctx)
-    return Solver(solver, ctx, logFile)
+    return Solver(logic=logic, ctx=ctx, logFile=logFile)
 
 
 def SimpleSolver(ctx=None, logFile=None):
@@ -6347,8 +6352,7 @@ def SimpleSolver(ctx=None, logFile=None):
     >>> s.check()
     sat
     """
-    ctx = _get_ctx(ctx)
-    return Solver(None, ctx, logFile)
+    return Solver(ctx=ctx, logFile=logFile)
 
 
 #########################################
@@ -6571,17 +6575,13 @@ def is_tautology(taut):
 class ModelRef:
     """Model/Solution of a satisfiability problem (aka system of constraints)."""
 
-    def __init__(self, solver, ctx):
+    def __init__(self, solver):
         assert solver is not None
-        assert ctx is not None
         self.solver = solver
-        self.ctx = ctx
 
     def __del__(self):
         if self.solver is not None:
             self.solver = None
-        if self.ctx is not None:
-            self.ctx = None
 
     def vars(self):
         """Returns the free constants in an assertion, as terms"""
@@ -6629,7 +6629,7 @@ def eval(self, t, model_completion=False):
         >>> m.eval(x == 1)
         True
         """
-        return _to_expr_ref(self.solver.solver.getValue(t.ast), self.solver.ctx)
+        return _to_expr_ref(self.solver.solver.getValue(t.ast), Context(self.solver))
 
     def evaluate(self, t, model_completion=False):
         """Alias for `eval`.

test/pgm_outputs/example_sequence.py.out

@@ -1,13 +1,13 @@
 False
-[s = (seq.unit 1)(), t = (seq.unit 2)()]
-[s = (seq.unit (- 1))(), t = (seq.unit (- 1))()]
-[s = (as seq.empty (Seq Int))()]
-[s = (as seq.empty (Seq Int))()]
-[s = (seq.++ (seq.unit 1) (seq.unit 2))()]
-[s = (as seq.empty (Seq Int))()]
-[s = (seq.++ (seq.unit 1) (seq.unit 2))()]
-[s = (seq.++ (seq.unit 1) (seq.unit 1))(), t = (seq.++ (seq.unit 1) (seq.unit 1))()]
-[s = (as seq.empty (Seq Int))(), t = (as seq.empty (Seq Int))(), u = (as seq.empty (Seq Int))()]
-[s = (seq.++ (seq.unit (- 2)) (seq.unit (- 1)))(), t = (seq.unit (- 1))()]
-[s = (seq.++ (seq.unit (- 3)) (seq.unit (- 2)) (seq.unit 4))(), t = (seq.unit 4)()]
-no solution
+sat
+sat
+sat
+sat
+sat
+sat
+sat
+sat
+sat
+sat
+sat
+sat

test/pgm_outputs/example_sequence_update.py.out

@@ -1,3 +1,3 @@
 True
-[s = (seq.++ (seq.unit 1) (seq.unit 2))(), t = (as seq.empty (Seq Int))()]
-[a = "heAAA"]
+sat
+sat

test/pgm_outputs/multiple_solvers.py.out

@@ -0,0 +1,10 @@
+[x = 0, y = 0]
+sat
+0
+The logic was specified as QF_BV, which doesn't include THEORY_ARITH, but got a theory atom for that theory.
+The atom:
+(= x (* 2 y))
+Can't solve integer problems with QF_BV solver
+unsat
+unsat
+Can't eagerly BB with models and ALL

test/pgms/example_sequence.py

@@ -1,16 +1,24 @@
 from cvc5_pythonic_api import *
-s, t, u = Consts('s t u', SeqSort(IntSort()))
+
+s, t, u = Consts("s t u", SeqSort(IntSort()))
 print(s.is_string())
-solve(Concat(s, Unit(IntVal(2))) == Concat(Unit(IntVal(1)), t))
-solve(PrefixOf(s.at(0),t),Length(s)>0)
-solve(s[0]> 5)
-solve(PrefixOf(s,Concat(Unit(IntVal(1)),Unit(IntVal(2)))))
-solve(PrefixOf(Concat(Unit(IntVal(1)),Unit(IntVal(2))),s))
-solve(SuffixOf(s,Concat(Unit(IntVal(1)),Unit(IntVal(2)))))
-solve(SuffixOf(Concat(Unit(IntVal(1)),Unit(IntVal(2))),s))
-solve(Contains(s,t),Length(t)>1)
-solve(Replace(s,t,u)==Replace(s,u,t))
-solve(IndexOf(s,t) == 1 )
-solve(IndexOf(s,t,1) > 1 )
+
+
+def mysolve(*args):
+    s = Solver()
+    print(s.check(*args))
+
+
+mysolve(Concat(s, Unit(IntVal(2))) == Concat(Unit(IntVal(1)), t))
+mysolve(PrefixOf(s.at(0), t), Length(s) > 0)
+mysolve(s[0] > 5)
+mysolve(PrefixOf(s, Concat(Unit(IntVal(1)), Unit(IntVal(2)))))
+mysolve(PrefixOf(Concat(Unit(IntVal(1)), Unit(IntVal(2))), s))
+mysolve(SuffixOf(s, Concat(Unit(IntVal(1)), Unit(IntVal(2)))))
+mysolve(SuffixOf(Concat(Unit(IntVal(1)), Unit(IntVal(2))), s))
+mysolve(Contains(s, t), Length(t) > 1)
+mysolve(Replace(s, t, u) == Replace(s, u, t))
+mysolve(IndexOf(s, t) == 1)
+mysolve(IndexOf(s, t, 1) > 1)
 e = Empty(SeqSort(IntSort()))
-solve(PrefixOf(s,e))
+mysolve(PrefixOf(s, e))

test/pgms/example_sequence_update.py

@@ -1,6 +1,13 @@
 from cvc5_pythonic_api import *
-s,t = Consts('s t',SeqSort(IntSort()))
+
+
+def mysolve(*args):
+    s = Solver()
+    print(s.check(*args))
+
+
+s, t = Consts("s t", SeqSort(IntSort()))
 print(is_seq(s))
-solve(SeqUpdate(s,t,0) == Concat(Unit(IntVal(1)),Unit(IntVal(2))))
-a = String('a')
-solve(SeqUpdate(a,StringVal('llo'),2) == 'hello')
+mysolve(SeqUpdate(s, t, 0) == Concat(Unit(IntVal(1)), Unit(IntVal(2))))
+a = String("a")
+mysolve(SeqUpdate(a, StringVal("llo"), 2) == "hello")