-
Notifications
You must be signed in to change notification settings - Fork 1
Requirements
- Python
- CPU
- PySTP build instructions
Nice requires a Python interpreter to run. In particular the standard C/Python implementation from python.org, version 2.6 or later, is required to successfully run the symbolic engine. The current version is developed and tested with versions 2.6/2.7 available in Debian and Ubuntu.
If graph generation is enabled (option -g <file.dot>), the pydot module is required.
The symbolic interpreter uses the STP solver library and the pystp Python bindings. They are the only pieces of code that need to be compiled.
The Nice distribution contains a version of pystp.so (that contains STP linked statically) compiled for Linux on Intel x64 (64 bit). While compiling STP on Linux is straightforward, pystp could require some changes to the Makefile.
A version compiled for a 32 bit architecture is available under third_party/lib32/pystp.so. You should copy that file in sym_exec/symbolic and overwrite the 64 bits one.
You will know that there is an architecture compatibility problem if NICE reports:
nice.utils: Cannot import <path-to-pystp.so>: wrong ELF class: ELFCLASS64
Both binary versions are compiled on Ubuntu 11.10 and are known to work on Ubuntu 11.04 and Debian 6.0.3.
PySTP is available on Google Code: http://code.google.com/p/pystp/
The current version of PySTP tries to link with a dynamic version of libstp, creating it on the fly during compilation. This fails because the STP library does no longer contain all the files pystp expects.
Also, on 64 bits (x86_64) machines, libstp.a needs to be compiled with -fPIC:
--- scripts/Makefile.common (revision 1434)
+++ scripts/Makefile.common (working copy)
@@ -10,7 +10,7 @@
-include $(TOP)/scripts/config.info
-OPTIMIZE = -O3 -DNDEBUG -march=native -fomit-frame-pointer # Optimization
+OPTIMIZE = -O3 -DNDEBUG -march=native -fomit-frame-pointer -fpic # Optimization
#OPTIMIZE = -O3 -g # Debug
# To enable 128-bit indices in the array propagators. Put the INDICES_128BITS
We found that pystp.so can be linked against libstp.a (the static version), simply by changing the pystp Makefile to have it point to the static library:
--- pystp-0.2/Makefile 2010-08-08 14:15:29.000000000 +0200
+++ pystp-0.2-mod/Makefile 2011-11-09 14:25:24.977104940 +0100
@@ -26,7 +26,7 @@ CFLAGS=`python-config --include` -fpic
all: pystp.so
-pystp.so: $(OBJ) libstp.so
+pystp.so: $(OBJ) libstp.a
$(CXX) -L. $(OBJ) $(CFLAGS) -shared -o $@ -lstp
# Python module
Remember to copy the libstp.a file inside the pystp directory.
Another simple patch is needed to reduce the amount of debug output being generated by pystp:
diff -Narup pystp-0.2/pystp_common.h pystp-0.2-mod//pystp_common.h
--- pystp-0.2/pystp_common.h 2010-08-08 14:15:29.000000000 +0200
+++ pystp-0.2-mod/pystp_common.h 2011-04-28 17:01:12.784297997 +0200
@@ -31,7 +31,7 @@
#include "pystp_expr.h"
/* if defined, debug mode is enabled */
-#define DEBUG_MODE
+//#define DEBUG_MODE
#define TYPE_BOOL 0
#define TYPE_ARRAY 1