How to compile Boolector 3.0.0 with MiniSat linked in?

[Fred]

Hi,

I am compiling MiniSat 2.2.0 as a library ("make libr") under <boolector dir>/deps/minisat. I get the library "lib_release.a" with a soft link "lib.a" pointing to it. Then I am trying to compile Boolector 3.0.0 and I want to link MiniSat in so I can use it from Boolector. But while running the ./configure.sh script, MiniSat is not found.

Is it because MiniSat does not get compiled as a *shared* library? Or what should I do?

Thanks,

Fred

[Mathias Preiner]

Hi Fred,

The contrib/setup-* scripts install all dependencies to deps/install. If
you compile MiniSat yourself, you have to install MiniSat to deps/install.

You can do that with the MiniSat build system as follows

make config prefix=absolute/path/to/deps/install
make install

Cheers,
Mathias

> --
> You received this message because you are subscribed to the Google
> Groups "Boolector" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to boolector+...@googlegroups.com
> <mailto:boolector+...@googlegroups.com>.
> To post to this group, send email to bool...@googlegroups.com
> <mailto:bool...@googlegroups.com>.
> Visit this group at https://groups.google.com/group/boolector.
> For more options, visit https://groups.google.com/d/optout.

[Fred]

Thanks for the quick answer Mathias.

I can see that if you pass "deps/install" to the setup-* scripts, they will clone the SAT solvers and compile them there but I believe that the setup-minisat script is outdated. MiniSat 2.2.0 does not compile as 1.14. It has two versions now (core and simp). Basically, when you run setup-minisat.sh, it does not work anymore. Thus, I was trying to do everything manually.

Moreover, install is not a target in the MiniSat makefile anymore.

From my little understanding of makefiles, I believe MiniSat makefile does not produce the right output anymore for Boolector.

That being said, I did try what you wrote and it does not work. I could get all SAT solvers to link into Boolector, *except* MiniSat (because of its new build system I believe). I fear you will have to download and look at MiniSat's new makefile (and mk template) to understand what's broken. I could figure how to compile MiniSat as a release library but then Boolector's CMake script still does not find it even though it finds all three others... Maybe the CMake script does not search for the right files anymore, I don't know.

Thanks!

Fred

Le jeudi 11 avril 2019 13:45:21 UTC-4, Mathias Preiner a écrit :

Hi Fred,

The contrib/setup-* scripts install all dependencies to deps/install. If
you compile MiniSat yourself, you have to install MiniSat to deps/install.

You can do that with the MiniSat build system as follows

make config prefix=absolute/path/to/deps/install
make install

Cheers,
Mathias

On 4/11/19 10:03 AM, Fred wrote:
> Hi,
>
> I am compiling MiniSat 2.2.0 as a library ("make libr") under <boolector
> dir>/deps/minisat. I get the library "lib_release.a" with a soft link
> "lib.a" pointing to it. Then I am trying to compile Boolector 3.0.0 and
> I want to link MiniSat in so I can use it from Boolector. But while
> running the ./configure.sh script, MiniSat is not found.
>
> Is it because MiniSat does not get compiled as a *shared* library? Or
> what should I do?
>
> Thanks,
>
> Fred
>
> --
> You received this message because you are subscribed to the Google
> Groups "Boolector" group.
> To unsubscribe from this group and stop receiving emails from it, send

> an email to bool...@googlegroups.com
> <mailto:bool...@googlegroups.com>.

[Mathias Preiner]

This is a bit surprising to me. Doing a fresh clone of the Boolector
repository and setting up dependencies works for me without any problems:

git clone https://github.com/boolector/boolector.git
cd boolector

./contrib/setup-btor2tools.sh
./contrib/setup-minisat.sh
./configure.sh
cd build
make

What are the exact steps you tried?

Mathias

> > an email to bool...@googlegroups.com <javascript:>
> > <mailto:bool...@googlegroups.com <javascript:>>.

> > To post to this group, send email to bool...@googlegroups.com

> <javascript:>
> > <mailto:bool...@googlegroups.com <javascript:>>.

> > Visit this group at https://groups.google.com/group/boolector

> <https://groups.google.com/group/boolector>.

> > For more options, visit https://groups.google.com/d/optout

> <https://groups.google.com/d/optout>.

>
> --
> You received this message because you are subscribed to the Google
> Groups "Boolector" group.
> To unsubscribe from this group and stop receiving emails from it, send

> an email to boolector+...@googlegroups.com
> <mailto:boolector+...@googlegroups.com>.

[Mathias Preiner]

What MiniSat version are you using? contrib/setup-minisat.sh clones the
MiniSat repository from https://github.com/niklasso/minisat.git and we
use version 2.2.0 by default.

On 4/11/19 11:40 AM, Fred wrote:

> > an email to bool...@googlegroups.com <javascript:>
> > <mailto:bool...@googlegroups.com <javascript:>>.

> > To post to this group, send email to bool...@googlegroups.com

> <javascript:>
> > <mailto:bool...@googlegroups.com <javascript:>>.

> > Visit this group at https://groups.google.com/group/boolector

> <https://groups.google.com/group/boolector>.

> > For more options, visit https://groups.google.com/d/optout

> <https://groups.google.com/d/optout>.

>
> --
> You received this message because you are subscribed to the Google
> Groups "Boolector" group.
> To unsubscribe from this group and stop receiving emails from it, send

> an email to boolector+...@googlegroups.com
> <mailto:boolector+...@googlegroups.com>.

[Fred]

The only difference I see is that I configure Boolector for --python. But it should not change anything. Let me try it again. I'll get back to you.

Thanks.

[Mathias Preiner]

Oh ok, we explicitly disable MiniSat if shared libraries are built,
which is needed for --python.

I'll have a look to figure out if this can be fixed.

Mathias

[Fred]

Thank you very much for looking into this!

From what I just experienced, I believe you also disable PicoSAT when --python is enabled, right? I just noticed that PicoSAT, althought the setup script was run, also does not link into Boolector when --python is used. Or at least I do not see it in the output of ./configure --python. I did not try explicitely in Boolector afterwards.

Fred

[Mathias Preiner]

Yes that's right, we also disable PicoSAT if you configure with --python.

I'll add configure messages to make this more clear to the user.

Mathias

[Mathias Preiner]

What you can do is configure Boolector with --python --shared. This will
not disable MiniSat and PicoSAT, but will dynamically link the SAT
solvers against libboolector.

Mathias

On 4/11/19 8:44 PM, Fred wrote:

[Fred]

Hi Mathias,

Yes I confirm that adding --shared works. Thanks very much again!

I've also made sure that the flag -flto was added in all 6 tools while compiling and linking (btor2tools, minisat, picosat, lingeling, cadical, boolector).

Fred