PSI: P-Stable semantics implementation
From this site is possible to download the source code of the prototype implementing P-Stable semantic with simplification capabilitites.
Note that the prototype has been tested only under linux. The makefile included refers to an older version and DO NOT work.
The tool has been written with java 1.6 in mind, use older versions at your own risk. In order to make it works you must add to your classpath the Apache foundation IO-Commons utilities avaliable at this addresshttp://commons.apache.org/io/index.html
The prototype makes use of two external programs
- Lparse, which is responsable of the grounding of the programs.
- Minisat, the SAT-solver which computes the models. I'm using a slightly modified version which doesn't print all the output of the original one but just informations about satisfiability and the found model in case of positive answer. So, don't use the version avaliable at its web site but this one: minisat_1.14.tar.gz. This is a precompiled version for linux, if you want the source code of this modified version click here
Note that this two programs are executed using the method exec of the class Runtime of java. The prototype looks for them in a folder named "tools" (capitalization matter) which must be created inside the working directory. I succesfully compiled both of them under windows but the procedure was quite cocumbersome. By the way the prototype is likely not going to work under windows because of some recent changes I did when I included the simplification routine. Maybe in the future a working version for window will be published.
HOW TO COMPILE
- mkdir Pstable; cd Pstable/
- mkdir tools
- mkdir lib
- mkdir bin
- copy Lparse and Minisat in tools/
- copy the Apache foundation IO-Commons in lib/
- cd src/
- javac -classpath ../lib/commons-io-1.4.jar:. main/PSI.java -d ../bin