F* Challenge or The Tale of Tails

F* is a verification-oriented programming language developed at Microsoft Research. If you already know F#, or OCaml, or Haskell, or another language from ML family, you’ll find it familiar.

[Originally posted here].

###Resources:

To start experimenting with the language on your machine you need .NET 4.0. With Windows that’s it – just start enjoying verifications. But things are getting more interesting if you’re a mono user, when you want to compile the “right” compiler with blackjack and everything.

F* Download includes the sources and some binaries to bootstrap the compiler.
There is a dependency on Z3, we need F# PowerPack libs, fslex, fsyacc and i386 version of dylib for Mac and mono version of Microsoft.Z3.dll library (either compile a new one or download here or here).

But first of all, need to admit it works only for the small programs now. That’s why I ain’t gonna list the steps now. They are actually quite straightforward – update the paths 1 and fix the errors if any (e.g. I replaced the reserved word const with cnst). You can also define MONO symbol and add references to z3mono.dll.

The first wall is Certify.dll rule – got StackOverflow here. Given the .dll which is in bin folder by default, everything else compiles, including fstar.exe.

At this point only the simplest programs can be successfully verified. Why only them?

F* relies on tail call optimizations – lots and lots of recursive functions here. Consider the following simple function, it does nothing usefull but illustrates the problem:

 1: 
 2: 
 3: 
 4: 
 5: 
 6: 
let rec f x cont =                                                       
    if x < 0 then 0
    elif x = 0 then cont x
    else f (x-1) (fun x -> f x cont)

f 250000 id //SO

We can verify that the .tail instructions are where expected:

 1: 
 2: 
 3: 
 4: 
 5: 
 6:   

 7: 
 8: 
 9: 
10: 
11: 
12: 
13: 
14: 
15: 
16: 
17: 
18: 
19: 
20: 
21: 
22: 
23: 
24: 
25: 
26: 
27:   

28: 
29: 
30: 
31: 
32: 
33: 
34:   

