1 of 10

Z3 API

2 of 10

Overview

  • How to declare vocabulary
  • How to create a logic expression
  • How to transform a logic expression
  • How to perform various inferences
  • Limitations

3 of 10

How to declare the vocabulary

Declare variables:

  • p = Const(“p”, BoolSort())
  • i = Const(“i”, IntSort())
  • x = Const(“x”, RealSort())
  • Const(name, sort)

Declare function/predicate (always total !)

  • q = Function(“q”, IntSort(), BoolSort())
  • f = Function(“f”, IntSort(), IntSort())
  • Function(name, *signature)

​

​

Declare constructed type

  • color = EnumSort(“color”, [“red”, “blue”])
  • EnumSort(name, objects)
  • Color = Datatype('Color')
  • Color.declare('rgb', , ('red', IntSort()), ('blue', IntSort()), (‘green’, IntSort()))

Not used:

  • bitVector, Array

​

4 of 10

How to create Z3 expressions

Arithmetic, Equality, Comparisons

  • i == 0
  • 0 < x + y

Function application

  • q(1)
  • f(x,y)

Logic connectives

  • And(p, x<0)
  • Or, Not, Implies
  • equivalence : p == (x<0)

If-then-else expression:

  • if(p, x, y)
  • if(cond, expr_if_true, expr_if_false)
  • (Used in translation of structure)

Quantifiers

  • x=Freshconst(IntSort())
  • ForAll([x], Implies(x<0, x<1))
  • Exists([c], color_of_box(c))
  • FreshConst(sort)
  • ForAll(variables, body)
  • Exists(variables, body)

5 of 10

How to transform a Z3 expression

Built-in transformation

  • substitute(x+1, [(x, y+1)]) → y+1+1
  • substitute(expr, substitutions)
  • simplify(expr)

Inspection

  • expr.sort().name(): ‘Bool’, ‘Int’, ...
  • expr.decl().name(): top predicate, operator
  • expr.children(): children
  • is_true(e), is_bool(e), is_and(e), is_app(e), ..

Convert to CNF

  • print(describe_tactics()) // documentation
  • g = Goal()
  • g.add(Expr)
  • toCNF = Tactic(‘tseitin-cnf’)
  • print(toCNF(g))

​

6 of 10

How to perform inference

Model generation (All-SAT)

  • s=Solver()
  • s.add(expr)
  • while s.check()==sat:
    • m=s.model()
    • e=m.eval(expr2)
    • exclude_model = ...
    • s.add(exclude_model)

​

​

Model expansion

  • idem

Model Optimisation

  • s=Solver()
  • s.add(expr)
  • s.minimize(score_expr)
  • If s.check()=sat:
    • m=s.model()
    • ...

7 of 10

How to perform inference (2)

Propagation

  • s = Solver()
  • s.add(expr)
  • for atom in candidates:
    • result, consq = s.consequences([], [atom])
    • if result == sat:
      • # analyse the different possibilities:
      • # consq == [] if not a consq
      • # consq == [True => atom] if consq
      • # consq == [True => not(atom)]
      • # can also be used for numeric var

​

Explanation from user choices

  • s = Solver()
  • s.add(expr)
  • res, consq = s.consequences(assumptions, [toExplain])
  • # analyse the different possibilities:
  • # consq == [True ⇒ toExplain]
  • # consq == [assumption ⇒ toExplain]
  • # consq == [And(some_ass) ⇒ toExplain]

8 of 10

How to perform inference (3)

Explanation (rules)

  • s = Solver(); ps=[ ]
  • for r in rules:
    • p = Const(“p” + str(i), BoolSort())
    • ps.append(p)
    • s.add(p ⇒ r)
    • // or use assert_and_track(r, p)
  • s.check(ps)
  • For r in s.unsat_core():
    • print(r)

​

9 of 10

How to perform inference (4)

TODO:

  • relevance
  • propagate uncertainty
  • compare, …
  • recursive definitions

​

10 of 10

Limitations

  • Does not work well with non-linear equations (e.g. Surface)
    • No support for transcendental functions
  • Optimisation with quantified constraints is partially supported