2
1

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?

More than 5 years have passed since last update.

F#でZ3

Posted at

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. 最後の出力処理がいまいち。とりあえず出力するようにしただけって感じ。
2
1
0

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
2
1

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?