Fix differences to z3 API

[yoni206]

1. 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

2. 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.