PV1 ⊧ µZcomputes fixed points of a set of constraints

Application domain/field

• Fixed points
• Constraints
• SMT solving

Type of tool

Fixed point engine/calculator

Expected input

• Set of relations
• Rules (Horn clauses)
• Ground facts (unit clauses)

Format:

One of the following:

• SMT-LIB 2 format, extended with commands rule and query to add rules and start the fix-point search
• Bddbddb format
• Tuple format

Expected output

It computes fixed points with constraints.

Comments

Part of Z3