2 people like it.

Eternity 2 Solver via Z3

Eternity 2 Solver 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: 
141: 
142: 
143: 
144: 
145: 
146: 
147: 
148: 
149: 
150: 
151: 
152: 
153: 
154: 
155: 
156: 
157: 
158: 
159: 
160: 
161: 
162: 
163: 
164: 
165: 
166: 

// Eternity 2 Solver via Z3
// https://en.wikipedia.org/wiki/Eternity_II_puzzle

#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 : unit -> 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 Distinct : Expr[] -> BoolExpr = fun exprs -> ctx.MkDistinct(exprs)


type Piece = { Id : int; RotationId : int; Up : char; Down : char; Left : char; Right : char }

let rotations : string -> int -> Piece[] = fun piece index ->
    let piece = { Id = index; RotationId = 0; Up = piece.[2]; Down = piece.[0]; Left = piece.[1]; Right = piece.[3]  }
    [| piece;
       { Id = index; RotationId = 0; Up = piece.Left; Down = piece.Right; Left = piece.Down; Right = piece.Up  }
       { Id = index; RotationId = 0; Up = piece.Down; Down = piece.Up; Left = piece.Right; Right = piece.Left  }
       { Id = index; RotationId = 0; Up = piece.Right; Down = piece.Left; Left = piece.Up; Right = piece.Down  }|]

let dim = 4
let puzzle = [|"YXXB"; "YBXX"; "XBBX"; "XYYX"; "UUUP"; "PUPP"; "UUPP"; "UUPP"; 
               "YXYP"; "BXBP"; "YXBP"; "BXYP"; "YXYU"; "BXBU"; "BXYU"; "YXBU"|]
let pieces = 
    puzzle
    |> Array.mapi (fun i piece -> rotations piece i)
    |> Array.collect id
    |> Array.mapi (fun i piece -> { piece with RotationId = i })
    |> Array.splitInto dim 


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

let validValues : BoolExpr =
    let pieces = pieces |> Array.collect id
    And [| for i in {0..dim - 1} do
            for j in {0..dim - 1} do 
                yield Or [| for piece in pieces do yield Eq (varPieces.[i].[j]) (Int piece.RotationId 8u) |] |]

let distinct = 
    let pieces = pieces |> Array.collect id
    let tempVars = 
        [| for i in {0..dim - 1} ->
            [| for j in {0..dim - 1} -> IntVar (sprintf "Y_%d_%d" i j) 8u |] |]
    let maps =
        And [| for i in {0..dim - 1} do
                for j in {0..dim - 1} do 
                    for piece in pieces do 
                        yield Ite (Eq varPieces.[i].[j] (Int piece.RotationId 8u)) (Eq tempVars.[i].[j] (Int piece.Id 8u)) True :?> _ |]
    
    let distinctValues = tempVars |> Array.collect id |> Array.map (fun v -> v :> Expr) |> Distinct
    And [|maps; distinctValues|]

