F#でZ3

F#からSMTソルバのz3を使ってみようと思った。
4-queens puzzle using z3-haskell HEAD と同じような書き方ができるかちょっと実験。

open Microsoft.Z3

module Z3Module =
    type Z3_() =
        let ctx = new Context()
        member val Context = ctx with get
        member val Solver = ctx.MkSolver() with get
        member val Status = Status.UNKNOWN with get, set
        member val Values : string list = [] with get, set

    type Expr2 =
        | IntExpr2 of IntExpr
        | BoolExpr2 of BoolExpr
        | ArithExpr2 of ArithExpr
        | IntExpr3 of int
        | AbsExpr2 of Expr2
        | NotExpr2 of Expr2
        | EqExpr2 of Expr2 * Expr2
        | LeExpr2 of Expr2 * Expr2
        | AndExpr2 of Expr2 * Expr2
        | SubExpr2 of Expr2 * Expr2
        | DistinctExpr2 of Expr2 list

        static member Abs (x: Expr2) = AbsExpr2 x
        static member Not (x: Expr2) = NotExpr2 x

        static member (-) (x: Expr2, y: Expr2) = SubExpr2(x, y)

        static member (==*) (x : int, y: int) = EqExpr2(IntExpr3(x), IntExpr3(y))
        static member (==*) (x : Expr2, y: int) = EqExpr2(x, IntExpr3(y))
        static member (==*) (x : int, y: Expr2) = EqExpr2(IntExpr3(x), y)
        static member (==*) (x : Expr2, y: Expr2) = EqExpr2(x, y)
        static member (<=*) (x : int, y: int) = LeExpr2(IntExpr3(x), IntExpr3(y))
        static member (<=*) (x : Expr2, y: int) = LeExpr2(x, IntExpr3(y))
        static member (<=*) (x : int, y: Expr2) = LeExpr2(IntExpr3(x), y)
        static member (<=*) (x : Expr2, y: Expr2) = LeExpr2(x, y)

        static member (&&*) (x: Expr2, y: Expr2) = AndExpr2(x, y)

        static member Distinct (x: Expr2 list) = DistinctExpr2 x

    let intConst (ctx : Context) (name: string) = Expr2.IntExpr2(ctx.MkIntConst(name))
    let not_ (x: Expr2) = Expr2.Not x
    let distinct (x : Expr2 list) = Expr2.Distinct x
    let rec makeExpr (e : Expr2) (ctx : Context) =
        match e with
        | IntExpr3(x) -> ctx.MkInt(x) :> Expr
        | BoolExpr2(x) -> x :> Expr
        | IntExpr2(x) -> x :> Expr
        | ArithExpr2(x) -> x :> Expr
        | EqExpr2(x, y) -> ctx.MkEq((makeExpr x ctx), (makeExpr y ctx)) :> Expr
        | LeExpr2(x, y) -> ctx.MkLe((makeExpr x ctx) :?> ArithExpr, (makeExpr y ctx) :?> ArithExpr) :> Expr
        | SubExpr2(x, y) -> ctx.MkSub((makeExpr x ctx) :?> ArithExpr, (makeExpr y ctx) :?> ArithExpr) :> Expr
        | AndExpr2(x, y) -> ctx.MkAnd((makeExpr x ctx) :?> BoolExpr, (makeExpr y ctx) :?> BoolExpr) :> Expr
        | AbsExpr2(x) ->
            let x0 = (makeExpr x ctx) :?> ArithExpr
            ctx.MkITE(ctx.MkGe(x0, ctx.MkInt(0)), x0, ctx.MkUnaryMinus(x0))
        | NotExpr2(x) -> ctx.MkNot((makeExpr x ctx) :?> BoolExpr) :> Expr
        | DistinctExpr2(x) -> 
            ctx.MkDistinct(x |> List.map (fun z -> makeExpr z ctx) |> List.toArray) :> Expr
    let assert_ (x : Expr2) (ctx : Context) (sol : Solver) = sol.Assert(makeExpr x ctx :?> BoolExpr)
    let evalT (x : Expr2 list) (m : Model) (ctx: Context) =
        x
        |> List.map
            (fun e ->
                let j = makeExpr e ctx
                m.Evaluate(j).ToString())
    let checkModel (f : Model -> Context -> string list) (ctx : Context) (sol : Solver) =
        let status = sol.Check ()
        (status, if status.HasFlag(Status.SATISFIABLE) then f sol.Model ctx else [])
    let evalZ3 (z3 : Z3_) (f : string -> unit) =
        f(z3.Status.ToString())
        f(System.String.Join(", ", z3.Values |> List.toArray))
        let ss =
            z3.Solver.Statistics.Entries
            |> Seq.map (fun x -> x.Key + ": " + x.Value)
            |> Seq.toArray
        f(System.String.Join(", ", ss))

open Z3Module

type Z3Builder() =
    let z3 = new Z3_()
    let mutable c = 0
    member x.Bind(comp, (func: Expr2 -> 'a)) =
        let name = "p" + (c.ToString())
        c <- c + 1
        name |> (comp z3.Context) |> func  
    member x.Bind(comp, (func: unit -> 'a)) =
        comp z3.Context z3.Solver
        func()
    member x.ReturnFrom (f: Context -> Solver -> Status * (string list)) =
        let (status, values) = (f z3.Context z3.Solver)
        z3.Status <- status
        z3.Values <- values
        z3

let z3  = new Z3Builder()

[<EntryPoint>]
let main argv = 
    let x = 
        z3 {
            let diagonal r c r' c' = abs(c'-c) ==* abs(r'-r)
            let! q1 = intConst
            let! q2 = intConst
            let! q3 = intConst
            let! q4 = intConst
            do! assert_ ((1 <=* q1) &&* (q1 <=* 4))
            do! assert_ ((1 <=* q2) &&* (q2 <=* 4))
            do! assert_ ((1 <=* q3) &&* (q3 <=* 4))
            do! assert_ ((1 <=* q4) &&* (q4 <=* 4))
            do! assert_ (distinct [q1;q2;q3;q4])
            do! assert_ (not_ (diagonal 1 q1 2 q2))
            do! assert_ (not_ (diagonal 1 q1 3 q3))
            do! assert_ (not_ (diagonal 1 q1 4 q4))
            do! assert_ (not_ (diagonal 2 q2 3 q3))
            do! assert_ (not_ (diagonal 2 q2 4 q4))
            do! assert_ (not_ (diagonal 3 q3 4 q4))
            return! checkModel (evalT [q1;q2;q3;q4])
        }
    Z3Module.evalZ3 x (fun s -> printfn "%s" s)
    0 

結果

---

SATISFIABLE
2, 4, 1, 3
conflicts: 7, decisions: 22, propagations: 105, binary propagations: 66, final checks: 1, added eqs: 8, mk clause: 69, del clause: 15, arith conflicts: 4, add rows: 30, pivots: 15, assert lower: 45, assert upper: 50, assert diseq: 37, bound prop: 19, fixed eqs: 3, offset eqs: 4, eq adapter: 18

---

やってみたはいいが疑問点。

1. コンピュテーション式を使ったのはいいのだけど、let!, do!, return! を使うので良いのか？
2. 数値とIntConstを比較するところの演算子定義が力技すぎる気が。
3. 最後の出力処理がいまいち。とりあえず出力するようにしただけって感じ。