What are the most important differences between IDP3 and IDP-Z3

Question

The newest version of the IDP system is called IDP-Z3 and is based on Microsoft's Z3 solver. (see https://www.idp-z3.be/)

Both are based on the FO(.) language, but the syntax is slightly different.

What are the most important differences in syntax, semantics, functionality, philosophy ...?

Answer 1

The IDP-Z3 docs contain a subsection detailing syntax/functionality changes, though it does not seem complete. It should probably be updated based on the answers received here.

Of the top of my head, other syntax changes are as follows.

Vocabulary:

• No more isa ... or constructed from for types. Regardless of the type, their interpretation is written as T := {a, b, ...} or T := {0..10}.
• All symbol declarations now follow the same structure: symbol_name : arg_0 * .. * arg_n -> arg_m.

Theory:

• Quantification syntax is now of the form !x in Type instead of !x[Type].
• 0-ary symbols need to be applied by writing (), e.g. p().
• The sum aggregate's syntax is now sum(lambda t in T: phi). This can be combined with an if .. then .. else .. expression to have a conditional sum. An example: total_cost() = sum(lambda x in items: if in_cart(x) then cost(x) else 0). Min/max aggregates are also changed similarly.

Structure:

• Interpretations use := instead of = and must end with a period, e.g. p := true. and human := {Ann, Jef}..

Procedure: the procedure now runs Python instead of Lua. This is elaborated upon in the docs.