Z3 QBFの式をpcnfに直接変換する

Question

私はQ3定理証明（Z3Pyを使う：PythonのZ3 API）を使ってQBF（Quantified Boolean formula）を作成しています。

q3の形式でqbfの式を直接Prenex normal formに変換する方法はありますか？

Answer 1

私はPrenexに変換するための戦術はないと思っていますが、確かに定量化 - 除去の戦術を適用し、さらに数式を処理することができます。変換された数式は機械的に生成されるので、実際にはオリジナルのようには見えません。ここで

は例です：ここでは

from z3 import * 

f = Function('f', IntSort(), IntSort(), IntSort()) 
x, y = Ints('x y') 
p = ForAll(x, Or(x == 2, Exists(y, f (x, y) == 0))) 

print Tactic('qe')(p) 

qe記号消去戦術です。これは、生成します。

[[Not(Exists(x!0, 
      Not(Or(x!0 == 2, 
        Exists(x!1, 
          And(f(x!0, x!1) <= 0, 
           f(x!0, x!1) >= 0))))))]] 

を戦術上の素敵なチュートリアルについては、こちらをご覧ください：http://ericpony.github.io/z3py-tutorial/strategies-examples.htm

Answer 2

あなたは定義によってprenexの形態であろうskolemize戦術（SNF）を使用することができます。しかし、それはまたあなたが望むものではない存在量をなくすでしょう。ここに例があります。

(declare-fun a (Int) Bool) 
(declare-fun b (Int) Bool) 
(declare-fun c (Int) Bool) 
(assert 
    (forall ((x Int)) 
    (or 
     (exists ((y Int)) 
     (a y) 
    ) 
     (exists ((z Int)) 
     (=> 
      (b z) 
      (c x) 
     ) 
    ) 
    ) 
) 
) 
(apply 
    (and-then 
    ; mode (symbol) NNF translation mode: skolem (skolem normal form), quantifiers (skolem normal form + quantifiers in NNF), full (default: skolem) 
    (using-params snf :mode skolem) 
) 
    :print_benchmark true 
    :print false 
) 

Z3はそれはあなたがbashシェルから

echo "(help-tactic)" | ./z3 -in | less 

を実行することによって利用できる戦術を見ることができます

(declare-fun c (Int) Bool) 
(declare-fun b (Int) Bool) 
(declare-fun a (Int) Bool) 
(assert (forall ((x Int)) 
      (or (exists ((y Int)) (a y)) (exists ((z Int)) (=> (b z) (c x)))))) 
(check-sat) 

のようなものを使用して応答します上記に与えられています。

残念ながら、私はそれがプレックスへの変換を行っているとは言いません。