Sonntag, 25. September 2016

Troubleshooting with Z3: unknown function/constant

-- Aus dem Archiv / From the archives --
This post is in German.

Fehler sind immer besonders fies. Beim Programmieren tauchen immer Fehler auf, weswegen man sich darauf geeinigt hat, bestimmte Fehler bereits vor dem Erstellen des Programms mit dem Compiler abzufangen. Derart Fehler sind einfach zu finden und oft einfach zu beheben. Oderso glaubt man… In diesem Projekt erzeuge ich "Z3 code" aus Java und lasse den erzeugten Code über die Befehlszeile ausführen. Es ist nicht wirklich schwierig, die relationalen Ausdrücke von Z3 zu erzeugen, aber dennoch passieren einem beim programmieren manchmal recht grundlegende Fehler.

(Ich habe diesen Beitrag irgendwann 2012 verfasst. Ich hoffe, das Problem ist noch aktuell.)

Z3 untersucht das gegebene SMT-Modell auf Unstimmigkeiten und teilt sie dem Benutzer mit. Häufig sieht das dann so aus:(error "line 101 column 30: unknown function/constant in_11")
Dieser Fehler besagt, dass ein im Modell verwendeter Bezeichner “in_11” nicht korrekt deklariert wurde. Z3 hat an dieser Stelle eine Funktion erwartet und keine gefunden. Das kann zwei Ursachen haben:
  1. Die Deklarationen sind unvollständig oder fehlerhaft und wir sollten dafür sorgen, dass “in_11” deklariert wird.
  2. Der Aufruf von “in_11” ist fehlerhaft. In diesem Fall hat man sich möglicherweise vertippt.
In letzterem Fall stellt sich außerdem die Frage, was denn anstelle von “in_11” stehen sollte. Der Kontext zu diesem Fehler ist wie folgt:
;...
(declare-fun in_1 (Atom Rel1) Bool)
(declare-fun in_2 (Atom Atom Rel2) Bool)
(declare-fun join_1x2 (Rel1 Rel2) Rel1)

(assert 
; axiom for join_1x2
  (! 
    (forall ((A Rel1)(B Rel2)(y0 Atom)) (= 
      (in_11 y0 (join_1x2 A B)) 
      (exists ((x Atom)) (and 
        (in_1 x A) 
        (in_2 x y0 B)
      ))
    )) 
    :named ax8 
  ) 
)
Die fehlerhafte Zeile ist ein Aufruf mit zwei Argumenten: y0 und (join_1x2 A B). y0 ist eine durch den Quantor “forall” gebundene Variable mit dem Sort “Atom” und join_1x2 gibt den Sort “Rel1” zurück. Wir wollten also eine Funktion aufrufen, die zwei Argumente vom Typ Atom und Rel1 akzeptiert. Diese Funktion gibt es und sie heißt “in_1”. Die Ursache für unseren Fehler war hier also ein Tippfehler und der Aufruf lautete korrekt:
 (in_1 y0 (join_1x2 A B))
“unknown function/constant” ist ein relativ einfach zu behebender Fehler, wenn man das SMT-Modell von Hand getippt hat.

In meinem Fall wird das Modell automatisch generiert und das bedeutet, dass man nicht nur den Tippfehler korrigieren muss, sondern auch den Code der ihn erzeugt.


Keine Kommentare:

Kommentar veröffentlichen