let constraints = 
    let n = dim - 1
    let pieces = pieces |> Array.collect id
    let findUp c = pieces |> Array.filter (fun piece -> piece.Up = c) 
    let findDown c = pieces |> Array.filter (fun piece -> piece.Down = c) 
    let findLeft c = pieces |> Array.filter (fun piece -> piece.Left = c) 
    let findRight c = pieces |> Array.filter (fun piece -> piece.Right = c) 
    And [| for i in {0..n} do
                for j in {0..n} do 
                    match i, j with
                    | 0, 0 -> 
                        let pieces = pieces |> Array.filter (fun piece -> piece.Up = 'X' && piece.Left = 'X')
                        yield Or [| for piece in pieces do
                                        yield And [| Eq varPieces.[0].[0] (Int piece.RotationId 8u);
                                                     Or (piece.Down |> findUp |> Array.filter (fun piece -> piece.Left = 'X') |> Array.map (fun piece -> Eq varPieces.[1].[0] (Int piece.RotationId 8u)));
                                                     Or (piece.Right |> findLeft |> Array.filter (fun piece -> piece.Up = 'X') |> Array.map (fun piece -> Eq varPieces.[0].[1] (Int piece.RotationId 8u))) |]
                                 |]
                    | 0, j when j = n -> 
                        let pieces = pieces |> Array.filter (fun piece -> piece.Up = 'X' && piece.Right = 'X')
                        yield Or [| for piece in pieces do
                                        yield And [| Eq varPieces.[0].[n] (Int piece.RotationId 8u);
                                                     Or (piece.Left |> findRight |> Array.filter (fun piece -> piece.Up = 'X') |> Array.map (fun piece -> Eq varPieces.[0].[n - 1] (Int piece.RotationId 8u)));
                                                     Or (piece.Down |> findUp |> Array.filter (fun piece -> piece.Right = 'X') |> Array.map (fun piece -> Eq varPieces.[1].[n] (Int piece.RotationId 8u))) |]
                                 |]
                    | i, 0 when i = n ->
                        let pieces = pieces |> Array.filter (fun piece -> piece.Down = 'X' && piece.Left = 'X')
                        yield Or [| for piece in pieces do
                                        yield And [| Eq varPieces.[n].[0] (Int piece.RotationId 8u);
                                                     Or (piece.Up |> findDown |> Array.filter (fun piece -> piece.Left = 'X') |> Array.map (fun piece -> Eq varPieces.[n - 1].[0] (Int piece.RotationId 8u)));
                                                     Or (piece.Right |> findLeft |> Array.filter (fun piece -> piece.Down = 'X') |> Array.map (fun piece -> Eq varPieces.[n].[1] (Int piece.RotationId 8u))) |]
                                 |]
                    | i, j when i = n && j = n -> 
                        let pieces = pieces |> Array.filter (fun piece -> piece.Down = 'X' && piece.Right = 'X')
                        yield Or [| for piece in pieces do
                                        yield And [| Eq varPieces.[n].[n] (Int piece.RotationId 8u);
                                                     Or (piece.Up |> findDown |> Array.filter (fun piece -> piece.Right = 'X') |> Array.map (fun piece -> Eq varPieces.[n - 1].[n] (Int piece.RotationId 8u)));
                                                     Or (piece.Left |> findRight |> Array.filter (fun piece -> piece.Down = 'X') |> Array.map (fun piece -> Eq varPieces.[n].[n - 1] (Int piece.RotationId 8u))) |]
                                 |]
                    | 0, j ->
                        let pieces = pieces |> Array.filter (fun piece -> piece.Up = 'X' )
                        yield Or [| for piece in pieces do
                                        yield And [| Eq varPieces.[0].[j] (Int piece.RotationId 8u);
                                                     Or (piece.Down |> findUp |> Array.map (fun piece -> Eq varPieces.[1].[j] (Int piece.RotationId 8u)))
                                                     Or (piece.Left |> findRight |> Array.filter (fun piece -> piece.Up = 'X') |> Array.map (fun piece -> Eq varPieces.[0].[j - 1] (Int piece.RotationId 8u)));
                                                     Or (piece.Right |> findLeft |> Array.filter (fun piece -> piece.Up = 'X') |> Array.map (fun piece -> Eq varPieces.[0].[j + 1] (Int piece.RotationId 8u))) |]
                                 |]
                    | i, 0 ->
                        let pieces = pieces |> Array.filter (fun piece -> piece.Left = 'X' )
                        yield Or [| for piece in pieces do
                                        yield And [| Eq varPieces.[i].[0] (Int piece.RotationId 8u);
                                                     Or (piece.Right |> findLeft |> Array.map (fun piece -> Eq varPieces.[i].[1] (Int piece.RotationId 8u)))
                                                     Or (piece.Up |> findDown |> Array.filter (fun piece -> piece.Left = 'X') |> Array.map (fun piece -> Eq varPieces.[i - 1].[0] (Int piece.RotationId 8u)));
                                                     Or (piece.Down |> findUp |> Array.filter (fun piece -> piece.Left = 'X') |> Array.map (fun piece -> Eq varPieces.[i + 1].[0] (Int piece.RotationId 8u))) |]
                                 |]
                    | i, j when i = n ->
                        let pieces = pieces |> Array.filter (fun piece -> piece.Down = 'X' )
                        yield Or [| for piece in pieces do
                                        yield And [| Eq varPieces.[n].[j] (Int piece.RotationId 8u);
                                                     Or (piece.Up |> findDown |> Array.map (fun piece -> Eq varPieces.[n - 1].[j] (Int piece.RotationId 8u)))
                                                     Or (piece.Left |> findRight |> Array.filter (fun piece -> piece.Down = 'X') |> Array.map (fun piece -> Eq varPieces.[n].[j - 1] (Int piece.RotationId 8u)));
                                                     Or (piece.Right |> findLeft |> Array.filter (fun piece -> piece.Down = 'X') |> Array.map (fun piece -> Eq varPieces.[n].[j + 1] (Int piece.RotationId 8u))) |]
                                 |]
                    | i, j when j = n ->
                        let pieces = pieces |> Array.filter (fun piece -> piece.Right = 'X' )
                        yield Or [| for piece in pieces do
                                        yield And [| Eq varPieces.[i].[n] (Int piece.RotationId 8u);
                                                     Or (piece.Left |> findRight |> Array.map (fun piece -> Eq varPieces.[i].[n - 1] (Int piece.RotationId 8u)))
                                                     Or (piece.Up |> findDown |> Array.filter (fun piece -> piece.Right = 'X') |> Array.map (fun piece -> Eq varPieces.[i - 1].[n] (Int piece.RotationId 8u)));
                                                     Or (piece.Down |> findUp |> Array.filter (fun piece -> piece.Right = 'X') |> Array.map (fun piece -> Eq varPieces.[i + 1].[n] (Int piece.RotationId 8u))) |]
                                 |]
                    | i, j -> 
                        let pieces = pieces |> Array.filter (fun piece -> piece.Up <> 'X' && piece.Down <> 'X' && piece.Left <> 'X' && piece.Right <> 'X' )
                        yield Or [| for piece in pieces do
                                        yield And [| Eq varPieces.[i].[j] (Int piece.RotationId 8u);
                                                     Or (piece.Up |> findDown |> Array.map (fun piece -> Eq varPieces.[i - 1].[j] (Int piece.RotationId 8u)))
                                                     Or (piece.Down |> findUp |> Array.map (fun piece -> Eq varPieces.[i + 1].[j] (Int piece.RotationId 8u)));
                                                     Or (piece.Left |> findRight |> Array.map (fun piece -> Eq varPieces.[i].[j - 1] (Int piece.RotationId 8u)));
                                                     Or (piece.Right |> findLeft |> Array.map (fun piece -> Eq varPieces.[i].[j + 1] (Int piece.RotationId 8u))) |]
                                 |] |]

