Quantifier dans Z3

Question

Fondamentalement, je veux demander Z3 de me donner un entier arbitraire dont la valeur est supérieure à 10. J'écrire les déclarations suivantes:

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

Comment puis-je appliquer cette quantificateurs à mon modèle? Je sais que vous pouvez écrire (affirmer (> x 10)) pour y parvenir. Mais je veux dire que je veux un quantificateur dans mon modèle donc chaque fois que je déclare une constante entière dont la valeur est garantie supérieure à 10. Donc je n'ai pas besoin d'insérer une instruction (assert (> x 10)) pour chaque constante entière déclaré.

Answer 1

Lorsque vous utilisez (assert (forall ((i Int)) (> i 10))), i est une variable liée et la formule quantifiée est équivalente à une valeur de vérité, qui est false dans ce cas.

Je pense que vous voulez définir une macro à l'aide quantificateurs:

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

Et vous pouvez les utiliser pour éviter la répétition de code:

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

Il est essentiellement la façon de définir des macros en utilisant des fonctions non interprétées lorsque vous travaillez avec l'API Z3. Notez que vous devez définir (set-option :macro-finder true) pour que Z3 remplace les quantificateurs universels par les corps de ces fonctions.

Cependant, si vous travaillez avec l'interface textuelle, la macro dans define-fun SMT-LIB v2 est un moyen plus facile de faire ce que vous voulez:

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