Differences with Z3 API

[Eladkay]

Two examples of differences of the CVC5 API to the Z3 API:

1. This function tries to block a model from a solver:

def _block_model(solver: Solver, model: ModelRef):
    if CVC5:
        solver.add(Or([f != model[f] for f in model.decls() if getattr(f, "arity", lambda: 0)() == 0 and
                            not SOME_REGEX.fullmatch(str(f))]))
    else:
        solver.add(Or([f() != model[f] for f in model.decls() if f.arity() == 0 and
                            not SOME_REGEX.fullmatch(f.name())]))

Z3 defines model.decls() as functions that need to be called, even for constants having arity 0. CVC5 does not even define the arity method on constants (requiring the getattr trick above) nor the name method (requiring the use of str).

2. For expressions that are of a datatype (ADT) sort, you can get the name of the constructor in Z3 like so:

exp.decl().name()

In CVC5, this throws:

       exp.decl().name()
       ^^^^^^^^^^
  File "/Users/snip/lib/cvc5/build/src/api/python/cvc5/pythonic/cvc5_pythonic.py", line 418, in
decl
    raise SMTException("Declarations for non-function applications")
cvc5.pythonic.cvc5_pythonic.SMTException: Declarations for non-function applications

Probably because constructors are not considered uninterpreted function applications.