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.

[Eladkay]

More differences:

1. The Z3 module has set_param for global options:

   z3.set_param("unsat_core", True)
   z3.set_param("model", True)
   z3.set_param("model_validate", True)
   z3.set_param("model.completion", True)

   This is not supported in CVC5 and I don't see an obvious alternative.

2. Z3 has Solver.from_string:

   s = z3.Solver()
   s.from_string("\n".join(query))

   This is also not supported in CVC5 and in fact I'm not aware of any way to process SMTLIB programmatically in CVC5 (maybe I'm wrong though).

3. Z3 models have Model.sorts that returns the list of sorts involved in the model:

       z3sort_names = set(s.name() for s in z3sorts) | set(self.sorts.keys())

   Not in CVC5.

4. Z3 uninterpreted sorts have Model.get_universe(SortRef) returning all elements in the interpretation: univ = z3model.get_universe(z3sort) may return:

   [node!val!4,
   node!val!2,
   node!val!5,
   node!val!3,
   node!val!0,
   node!val!1]

   Not in CVC5.