Quantifizierer und Arrays in Z3

Question

Z3 antwortet mit "unbekannt", wenn Sie diesen Code mit quantifiers über Arrays gegeben:

(declare-const ia Int) 
(declare-const ib Int) 
(declare-const la Int) 
(declare-const lb Int) 
(declare-const A (Array Int Int)) 
(declare-const a (Array Int Int)) 
(declare-const b (Array Int Int)) 

(assert 
    (exists 
     ((ia_1 Int) (ia_2 Int) (ib_1 Int) (la_0 Int) (lb_0 Int) (A_0 (Array Int Int)) (a_0 (Array Int Int)) (b_0 (Array Int Int))) 
     (and (= ia ia_2) (= ib ib_1) (= la la_0) (= lb lb_0) (= A A_0) (= a a_0) (= b b_0) (= ia_1 0) (= ib_1 0) (< ia_1 la_0) (< ib_1 lb_0) (< (select a_0 ia_1) (select b_0 ib_1)) (= ia_2 (+ ia_1 1))))) 

(assert 
    (not 
     (exists 
      ((ia_1 Int) (ib_1 Int) (la_0 Int) (lb_0 Int) (A_0 (Array Int Int)) (a_0 (Array Int Int)) (b_0 (Array Int Int))) 
      (and (= ia ia_1) (= ib ib_1) (= la la_0) (= lb lb_0) (= A A_0) (= a a_0) (= b b_0) (= ib_1 0))))) 

(check-sat) 

Gibt es eine Möglichkeit, die richtige Antwort ("unsat") in einem solchen Fall zu erhalten?

edit: Z3 antwortet korrekt mit "sat", wenn z. B. die Bedingung (= ia_1 0) zur zweiten Konjunktion hinzugefügt wird.

Answer 1

Hier ist "unbekannt" eine "richtige" Antwort. Im Allgemeinen sind Quantifizierer über Arrays nicht entscheidbar (zumindest nicht unter weiteren Annahmen). Z3 gibt dieses Beispiel auf, weil seine Standard-Quantifiziererinstantiierungsheuristiken nicht die richtigen Instanziierungsmuster aufgreifen. Weitere Informationen finden Sie im Abschnitt quantifiers in the Z3 tutorial.

Wir können unsere eigenen Instanziierungsmuster angeben, um Z3 zu helfen, oder wir können zumindest das Problem neu formulieren, damit die Heuristiken die richtigen Muster automatisch finden. In diesem Fall war ich erfolgreich durch die zweite quantifier Umschreiben etwa so:

(assert 
    (forall ((la_0 Int) (lb_0 Int) (A_0 (Array Int Int))) 
      (and 
       (= A A_0) 
       (= la la_0) 
       (= lb lb_0) 
       (forall ((b_0 (Array Int Int)) (ib_1 Int)) 
        (and 
         (= b b_0) 
         (= ib ib_1) 
         (= ib_1 0) 
         (forall ((a_0 (Array Int Int)) (ia_1 Int)) 
          (not (and (= ia ia_1) (= a a_0))))      
         ))))) 

Mit weniger Argumenten für jeden Unter quantifier, stehen die Chancen besser, dass es etwas abholen nützlich (glaube ich), aber das wird natürlich nicht immer genug.