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」を false (つまり、「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)

私が見る利点は、forall-constraint に触れずに FPolicy(0 1 30) == false のように変更できることです。明らかな欠点は、基本的にすべての引数タプルを 2 回言及する必要があることと、作成されたモデルがかなり複雑になることです。

より良い解決策が見られることを楽しみにしています:-)

于 2012-01-05T08:54:36.830 に答える