3

我有一个快速的问题。我编写了一个简单的程序（使用 Z3 NET API）并得到如下输出。

程序（部分）：

        Sort[] domain = new Sort[3];
        domain[0] = intT;  
        domain[1] = intT;          
        domain[2] = intT;  
        FPolicy = z3.MkFuncDecl("FPolicy", domain, boolT);      

        Term[] args = new Term[3];
        args[0] = z3.MkNumeral(0, intT);
        args[1] = z3.MkNumeral(1, intT);
        args[2] = z3.MkNumeral(30, intT);
        z3.AssertCnstr(z3.MkApp(FPolicy, args));

        args[1] = z3.MkNumeral(2, intT);
        args[2] = z3.MkNumeral(20, intT);
        z3.AssertCnstr(z3.MkApp(FPolicy, args));

输出：

FPolicy -> {
  0 1 30 -> true
  0 2 20 -> true     
  else -> true
}

我想知道我是否可以将“else -> true”设为假（即“else -> false”）。

4

2 回答 2

4
于 2012-01-05T18:23:44.573 回答
1

下面的（RiSE4fun 链接）怎么样？

(set-option :MBQI true)

(declare-fun FPolicy (Int Int Int) Bool)

(assert (forall ((x1 Int) (x2 Int) (x3 Int)) (!
  (implies
    (not
      (or
        (and (= x1 0) (= x2 1) (= x3 30))
        (and (= x1 0) (= x2 2) (= x3 20))))
      (= (FPolicy x1 x2 x3) false))
  :pattern (FPolicy x1 x2 x3))))

(assert (FPolicy 0 1 30))
(assert (FPolicy 0 2 20))

(check-sat)
(get-model)

我可以看到的优势是您可以将其更改为 FPolicy(0 1 30) == false 而无需触及 forall-constraint。明显的缺点是您基本上必须两次提及所有参数元组，并且创建的模型相当复杂。

我期待看到更好的解决方案:-)

于 2012-01-05T08:54:36.830 回答