		Search-engine friendly clone of the ACL2 documentation.

Ipasir

Building-an-ipasir-solver-library

How to obtain an ipasir backend implementation.

There are several SAT solver libraries that implement the IPASIR interface; in particular, the entrants in the 2016 and 2017 SAT Competitions are available, respectively, here and here. However, the build scripts for these libraries are configured to produce a static library, and we need a shared library so that we can link it into a running Lisp session. We'll walk through the steps necessary to adapt the makefile to build a Linux shared library for glucose, whose sources are available here.

First, ensure that you have gcc and g++ version 6 or greater.

Unzip the archive and edit the file "sat/glucose4/makefile" as follows:

Add " -fPIC" to the CXXFLAGS to build position-independent code, required for shared libraries.
Add the line "export CXXFLAGS" below the setting of CXXFLAGS, so that those flags apply to the recursive make of the core solver library.
Fix a typo: replace the occurrence of "CXXLAGS" with "CXXFLAGS".

Or apply the following patch instead:

32,33c32,33
< CXXFLAGS= -g -std=c++11 -Wall -DNDEBUG -O3
<
---
> CXXFLAGS= -g -std=c++11 -Wall -DNDEBUG -O3 -fPIC
> export CXXFLAGS
70c70
< 	$(CXX) -g  -std=c++11 $(CXXLAGS) \
---
> 	$(CXX) -g  -std=c++11 $(CXXFLAGS) \

After fixing the makefile, run "make". This should produce files "ipasirglucoseglue.o" and "libipasirglucose4.a".

Link those two files into a shared library. For Linux, this can be done as follows:

g++ -shared -Wl,-soname,libipasirglucose4.so -o libipasirglucose4.so \
    ipasirglucoseglue.o libipasirglucose4.a

(Note: Counterintuitively, it is important that the .o file is listed before the .a file.)

Finally, move the resulting shared library "libipasirglucose4.so" to a permanent location and either:

Ensure that the directory containing the shared library is listed in your $LD_LIBRARY_PATH environment variable. (Note: this assumes the library is named "libipasirglucose4.so"; if you name it something else, then also set $IPASIR_SHARED_LIBRARY to its filename, e.g. "foobar.so".)
Or, just set the $IPASIR_SHARED_LIBRARY environment variable to the full absolute path of the shared library.
If you want to be really fancy, install the shared library into your system libraries using ldconfig or similar. However, our build system isn't smart enough to tell that you have done this, so you should also set $IPASIR_SHARED_LIBRARY to the name of the installed library, e.g. "libipasirglucose4.so", otherwise these IPASIR-related books will be skipped when building the community books.