2 people like it.

Countdown problem via Z3

Countdown problem 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: 

// Countdown problem via Z3

#r "bin/Microsoft.Z3.dll"

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

module Solver = 
    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 Gt : ArithExpr -> ArithExpr -> BoolExpr = fun l r -> ctx.MkGt(l, r) 
    let Le : ArithExpr -> ArithExpr -> BoolExpr = fun l r -> ctx.MkLe(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 Sub : ArithExpr -> ArithExpr -> ArithExpr = fun l r -> ctx.MkSub(l, r)
    let Mul : ArithExpr -> ArithExpr -> ArithExpr = fun l r -> ctx.MkMul(l, r)
    let Div : ArithExpr -> ArithExpr -> ArithExpr = fun l r -> ctx.MkDiv(l, r)
    let Mod : IntExpr -> IntExpr -> IntExpr = fun l r -> ctx.MkMod(l, r)
    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 ArrayVar : string -> ArrayExpr = fun v -> ctx.MkConst(v, ctx.MkArraySort(ctx.IntSort, ctx.IntSort)) :?> _
    let Get : ArrayExpr -> ArithExpr -> ArithExpr = fun array index -> ctx.MkSelect(array, index) :?> _
    let Set : ArrayExpr -> ArithExpr -> ArithExpr -> ArrayExpr = fun array index v -> ctx.MkStore(array, index, v)
    let distinct : Expr[] -> BoolExpr = fun exprs -> ctx.MkDistinct(exprs)


    let eval : (IntExpr * IntExpr) list -> IntExpr -> BoolExpr = fun ops target -> 
        let rec eval' : (IntExpr * IntExpr) list -> IntExpr -> ArrayExpr -> BoolExpr = 
            fun ops sp st ->
                match ops with
                | [] -> And [|Eq (Get st sp) target; Eq sp (Int 1) |]
                | (op, opr) :: ops -> 
                    let sp' = FreshVar ()
                    let validOp = 
                        Ite (Eq op (Int 0)) 
                            (Eq sp' (Add sp (Int 1))) 
                            (Ite (Eq op (Int 1)) 
                                (Eq sp' (Sub sp (Int 1))) 
                                False) :?> BoolExpr
                    let validAdd = 
                        Ite (And [|(Eq op (Int 1)); (Eq opr (Int 0))|])
                             (Le (Get st (Sub sp (Int 1))) (Get st sp))
                             True :?> BoolExpr
                    let validSub = 
                        Ite (And [|(Eq op (Int 1)); (Eq opr (Int 1))|])
                             (Gt (Get st (Sub sp (Int 1))) (Get st sp))
                             True :?> BoolExpr
                    let validMul = 
                        Ite (And [|(Eq op (Int 1)); (Eq opr (Int 2))|])
                             (And [|Not (Eq (Get st (Sub sp (Int 1))) (Int 1));
                                    Not (Eq (Get st sp) (Int 1));
                                    Le (Get st (Sub sp (Int 1))) (Get st sp) |])
                             True :?> BoolExpr
                    let validDiv = 
                        Ite (And [|(Eq op (Int 1)); (Eq opr (Int 3))|])
                             (And [|(Eq (Mod ((Get st (Sub sp (Int 1))) :?> _) ((Get st sp) :?> _)) (Int 0)); 
                                    (Not (Eq (Get st sp) (Int 1)));
                                    (Not (Eq (Get st sp) (Int 0)));|])
                             True :?> BoolExpr
                                                 
                    let st' = 
                        Ite (Eq op (Int 0))
                            (Set st sp' opr)
                            (Ite (Eq op (Int 1))
                                        (Ite (Eq opr (Int 0)) 
                                            (Set st sp' (Add (Get st (Sub sp (Int 1))) (Get st sp))) 
                                            (Ite (Eq opr (Int 1)) 
                                                (Set st sp' (Sub (Get st (Sub sp (Int 1))) (Get st sp))) 
                                                (Ite (Eq opr (Int 2)) 
                                                    (Set st sp' (Mul (Get st (Sub sp (Int 1))) (Get st sp))) 
                                                    (Ite (Eq opr (Int 3)) 
                                                        (Set st sp' (Div (Get st (Sub sp (Int 1))) (Get st sp)))  
                                                        st))))
                                     
                                    st) :?> ArrayExpr
                    And [|validOp; validAdd; validSub; validMul; validDiv; (Gt sp' (Int 0)); eval' ops sp' st'|]

        let sp = IntVar "sp"
        let st = ArrayVar "st"
        And [|(Eq sp (Int 0)); eval' ops sp st;|]

    let rec distinctOperants : (IntExpr * IntExpr) list -> Expr list -> BoolExpr =
        fun ops oprs ->
            match ops with
            | [] -> oprs |> List.toArray |> distinct
            | (op, opr) :: ops -> 
                let opr' = FreshVar ()
                let ite =
                    Ite (Eq op (Int 0))
                        (Eq opr opr')
                        True :?> BoolExpr
                And [|ite; distinctOperants ops ((opr' :> _) :: oprs)|]

    let rec rpnEval : (int * int) list -> int list -> int list =
        fun ops st ->
            match ops with
            | [] -> st 
            | (op, opr) :: ops -> 
                match op with
                | 0 -> rpnEval ops (opr :: st)
                | 1 -> 
                    match st with
                    | x :: y :: st' ->
                        match opr with
                        | 0 -> rpnEval ops ((y + x) :: st')
                        | 1 -> rpnEval ops ((y - x) :: st')
                        | 2 -> rpnEval ops ((y * x) :: st')
                        | 3 -> rpnEval ops ((y / x) :: st')
                        | _ -> failwith "oups"
                    | _ -> failwith "oups"
                | _ -> failwith "oups"


    let solve : int list -> int -> int -> (int * int) list option = 
        fun nums target numOfInstrs ->
            let ops = [ for i in {0..numOfInstrs - 1} -> (IntVar (sprintf "op-%d" i), IntVar (sprintf "opr-%d" i)) ]
            let validEval = eval ops (Int target)
            let validRanges = 
                And 
                    [| for (op, opr) in ops do
                            yield Ite (Eq op (Int 0)) 
                                    (Or [| for num in nums -> Eq opr (Int num) |])
                                    (Or [| for i in {0..3} -> Eq opr (Int i)|]) :?> BoolExpr
                    |]

            let validDistinctOprs = distinctOperants ops []
            let solver = ctx.MkSolver()
            solver.Assert(And [|validRanges; validDistinctOprs; validEval|])
            if solver.Check() = Status.SATISFIABLE then
                let model = solver.Model
                let ops' = [ for (op, opr) in ops -> (Int32.Parse(string (model.Evaluate(op)))), (Int32.Parse (string (model.Evaluate(opr)))) ]
                if rpnEval ops' [] = [target] then
                    Some ops'
                else failwith "oups"
            else None
            

let nums = [1; 3; 7; 10; 25; 50]
let target = 765

Solver.solve nums target 7
namespace System
namespace System.IO
namespace System.Runtime
namespace System.Runtime.InteropServices
namespace System.Collections
namespace System.Collections.Generic
namespace Microsoft
namespace Microsoft.Z3
type Solver =
  inherit Z3Object
  member Add : [<ParamArray>] constraints:BoolExpr[] -> unit
  member Assert : [<ParamArray>] constraints:BoolExpr[] -> unit
  member AssertAndTrack : constraints:BoolExpr[] * ps:BoolExpr[] -> unit + 1 overload
  member Assertions : BoolExpr[]
  member Check : [<ParamArray>] assumptions:Expr[] -> Status
  member Consequences : assumptions:IEnumerable<BoolExpr> * variables:IEnumerable<Expr> * consequences:BoolExpr[] -> Status
  member Help : string
  member Model : Model
  member NumAssertions : uint32
  member NumScopes : uint32
  ...

Full name: Microsoft.Z3.Solver
val ctx : Context

Full name: Script.Solver.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.Solver.True
type BoolExpr =
  inherit Expr

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

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

Full name: Script.Solver.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.Solver.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.Solver.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.Solver.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 Gt : l:ArithExpr -> r:ArithExpr -> BoolExpr

Full name: Script.Solver.Gt
type ArithExpr =
  inherit Expr

Full name: Microsoft.Z3.ArithExpr
val l : ArithExpr
val r : ArithExpr
Context.MkGt(t1: ArithExpr, t2: ArithExpr) : BoolExpr
val Le : l:ArithExpr -> r:ArithExpr -> BoolExpr

Full name: Script.Solver.Le
Context.MkLe(t1: ArithExpr, t2: ArithExpr) : BoolExpr
val Ite : p:BoolExpr -> t:Expr -> e:Expr -> Expr

Full name: Script.Solver.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.Solver.Add
Context.MkAdd(t: IEnumerable<ArithExpr>) : ArithExpr
Context.MkAdd([<ParamArray>] t: ArithExpr []) : ArithExpr
val Sub : l:ArithExpr -> r:ArithExpr -> ArithExpr

Full name: Script.Solver.Sub
Context.MkSub([<ParamArray>] t: ArithExpr []) : ArithExpr
val Mul : l:ArithExpr -> r:ArithExpr -> ArithExpr

Full name: Script.Solver.Mul
Context.MkMul(t: IEnumerable<ArithExpr>) : ArithExpr
Context.MkMul([<ParamArray>] t: ArithExpr []) : ArithExpr
val Div : l:ArithExpr -> r:ArithExpr -> ArithExpr

Full name: Script.Solver.Div
Context.MkDiv(t1: ArithExpr, t2: ArithExpr) : ArithExpr
val Mod : l:IntExpr -> r:IntExpr -> IntExpr

Full name: Script.Solver.Mod
val l : IntExpr
val r : IntExpr
Context.MkMod(t1: IntExpr, t2: IntExpr) : IntExpr
val And : bools:BoolExpr [] -> BoolExpr

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

Full name: Script.Solver.Or
Context.MkOr(t: IEnumerable<BoolExpr>) : BoolExpr
Context.MkOr([<ParamArray>] t: BoolExpr []) : BoolExpr
val Not : bool:BoolExpr -> BoolExpr

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

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

Full name: Microsoft.FSharp.Core.bool
Context.MkNot(a: BoolExpr) : BoolExpr
val ArrayVar : v:string -> ArrayExpr

Full name: Script.Solver.ArrayVar
type ArrayExpr =
  inherit Expr

Full name: Microsoft.Z3.ArrayExpr
val v : string
Context.MkConst(f: FuncDecl) : Expr
Context.MkConst(name: string, range: Sort) : Expr
Context.MkConst(name: Symbol, range: Sort) : Expr
Context.MkArraySort(domain: Sort, range: Sort) : ArraySort
property Context.IntSort: IntSort
val Get : array:ArrayExpr -> index:ArithExpr -> ArithExpr

Full name: Script.Solver.Get
Multiple items
val array : ArrayExpr

--------------------
type 'T array = 'T []

Full name: Microsoft.FSharp.Core.array<_>
val index : ArithExpr
Context.MkSelect(a: ArrayExpr, i: Expr) : Expr
Multiple items
val Set : array:ArrayExpr -> index:ArithExpr -> v:ArithExpr -> ArrayExpr

Full name: Script.Solver.Set

--------------------
module Set

from Microsoft.FSharp.Collections

--------------------
type Set<'T (requires comparison)> =
  interface IComparable
  interface IEnumerable
  interface IEnumerable<'T>
  interface ICollection<'T>
  new : elements:seq<'T> -> Set<'T>
  member Add : value:'T -> Set<'T>
  member Contains : value:'T -> bool
  override Equals : obj -> bool
  member IsProperSubsetOf : otherSet:Set<'T> -> bool
  member IsProperSupersetOf : otherSet:Set<'T> -> bool
  ...

Full name: Microsoft.FSharp.Collections.Set<_>

--------------------
new : elements:seq<'T> -> Set<'T>
val v : ArithExpr
Context.MkStore(a: ArrayExpr, i: Expr, v: Expr) : ArrayExpr
val distinct : exprs:Expr [] -> BoolExpr

Full name: Script.Solver.distinct
val exprs : Expr []
Context.MkDistinct([<ParamArray>] args: Expr []) : BoolExpr
val eval : ops:(IntExpr * IntExpr) list -> target:IntExpr -> BoolExpr

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

Full name: Microsoft.FSharp.Collections.list<_>
val ops : (IntExpr * IntExpr) list
val target : IntExpr
val eval' : ((IntExpr * IntExpr) list -> IntExpr -> ArrayExpr -> BoolExpr)
val sp : IntExpr
val st : ArrayExpr
val op : IntExpr
val opr : IntExpr
val sp' : IntExpr
val validOp : BoolExpr
val validAdd : BoolExpr
val validSub : BoolExpr
val validMul : BoolExpr
val validDiv : BoolExpr
val st' : ArrayExpr
val distinctOperants : ops:(IntExpr * IntExpr) list -> oprs:Expr list -> BoolExpr

Full name: Script.Solver.distinctOperants
val oprs : Expr list
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 toArray : list:'T list -> 'T []

Full name: Microsoft.FSharp.Collections.List.toArray
val opr' : IntExpr
val ite : BoolExpr
val rpnEval : ops:(int * int) list -> st:int list -> int list

Full name: Script.Solver.rpnEval
val ops : (int * int) list
val st : int list
val op : int
val opr : int
val x : int
val y : int
val st' : int list
val failwith : message:string -> 'T

Full name: Microsoft.FSharp.Core.Operators.failwith
val solve : nums:int list -> target:int -> numOfInstrs:int -> (int * int) list option

Full name: Script.Solver.solve
type 'T option = Option<'T>

Full name: Microsoft.FSharp.Core.option<_>
val nums : int list
val target : int
val numOfInstrs : int
val i : int
val sprintf : format:Printf.StringFormat<'T> -> 'T

Full name: Microsoft.FSharp.Core.ExtraTopLevelOperators.sprintf
val validEval : BoolExpr
val validRanges : BoolExpr
val num : int
val validDistinctOprs : BoolExpr
val solver : Solver
Context.MkSolver(t: Tactic) : Solver
Context.MkSolver(logic: string) : Solver
Context.MkSolver(?logic: Symbol) : Solver
Solver.Assert([<ParamArray>] constraints: BoolExpr []) : unit
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
property Solver.Model: Model
val ops' : (int * int) list
type Int32 =
  struct
    member CompareTo : value:obj -> int + 1 overload
    member Equals : obj:obj -> bool + 1 overload
    member GetHashCode : unit -> int
    member GetTypeCode : unit -> TypeCode
    member ToString : unit -> string + 3 overloads
    static val MaxValue : int
    static val MinValue : int
    static member Parse : s:string -> int + 3 overloads
    static member TryParse : s:string * result:int -> bool + 1 overload
  end

Full name: System.Int32
Int32.Parse(s: string) : int
Int32.Parse(s: string, provider: IFormatProvider) : int
Int32.Parse(s: string, style: Globalization.NumberStyles) : int
Int32.Parse(s: string, style: Globalization.NumberStyles, provider: IFormatProvider) : int
Model.Evaluate(t: Expr, ?completion: bool) : Expr
union case Option.Some: Value: 'T -> Option<'T>
union case Option.None: Option<'T>
val nums : int list

Full name: Script.nums
val target : int

Full name: Script.target
Raw view Test code New version

More information

Link:http://fssnip.net/7TB
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.