Microsoft Research Community

The native text format provides for a low-level way of interfacing with Z3.

You should use this format when using Z3 over a text pipe from a tool
that provides an abstract syntax tree that you can traverse and serialize.

You must provide all the patterns that are going to be used by Z3 when using
the native text format. In particular, a quantifier takes a list of alternative patterns,

each pattern is a list of terms. If there is more than one term in a pattern, then it
is called a multi-pattern.

In the example below, we use the managed API to build a quantifier.
We log when asserting the quantifier, and show the resulting log,

which is in the native text format.

> type patterns.fs

open Microsoft.Z3

open System.Collections.Generic

open System

let par = new Config()

do  par.SetParamValue("MODEL", "true")

do  par.SetParamValue("TYPE_CHECK", "true")

let z3 = new Context(par)

let intT = z3.MkIntType()

let A1 = z3.MkArrayType(intT, intT)

let (|||) x y = z3.MkOr(x,y)

let (===) x y = z3.MkEq(x,y)

let i = z3.MkBound(0ul, intT)

let j = z3.MkBound(1ul, intT)

let a = z3.MkBound(2ul, A1)

let v = z3.MkBound(3ul, intT)

let read a i = z3.MkArraySelect(a,i)

let write a i v = z3.MkArrayStore(a,i,v)

let types = Array.map z3.GetType [| v; a; j; i |]

let names = Array.map (fun (s:string) -> z3.MkSymbol(s)) [| "v"; "a"; "j"; "i" |]

let pat1 = z3.MkPattern [| (read (write a i v) j) |]

let pat2 = z3.MkPattern [| (write a i v); (read a j) |]

let patterns = [| pat1; pat2 |]

let body = (i === j) ||| ((read (write a i v) j) === (read a j))

let q = z3.MkForall(0ul, patterns, types, names, body)

do Console.WriteLine("{0}", z3.ToString(q))

do ignore(z3.Log("array.z3"))

do z3.AssertCnstr(q)

do z3.CloseLog()

> patterns.exe

(forall (v int) (a (array int int)) (j int) (i int)  { ((select (store a i v) j))  ((store a i v) (select a j))  } (or (= i j) (= (select (store a i v) j) (select a j))))

> type array.z3

Ty $13 int BUILTIN arith 1

Ty $169 array BUILTIN array 0 $13 $13

Var $171 1 $13

Var $172 2 $169

App $179 select $172 $171

Var $173 3 $13

Var $170 0 $13

App $175 store $172 $170 $173

Pat $180 $175 $179

App $177 select $175 $171

Pat $178 $177

Ty $1 bool BUILTIN basic 0 Size 2

App $183 = $177 $179

App $182 = $170 $171

App $184 or $182 $183
Qua $185 FORALL 1 "null" "null" 4 v $13 a $169 j $13 i $13 2 $178 $180 $184
Assert $185