35: 
36: 
37: 
38: 
39: 
.method public static 
  int32 f (int32 x,
	 class [FSharp.Core]Microsoft.FSharp.Core.FSharpFunc`2<int32, int32> cont
	 ) cil managed	
{	
 .custom instance void [FSharp.Core]Microsoft.FSharp.Core
	.CompilationArgumentCountsAttribute::.ctor(int32[]) = (
		01 00 02 00 00 00 01 00 00 00 01 00 00 00 00 00
	)
	// Method begins at RVA 0x2050
	// Code size 35 (0x23)
	.maxstack 8
	// loop start
	 IL_0000: nop
	 IL_0001: ldarg.0
	 IL_0002: ldc.i4.0
	 IL_0003: bge.s IL_0007
  
	 IL_0005: ldc.i4.0
	 IL_0006: ret
  
	 IL_0007: ldarg.0
	 IL_0008: brtrue.s IL_0014
  
	 IL_000a: ldarg.1
	 IL_000b: ldarg.0
	 IL_000c: tail.  // cont x
	 IL_000e: callvirt instance !1 class 
           [FSharp.Core]Microsoft.FSharp.Core.FSharpFunc`2<int32, int32>::Invoke(!0)
	 IL_0013: ret
  
	 IL_0014: ldarg.0
	 IL_0015: ldc.i4.1
	 IL_0016: sub
	 IL_0017: ldarg.1
	 IL_0018: newobj instance void Tailcalls/f@4::.ctor(
           class [FSharp.Core]Microsoft.FSharp.Core.FSharpFunc`2<int32, int32>) 
	 IL_001d: starg.s cont
	 IL_001f: starg.s x
	 IL_0021: br.s IL_0000
	 // end loop
}  // end of method Tailcalls::f
 1: 
 2: 
 3: 
 4: 
 5: 
 6: 
 7: 
 8: 
 9: 
10: 
11:   

12: 
13:   

14: 
15: 
.method public strict virtual 
instance int32 Invoke (int32 x) cil managed 
{
	// Method begins at RVA 0x2084
	// Code size 16 (0x10)
	.maxstack 8

	IL_0000: nop
	IL_0001: ldarg.1
	IL_0002: ldarg.0
	IL_0003: ldfld class 
          [FSharp.Core]Microsoft.FSharp.Core.FSharpFunc`2<int32, int32> Tailcalls/f@4::cont
	IL_0008: tail.  // f x cont
	IL_000a: call int32 Tailcalls::f(int32, 
          class [FSharp.Core]Microsoft.FSharp.Core.FSharpFunc`2<int32, int32>)
	IL_000f: ret
}  // end of method f@4::Invoke

Does it work? Well, for .NET the answer is yes. But on mono the continuation part makes the stack grow. Manipulations with stack size are not the solution, so the sources modification seems to be a way to go.

There’s an old issue with tail calls when called and caller functions have different number of parameters. I thought that can be the case, because of FSharpFunc Invoke/InvokeFast methods, and created a special type for arguments, so all functions had a single parameter. It isn’t.

I still believe it is possible to get F* working on mono 2. Hope to find some spare time to dig into the logic and check how it can be rewritten with a simpler recursion, just extremely busy right now ). I also shared some ideas with Nikhil Swamy from F* team – he experimented with mono builds too and definitely knows much better what can be done. That’s an interesting challenge and, of course, the fresh ideas are very welcome!

 

val f : int -> (int -> int) -> int

Full name: Test.f

val x : int

type: int
implements: System.IComparable
implements: System.IFormattable
implements: System.IConvertible
implements: System.IComparable<int>
implements: System.IEquatable<int>
inherits: System.ValueType

val cont : (int -> int)

val id : 'T -> 'T

Full name: Microsoft.FSharp.Core.Operators.id

  1. it’s better to include the full paths – for example I usually happily forget that fsc on my machine means Fast Scala Compiler and waste the time trying to get why it rejects .fs files.

  2. everything comes to electricity at the end, right? ;)

Z3 Mono Starter

Have you ever thought how exciting verification tools are? How do you prove the correctness of a program? Of course, the green tests bring some confidence… but we all know it’s not a proof.

[Originally posted here].

Pex Logo

Just look at Pex, it definitely can’t leave anybody cold (recommendation: skip this step for now, it was a trap).

But this story is not about Pex, but what powers it - Z3, an efficient SMT solver from Microsoft Research. You may ask why you should care (at least I always  do when looking at something new - a tool/language/app/whatever), the answer is simple - because we want the proof, not only a bunch of valid inputs. The work made me a bit paranoid to this point - it takes more time, but the shining correctness allows you not to worry about how much customers can lose just because someone forgot about a not-likely-to-happen workflow, like an unexpected negative number from nowhere -> power -> NaN (surprise, surprise!).

###Resources:

Z3 Logo

Z3 is supported on Windows, OSX, Linux and FreeBSD and has an extensive API:  C, C++, OCaml, .NET languages, Python, Java.

###Z3 + Mono The standard Z3 distrubution for OSX comes with x64 binaries, but to get it working with Mono we need to compile it ourselves with x86 architecture.

1. Download the sources here.
2. Open the folder and generate the makefiles.

 1: 
 2: 
python scripts/mk_make.py
cd build

3. We’re interested in config.mk file. By default the result architecture is x86_x64, that’s where the compiler flags help:

 1:   

 2: 
 3: 
CXXFLAGS= -D_MP_INTERNAL -m32  -c -fopenmp -mfpmath=sse -O3
 -D _EXTERNAL_RELEASE -fomit-frame-pointer -fPIC -msse -msse2
LINK_FLAGS=-m32
SLINK_FLAGS=-dynamiclib -m32

Update: according to the Yu’s comment you might need to replace the option -fopenmp with -D_NO_OMP_.

4. Just make it 1. The recent Z3 versions require a little change as compiler gives typename outside of template error, I just removed typename from fdd.h.

5. Check the architecture

 1: 
 2: 
$ lipo -info libz3.dylib
 Non-fat file: libz3.dylib is architecture: i386

6.  cd to z3/src/api/dotnet folder and compile Microsoft.Z3.csproj with Mono/.NET 4.0 as a target framework 2. Also you’d need to add a config file to map libz3.dll to our fresh native libz3.dylib.

 1: 
 2: 
 3: 
 4: 
<?xml version="1.0" encoding="utf-8">
<configuration>
    <dllmap dll="libz3.dll" target="libz3.dylib" os="osx" cpu="x86"/>
</configuration>

Now we are ready to try it!

###Examples time
Let’s start with a simple script using official Z3 API, the C# version of examples below can be found in Z3 repository. There’s also a nice set of F# examples - I couldn’t leave it just in comments - Z3Fs, a DSL to solve SMT problems by  @dungpa.

For simplicity we assume that Microsoft.Z3.dll, config and libz3.dylib are in the script’s folder.

Prove that x = y implies g(x) = g(y).

 1: 
 2: 
 3: 
 4: 
 5: 
 6: 
 7: 
 8: 
 9: 
10: 
11: 
12: 
13: 
14: 
15: 
16: 
17: 
18: 
19: 
20: 
21: 
22: 
23: 
24: 
25: 
26: 
27: 
28: 
29: 
30: 
31: 
32: 
33: 
34: 
35: 
36: 
#r "Microsoft.Z3.dll"  
  
usings  
  
let prove (ctx: Context) f =  
    let s = ctx.MkSolver()  
    s.Assert (ctx.MkNot f)  
    match s.Check() with  
    | Status.UNKNOWN -> printfn "unknown because %A" s.ReasonUnknown  
    | Status.SATISFIABLE -> printfn "error"  
    | _ -> printfn "ok, proof: %A" s.Proof  
    
///Prove that x = y implies g(x) = g(y)
let proveSample() =  
    create context

    //create uninterpreted type
    let U = ctx.MkUninterpretedSort (ctx.MkSymbol "U")
    //declare function g
    let g = ctx.MkFuncDecl("g", U, U)

    //create x and y
    let x = ctx.MkConst("x", U)
    let y = ctx.MkConst("y", U)
   //create g(x), g(y)
    let gx, gy = g.[x], g.[y]

    //assert x = y
    let eq = ctx.MkEq(x, y)

    //prove g(x) = g(y)
    let f = ctx.MkEq(gx, gy)
    printfn "prove: x = y implies g(x) = g(y)"
    prove ctx (ctx.MkImplies(eq, f))

proveSample()

Well, it’s a pain to write all those ctx.Mk*. That’s where F# quotations come to hand. Some papers and slides mention Z3 support for quotations, though they seem to be a bit outdated - haven’t seen anything similar in the sources. Here is an example of what it can look like.

Simplify expression “x + (y - (x + z))”

 1: 
 2: 
 3: 
 4: 
 5: 
 6: 
 7: 
 8: 
 9: 
10: 
11: 
12: 
13: 
14: 
15: 
16: 
17: 
18: 
19: 
20: 
21: 
22: 
///SimplifiedSpecificCall
let inline (|Func|_|) expr = (...)

///From quotations to Z3 objects
let z3 expr =
    create context
    let rec unquote expr =
        match expr with
        | Func <@@ (+) @@> [x; y] -> ctx.MkAdd (unquote x, unquote y)
        | Func <@@ (-) @@> [x; y] -> ctx.MkSub (unquote x, unquote y)
        | Lambdas (_, e) -> unquote e
        | Var var -> ctx.MkIntConst var.Name :> ArithExpr
        | x -> failwith (sprintf "unknown expression %A" x)
    unquote expr

///Simplify expression "x + (y - (x + z))"
let simplifier() =
    let t1 = z3 <@@ fun x y z -> x + (y - (x + z)) @@>  
    let t2 = t1.Simplify()
    printfn "%A -> %A" t1 t2

simplifier()

Looks much better, doesn’t it?

Next time: bringing another f-language to mono…

open System
open Microsoft.Z3
open Microsoft.FSharp.Quotations
open DerivedPatterns
open Patterns

val prove : Context -> BoolExpr -> unit

Full name: GoZ3.prove

val ctx : Context

type: Context
implements: IDisposable

type Context =
class
new : unit -> Microsoft.Z3.Context
new : System.Collections.Generic.Dictionary<string,string> -> Microsoft.Z3.Context
member And : Microsoft.Z3.Probe * Microsoft.Z3.Probe -> Microsoft.Z3.Probe
member AndThen : Microsoft.Z3.Tactic * Microsoft.Z3.Tactic * Microsoft.Z3.Tactic [] -> Microsoft.Z3.Tactic
member BenchmarkToSMTString : string * string * string * string * Microsoft.Z3.BoolExpr [] * Microsoft.Z3.BoolExpr -> string
member BoolSort : Microsoft.Z3.BoolSort
member Cond : Microsoft.Z3.Probe * Microsoft.Z3.Tactic * Microsoft.Z3.Tactic -> Microsoft.Z3.Tactic
member ConstProbe : float -> Microsoft.Z3.Probe
member Dispose : unit -> unit
member Eq : Microsoft.Z3.Probe * Microsoft.Z3.Probe -> Microsoft.Z3.Probe
member Fail : unit -> Microsoft.Z3.Tactic
member FailIf : Microsoft.Z3.Probe -> Microsoft.Z3.Tactic
member FailIfNotDecided : unit -> Microsoft.Z3.Tactic
member Ge : Microsoft.Z3.Probe * Microsoft.Z3.Probe -> Microsoft.Z3.Probe
member GetParamValue : string -> string
member Gt : Microsoft.Z3.Probe * Microsoft.Z3.Probe -> Microsoft.Z3.Probe
member IntSort : Microsoft.Z3.IntSort
member Interrupt : unit -> unit
member Le : Microsoft.Z3.Probe * Microsoft.Z3.Probe -> Microsoft.Z3.Probe
member Lt : Microsoft.Z3.Probe * Microsoft.Z3.Probe -> Microsoft.Z3.Probe
member MkAdd : Microsoft.Z3.ArithExpr [] -> Microsoft.Z3.ArithExpr
member MkAnd : Microsoft.Z3.BoolExpr [] -> Microsoft.Z3.BoolExpr
member MkApp : Microsoft.Z3.FuncDecl * Microsoft.Z3.Expr [] -> Microsoft.Z3.Expr
member MkArrayConst : Microsoft.Z3.Symbol * Microsoft.Z3.Sort * Microsoft.Z3.Sort -> Microsoft.Z3.ArrayExpr
member MkArrayConst : string * Microsoft.Z3.Sort * Microsoft.Z3.Sort -> Microsoft.Z3.ArrayExpr
member MkArraySort : Microsoft.Z3.Sort * Microsoft.Z3.Sort -> Microsoft.Z3.ArraySort
member MkBV : string * uint32 -> Microsoft.Z3.BitVecNum
member MkBV : int * uint32 -> Microsoft.Z3.BitVecNum
member MkBV : uint32 * uint32 -> Microsoft.Z3.BitVecNum
member MkBV : int64 * uint32 -> Microsoft.Z3.BitVecNum
member MkBV : uint64 * uint32 -> Microsoft.Z3.BitVecNum
member MkBV2Int : Microsoft.Z3.BitVecExpr * bool -> Microsoft.Z3.IntExpr
member MkBVAND : Microsoft.Z3.BitVecExpr * Microsoft.Z3.BitVecExpr -> Microsoft.Z3.BitVecExpr
member MkBVASHR : Microsoft.Z3.BitVecExpr * Microsoft.Z3.BitVecExpr -> Microsoft.Z3.BitVecExpr
member MkBVAdd : Microsoft.Z3.BitVecExpr * Microsoft.Z3.BitVecExpr -> Microsoft.Z3.BitVecExpr
member MkBVAddNoOverflow : Microsoft.Z3.BitVecExpr * Microsoft.Z3.BitVecExpr * bool -> Microsoft.Z3.BoolExpr
member MkBVAddNoUnderflow : Microsoft.Z3.BitVecExpr * Microsoft.Z3.BitVecExpr -> Microsoft.Z3.BoolExpr
member MkBVConst : Microsoft.Z3.Symbol * uint32 -> Microsoft.Z3.BitVecExpr
member MkBVConst : string * uint32 -> Microsoft.Z3.BitVecExpr
member MkBVLSHR : Microsoft.Z3.BitVecExpr * Microsoft.Z3.BitVecExpr -> Microsoft.Z3.BitVecExpr
member MkBVMul : Microsoft.Z3.BitVecExpr * Microsoft.Z3.BitVecExpr -> Microsoft.Z3.BitVecExpr
member MkBVMulNoOverflow : Microsoft.Z3.BitVecExpr * Microsoft.Z3.BitVecExpr * bool -> Microsoft.Z3.BoolExpr
member MkBVMulNoUnderflow : Microsoft.Z3.BitVecExpr * Microsoft.Z3.BitVecExpr -> Microsoft.Z3.BoolExpr
member MkBVNAND : Microsoft.Z3.BitVecExpr * Microsoft.Z3.BitVecExpr -> Microsoft.Z3.BitVecExpr
member MkBVNOR : Microsoft.Z3.BitVecExpr * Microsoft.Z3.BitVecExpr -> Microsoft.Z3.BitVecExpr
member MkBVNeg : Microsoft.Z3.BitVecExpr -> Microsoft.Z3.BitVecExpr
member MkBVNegNoOverflow : Microsoft.Z3.BitVecExpr -> Microsoft.Z3.BoolExpr
member MkBVNot : Microsoft.Z3.BitVecExpr -> Microsoft.Z3.BitVecExpr
member MkBVOR : Microsoft.Z3.BitVecExpr * Microsoft.Z3.BitVecExpr -> Microsoft.Z3.BitVecExpr
member MkBVRedAND : Microsoft.Z3.BitVecExpr -> Microsoft.Z3.BitVecExpr
member MkBVRedOR : Microsoft.Z3.BitVecExpr -> Microsoft.Z3.BitVecExpr
member MkBVRotateLeft : uint32 * Microsoft.Z3.BitVecExpr -> Microsoft.Z3.BitVecExpr
member MkBVRotateLeft : Microsoft.Z3.BitVecExpr * Microsoft.Z3.BitVecExpr -> Microsoft.Z3.BitVecExpr
member MkBVRotateRight : uint32 * Microsoft.Z3.BitVecExpr -> Microsoft.Z3.BitVecExpr
member MkBVRotateRight : Microsoft.Z3.BitVecExpr * Microsoft.Z3.BitVecExpr -> Microsoft.Z3.BitVecExpr
member MkBVSDiv : Microsoft.Z3.BitVecExpr * Microsoft.Z3.BitVecExpr -> Microsoft.Z3.BitVecExpr
member MkBVSDivNoOverflow : Microsoft.Z3.BitVecExpr * Microsoft.Z3.BitVecExpr -> Microsoft.Z3.BoolExpr
member MkBVSGE : Microsoft.Z3.BitVecExpr * Microsoft.Z3.BitVecExpr -> Microsoft.Z3.BoolExpr
member MkBVSGT : Microsoft.Z3.BitVecExpr * Microsoft.Z3.BitVecExpr -> Microsoft.Z3.BoolExpr
member MkBVSHL : Microsoft.Z3.BitVecExpr * Microsoft.Z3.BitVecExpr -> Microsoft.Z3.BitVecExpr
member MkBVSLE : Microsoft.Z3.BitVecExpr * Microsoft.Z3.BitVecExpr -> Microsoft.Z3.BoolExpr
member MkBVSLT : Microsoft.Z3.BitVecExpr * Microsoft.Z3.BitVecExpr -> Microsoft.Z3.BoolExpr
member MkBVSMod : Microsoft.Z3.BitVecExpr * Microsoft.Z3.BitVecExpr -> Microsoft.Z3.BitVecExpr
member MkBVSRem : Microsoft.Z3.BitVecExpr * Microsoft.Z3.BitVecExpr -> Microsoft.Z3.BitVecExpr
member MkBVSub : Microsoft.Z3.BitVecExpr * Microsoft.Z3.BitVecExpr -> Microsoft.Z3.BitVecExpr
member MkBVSubNoOverflow : Microsoft.Z3.BitVecExpr * Microsoft.Z3.BitVecExpr -> Microsoft.Z3.BoolExpr
member MkBVSubNoUnderflow : Microsoft.Z3.BitVecExpr * Microsoft.Z3.BitVecExpr * bool -> Microsoft.Z3.BoolExpr
member MkBVUDiv : Microsoft.Z3.BitVecExpr * Microsoft.Z3.BitVecExpr -> Microsoft.Z3.BitVecExpr
member MkBVUGE : Microsoft.Z3.BitVecExpr * Microsoft.Z3.BitVecExpr -> Microsoft.Z3.BoolExpr
member MkBVUGT : Microsoft.Z3.BitVecExpr * Microsoft.Z3.BitVecExpr -> Microsoft.Z3.BoolExpr
member MkBVULE : Microsoft.Z3.BitVecExpr * Microsoft.Z3.BitVecExpr -> Microsoft.Z3.BoolExpr
member MkBVULT : Microsoft.Z3.BitVecExpr * Microsoft.Z3.BitVecExpr -> Microsoft.Z3.BoolExpr
member MkBVURem : Microsoft.Z3.BitVecExpr * Microsoft.Z3.BitVecExpr -> Microsoft.Z3.BitVecExpr
member MkBVXNOR : Microsoft.Z3.BitVecExpr * Microsoft.Z3.BitVecExpr -> Microsoft.Z3.BitVecExpr
member MkBVXOR : Microsoft.Z3.BitVecExpr * Microsoft.Z3.BitVecExpr -> Microsoft.Z3.BitVecExpr
member MkBitVecSort : uint32 -> Microsoft.Z3.BitVecSort
member MkBool : bool -> Microsoft.Z3.BoolExpr
member MkBoolConst : Microsoft.Z3.Symbol -> Microsoft.Z3.BoolExpr
member MkBoolConst : string -> Microsoft.Z3.BoolExpr
member MkBoolSort : unit -> Microsoft.Z3.BoolSort
member MkBound : uint32 * Microsoft.Z3.Sort -> Microsoft.Z3.Expr
member MkConcat : Microsoft.Z3.BitVecExpr * Microsoft.Z3.BitVecExpr -> Microsoft.Z3.BitVecExpr
member MkConst : Microsoft.Z3.FuncDecl -> Microsoft.Z3.Expr
member MkConst : Microsoft.Z3.Symbol * Microsoft.Z3.Sort -> Microsoft.Z3.Expr
member MkConst : string * Microsoft.Z3.Sort -> Microsoft.Z3.Expr
member MkConstArray : Microsoft.Z3.Sort * Microsoft.Z3.Expr -> Microsoft.Z3.ArrayExpr
member MkConstDecl : Microsoft.Z3.Symbol * Microsoft.Z3.Sort -> Microsoft.Z3.FuncDecl
member MkConstDecl : string * Microsoft.Z3.Sort -> Microsoft.Z3.FuncDecl
member MkConstructor : Microsoft.Z3.Symbol * Microsoft.Z3.Symbol * Microsoft.Z3.Symbol [] * Microsoft.Z3.Sort [] * uint32 [] -> Microsoft.Z3.Constructor
member MkConstructor : string * string * string [] * Microsoft.Z3.Sort [] * uint32 [] -> Microsoft.Z3.Constructor
member MkDatatypeSort : Microsoft.Z3.Symbol * Microsoft.Z3.Constructor [] -> Microsoft.Z3.DatatypeSort
member MkDatatypeSort : string * Microsoft.Z3.Constructor [] -> Microsoft.Z3.DatatypeSort
member MkDatatypeSorts : Microsoft.Z3.Symbol [] * Microsoft.Z3.Constructor [] [] -> Microsoft.Z3.DatatypeSort []
member MkDatatypeSorts : string [] * Microsoft.Z3.Constructor [] [] -> Microsoft.Z3.DatatypeSort []
member MkDistinct : Microsoft.Z3.Expr [] -> Microsoft.Z3.BoolExpr
member MkDiv : Microsoft.Z3.ArithExpr * Microsoft.Z3.ArithExpr -> Microsoft.Z3.ArithExpr
member MkEmptySet : Microsoft.Z3.Sort -> Microsoft.Z3.Expr
member MkEnumSort : Microsoft.Z3.Symbol * Microsoft.Z3.Symbol [] -> Microsoft.Z3.EnumSort
member MkEnumSort : string * string [] -> Microsoft.Z3.EnumSort
member MkEq : Microsoft.Z3.Expr * Microsoft.Z3.Expr -> Microsoft.Z3.BoolExpr
member MkExists : Microsoft.Z3.Expr [] * Microsoft.Z3.Expr * uint32 * Microsoft.Z3.Pattern [] * Microsoft.Z3.Expr [] * Microsoft.Z3.Symbol * Microsoft.Z3.Symbol -> Microsoft.Z3.Quantifier
member MkExists : Microsoft.Z3.Sort [] * Microsoft.Z3.Symbol [] * Microsoft.Z3.Expr * uint32 * Microsoft.Z3.Pattern [] * Microsoft.Z3.Expr [] * Microsoft.Z3.Symbol * Microsoft.Z3.Symbol -> Microsoft.Z3.Quantifier
member MkExtract : uint32 * uint32 * Microsoft.Z3.BitVecExpr -> Microsoft.Z3.BitVecExpr
member MkFalse : unit -> Microsoft.Z3.BoolExpr
member MkFiniteDomainSort : Microsoft.Z3.Symbol * uint64 -> Microsoft.Z3.FiniteDomainSort
member MkFiniteDomainSort : string * uint64 -> Microsoft.Z3.FiniteDomainSort
member MkFixedpoint : unit -> Microsoft.Z3.Fixedpoint
member MkForall : Microsoft.Z3.Expr [] * Microsoft.Z3.Expr * uint32 * Microsoft.Z3.Pattern [] * Microsoft.Z3.Expr [] * Microsoft.Z3.Symbol * Microsoft.Z3.Symbol -> Microsoft.Z3.Quantifier
member MkForall : Microsoft.Z3.Sort [] * Microsoft.Z3.Symbol [] * Microsoft.Z3.Expr * uint32 * Microsoft.Z3.Pattern [] * Microsoft.Z3.Expr [] * Microsoft.Z3.Symbol * Microsoft.Z3.Symbol -> Microsoft.Z3.Quantifier
member MkFreshConst : string * Microsoft.Z3.Sort -> Microsoft.Z3.Expr
member MkFreshConstDecl : string * Microsoft.Z3.Sort -> Microsoft.Z3.FuncDecl
member MkFreshFuncDecl : string * Microsoft.Z3.Sort [] * Microsoft.Z3.Sort -> Microsoft.Z3.FuncDecl
member MkFullSet : Microsoft.Z3.Sort -> Microsoft.Z3.Expr
member MkFuncDecl : Microsoft.Z3.Symbol * Microsoft.Z3.Sort [] * Microsoft.Z3.Sort -> Microsoft.Z3.FuncDecl
member MkFuncDecl : Microsoft.Z3.Symbol * Microsoft.Z3.Sort * Microsoft.Z3.Sort -> Microsoft.Z3.FuncDecl
member MkFuncDecl : string * Microsoft.Z3.Sort [] * Microsoft.Z3.Sort -> Microsoft.Z3.FuncDecl
member MkFuncDecl : string * Microsoft.Z3.Sort * Microsoft.Z3.Sort -> Microsoft.Z3.FuncDecl
member MkGe : Microsoft.Z3.ArithExpr * Microsoft.Z3.ArithExpr -> Microsoft.Z3.BoolExpr
member MkGoal : bool * bool * bool -> Microsoft.Z3.Goal
member MkGt : Microsoft.Z3.ArithExpr * Microsoft.Z3.ArithExpr -> Microsoft.Z3.BoolExpr
member MkITE : Microsoft.Z3.BoolExpr * Microsoft.Z3.Expr * Microsoft.Z3.Expr -> Microsoft.Z3.Expr
member MkIff : Microsoft.Z3.BoolExpr * Microsoft.Z3.BoolExpr -> Microsoft.Z3.BoolExpr
member MkImplies : Microsoft.Z3.BoolExpr * Microsoft.Z3.BoolExpr -> Microsoft.Z3.BoolExpr
member MkInt : string -> Microsoft.Z3.IntNum
member MkInt : int -> Microsoft.Z3.IntNum
member MkInt : uint32 -> Microsoft.Z3.IntNum
member MkInt : int64 -> Microsoft.Z3.IntNum
member MkInt : uint64 -> Microsoft.Z3.IntNum
member MkInt2BV : uint32 * Microsoft.Z3.IntExpr -> Microsoft.Z3.BitVecExpr
member MkInt2Real : Microsoft.Z3.IntExpr -> Microsoft.Z3.RealExpr
member MkIntConst : Microsoft.Z3.Symbol -> Microsoft.Z3.IntExpr
member MkIntConst : string -> Microsoft.Z3.IntExpr
member MkIntSort : unit -> Microsoft.Z3.IntSort
member MkIsInteger : Microsoft.Z3.RealExpr -> Microsoft.Z3.BoolExpr
member MkLe : Microsoft.Z3.ArithExpr * Microsoft.Z3.ArithExpr -> Microsoft.Z3.BoolExpr
member MkListSort : Microsoft.Z3.Symbol * Microsoft.Z3.Sort -> Microsoft.Z3.ListSort
member MkListSort : string * Microsoft.Z3.Sort -> Microsoft.Z3.ListSort
member MkLt : Microsoft.Z3.ArithExpr * Microsoft.Z3.ArithExpr -> Microsoft.Z3.BoolExpr
member MkMap : Microsoft.Z3.FuncDecl * Microsoft.Z3.ArrayExpr [] -> Microsoft.Z3.ArrayExpr
member MkMod : Microsoft.Z3.IntExpr * Microsoft.Z3.IntExpr -> Microsoft.Z3.IntExpr
member MkMul : Microsoft.Z3.ArithExpr [] -> Microsoft.Z3.ArithExpr
member MkNot : Microsoft.Z3.BoolExpr -> Microsoft.Z3.BoolExpr
member MkNumeral : string * Microsoft.Z3.Sort -> Microsoft.Z3.Expr
member MkNumeral : int * Microsoft.Z3.Sort -> Microsoft.Z3.Expr
member MkNumeral : uint32 * Microsoft.Z3.Sort -> Microsoft.Z3.Expr
member MkNumeral : int64 * Microsoft.Z3.Sort -> Microsoft.Z3.Expr
member MkNumeral : uint64 * Microsoft.Z3.Sort -> Microsoft.Z3.Expr
member MkOr : Microsoft.Z3.BoolExpr [] -> Microsoft.Z3.BoolExpr
member MkParams : unit -> Microsoft.Z3.Params
member MkPattern : Microsoft.Z3.Expr [] -> Microsoft.Z3.Pattern
member MkPower : Microsoft.Z3.ArithExpr * Microsoft.Z3.ArithExpr -> Microsoft.Z3.ArithExpr
member MkProbe : string -> Microsoft.Z3.Probe
member MkQuantifier : bool * Microsoft.Z3.Expr [] * Microsoft.Z3.Expr * uint32 * Microsoft.Z3.Pattern [] * Microsoft.Z3.Expr [] * Microsoft.Z3.Symbol * Microsoft.Z3.Symbol -> Microsoft.Z3.Quantifier
member MkQuantifier : bool * Microsoft.Z3.Sort [] * Microsoft.Z3.Symbol [] * Microsoft.Z3.Expr * uint32 * Microsoft.Z3.Pattern [] * Microsoft.Z3.Expr [] * Microsoft.Z3.Symbol * Microsoft.Z3.Symbol -> Microsoft.Z3.Quantifier
member MkReal : string -> Microsoft.Z3.RatNum
member MkReal : int -> Microsoft.Z3.RatNum
member MkReal : uint32 -> Microsoft.Z3.RatNum
member MkReal : int64 -> Microsoft.Z3.RatNum
member MkReal : uint64 -> Microsoft.Z3.RatNum
member MkReal : int * int -> Microsoft.Z3.RatNum
member MkReal2Int : Microsoft.Z3.RealExpr -> Microsoft.Z3.IntExpr
member MkRealConst : Microsoft.Z3.Symbol -> Microsoft.Z3.RealExpr
member MkRealConst : string -> Microsoft.Z3.RealExpr
member MkRealSort : unit -> Microsoft.Z3.RealSort
member MkRem : Microsoft.Z3.IntExpr * Microsoft.Z3.IntExpr -> Microsoft.Z3.IntExpr
member MkRepeat : uint32 * Microsoft.Z3.BitVecExpr -> Microsoft.Z3.BitVecExpr
member MkSelect : Microsoft.Z3.ArrayExpr * Microsoft.Z3.Expr -> Microsoft.Z3.Expr
member MkSetAdd : Microsoft.Z3.Expr * Microsoft.Z3.Expr -> Microsoft.Z3.Expr
member MkSetComplement : Microsoft.Z3.Expr -> Microsoft.Z3.Expr
member MkSetDel : Microsoft.Z3.Expr * Microsoft.Z3.Expr -> Microsoft.Z3.Expr
member MkSetDifference : Microsoft.Z3.Expr * Microsoft.Z3.Expr -> Microsoft.Z3.Expr
member MkSetIntersection : Microsoft.Z3.Expr [] -> Microsoft.Z3.Expr
member MkSetMembership : Microsoft.Z3.Expr * Microsoft.Z3.Expr -> Microsoft.Z3.Expr
member MkSetSort : Microsoft.Z3.Sort -> Microsoft.Z3.SetSort
member MkSetSubset : Microsoft.Z3.Expr * Microsoft.Z3.Expr -> Microsoft.Z3.Expr
member MkSetUnion : Microsoft.Z3.Expr [] -> Microsoft.Z3.Expr
member MkSignExt : uint32 * Microsoft.Z3.BitVecExpr -> Microsoft.Z3.BitVecExpr
member MkSimpleSolver : unit -> Microsoft.Z3.Solver
member MkSolver : Microsoft.Z3.Symbol -> Microsoft.Z3.Solver
member MkSolver : string -> Microsoft.Z3.Solver
member MkSolver : Microsoft.Z3.Tactic -> Microsoft.Z3.Solver
member MkStore : Microsoft.Z3.ArrayExpr * Microsoft.Z3.Expr * Microsoft.Z3.Expr -> Microsoft.Z3.ArrayExpr
member MkSub : Microsoft.Z3.ArithExpr [] -> Microsoft.Z3.ArithExpr
member MkSymbol : int -> Microsoft.Z3.IntSymbol
member MkSymbol : string -> Microsoft.Z3.StringSymbol
member MkTactic : string -> Microsoft.Z3.Tactic
member MkTermArray : Microsoft.Z3.ArrayExpr -> Microsoft.Z3.Expr
member MkTrue : unit -> Microsoft.Z3.BoolExpr
member MkTupleSort : Microsoft.Z3.Symbol * Microsoft.Z3.Symbol [] * Microsoft.Z3.Sort [] -> Microsoft.Z3.TupleSort
member MkUnaryMinus : Microsoft.Z3.ArithExpr -> Microsoft.Z3.ArithExpr
member MkUninterpretedSort : Microsoft.Z3.Symbol -> Microsoft.Z3.UninterpretedSort
member MkUninterpretedSort : string -> Microsoft.Z3.UninterpretedSort
member MkXor : Microsoft.Z3.BoolExpr * Microsoft.Z3.BoolExpr -> Microsoft.Z3.BoolExpr
member MkZeroExt : uint32 * Microsoft.Z3.BitVecExpr -> Microsoft.Z3.BitVecExpr
member Not : Microsoft.Z3.Probe -> Microsoft.Z3.Probe
member NumProbes : uint32
member NumSMTLIBAssumptions : uint32
member NumSMTLIBDecls : uint32
member NumSMTLIBFormulas : uint32
member NumSMTLIBSorts : uint32
member NumTactics : uint32
member Or : Microsoft.Z3.Probe * Microsoft.Z3.Probe -> Microsoft.Z3.Probe
member OrElse : Microsoft.Z3.Tactic * Microsoft.Z3.Tactic -> Microsoft.Z3.Tactic
member ParAndThen : Microsoft.Z3.Tactic * Microsoft.Z3.Tactic -> Microsoft.Z3.Tactic
member ParOr : Microsoft.Z3.Tactic [] -> Microsoft.Z3.Tactic
member ParseSMTLIB2File : string * Microsoft.Z3.Symbol [] * Microsoft.Z3.Sort [] * Microsoft.Z3.Symbol [] * Microsoft.Z3.FuncDecl [] -> Microsoft.Z3.BoolExpr
member ParseSMTLIB2String : string * Microsoft.Z3.Symbol [] * Microsoft.Z3.Sort [] * Microsoft.Z3.Symbol [] * Microsoft.Z3.FuncDecl [] -> Microsoft.Z3.BoolExpr
member ParseSMTLIBFile : string * Microsoft.Z3.Symbol [] * Microsoft.Z3.Sort [] * Microsoft.Z3.Symbol [] * Microsoft.Z3.FuncDecl [] -> unit
member ParseSMTLIBString : string * Microsoft.Z3.Symbol [] * Microsoft.Z3.Sort [] * Microsoft.Z3.Symbol [] * Microsoft.Z3.FuncDecl [] -> unit
member PrintMode : -> Microsoft.Z3.Z3_ast_print_mode with deb set
member ProbeDescription : string -> string
member ProbeNames : string []
member RealSort : Microsoft.Z3.RealSort
member Repeat : Microsoft.Z3.Tactic * uint32 -> Microsoft.Z3.Tactic
member SMTLIBAssumptions : Microsoft.Z3.BoolExpr []
member SMTLIBDecls : Microsoft.Z3.FuncDecl []
member SMTLIBFormulas : Microsoft.Z3.BoolExpr []
member SMTLIBSorts : Microsoft.Z3.Sort []
member SimplifyHelp : unit -> string
member SimplifyParameterDescriptions : Microsoft.Z3.ParamDescrs
member Skip : unit -> Microsoft.Z3.Tactic
member TacticDescription : string -> string
member TacticNames : string []
member Then : Microsoft.Z3.Tactic * Microsoft.Z3.Tactic * Microsoft.Z3.Tactic [] -> Microsoft.Z3.Tactic
member TryFor : Microsoft.Z3.Tactic * uint32 -> Microsoft.Z3.Tactic
member UnwrapAST : Microsoft.Z3.AST -> System.IntPtr
member UpdateParamValue : string * string -> unit
member UsingParams : Microsoft.Z3.Tactic * Microsoft.Z3.Params -> Microsoft.Z3.Tactic
member When : Microsoft.Z3.Probe * Microsoft.Z3.Tactic -> Microsoft.Z3.Tactic
member With : Microsoft.Z3.Tactic * Microsoft.Z3.Params -> Microsoft.Z3.Tactic
member WrapAST : System.IntPtr -> Microsoft.Z3.AST
static member ToggleWarningMessages : bool -> unit
end

Full name: Microsoft.Z3.Context

type: Context
implements: IDisposable

val f : BoolExpr

type: BoolExpr
implements: IDisposable
implements: IComparable
inherits: Expr
inherits: AST
inherits: Z3Object

val s : Solver

type: Solver
implements: IDisposable
inherits: Z3Object

Multiple overloadsContext.MkSolver(t: Tactic) : Solver

Context.MkSolver(logic: string) : Solver

Context.MkSolver(logic: Symbol) : Solver

Solver.Assert(constraints: BoolExpr []) : unit
Context.MkNot(a: BoolExpr) : BoolExpr
Solver.Check(assumptions: Expr []) : Status

type Status =
| UNSATISFIABLE = -1
| UNKNOWN = 0
| SATISFIABLE = 1

Full name: Microsoft.Z3.Status

type: Status
inherits: Enum
inherits: ValueType

field Status.UNKNOWN = 0

val printfn : Printf.TextWriterFormat<'T> -> 'T

Full name: Microsoft.FSharp.Core.ExtraTopLevelOperators.printfn

property Solver.ReasonUnknown: string
field Status.SATISFIABLE = 1
property Solver.Proof: Expr

val proveSample : unit -> unit

Full name: GoZ3.proveSample

Prove that x = y implies g(x) = g(y)

let prms = System.Collections.Generic.Dictionary (dict [ "proof", "true" ])
let ctx = new Context(prms)

val U : UninterpretedSort

type: UninterpretedSort
implements: IDisposable
implements: IComparable
inherits: Sort
inherits: AST
inherits: Z3Object

Multiple overloadsContext.MkUninterpretedSort(str: string) : UninterpretedSort

Context.MkUninterpretedSort(s: Symbol) : UninterpretedSort

Multiple overloadsContext.MkSymbol(name: string) : StringSymbol

Context.MkSymbol(i: int) : IntSymbol

val g : FuncDecl

type: FuncDecl
implements: IDisposable
implements: IComparable
inherits: AST
inherits: Z3Object

Multiple overloadsContext.MkFuncDecl(name: string, domain: Sort, range: Sort) : FuncDecl

Context.MkFuncDecl(name: string, domain: Sort [], range: Sort) : FuncDecl

Context.MkFuncDecl(name: Symbol, domain: Sort, range: Sort) : FuncDecl

Context.MkFuncDecl(name: Symbol, domain: Sort [], range: Sort) : FuncDecl

val x : Expr

type: Expr
implements: IDisposable
implements: IComparable
inherits: AST
inherits: Z3Object

Multiple overloadsContext.MkConst(f: FuncDecl) : Expr

Context.MkConst(name: string, range: Sort) : Expr

Context.MkConst(name: Symbol, range: Sort) : Expr

val y : Expr

type: Expr
implements: IDisposable
implements: IComparable
inherits: AST
inherits: Z3Object

val gx : Expr

type: Expr
implements: IDisposable
implements: IComparable
inherits: AST
inherits: Z3Object

val gy : Expr

type: Expr
implements: IDisposable
implements: IComparable
inherits: AST
inherits: Z3Object

val eq : BoolExpr

type: BoolExpr
implements: IDisposable
implements: IComparable
inherits: Expr
inherits: AST
inherits: Z3Object

Context.MkEq(x: Expr, y: Expr) : BoolExpr
Context.MkImplies(t1: BoolExpr, t2: BoolExpr) : BoolExpr
Multiple itemstype Func<'T1,'T2,'T3,'T4,'T5,'T6,'T7,'T8,'T9,'T10,'T11,'T12,'T13,'T14,'T15,'T16,'TResult> =
delegate of 'T1 * 'T2 * 'T3 * 'T4 * 'T5 * 'T6 * 'T7 * 'T8 * 'T9 * 'T10 * 'T11 * 'T12 * 'T13 * 'T14 * 'T15 * 'T16 -> 'TResultFull name: System.Func<_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_>type: Func<'T1,'T2,'T3,'T4,'T5,'T6,'T7,'T8,'T9,'T10,'T11,'T12,'T13,'T14,'T15,'T16,'TResult>
implements: ICloneable
implements: Runtime.Serialization.ISerializable
inherits: MulticastDelegate
inherits: Delegate--------------------type Func<'T1,'T2,'T3,'T4,'T5,'T6,'T7,'T8,'T9,'T10,'T11,'T12,'T13,'T14,'T15,'TResult> =
delegate of 'T1 * 'T2 * 'T3 * 'T4 * 'T5 * 'T6 * 'T7 * 'T8 * 'T9 * 'T10 * 'T11 * 'T12 * 'T13 * 'T14 * 'T15 -> 'TResult

Full name: System.Func<_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_>

type: Func<'T1,'T2,'T3,'T4,'T5,'T6,'T7,'T8,'T9,'T10,'T11,'T12,'T13,'T14,'T15,'TResult>
implements: ICloneable
implements: Runtime.Serialization.ISerializable
inherits: MulticastDelegate
inherits: Delegate

--------------------

type Func<'T1,'T2,'T3,'T4,'T5,'T6,'T7,'T8,'T9,'T10,'T11,'T12,'T13,'T14,'TResult> =
delegate of 'T1 * 'T2 * 'T3 * 'T4 * 'T5 * 'T6 * 'T7 * 'T8 * 'T9 * 'T10 * 'T11 * 'T12 * 'T13 * 'T14 -> 'TResult

Full name: System.Func<_,_,_,_,_,_,_,_,_,_,_,_,_,_,_>

type: Func<'T1,'T2,'T3,'T4,'T5,'T6,'T7,'T8,'T9,'T10,'T11,'T12,'T13,'T14,'TResult>
implements: ICloneable
implements: Runtime.Serialization.ISerializable
inherits: MulticastDelegate
inherits: Delegate

--------------------

type Func<'T1,'T2,'T3,'T4,'T5,'T6,'T7,'T8,'T9,'T10,'T11,'T12,'T13,'TResult> =
delegate of 'T1 * 'T2 * 'T3 * 'T4 * 'T5 * 'T6 * 'T7 * 'T8 * 'T9 * 'T10 * 'T11 * 'T12 * 'T13 -> 'TResult

Full name: System.Func<_,_,_,_,_,_,_,_,_,_,_,_,_,_>

type: Func<'T1,'T2,'T3,'T4,'T5,'T6,'T7,'T8,'T9,'T10,'T11,'T12,'T13,'TResult>
implements: ICloneable
implements: Runtime.Serialization.ISerializable
inherits: MulticastDelegate
inherits: Delegate

--------------------

type Func<'T1,'T2,'T3,'T4,'T5,'T6,'T7,'T8,'T9,'T10,'T11,'T12,'TResult> =
delegate of 'T1 * 'T2 * 'T3 * 'T4 * 'T5 * 'T6 * 'T7 * 'T8 * 'T9 * 'T10 * 'T11 * 'T12 -> 'TResult

Full name: System.Func<_,_,_,_,_,_,_,_,_,_,_,_,_>

type: Func<'T1,'T2,'T3,'T4,'T5,'T6,'T7,'T8,'T9,'T10,'T11,'T12,'TResult>
implements: ICloneable
implements: Runtime.Serialization.ISerializable
inherits: MulticastDelegate
inherits: Delegate

--------------------

type Func<'T1,'T2,'T3,'T4,'T5,'T6,'T7,'T8,'T9,'T10,'T11,'TResult> =
delegate of 'T1 * 'T2 * 'T3 * 'T4 * 'T5 * 'T6 * 'T7 * 'T8 * 'T9 * 'T10 * 'T11 -> 'TResult

Full name: System.Func<_,_,_,_,_,_,_,_,_,_,_,_>

type: Func<'T1,'T2,'T3,'T4,'T5,'T6,'T7,'T8,'T9,'T10,'T11,'TResult>
implements: ICloneable
implements: Runtime.Serialization.ISerializable
inherits: MulticastDelegate
inherits: Delegate

--------------------

type Func<'T1,'T2,'T3,'T4,'T5,'T6,'T7,'T8,'T9,'T10,'TResult> =
delegate of 'T1 * 'T2 * 'T3 * 'T4 * 'T5 * 'T6 * 'T7 * 'T8 * 'T9 * 'T10 -> 'TResult

Full name: System.Func<_,_,_,_,_,_,_,_,_,_,_>

type: Func<'T1,'T2,'T3,'T4,'T5,'T6,'T7,'T8,'T9,'T10,'TResult>
implements: ICloneable
implements: Runtime.Serialization.ISerializable
inherits: MulticastDelegate
inherits: Delegate

--------------------

type Func<'T1,'T2,'T3,'T4,'T5,'T6,'T7,'T8,'T9,'TResult> =
delegate of 'T1 * 'T2 * 'T3 * 'T4 * 'T5 * 'T6 * 'T7 * 'T8 * 'T9 -> 'TResult

Full name: System.Func<_,_,_,_,_,_,_,_,_,_>

type: Func<'T1,'T2,'T3,'T4,'T5,'T6,'T7,'T8,'T9,'TResult>
implements: ICloneable
implements: Runtime.Serialization.ISerializable
inherits: MulticastDelegate
inherits: Delegate

--------------------

type Func<'T1,'T2,'T3,'T4,'T5,'T6,'T7,'T8,'TResult> =
delegate of 'T1 * 'T2 * 'T3 * 'T4 * 'T5 * 'T6 * 'T7 * 'T8 -> 'TResult

Full name: System.Func<_,_,_,_,_,_,_,_,_>

type: Func<'T1,'T2,'T3,'T4,'T5,'T6,'T7,'T8,'TResult>
implements: ICloneable
implements: Runtime.Serialization.ISerializable
inherits: MulticastDelegate
inherits: Delegate

--------------------

type Func<'T1,'T2,'T3,'T4,'T5,'T6,'T7,'TResult> =
delegate of 'T1 * 'T2 * 'T3 * 'T4 * 'T5 * 'T6 * 'T7 -> 'TResult

Full name: System.Func<_,_,_,_,_,_,_,_>

type: Func<'T1,'T2,'T3,'T4,'T5,'T6,'T7,'TResult>
implements: ICloneable
implements: Runtime.Serialization.ISerializable
inherits: MulticastDelegate
inherits: Delegate

--------------------

type Func<'T1,'T2,'T3,'T4,'T5,'T6,'TResult> =
delegate of 'T1 * 'T2 * 'T3 * 'T4 * 'T5 * 'T6 -> 'TResult

Full name: System.Func<_,_,_,_,_,_,_>

type: Func<'T1,'T2,'T3,'T4,'T5,'T6,'TResult>
implements: ICloneable
implements: Runtime.Serialization.ISerializable
inherits: MulticastDelegate
inherits: Delegate

--------------------

type Func<'T1,'T2,'T3,'T4,'T5,'TResult> =
delegate of 'T1 * 'T2 * 'T3 * 'T4 * 'T5 -> 'TResult

Full name: System.Func<_,_,_,_,_,_>

type: Func<'T1,'T2,'T3,'T4,'T5,'TResult>
implements: ICloneable
implements: Runtime.Serialization.ISerializable
inherits: MulticastDelegate
inherits: Delegate

--------------------

type Func<'T1,'T2,'T3,'T4,'TResult> =
delegate of 'T1 * 'T2 * 'T3 * 'T4 -> 'TResult

Full name: System.Func<_,_,_,_,_>

type: Func<'T1,'T2,'T3,'T4,'TResult>
implements: ICloneable
implements: Runtime.Serialization.ISerializable
inherits: MulticastDelegate
inherits: Delegate

--------------------

type Func<'T1,'T2,'T3,'TResult> =
delegate of 'T1 * 'T2 * 'T3 -> 'TResult

Full name: System.Func<_,_,_,_>

type: Func<'T1,'T2,'T3,'TResult>
implements: ICloneable
implements: Runtime.Serialization.ISerializable
inherits: MulticastDelegate
inherits: Delegate

--------------------

type Func<'T1,'T2,'TResult> =
delegate of 'T1 * 'T2 -> 'TResult

Full name: System.Func<_,_,_>

type: Func<'T1,'T2,'TResult>
implements: ICloneable
implements: Runtime.Serialization.ISerializable
inherits: MulticastDelegate
inherits: Delegate

--------------------

type Func<'T,'TResult> =
delegate of 'T -> 'TResult

Full name: System.Func<_,_>

type: Func<'T,'TResult>
implements: ICloneable
implements: Runtime.Serialization.ISerializable
inherits: MulticastDelegate
inherits: Delegate

--------------------

type Func<'TResult> =
delegate of unit -> 'TResult

Full name: System.Func<_>

type: Func<'TResult>
implements: ICloneable
implements: Runtime.Serialization.ISerializable
inherits: MulticastDelegate
inherits: Delegate

--------------------

Func('T1 -> 'T2 -> 'T3 -> 'T4 -> 'T5 -> 'T6 -> 'T7 -> 'T8 -> 'T9 -> 'T10 -> 'T11 -> 'T12 -> 'T13 -> 'T14 -> 'T15 -> 'T16 -> 'TResult)

--------------------

Func('T1 -> 'T2 -> 'T3 -> 'T4 -> 'T5 -> 'T6 -> 'T7 -> 'T8 -> 'T9 -> 'T10 -> 'T11 -> 'T12 -> 'T13 -> 'T14 -> 'T15 -> 'TResult)

--------------------

Func('T1 -> 'T2 -> 'T3 -> 'T4 -> 'T5 -> 'T6 -> 'T7 -> 'T8 -> 'T9 -> 'T10 -> 'T11 -> 'T12 -> 'T13 -> 'T14 -> 'TResult)

--------------------

Func('T1 -> 'T2 -> 'T3 -> 'T4 -> 'T5 -> 'T6 -> 'T7 -> 'T8 -> 'T9 -> 'T10 -> 'T11 -> 'T12 -> 'T13 -> 'TResult)

--------------------

Func('T1 -> 'T2 -> 'T3 -> 'T4 -> 'T5 -> 'T6 -> 'T7 -> 'T8 -> 'T9 -> 'T10 -> 'T11 -> 'T12 -> 'TResult)

--------------------

Func('T1 -> 'T2 -> 'T3 -> 'T4 -> 'T5 -> 'T6 -> 'T7 -> 'T8 -> 'T9 -> 'T10 -> 'T11 -> 'TResult)

--------------------

Func('T1 -> 'T2 -> 'T3 -> 'T4 -> 'T5 -> 'T6 -> 'T7 -> 'T8 -> 'T9 -> 'T10 -> 'TResult)

--------------------

Func('T1 -> 'T2 -> 'T3 -> 'T4 -> 'T5 -> 'T6 -> 'T7 -> 'T8 -> 'T9 -> 'TResult)

--------------------

Func('T1 -> 'T2 -> 'T3 -> 'T4 -> 'T5 -> 'T6 -> 'T7 -> 'T8 -> 'TResult)

--------------------

Func('T1 -> 'T2 -> 'T3 -> 'T4 -> 'T5 -> 'T6 -> 'T7 -> 'TResult)

--------------------

Func('T1 -> 'T2 -> 'T3 -> 'T4 -> 'T5 -> 'T6 -> 'TResult)

--------------------

Func('T1 -> 'T2 -> 'T3 -> 'T4 -> 'T5 -> 'TResult)

--------------------

Func('T1 -> 'T2 -> 'T3 -> 'T4 -> 'TResult)

--------------------

Func('T1 -> 'T2 -> 'T3 -> 'TResult)

--------------------

Func('T1 -> 'T2 -> 'TResult)

--------------------

Func('T -> 'TResult)

--------------------

Func(unit -> 'TResult)

val expr : Expr
match expr with
| Lambdas(_,(Call(_,minfo1,_))) -> function
| Call(obj, minfo2, args) when minfo1.MetadataToken = minfo2.MetadataToken ->
Some args
| _ -> None
| _ -> failwith "invalid template parameter"

val z3 : Expr -> ArithExpr

Full name: GoZ3.z3

From quotations to Z3 objects

let prms = System.Collections.Generic.Dictionary (dict [ "proof", "true" ])
let ctx = new Context()
val unquote : (Expr -> ArithExpr)

Multiple itemsactive recognizer Func: Expr -> Expr -> Expr list optionFull name: GoZ3.( |Func|_| )

Simplified SpecificCall

--------------------

type Func<'T1,'T2,'T3,'T4,'T5,'T6,'T7,'T8,'T9,'T10,'T11,'T12,'T13,'T14,'T15,'T16,'TResult> =
delegate of 'T1 * 'T2 * 'T3 * 'T4 * 'T5 * 'T6 * 'T7 * 'T8 * 'T9 * 'T10 * 'T11 * 'T12 * 'T13 * 'T14 * 'T15 * 'T16 -> 'TResult

Full name: System.Func<_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_>

type: Func<'T1,'T2,'T3,'T4,'T5,'T6,'T7,'T8,'T9,'T10,'T11,'T12,'T13,'T14,'T15,'T16,'TResult>
implements: ICloneable
implements: Runtime.Serialization.ISerializable
inherits: MulticastDelegate
inherits: Delegate

--------------------

type Func<'T1,'T2,'T3,'T4,'T5,'T6,'T7,'T8,'T9,'T10,'T11,'T12,'T13,'T14,'T15,'TResult> =
delegate of 'T1 * 'T2 * 'T3 * 'T4 * 'T5 * 'T6 * 'T7 * 'T8 * 'T9 * 'T10 * 'T11 * 'T12 * 'T13 * 'T14 * 'T15 -> 'TResult

Full name: System.Func<_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_>

type: Func<'T1,'T2,'T3,'T4,'T5,'T6,'T7,'T8,'T9,'T10,'T11,'T12,'T13,'T14,'T15,'TResult>
implements: ICloneable
implements: Runtime.Serialization.ISerializable
inherits: MulticastDelegate
inherits: Delegate

--------------------

type Func<'T1,'T2,'T3,'T4,'T5,'T6,'T7,'T8,'T9,'T10,'T11,'T12,'T13,'T14,'TResult> =
delegate of 'T1 * 'T2 * 'T3 * 'T4 * 'T5 * 'T6 * 'T7 * 'T8 * 'T9 * 'T10 * 'T11 * 'T12 * 'T13 * 'T14 -> 'TResult

Full name: System.Func<_,_,_,_,_,_,_,_,_,_,_,_,_,_,_>

type: Func<'T1,'T2,'T3,'T4,'T5,'T6,'T7,'T8,'T9,'T10,'T11,'T12,'T13,'T14,'TResult>
implements: ICloneable
implements: Runtime.Serialization.ISerializable
inherits: MulticastDelegate
inherits: Delegate

--------------------

type Func<'T1,'T2,'T3,'T4,'T5,'T6,'T7,'T8,'T9,'T10,'T11,'T12,'T13,'TResult> =
delegate of 'T1 * 'T2 * 'T3 * 'T4 * 'T5 * 'T6 * 'T7 * 'T8 * 'T9 * 'T10 * 'T11 * 'T12 * 'T13 -> 'TResult

Full name: System.Func<_,_,_,_,_,_,_,_,_,_,_,_,_,_>

type: Func<'T1,'T2,'T3,'T4,'T5,'T6,'T7,'T8,'T9,'T10,'T11,'T12,'T13,'TResult>
implements: ICloneable
implements: Runtime.Serialization.ISerializable
inherits: MulticastDelegate
inherits: Delegate

--------------------

type Func<'T1,'T2,'T3,'T4,'T5,'T6,'T7,'T8,'T9,'T10,'T11,'T12,'TResult> =
delegate of 'T1 * 'T2 * 'T3 * 'T4 * 'T5 * 'T6 * 'T7 * 'T8 * 'T9 * 'T10 * 'T11 * 'T12 -> 'TResult

Full name: System.Func<_,_,_,_,_,_,_,_,_,_,_,_,_>

type: Func<'T1,'T2,'T3,'T4,'T5,'T6,'T7,'T8,'T9,'T10,'T11,'T12,'TResult>
implements: ICloneable
implements: Runtime.Serialization.ISerializable
inherits: MulticastDelegate
inherits: Delegate

--------------------

type Func<'T1,'T2,'T3,'T4,'T5,'T6,'T7,'T8,'T9,'T10,'T11,'TResult> =
delegate of 'T1 * 'T2 * 'T3 * 'T4 * 'T5 * 'T6 * 'T7 * 'T8 * 'T9 * 'T10 * 'T11 -> 'TResult

Full name: System.Func<_,_,_,_,_,_,_,_,_,_,_,_>

type: Func<'T1,'T2,'T3,'T4,'T5,'T6,'T7,'T8,'T9,'T10,'T11,'TResult>
implements: ICloneable
implements: Runtime.Serialization.ISerializable
inherits: MulticastDelegate
inherits: Delegate

--------------------

type Func<'T1,'T2,'T3,'T4,'T5,'T6,'T7,'T8,'T9,'T10,'TResult> =
delegate of 'T1 * 'T2 * 'T3 * 'T4 * 'T5 * 'T6 * 'T7 * 'T8 * 'T9 * 'T10 -> 'TResult

Full name: System.Func<_,_,_,_,_,_,_,_,_,_,_>

type: Func<'T1,'T2,'T3,'T4,'T5,'T6,'T7,'T8,'T9,'T10,'TResult>
implements: ICloneable
implements: Runtime.Serialization.ISerializable
inherits: MulticastDelegate
inherits: Delegate

--------------------

type Func<'T1,'T2,'T3,'T4,'T5,'T6,'T7,'T8,'T9,'TResult> =
delegate of 'T1 * 'T2 * 'T3 * 'T4 * 'T5 * 'T6 * 'T7 * 'T8 * 'T9 -> 'TResult

Full name: System.Func<_,_,_,_,_,_,_,_,_,_>

type: Func<'T1,'T2,'T3,'T4,'T5,'T6,'T7,'T8,'T9,'TResult>
implements: ICloneable
implements: Runtime.Serialization.ISerializable
inherits: MulticastDelegate
inherits: Delegate

--------------------

type Func<'T1,'T2,'T3,'T4,'T5,'T6,'T7,'T8,'TResult> =
delegate of 'T1 * 'T2 * 'T3 * 'T4 * 'T5 * 'T6 * 'T7 * 'T8 -> 'TResult

Full name: System.Func<_,_,_,_,_,_,_,_,_>

type: Func<'T1,'T2,'T3,'T4,'T5,'T6,'T7,'T8,'TResult>
implements: ICloneable
implements: Runtime.Serialization.ISerializable
inherits: MulticastDelegate
inherits: Delegate

--------------------

type Func<'T1,'T2,'T3,'T4,'T5,'T6,'T7,'TResult> =
delegate of 'T1 * 'T2 * 'T3 * 'T4 * 'T5 * 'T6 * 'T7 -> 'TResult

Full name: System.Func<_,_,_,_,_,_,_,_>

type: Func<'T1,'T2,'T3,'T4,'T5,'T6,'T7,'TResult>
implements: ICloneable
implements: Runtime.Serialization.ISerializable
inherits: MulticastDelegate
inherits: Delegate

--------------------

type Func<'T1,'T2,'T3,'T4,'T5,'T6,'TResult> =
delegate of 'T1 * 'T2 * 'T3 * 'T4 * 'T5 * 'T6 -> 'TResult

Full name: System.Func<_,_,_,_,_,_,_>

type: Func<'T1,'T2,'T3,'T4,'T5,'T6,'TResult>
implements: ICloneable
implements: Runtime.Serialization.ISerializable
inherits: MulticastDelegate
inherits: Delegate

--------------------

type Func<'T1,'T2,'T3,'T4,'T5,'TResult> =
delegate of 'T1 * 'T2 * 'T3 * 'T4 * 'T5 -> 'TResult

Full name: System.Func<_,_,_,_,_,_>

type: Func<'T1,'T2,'T3,'T4,'T5,'TResult>
implements: ICloneable
implements: Runtime.Serialization.ISerializable
inherits: MulticastDelegate
inherits: Delegate

--------------------

type Func<'T1,'T2,'T3,'T4,'TResult> =
delegate of 'T1 * 'T2 * 'T3 * 'T4 -> 'TResult

Full name: System.Func<_,_,_,_,_>

type: Func<'T1,'T2,'T3,'T4,'TResult>
implements: ICloneable
implements: Runtime.Serialization.ISerializable
inherits: MulticastDelegate
inherits: Delegate

--------------------

type Func<'T1,'T2,'T3,'TResult> =
delegate of 'T1 * 'T2 * 'T3 -> 'TResult

Full name: System.Func<_,_,_,_>

type: Func<'T1,'T2,'T3,'TResult>
implements: ICloneable
implements: Runtime.Serialization.ISerializable
inherits: MulticastDelegate
inherits: Delegate

--------------------

type Func<'T1,'T2,'TResult> =
delegate of 'T1 * 'T2 -> 'TResult

Full name: System.Func<_,_,_>

type: Func<'T1,'T2,'TResult>
implements: ICloneable
implements: Runtime.Serialization.ISerializable
inherits: MulticastDelegate
inherits: Delegate

--------------------

type Func<'T,'TResult> =
delegate of 'T -> 'TResult

Full name: System.Func<_,_>

type: Func<'T,'TResult>
implements: ICloneable
implements: Runtime.Serialization.ISerializable
inherits: MulticastDelegate
inherits: Delegate

--------------------

type Func<'TResult> =
delegate of unit -> 'TResult

Full name: System.Func<_>

type: Func<'TResult>
implements: ICloneable
implements: Runtime.Serialization.ISerializable
inherits: MulticastDelegate
inherits: Delegate

--------------------

Func('T1 -> 'T2 -> 'T3 -> 'T4 -> 'T5 -> 'T6 -> 'T7 -> 'T8 -> 'T9 -> 'T10 -> 'T11 -> 'T12 -> 'T13 -> 'T14 -> 'T15 -> 'T16 -> 'TResult)

--------------------

Func('T1 -> 'T2 -> 'T3 -> 'T4 -> 'T5 -> 'T6 -> 'T7 -> 'T8 -> 'T9 -> 'T10 -> 'T11 -> 'T12 -> 'T13 -> 'T14 -> 'T15 -> 'TResult)

--------------------

Func('T1 -> 'T2 -> 'T3 -> 'T4 -> 'T5 -> 'T6 -> 'T7 -> 'T8 -> 'T9 -> 'T10 -> 'T11 -> 'T12 -> 'T13 -> 'T14 -> 'TResult)

--------------------

Func('T1 -> 'T2 -> 'T3 -> 'T4 -> 'T5 -> 'T6 -> 'T7 -> 'T8 -> 'T9 -> 'T10 -> 'T11 -> 'T12 -> 'T13 -> 'TResult)

--------------------

Func('T1 -> 'T2 -> 'T3 -> 'T4 -> 'T5 -> 'T6 -> 'T7 -> 'T8 -> 'T9 -> 'T10 -> 'T11 -> 'T12 -> 'TResult)

--------------------

Func('T1 -> 'T2 -> 'T3 -> 'T4 -> 'T5 -> 'T6 -> 'T7 -> 'T8 -> 'T9 -> 'T10 -> 'T11 -> 'TResult)

--------------------

Func('T1 -> 'T2 -> 'T3 -> 'T4 -> 'T5 -> 'T6 -> 'T7 -> 'T8 -> 'T9 -> 'T10 -> 'TResult)

--------------------

Func('T1 -> 'T2 -> 'T3 -> 'T4 -> 'T5 -> 'T6 -> 'T7 -> 'T8 -> 'T9 -> 'TResult)

--------------------

Func('T1 -> 'T2 -> 'T3 -> 'T4 -> 'T5 -> 'T6 -> 'T7 -> 'T8 -> 'TResult)

--------------------

Func('T1 -> 'T2 -> 'T3 -> 'T4 -> 'T5 -> 'T6 -> 'T7 -> 'TResult)

--------------------

Func('T1 -> 'T2 -> 'T3 -> 'T4 -> 'T5 -> 'T6 -> 'TResult)

--------------------

Func('T1 -> 'T2 -> 'T3 -> 'T4 -> 'T5 -> 'TResult)

--------------------

Func('T1 -> 'T2 -> 'T3 -> 'T4 -> 'TResult)

--------------------

Func('T1 -> 'T2 -> 'T3 -> 'TResult)

--------------------

Func('T1 -> 'T2 -> 'TResult)

--------------------

Func('T -> 'TResult)

--------------------

Func(unit -> 'TResult)

val x : Expr
val y : Expr
Context.MkAdd(t: ArithExpr []) : ArithExpr
Context.MkSub(t: ArithExpr []) : ArithExpr

active recognizer Lambdas: Expr -> (Var list list * Expr) option

Full name: Microsoft.FSharp.Quotations.DerivedPatterns.( |Lambdas|_| )

val e : Expr

Multiple itemsactive recognizer Var: Expr -> Var optionFull name: Microsoft.FSharp.Quotations.Patterns.( |Var|_| )

--------------------

type Var =
class
interface IComparable
new : name:string * typ:Type * ?isMutable:bool -> Var
member IsMutable : bool
member Name : string
member Type : Type
static member Global : name:string * typ:Type -> Var
end

Full name: Microsoft.FSharp.Quotations.Var

type: Var
implements: IComparable

val var : Var

type: Var
implements: IComparable

Multiple overloadsContext.MkIntConst(name: string) : IntExpr

Context.MkIntConst(name: Symbol) : IntExpr

property Var.Name: string

type ArithExpr =
class
inherit Microsoft.Z3.Expr
end

Full name: Microsoft.Z3.ArithExpr

type: ArithExpr
implements: IDisposable
implements: IComparable
inherits: Expr
inherits: AST
inherits: Z3Object

val failwith : string -> 'T

Full name: Microsoft.FSharp.Core.Operators.failwith

val sprintf : Printf.StringFormat<'T> -> 'T

Full name: Microsoft.FSharp.Core.ExtraTopLevelOperators.sprintf

val simplifier : unit -> unit

Full name: GoZ3.simplifier

Simplify expression "x + (y - (x + z))"

val t1 : ArithExpr

type: ArithExpr
implements: IDisposable
implements: IComparable
inherits: Expr
inherits: AST
inherits: Z3Object

val x : int

type: int
implements: IComparable
implements: IFormattable
implements: IConvertible
implements: IComparable<int>
implements: IEquatable<int>
inherits: ValueType

val y : int

type: int
implements: IComparable
implements: IFormattable
implements: IConvertible
implements: IComparable<int>
implements: IEquatable<int>
inherits: ValueType

val z : int

type: int
implements: IComparable
implements: IFormattable
implements: IConvertible
implements: IComparable<int>
implements: IEquatable<int>
inherits: ValueType

val t2 : Expr

type: Expr
implements: IDisposable
implements: IComparable
inherits: AST
inherits: Z3Object

Expr.Simplify(p: Params) : Expr
  1. don’t forget to clean up (.a and .obj files) the folder if you have built x64 lib before.

  2. MD-generated makefile & co are available on github