kwantyfikatorów w Z3

Question

Zasadniczo, chcę zapytać Z3 mi dać dowolną liczbą całkowitą, której wartość jest większa niż 10. Więc piszę następujące oświadczenia:

(declare-const x (Int)) 
(assert (forall ((i Int)) (> i 10))) 
(check-sat) 
(get-value(x)) 

Jak mogę zastosować ten kwantyfikator do mojego modelu? Wiem, że możesz napisać (assert (> x 10)), aby to osiągnąć. Ale chodzi mi o to, że chcę kwantyfikatora w moim modelu, więc za każdym razem, gdy deklaruję stałą całkowitą, której wartość jest gwarantowana, jest większa niż 10. Więc nie muszę wstawiać instrukcji (assert (> x 10)) dla każdej stałej liczby całkowitej, która zdeklarowany.

Answer 1

Podczas korzystania (assert (forall ((i Int)) (> i 10))), i jest zmienna i ograniczoną ilościowo formuła jest równoważna wartości prawdy, która jest false w tym przypadku.

myślę chcesz zdefiniować makro z użyciem kwantyfikatorów:

(declare-fun greaterThan10 (Int) Bool) 
(assert (forall ((i Int)) (= (greaterThan10 i) (> i 10)))) 

I można z nich korzystać, aby uniknąć kodu powtórzenia:

(declare-const x (Int)) 
(declare-const y (Int)) 
(assert (greaterThan10 x)) 
(assert (greaterThan10 y)) 
(check-sat) 

To jest w istocie sposobem definiowania makr przy użyciu funkcji zinterpretowane kiedy pracujesz z interfejsem API Z3. Zauważ, że musisz ustawić (set-option :macro-finder true), aby Z3 zastąpił kwantyfikatory uniwersalne ciałami tych funkcji.

Jednakże, jeśli pracujesz z interfejsem tekstowym, makro define-fun w SMT-lib v2 jest łatwiejszy sposób, aby robić to, co chcesz:

(define-fun greaterThan10 ((i Int)) Bool 
    (> i 10))