Quantificatore in Z3

Question

Fondamentalmente, voglio chiedere Z3 a darmi un intero arbitrario il cui valore è superiore a 10. Così scrivo le seguenti dichiarazioni:

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

Come posso applicare questo quantificatore al mio modello? So che puoi scrivere (asserire (> x 10)) per raggiungere questo obiettivo. Ma voglio dire che voglio un quantificatore nel mio modello così ogni volta che dichiaro una costante intera il cui valore è garantito essere superiore a 10. Quindi non devo inserire istruzioni (assert (> x 10)) per ogni costante intera che dichiarato.

Answer 1

Quando si utilizza (assert (forall ((i Int)) (> i 10))), i è una variabile limitata e la formula quantificata è equivalente a un valore di verità, che in questo caso è false.

penso che si vuole definire una macro utilizzando quantificatori:

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

e si possono utilizzare per evitare di ripetizione del codice:

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

È essenzialmente il modo per definire le macro utilizzando le funzioni non interpretati quando lavori con l'API Z3. Notare che è necessario impostare (set-option :macro-finder true) in modo che Z3 sostituisca i quantificatori universali con corpi di tali funzioni.

Tuttavia, se si sta lavorando con l'interfaccia testuale, la macro define-fun in SMT-LIB V2 è un modo più semplice per fare ciò che si vuole:

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