量化公式的奇怪結果

當我使用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給定的字符串轉換爲相應的恆定在枚舉

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

該模型返回foo的解釋，返回C1無論如何

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

有人能指出我要去哪裏嗎？謝謝 PS MkForAll的兩個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。你能告訴我爲什麼嗎？

來源

2013-04-11 S.N.

是的，這看起來很奇怪。我正在研究它。 – 2013-04-12 01:51:11

好的謝謝。但是我現在還有一個問題。如果我將Foo的返回類型更改爲Sort3的集合而不是Sort3，並將約束更改爲返回某個集合，則它變得不可滿足，並且我不知道爲什麼。 UNF。 S/O不允許你在回覆框中做很多格式化，所以我「回答了我自己的問題」。請看看那裏 – 2013-04-13 03:31:43

我正要澄清Z3不返回Unsatisfiable但未知。經過一番探討，我認爲我的問題可能與MBQI有關，並且需要開啓。但是我不知道如何通過API來做到這一點。（這對主要的Z3文檔頁面沒有任何幫助，因爲有些類的鏈接如'STATUS'，我已經在codeplex上提交了一個錯誤報告。用戶指南介紹瞭如何僅爲SMTLIB接口打開它 – 2013-04-13 05:04:48

問題是量詞抽象。它不抽象你想要的變量。

let form = ctx.MkForall(types, names, body, std_weight, null, null, null, null) 
     :> BoolExpr

應改爲：

let form = ctx.MkForall(vars, body, std_weight, null, null, null, null) 
     :> BoolExpr

的背景是，Z3公開爲您量化變量兩種不同的方式。

選項1：您可以抽象出現在公式中的常量。您應該將這些常量的數組傳遞給量詞抽象。這是我更正使用的版本。選項2：您可以抽象公式中出現的de-Brujin指數。然後，您可以使用您在示例中使用的ctx.MkForall的重載。但它要求每當你引用一個綁定變量時，你就使用一個綁定索引（使用ctx.MkBound創建的東西）。

來源

2013-04-12 04:50:58

量化公式的奇怪結果

回答

相關問題