3 people like it.

Life patterns via Z3

Discovering Life patterns 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: 
 62: 
 63: 
 64: 
 65: 
 66: 
 67: 
 68: 
 69: 
 70: 
 71: 
 72: 
 73: 
 74: 
 75: 
 76: 
 77: 
 78: 
 79: 
 80: 
 81: 
 82: 
 83: 
 84: 
 85: 
 86: 
 87: 
 88: 
 89: 
 90: 
 91: 
 92: 
 93: 
 94: 
 95: 
 96: 
 97: 
 98: 
 99: 
100: 
101: 
102: 
103: 
104: 
105: 
106: 
107: 
108: 
109: 
110: 
111: 
112: 
113: 
114: 
115: 
116: 
117: 
118: 
119: 
120: 
121: 
122: 
123: 
124: 
125: 
126: 
127: 
128: 
129: 
130: 
131: 
132: 
133: 
134: 
135: 
136: 
137: 
138: 
139: 
140: 
// Life patterns via Z3
// Inspired by https://www.youtube.com/watch?v=g4lhrVPDUG0

#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 -> uint32 -> BitVecNum = fun v w -> ctx.MkBV(v, w)
let IntVar : string -> uint32 -> BitVecExpr = fun var w -> ctx.MkBVConst(var, w) 
let FreshVar : uint32 -> BitVecExpr = fun w -> ctx.MkBVConst(Guid.NewGuid().ToString(), w) 
let Eq : Expr -> Expr -> BoolExpr = fun l r -> ctx.MkEq(l, r) 
let Ite : BoolExpr -> Expr -> Expr -> Expr = fun p t e -> ctx.MkITE(p, t, e)
let And : BoolExpr[] -> BoolExpr = fun bools -> ctx.MkAnd(bools)
let Or : BoolExpr[] -> BoolExpr = fun bools -> ctx.MkOr(bools)
let Not : BoolExpr -> BoolExpr = fun bool -> ctx.MkNot(bool)
let Add : BitVecExpr -> BitVecExpr -> BitVecExpr = fun l r -> ctx.MkBVAdd(l, r)

let width = 15
let height = 7

let initBoard : Expr[][] = 
    [| for i in {0..height - 1} ->
            [| for j in {0..width - 1} -> IntVar (sprintf "X_%d_%d" i j) 1u :> _ |] |]

let finalBoard : Expr[][] = 
    [| for i in {0..height - 1} ->
            [| for j in {0..width - 1} -> IntVar (sprintf "Υ_%d_%d" i j) 1u :> _ |] |]

let pattern : int[][] = 
    [|[|0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0|];
      [|0; 1; 0; 0; 0; 1; 0; 1; 1; 1; 0; 1; 1; 1; 0|];
      [|0; 1; 0; 0; 0; 1; 0; 1; 0; 0; 0; 1; 0; 0; 0|]
      [|0; 1; 0; 0; 0; 1; 0; 1; 1; 0; 0; 1; 1; 0; 0|]
      [|0; 1; 0; 0; 0; 1; 0; 1; 0; 0; 0; 1; 0; 0; 0|]
      [|0; 1; 1; 1; 0; 1; 0; 1; 0; 0; 0; 1; 1; 1; 0|]
      [|0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0|]|]

let validValues = initBoard |> Array.collect id |> Array.map (fun x -> Or [|Eq x (Int 0 1u); Eq x (Int 1 1u)|] ) |> And
let validFinalPattern = 
    And [| for i in {0..height - 1} ->
            And [| for j in {0..width - 1} -> Eq finalBoard.[i].[j] (Int pattern.[i].[j] 1u) |] |]

let getNeighborhoods : Expr[][] -> int -> int -> Expr list = fun board i j ->
    match i, j with
    | 0, 0 -> [board.[0].[1]; board.[1].[0]; board.[1].[1] ]
    | i, j when i = height - 1 && j = width - 1 -> 
        [board.[i].[j - 1]; board.[i - 1].[j]; board.[i - 1].[j - 1] ] 
    | 0, j when j = width - 1 -> 
        [board.[0].[j - 1]; board.[1].[j - 1]; board.[1].[j] ]
    | i, 0 when i = height - 1 -> 
        [board.[i - 1].[0]; board.[i - 1].[1]; board.[i].[1] ]
    | 0, j -> 
        [board.[0].[j - 1]; board.[0].[j + 1]; board.[1].[j + 1]; board.[1].[j - 1]; board.[1].[j] ]
    | i, 0 -> 
        [board.[i - 1].[0]; board.[i + 1].[0]; board.[i + 1].[1]; board.[i - 1].[1]; board.[i].[1] ]
    | i, j when i = height - 1 -> 
        [board.[i].[j - 1]; board.[i].[j + 1]; board.[i - 1].[j + 1]; board.[i - 1].[j - 1]; board.[i - 1].[j] ] 
    | i, j when j = width - 1 -> 
        [board.[i - 1].[j]; board.[i + 1].[j]; board.[i + 1].[j - 1]; board.[i - 1].[j - 1]; board.[i].[j - 1] ] 
    | i, j -> 
        [board.[i - 1].[j - 1]; board.[i - 1].[j]; board.[i - 1].[j + 1]; 
         board.[i + 1].[j - 1]; board.[i + 1].[j]; board.[i + 1].[j + 1];
         board.[i].[j - 1]; board.[i].[j + 1] ]
    
