1

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

wheregetZ3Id将给定的字符串转换为 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

该模型返回对 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。你能告诉我为什么吗？

4

1 回答 1

1

问题是量词抽象。它不会抽象您想要的变量。

 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-12T04:50:58.233 回答