Sonntag, 25. September 2016

Final notice

Well, this it. No more updates to this blog. Thanks for reading, everyone!
You can load the source from the original site or straight from this link: Click here!

My institute:
My project site:

Jonathan Best: Programmieren in natürlicher Sprache: Der Eingabeassistent "Input & Verify AliceNLP", 2014.

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)

; 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.

Mittwoch, 2. Januar 2013

Using TeXstudio with git

I'm currently in the process of writing the actual document, my study thesis. Per custom, it is written in \mathrm{L\!\!^{{}_{\scriptstyle A}} \!\!\!\!\!\;\; T\!_{\displaystyle E} \! X}. The LaTeX editors for Windows are as bad as they come, but TeXstudio certainly isn't the worst. It also comes with a neat feature that commits your work to a SVN repository whenever you save your files.

Now, I don't use SVN, I use git instead. So I followed this advice on teaching TeXstudio to use git. First, open your command settings at Options → Configure TeXstudio → Commands → SVN and change the values for SVN and SVNADMIN to 'git'.

Then open bash and tell git to use the command 'ci':
git config --global "commit"
There you go. Now you can enable auto-commit at Options → Configure TeXstudio → SVN.
Be advised that these automatic checkins will clutter your repository. It may be a good idea to switch to a different branch before working with TeXstudio and pick/squash the changes to the master branch after you are done.

Dienstag, 4. Dezember 2012

How to run Alloy from the command line

I've recently started evaluating my Alloy models by script. This is a challenge, because Alloy does not offer simple command line parameters in order to be run from promt. However, there is a way, and Felix Chang tells us:
You can invoke it like this: (it will execute every command
in every Alloy file you specified, and if an assertion
has a counterexample, it will show the values of every sig
and every relation in that counterexample)
Here's a sample promt:
java -cp alloy4.jar file1.als file2.als
And the same thing for Alloy 4.2:
java -cp alloy4.2-rc.jar file1.als file2.als
This is actually a different program and it's important to account for the differences.

Mittwoch, 28. November 2012

How to build Z3 for Linux (for non-roots)

Now, suppose you are a normal user without root and you would like to run Z3 on Linux. How should you go about it? This blog posts documents what worked for me and I hope it will for you, too.

Set up a place for Z3 to be downloaded and built:
cd ~  # change to home folder
mkdir repositories  # create a folder called "repositories"
cd repositories  # go there
Once we are there, we can basically follow the readme instructions:
git clone  # downloads z3 source code
python scripts/
cd build
The last step is setting execute permissions on Z3:
chmod 751 z3
That's it! Now you can run Z3 from this path. Try it now:
~/repositories/z3/build/z3 -version

Montag, 19. November 2012

Verifiying proofs with Z3

The Z3 theorem prover has a command for constructing proofs: (get-proof). The resulting files are not meant "for human consumption" and you can probably see why:

((set-logic <null>)
(let ((@x41 (monotonicity (rewrite (= (<= 2 a) (>= a 2))) (= (not (<= 2 a)) (not (>= a 2))))))
(let (($x19 (<= 2 a)))
(let (($x20 (not $x19)))
(let ((@x26 (monotonicity (rewrite (= $x19 $x19)) (= $x20 $x20))))
(let ((@x27 (trans (rewrite (= (< a 2) $x20)) @x26 (= (< a 2) $x20))))
(let (($x7 (< a 2)))
(let ((@x29 (mp (mp (|and-elim| (asserted (and (> a 3) $x7)) $x7) @x27 $x20) @x26 $x20)))
(let ((@x42 (mp (mp (mp @x29 (|rewrite*| (= $x20 $x20)) $x20) @x26 $x20) @x41 (not (>= a 2)))))
(let (($x39 (>= a 2)))
(let (($x15 (not (<= a 3))))
(let ((@x18 (mp (|and-elim| (asserted (and (> a 3) $x7)) (> a 3)) (rewrite (= (> a 3) $x15)) $x15)))
(let ((@x64 (|unit-resolution| ((_ |th-lemma| arith farkas 1 1) (or $x39 (<= a 3))) (mp @x18 (|rewrite*| (= $x15 $x15)) $x15) $x39)))
(|unit-resolution| @x64 @x42 false)))))))))))))))
Looking good, right? Well, hardly.
Even with nicer formatting, line breaks, etc. the proof is not quite readable. Now, it looks like people have actually managed to work with these proofs and I'm quite curious about how they accomplished that. There is a description of all the symbols used in the proof, but what I'm lacking is some kind of command line parameter which simply feeds the proof back into Z3.

If I ever find one (or build one), I'll write down here.