z3 - 定量化された式による奇妙な結果

Question

ForAll 量指定子を使用すると、奇妙な結果が得られます。私の目標は、関数 foo の解釈を次のように制限することです。

\Ax,y. foo(x,y)= if x=A && y=B then C1 else C2

したがって、上記をコンテキストにアサートすると、本質的に上記と同等の foo の解釈が返されます。しかし、私はしません。私が返すのは次のようなものです

foo(x,y)= if x=A && y=B then C1 else C1

そして、私には理由がわかりません。私が使用しているコードは以下のとおりです (.net API 経由で Z3 にアクセス)

let ctx = new Context()
let Sort1 = ctx.MkEnumSort("S1", [|"A";"AA"|])
let Sort2 = ctx.MkEnumSort("S2", [|"B"|])
let Sort3 = ctx.MkEnumSort("S3", [|"C1";"C2"|]) 
let s1 = ctx.MkSymbol "s1"
let s2 = ctx.MkSymbol "s2"
let types = [|Sort1:>Sort; Sort2:>Sort |]
let names = [|s1:>Symbol ; s2:>Symbol|]
let vars = [| ctx.MkConst(names.[0],types.[0]);ctx.MkConst(names.[1],types.[1])|]

let FDecl = ctx.MkFuncDecl("foo", [|Sort1:>Sort;Sort2:>Sort|], Sort3) 
let f_body = ctx.MkITE(ctx.MkAnd(ctx.MkEq(vars.[0],getZ3Id("A",Sort1)), 
                                 ctx.MkEq(vars.[1], getZ3Id("B",Sort2))),
                       getZ3Id("C1",Sort3), 
                       getZ3Id("C2",Sort3)) 
let f_app = FDecl.Apply vars //ctx.MkApp(FDecl, vars)
let body = ctx.MkEq(f_app, f_body)

let std_weight = uint32 1
let form = ctx.MkForall(types, names, body, std_weight, null, null, null, null) 
           :> BoolExpr
let s = ctx.MkSolver() 
satisfy s [|form|]
s.Model

getZ3Id指定された文字列を Enum 内の対応する定数に変換する場所

let getZ3Id (id,sort:EnumSort) = 
  let matchingConst zconst = zconst.ToString().Equals(id)
  Array.find matchingConst sort.Consts

そしてsatisfy、次のとおりです。

let satisfy (s:Solver) formula =
    s.Assert (formula)
    let res = s.Check() 
    assert (res = Status.SATISFIABLE)
    s.Model

モデルは、何があっても C1 を返す foo の解釈を返します

(define-fun foo ((x!1 S1) (x!2 S2)) S3
  (ite (and (= x!1 A) (= x!2 B)) C1
    C1))

誰かが私が間違っているところを指摘できますか? ありがとう PS また、MkForAll への 2 つの API 呼び出しの違いは何ですか?

---

これが私のさらなる問題です：私が定義した場合

let set1 = Set.map (fun (p:string)-> ctx.MkConst(p,Sort3)) 
                   (new Set<string>(["C1"]))

fの本体を変更します

let f_body = ctx.MkITE(ctx.MkAnd(ctx.MkEq(vars.[0],getZ3Id("A",Sort1))), 
                                 ctx.MkEq(vars.[1], getZ3Id("B",Sort2))),
                       mkZ3Set ctx set1,
                       ctx.MkEmptySet Sort3)

どこ

let mkZ3Set (ctx:Context) exprs sort =
  Set.fold (fun xs x-> ctx.MkSetAdd(xs,x)) (ctx.MkEmptySet(sort)) exprs

Z3式は合理的に見えます

form= (forall ((s1 S1))
  (= (foo s1)
     (ite (and (= s1 A))
          (store ((as const (Array S3 Bool)) false) C1 true)
          ((as const (Array S3 Bool)) false))))

それでも Z3 は Unsatisfiable を返します。なぜか教えてくれますか？