let formula = And [|validValues; distinct; constraints|]

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

let model = solver.Model

for i in {0..dim - 1} do
    for j in {0..dim - 1} do
        let value = string <| model.Evaluate(IntVar (sprintf "Y_%d_%d" i j) 8u)
        printf "%s " value
    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 : unit -> w:uint32 -> BitVecExpr

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 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 Distinct : exprs:Expr [] -> BoolExpr

Full name: Script.Distinct
val exprs : Expr []
Context.MkDistinct([<ParamArray>] args: Expr []) : BoolExpr
type Piece =
  {Id: int;
   RotationId: int;
   Up: char;
   Down: char;
   Left: char;
   Right: char;}

Full name: Script.Piece
Piece.Id: int
Piece.RotationId: int
Piece.Up: char
Multiple items
val char : value:'T -> char (requires member op_Explicit)

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

--------------------
type char = Char

Full name: Microsoft.FSharp.Core.char
Piece.Down: char
Piece.Left: char
Piece.Right: char
val rotations : piece:string -> index:int -> Piece []

Full name: Script.rotations
val piece : string
val index : int
val piece : Piece
val dim : int

Full name: Script.dim
val puzzle : string []

Full name: Script.puzzle
val pieces : Piece [] []

Full name: Script.pieces
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 mapi : mapping:(int -> 'T -> 'U) -> array:'T [] -> 'U []

Full name: Microsoft.FSharp.Collections.Array.mapi
val i : int
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 splitInto : count:int -> array:'T [] -> 'T [] []

Full name: Microsoft.FSharp.Collections.Array.splitInto
val varPieces : Expr [] []

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

Full name: Microsoft.FSharp.Core.ExtraTopLevelOperators.sprintf
val validValues : BoolExpr

Full name: Script.validValues
val pieces : Piece []
val distinct : BoolExpr

Full name: Script.distinct
val tempVars : BitVecExpr [] []
val maps : BoolExpr
val distinctValues : BoolExpr
val map : mapping:('T -> 'U) -> array:'T [] -> 'U []

Full name: Microsoft.FSharp.Collections.Array.map
val v : BitVecExpr
val constraints : BoolExpr

Full name: Script.constraints
val n : int
val findUp : (char -> Piece [])
val c : char
val filter : predicate:('T -> bool) -> array:'T [] -> 'T []

Full name: Microsoft.FSharp.Collections.Array.filter
val findDown : (char -> Piece [])
val findLeft : (char -> Piece [])
val findRight : (char -> Piece [])
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 printf : format:Printf.TextWriterFormat<'T> -> 'T

Full name: Microsoft.FSharp.Core.ExtraTopLevelOperators.printf
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/7TH
Posted:6 years ago
Author:NIck Palladinos
Tags: puzzle , 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.