		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. One source is the ipasir distribution on github, which includes a few compatible solvers. Another source is the incremental solver submissions for the 2020 SAT competition. However, in most cases the build scripts for these libraries are configured to produce a static library, and we need a shared library in order to link it into a running Lisp session.

Easy Steps for building Glucose on Mac OS/Linux

This git repository contains wrappers for a few ipasir solvers and build scripts for creating dynamic libraries. The following sequence of commands has worked to build Glucose 4.1 on Linux and MacOS:

# Clone the repo into liveontologies-ipasir
git clone https://github.com/liveontologies/ipasir.git liveontologies-ipasir
cd liveontologies-ipasir

# Optional: check out a known-working commit
git checkout -b my-branch b183c8bf15f5c8f27246d630b2eb2c6df5ac453a

# make the glucose shared library
cd ipasir-glucose/src/main/native/
make library.version=4.1

This creates a shared library called libglucose-syrup.so on Linux or libglucose-syrup.dylib. To use it, set the IPASIR_SHARED_LIBRARY environment variable to that file's full path (optionally moving it to a convenient location first).

Note, the makefile used above relies upon a tarball of the Glucose sources being available for download from a personal webpage of one of the authors. If this tarball disappears, another location of the Glucose sources is this git repository.

Obsolete instructions for 2017 SAT competition Glucose

We describe the steps below for patching the build scripts for the 2017 SAT competition version of Glucose. Unfortunately, the web pages for the 2017 and previous SAT competitions are offline. We preserve the instructions here in case they are applicable to other solvers. For glucose, the binding and build files are available in the ACL2 distribution under books/centaur/ipasir/solver-glue/glucose4/.

Instructions for building IPASIR-compatible Glucose shared library from the SAT competition 2017 distribution:

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.