1 people like it.

Counting Evens and Odds via Z3

Counting Evens and Odds via Z3.

 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: 
40: 
41: 
42: 
43: 
44: 
45: 
46: 
47: 
48: 
49: 
50: 
51: 
52: 
53: 
54: 
55: 
56: 
57: 
58: 
59: 
60: 
61: 

// Evens and Odds via Z3

#r "bin/Microsoft.Z3.dll"

open System
open System.IO
open System.Runtime.InteropServices
open System.Collections.Generic
open Microsoft.Z3



let ctx = new Context([|("model", "true")|] |> dict |> Dictionary)

// helpers
let True : BoolExpr = ctx.MkTrue()
let False : BoolExpr = ctx.MkFalse()
let Int : int -> IntNum = fun v -> ctx.MkInt(v)
let IntVar : string -> IntExpr = fun var -> ctx.MkIntConst(var) 
let FreshVar : unit -> IntExpr = fun () -> ctx.MkIntConst(Guid.NewGuid().ToString()) 
let Eq : Expr -> Expr -> BoolExpr = fun l r -> ctx.MkEq(l, r) 
let Mod : IntExpr -> IntExpr -> IntExpr = fun l r -> ctx.MkMod(l, r)
let Ite : BoolExpr -> Expr -> Expr -> Expr = fun p t e -> ctx.MkITE(p, t, e)
let Add : ArithExpr -> ArithExpr -> ArithExpr = fun l r -> ctx.MkAdd(l, r)
let Mul : ArithExpr -> ArithExpr -> ArithExpr = fun l r -> ctx.MkMul(l, r)
let And : BoolExpr[] -> BoolExpr = fun bools -> ctx.MkAnd(bools)
let Or : BoolExpr[] -> BoolExpr = fun bools -> ctx.MkOr(bools)


