量化公式的奇怪结果

当我使用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

量化公式的奇怪结果

回答

相关问题