Z3 QBF 수식을 직접 pcnf로 변환

Question

저는 Z3 정리 프로버 (Z3Py : 파이썬의 Z3 API 사용)를 사용하여 QBF (Quantified Boolean formula)를 만듭니다.

Q3에서 qbf 수식을 Prenex normal form으로 직접 변환 할 수있는 방법이 있습니까?

Answer 1

나는 Prenex로 전환 할 전술이 있다고 생각하지 않지만, 수량 한정 제거 전술을 적용하고 공식을 더 처리 할 수는 있습니다. 변환 된 수식은 실제로 기계적으로 생성되므로 원본처럼 보이지 않습니다.

다음은 예입니다 :

여기 qe

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) 

은 정량 제거 전술이다. 이것은 생산 :

[[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)를 사용할 수 있습니다. 그러나 그것은 또한 당신이 원하는 것과는 다른 존재 한정어를 제거 할 것입니다. 여기에 예제가 있습니다. 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) 

같은 것을 응답한다 주어진다

(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 
) 

.

불행히도 나는 그것이 prenex 로의 변환을 언급 한 것을 볼 수 없습니다.