let rec compile : IntExpr list -> IntExpr -> IntExpr -> BoolExpr = 
    fun nums even odd ->
        match nums with
        | [] ->  And [|Eq even (Int 0); Eq odd (Int 0)|]
        | num :: nums -> 
            let even' = FreshVar ()
            let odd' = FreshVar ()
            let ite = 
                Ite (Eq (Mod num (Int 2)) (Int 0)) 
                                (And [|Eq even (Add even' (Int 1)); Eq odd odd'|])
                                (And [|Eq odd (Add odd' (Int 1)); Eq even even'|]) :?> BoolExpr
            And [|ite; compile nums even' odd'|]
        

let even = IntVar "even"
let odd = IntVar "odd"
let x = IntVar "x"
let twox = Mul (Int 2) x :?> IntExpr
let twoxplusone = Add (Mul (Int 2) x) (Int 1) :?> IntExpr
let testExpr = compile [Int 1; Int 2; Int 3;
                        twox; twoxplusone; 
                        Add twox twox :?> _; 
                        Add twoxplusone twoxplusone :?> _] even odd

let solver = ctx.MkSolver()
solver.Assert(testExpr)
let flag = solver.Check() = Status.SATISFIABLE

let model = solver.Model

string <| model.Evaluate(even) // 4
string <| model.Evaluate(odd) // 3
namespace System
namespace System.IO
namespace System.Runtime
namespace System.Runtime.InteropServices
namespace System.Collections
namespace System.Collections.Generic
namespace Microsoft
namespace Microsoft.Z3
val ctx : Context

Full name: Script.ctx
Multiple items
type Context =
  new : unit -> Context + 1 overload
  member ASTMap_DRQ : IDecRefQueue
  member ASTVector_DRQ : IDecRefQueue
  member AST_DRQ : IDecRefQueue
  member And : p1:Probe * p2:Probe -> Probe
  member AndThen : t1:Tactic * t2:Tactic * [<ParamArray>] ts:Tactic[] -> Tactic
  member ApplyResult_DRQ : IDecRefQueue
  member BenchmarkToSMTString : name:string * logic:string * status:string * attributes:string * assumptions:BoolExpr[] * formula:BoolExpr -> string
  member BoolSort : BoolSort
  member Cond : p:Probe * t1:Tactic * t2:Tactic -> Tactic
  ...

Full name: Microsoft.Z3.Context

--------------------
Context() : unit
Context(settings: Dictionary<string,string>) : unit
val dict : keyValuePairs:seq<'Key * 'Value> -> IDictionary<'Key,'Value> (requires equality)

Full name: Microsoft.FSharp.Core.ExtraTopLevelOperators.dict
Multiple items
type Dictionary<'TKey,'TValue> =
  new : unit -> Dictionary<'TKey, 'TValue> + 5 overloads
  member Add : key:'TKey * value:'TValue -> unit
  member Clear : unit -> unit
  member Comparer : IEqualityComparer<'TKey>
  member ContainsKey : key:'TKey -> bool
  member ContainsValue : value:'TValue -> bool
  member Count : int
  member GetEnumerator : unit -> Enumerator<'TKey, 'TValue>
  member GetObjectData : info:SerializationInfo * context:StreamingContext -> unit
  member Item : 'TKey -> 'TValue with get, set
  ...
  nested type Enumerator
  nested type KeyCollection
  nested type ValueCollection

Full name: System.Collections.Generic.Dictionary<_,_>

--------------------
Dictionary() : unit
Dictionary(capacity: int) : unit
Dictionary(comparer: IEqualityComparer<'TKey>) : unit
Dictionary(dictionary: IDictionary<'TKey,'TValue>) : unit
Dictionary(capacity: int, comparer: IEqualityComparer<'TKey>) : unit
Dictionary(dictionary: IDictionary<'TKey,'TValue>, comparer: IEqualityComparer<'TKey>) : unit
val True : BoolExpr

Full name: Script.True
type BoolExpr =
  inherit Expr

Full name: Microsoft.Z3.BoolExpr
Context.MkTrue() : BoolExpr
val False : BoolExpr

Full name: Script.False
Context.MkFalse() : BoolExpr
val Int : v:int -> IntNum

Full name: Script.Int
Multiple items
val int : value:'T -> int (requires member op_Explicit)

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

--------------------
type int = int32

Full name: Microsoft.FSharp.Core.int

--------------------
type int<'Measure> = int

Full name: Microsoft.FSharp.Core.int<_>
type IntNum =
  inherit IntExpr
  member BigInteger : BigInteger
  member Int : int
  member Int64 : int64
  member ToString : unit -> string
  member UInt : uint32
  member UInt64 : uint64

Full name: Microsoft.Z3.IntNum
val v : int
Context.MkInt(v: uint64) : IntNum
Context.MkInt(v: int64) : IntNum
Context.MkInt(v: uint32) : IntNum
Context.MkInt(v: int) : IntNum
Context.MkInt(v: string) : IntNum
val IntVar : var:string -> IntExpr

Full name: Script.IntVar
Multiple items
val string : value:'T -> string

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

--------------------
type string = String

Full name: Microsoft.FSharp.Core.string
type IntExpr =
  inherit ArithExpr

Full name: Microsoft.Z3.IntExpr
val var : string
Context.MkIntConst(name: string) : IntExpr
Context.MkIntConst(name: Symbol) : IntExpr
val FreshVar : unit -> IntExpr

Full name: Script.FreshVar
type unit = Unit

Full name: Microsoft.FSharp.Core.unit
Multiple items
type Guid =
  struct
    new : b:byte[] -> Guid + 4 overloads
    member CompareTo : value:obj -> int + 1 overload
    member Equals : o:obj -> bool + 1 overload
    member GetHashCode : unit -> int
    member ToByteArray : unit -> byte[]
    member ToString : unit -> string + 2 overloads
    static val Empty : Guid
    static member NewGuid : unit -> Guid
    static member Parse : input:string -> Guid
    static member ParseExact : input:string * format:string -> Guid
    ...
  end

Full name: System.Guid

--------------------
type GuidAttribute =
  inherit Attribute
  new : guid:string -> GuidAttribute
  member Value : string

Full name: System.Runtime.InteropServices.GuidAttribute

--------------------
Guid()
Guid(b: byte []) : unit
Guid(g: string) : unit
Guid(a: int, b: int16, c: int16, d: byte []) : unit
Guid(a: uint32, b: uint16, c: uint16, d: byte, e: byte, f: byte, g: byte, h: byte, i: byte, j: byte, k: byte) : unit
Guid(a: int, b: int16, c: int16, d: byte, e: byte, f: byte, g: byte, h: byte, i: byte, j: byte, k: byte) : unit

--------------------
GuidAttribute(guid: string) : unit
Guid.NewGuid() : Guid
val Eq : l:Expr -> r:Expr -> BoolExpr

Full name: Script.Eq
type Expr =
  inherit AST
  member Args : Expr[]
  member BoolValue : Z3_lbool
  member FuncDecl : FuncDecl
  member Index : uint32
  member IsAdd : bool
  member IsAlgebraicNumber : bool
  member IsAnd : bool
  member IsArithmeticNumeral : bool
  member IsArray : bool
  member IsArrayMap : bool
  ...

Full name: Microsoft.Z3.Expr
val l : Expr
val r : Expr
Context.MkEq(x: Expr, y: Expr) : BoolExpr
val Mod : l:IntExpr -> r:IntExpr -> IntExpr

Full name: Script.Mod
val l : IntExpr
val r : IntExpr
Context.MkMod(t1: IntExpr, t2: IntExpr) : IntExpr
val Ite : p:BoolExpr -> t:Expr -> e:Expr -> Expr

Full name: Script.Ite
val p : BoolExpr
val t : Expr
val e : Expr
Context.MkITE(t1: BoolExpr, t2: Expr, t3: Expr) : Expr
val Add : l:ArithExpr -> r:ArithExpr -> ArithExpr

Full name: Script.Add
type ArithExpr =
  inherit Expr

Full name: Microsoft.Z3.ArithExpr
val l : ArithExpr
val r : ArithExpr
Context.MkAdd(t: IEnumerable<ArithExpr>) : ArithExpr
Context.MkAdd([<ParamArray>] t: ArithExpr []) : ArithExpr
val Mul : l:ArithExpr -> r:ArithExpr -> ArithExpr

Full name: Script.Mul
Context.MkMul(t: IEnumerable<ArithExpr>) : ArithExpr
Context.MkMul([<ParamArray>] t: ArithExpr []) : ArithExpr
val And : bools:BoolExpr [] -> BoolExpr

Full name: Script.And
val bools : BoolExpr []
Context.MkAnd(t: IEnumerable<BoolExpr>) : BoolExpr
Context.MkAnd([<ParamArray>] t: BoolExpr []) : BoolExpr
val Or : bools:BoolExpr [] -> BoolExpr

Full name: Script.Or
Context.MkOr(t: IEnumerable<BoolExpr>) : BoolExpr
Context.MkOr([<ParamArray>] t: BoolExpr []) : BoolExpr
val compile : nums:IntExpr list -> even:IntExpr -> odd:IntExpr -> BoolExpr

Full name: Script.compile
type 'T list = List<'T>

Full name: Microsoft.FSharp.Collections.list<_>
val nums : IntExpr list
val even : IntExpr
val odd : IntExpr
val num : IntExpr
val even' : IntExpr
val odd' : IntExpr
val ite : BoolExpr
val even : IntExpr

Full name: Script.even
val odd : IntExpr

Full name: Script.odd
val x : IntExpr

Full name: Script.x
val twox : IntExpr

Full name: Script.twox
val twoxplusone : IntExpr

Full name: Script.twoxplusone
val testExpr : BoolExpr

Full name: Script.testExpr
val solver : Solver

Full name: Script.solver
Context.MkSolver(t: Tactic) : Solver
Context.MkSolver(logic: string) : Solver
Context.MkSolver(?logic: Symbol) : Solver
Solver.Assert([<ParamArray>] constraints: BoolExpr []) : unit
val flag : bool

Full name: Script.flag
Solver.Check([<ParamArray>] assumptions: Expr []) : Status
type Status =
  | UNSATISFIABLE = -1
  | UNKNOWN = 0
  | SATISFIABLE = 1

Full name: Microsoft.Z3.Status
field Status.SATISFIABLE = 1
val model : Model

Full name: Script.model
property Solver.Model: Model
Model.Evaluate(t: Expr, ?completion: bool) : Expr
Raw view Test code New version

More information

Link:http://fssnip.net/7Tv
Posted:7 years ago
Author:NIck Palladinos
Tags: z3

This web site is created using F# and Suave web server. It is hosted on Azure and the source code is on GitHub. Contributions are welcome!

The first version of fssnip.net has been created by @tomaspetricek back in 2010. This web site is a new, open-source and contribution-friendly version.