Fix differences to z3 API

[yoni206]

With cvc5 pythonic API, we can call e.g. Solver("QF_BV"), but in z3 we cannot (instead we need to use SolverFor:
Perhaps we should also not allow supplying the logic name to Solver?

>>> from cvc5.pythonic import *
>>> s = Solver("QF_BV")

>>> from z3 import *
>>> s = Solver("QF_BV")
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File "/Users/yonizohar/Library/Python/3.9/lib/python/site-packages/z3/z3.py", line 6950, in __init__
    assert solver is None or ctx is not None
AssertionError

Getting a value from a model is possible for arbitrary terms with the cvc5 pythonic API, but seems like it is possible only for variables in z3 API:

>>> from cvc5.pythonic import *
>>> a = Int("a")
>>> s = Solver()
>>> s.add(a + a == a)
>>> s.check()
sat
>>> m = s.model()
>>> m[a]
0
>>> m[a+a]
0
>>>

>>> from z3 import *
>>> a = Int("a")
>>> s = Solver()
>>> s.add(a + a == a)
>>> s.check()
sat
>>> m = s.model()
>>> m[a]
0
>>> m[a+a]
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File "/Users/yonizohar/Library/Python/3.9/lib/python/site-packages/z3/z3.py", line 6676, in __getitem__
    _z3_assert(False, "Integer, Z3 declaration, or Z3 constant expected")
  File "/Users/yonizohar/Library/Python/3.9/lib/python/site-packages
/z3/z3.py", line 107, in _z3_assert
    raise Z3Exception(msg)
z3.z3types.Z3Exception: Integer, Z3 declaration, or Z3 constant expected
>>>

[yoni206]

Discussed at the cvc5 meeting. It seems to make sense to disallow the first but to keep the second.

[caioraposo]

The current behaviour could also lead to inconsistances due to main_ctx()'s solver being a
different object from the user's -- essentially, two different instances of cvc5.cvc5_python_base.Solver. For instance, this is how z3 implements SolverFor:

def SolverFor(logic, ctx=None, logFile=None):
    """Create a solver customized for the given logic.
    ...
    """
    ctx = _get_ctx(ctx)
    logic = to_symbol(logic)
    return Solver(Z3_mk_solver_for_logic(ctx.ref(), logic), ctx, logFile)

And I think that's the way to go, and because most commands use main_ctx(), we run the risk of discharging assertions (to the global solver) that the user's one won't be aware.

[caioraposo]

Again, z3 avoids this redundant object by having this piece of code in the Solver class:

class Solver(Z3PPObject):
    def __init__(self, solver=None, ctx=None, logFile=None):
        ...
        if solver is None:
            self.solver = Z3_mk_solver(self.ctx.ref())
        else:
            self.solver = solver
        ...

What do you think, @alex-ozdemir?

[alex-ozdemir]

Hi @caioraposo . Does Yoni's PR #95 address this issue?

[caioraposo]

Not really; take a look at this:

>>> from cvc5_pythonic_api import *
>>> a = SolverFor("ALL").solver
>>> b = main_ctx().solver
>>> a is b
False

This can be problematic if, as in PR #106, we add constraints to b and check the satisfiability in a. So I believe the solver should be a singleton unless the user creates a new context, just like in z3py.

[alex-ozdemir]

I'm working to understand the issue here. Can you provide an example of a program that is valid again both APIs, but with differing behavior?

[alex-ozdemir]

I imagine we'll want to let #108 merge before addressing this.

[caioraposo]

I'll rethink the implementation of #106 as Context doesn't carry a solver anymore. But to provide you an example:

from cvc5_pythonic_api import *

s = SolverFor("ALL")
fact = Function('fact', IntSort(), IntSort())
n = Int('n')
RecAddDefinition(fact, n, If(n == 0, 1, n * fact(n - 1)))

s.add(Not(fact(5) == 120))
print(s.check())

cvc5:

sat

z3:

unsat