let countNeighborhoods : Expr[][] -> int -> int -> BitVecExpr -> BoolExpr = fun board i j c ->
    let rec count : Expr list -> BitVecExpr -> BoolExpr = fun exprs c ->
        match exprs with
        | [] -> Eq c (Int 0 4u)
        | expr :: exprs ->
            let c' = FreshVar 4u 
            let ite = 
                Ite (Eq expr (Int 1 1u)) 
                    (Eq c (Add c' (Int 1 4u)))
                    (Eq c c') :?> _
            And [|ite; count exprs c'|]
        
    count (getNeighborhoods board i j) c
    
    
let rules : Expr[][] -> Expr[][] -> BoolExpr = fun fromBoard toBoard ->
    And [| for i in {0..height - 1} ->
            And [| for j in {0..width - 1} do
                        let c = IntVar (sprintf "C_%d_%d" i j) 4u 
                        let b = countNeighborhoods fromBoard i j c
                        let ite = 
                            Ite (Eq fromBoard.[i].[j] (Int 1 1u))
                                (Ite (Or [|(Eq c (Int 0 4u)); (Eq c (Int 1 4u)) |])
                                     (Eq toBoard.[i].[j] (Int 0 1u))
                                     (Ite (Or [|(Eq c (Int 4 4u)); (Eq c (Int 5 4u)); 
                                                (Eq c (Int 6 4u)); (Eq c (Int 7 4u)); (Eq c (Int 8 4u)) |])
                                        (Eq toBoard.[i].[j] (Int 0 1u))
                                        (Ite (Or [|(Eq c (Int 2 4u)); (Eq c (Int 3 4u))|])
                                             (Eq toBoard.[i].[j] (Int 1 1u))
                                            False))) 
                                (Ite (Eq c (Int 3 4u)) 
                                    (Eq toBoard.[i].[j] (Int 1 1u))
                                    (Eq toBoard.[i].[j] (Int 0 1u))) :?> _
                        yield And [|b; ite|] |] |]
    

let formula = And [|validValues; validFinalPattern; rules initBoard finalBoard|]

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

let model = solver.Model


for i in {0..height - 1} do
    for j in {0..width - 1} do
        let value = string <| model.Evaluate(initBoard.[i].[j])
        let c = getNeighborhoods initBoard i j 
                |> List.filter (fun x -> string <| model.Evaluate(x) = "1") 
                |> List.length
        match value with
        | "1" -> 
            match c with
            | 0 | 1 -> printf " "
            | 4 | 5 | 6 | 7 | 8 -> printf " "
            | 2 | 3 -> printf "1"
            | _ -> failwith "oups"
        | "0" -> 
            match c with
            | 3 -> printf "1"
            | _ -> printf " "
        | _ -> failwith "oups"

    printfn ""
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 -> w:uint32 -> BitVecNum

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<_>
Multiple items
val uint32 : value:'T -> uint32 (requires member op_Explicit)

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

--------------------
type uint32 = UInt32

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

Full name: Microsoft.Z3.BitVecNum
val v : int
val w : uint32
Context.MkBV(v: uint64, size: uint32) : BitVecNum
Context.MkBV(v: int64, size: uint32) : BitVecNum
Context.MkBV(v: uint32, size: uint32) : BitVecNum
Context.MkBV(v: int, size: uint32) : BitVecNum
Context.MkBV(v: string, size: uint32) : BitVecNum
val IntVar : var:string -> w:uint32 -> BitVecExpr

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 BitVecExpr =
  inherit Expr
  member SortSize : uint32

Full name: Microsoft.Z3.BitVecExpr
val var : string
Context.MkBVConst(name: string, size: uint32) : BitVecExpr
Context.MkBVConst(name: Symbol, size: uint32) : BitVecExpr
val FreshVar : w:uint32 -> BitVecExpr

Full name: Script.FreshVar
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 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 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 Not : bool:BoolExpr -> BoolExpr

Full name: Script.Not
Multiple items
val bool : BoolExpr

--------------------
type bool = Boolean

Full name: Microsoft.FSharp.Core.bool
Context.MkNot(a: BoolExpr) : BoolExpr
val Add : l:BitVecExpr -> r:BitVecExpr -> BitVecExpr

Full name: Script.Add
val l : BitVecExpr
val r : BitVecExpr
Context.MkBVAdd(t1: BitVecExpr, t2: BitVecExpr) : BitVecExpr
val width : int

Full name: Script.width
val height : int

Full name: Script.height
val initBoard : Expr [] []

Full name: Script.initBoard
val i : int
val j : int
val sprintf : format:Printf.StringFormat<'T> -> 'T

Full name: Microsoft.FSharp.Core.ExtraTopLevelOperators.sprintf
val finalBoard : Expr [] []

Full name: Script.finalBoard
val pattern : int [] []

Full name: Script.pattern
val validValues : BoolExpr

Full name: Script.validValues
type Array =
  member Clone : unit -> obj
  member CopyTo : array:Array * index:int -> unit + 1 overload
  member GetEnumerator : unit -> IEnumerator
  member GetLength : dimension:int -> int
  member GetLongLength : dimension:int -> int64
  member GetLowerBound : dimension:int -> int
  member GetUpperBound : dimension:int -> int
  member GetValue : [<ParamArray>] indices:int[] -> obj + 7 overloads
  member Initialize : unit -> unit
  member IsFixedSize : bool
  ...

Full name: System.Array
val collect : mapping:('T -> 'U []) -> array:'T [] -> 'U []

Full name: Microsoft.FSharp.Collections.Array.collect
val id : x:'T -> 'T

Full name: Microsoft.FSharp.Core.Operators.id
val map : mapping:('T -> 'U) -> array:'T [] -> 'U []

Full name: Microsoft.FSharp.Collections.Array.map
val x : Expr
val validFinalPattern : BoolExpr

Full name: Script.validFinalPattern
val getNeighborhoods : board:Expr [] [] -> i:int -> j:int -> Expr list

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

Full name: Microsoft.FSharp.Collections.list<_>
val board : Expr [] []
val countNeighborhoods : board:Expr [] [] -> i:int -> j:int -> c:BitVecExpr -> BoolExpr

Full name: Script.countNeighborhoods
val c : BitVecExpr
val count : (Expr list -> BitVecExpr -> BoolExpr)
val exprs : Expr list
val expr : Expr
val c' : BitVecExpr
val ite : BoolExpr
val rules : fromBoard:Expr [] [] -> toBoard:Expr [] [] -> BoolExpr

Full name: Script.rules
val fromBoard : Expr [] []
val toBoard : Expr [] []
val b : BoolExpr
val formula : BoolExpr

Full name: Script.formula
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
val i : int32
val j : int32
val value : string
Model.Evaluate(t: Expr, ?completion: bool) : Expr
val c : int
Multiple items
type List<'T> =
  new : unit -> List<'T> + 2 overloads
  member Add : item:'T -> unit
  member AddRange : collection:IEnumerable<'T> -> unit
  member AsReadOnly : unit -> ReadOnlyCollection<'T>
  member BinarySearch : item:'T -> int + 2 overloads
  member Capacity : int with get, set
  member Clear : unit -> unit
  member Contains : item:'T -> bool
  member ConvertAll<'TOutput> : converter:Converter<'T, 'TOutput> -> List<'TOutput>
  member CopyTo : array:'T[] -> unit + 2 overloads
  ...
  nested type Enumerator

Full name: System.Collections.Generic.List<_>

--------------------
List() : unit
List(capacity: int) : unit
List(collection: IEnumerable<'T>) : unit
val filter : predicate:('T -> bool) -> list:'T list -> 'T list

Full name: Microsoft.FSharp.Collections.List.filter
val length : list:'T list -> int

Full name: Microsoft.FSharp.Collections.List.length
val printf : format:Printf.TextWriterFormat<'T> -> 'T

Full name: Microsoft.FSharp.Core.ExtraTopLevelOperators.printf
val failwith : message:string -> 'T

Full name: Microsoft.FSharp.Core.Operators.failwith
val printfn : format:Printf.TextWriterFormat<'T> -> 'T

Full name: Microsoft.FSharp.Core.ExtraTopLevelOperators.printfn
Raw view Test code New version

More information

Link:http://fssnip.net/7TO
Posted:6 years ago
Author:NIck Palladinos
Tags: z3 , life