5.3.11 fails to build with system minisat

[EvaSDK]

Hello there,

I am one of the Gentoo maintainers of link-grammar and following #415, I tried to build 5.3.11 against our system installation of minisat. We have two releases, basically the 2.2.0 release and the latest commit from their git tree from September 25th, 2013. The 2.2 release is simply not detected as valid, I guess some required features for link-grammar are missing so it falls back to bundled lib. With git HEAD though it fails with:

link-grammar-5.3.11  build configuration settings

    prefix:                         /usr
    C compiler:                     x86_64-pc-linux-gnu-gcc  -DUSE_PTHREADS=1 -DUSE_SAT_SOLVER=1 -DHAVE_SQLITE=1 -O2 -march=ivybridge -pipe -g -msse3 -mstackrealign -O3 -std=c11 -D_BSD_SOURCE -D_SVID_SOURCE -D_GNU_SOURCE -D_DEFAULT_SOURCE
    C++ compiler:                   x86_64-pc-linux-gnu-g++  -DUSE_PTHREADS=1 -DUSE_SAT_SOLVER=1 -DHAVE_SQLITE=1 -O2 -march=ivybridge -pipe -g -msse3 -mstackrealign -O3 -Wall -std=c++11
    Posix threads:                  yes
    Editline command-line history:  no
    UTF8 editline support:          no
    Java libraries:                 no
    Java interfaces:                
    Swig interfaces generator:      yes
    Perl interfaces:                no
    Perl install location:          
    Python2 interfaces:             no
    Python3 interfaces:             no
    ASpell spell checker:           no
    HunSpell spell checker:         yes
    HunSpell dictionary location:   /usr/share/myspell
    Boolean SAT parser:             yes
    SQLite-backed dictionary:       yes
    Viterbi algorithm parser:       no
    Corpus statistics database:     no
    RegEx tokenizer:                no

>>> Source configured.
>>> Compiling source in /var/tmp/portage/portage/dev-libs/link-grammar-5.3.11-r1/work/link-grammar-5.3.11 ...
make -j16 -l6.0 
Making all in link-grammar
make[1]: Entering directory '/var/tmp/portage/portage/dev-libs/link-grammar-5.3.11-r1/work/link-grammar-5.3.11-normal/link-grammar'
Making all in sat-solver
make[2]: Entering directory '/var/tmp/portage/portage/dev-libs/link-grammar-5.3.11-r1/work/link-grammar-5.3.11-normal/link-grammar/sat-solver'
  CXX      sat-encoder.lo
  CXX      fast-sprintf.lo
  CXX      variables.lo
  CXX      util.lo
  CXX      word-tag.lo
/var/tmp/portage/portage/dev-libs/link-grammar-5.3.11-r1/work/link-grammar-5.3.11/link-grammar/sat-solver/sat-encoder.cpp: In member function ‘void SATEncoder::generate_satisfaction_for_expression(int, int&, Exp*, char*, double)’:
/var/tmp/portage/portage/dev-libs/link-grammar-5.3.11-r1/work/link-grammar-5.3.11/link-grammar/sat-solver/sat-encoder.cpp:361:58: error: no matching function for call to ‘Minisat::Lit::Lit(int)’
       Lit lhs = Lit(_variables->string_cost(var, e->cost));
                                                          ^
In file included from /usr/include/minisat/core/Solver.h:29:0,
                 from /var/tmp/portage/portage/dev-libs/link-grammar-5.3.11-r1/work/link-grammar-5.3.11/link-grammar/sat-solver/sat-encoder.cpp:20:
/usr/include/minisat/core/SolverTypes.h:51:8: note: candidate: Minisat::Lit::Lit()
 struct Lit {
        ^
/usr/include/minisat/core/SolverTypes.h:51:8: note:   candidate expects 0 arguments, 1 provided
/usr/include/minisat/core/SolverTypes.h:51:8: note: candidate: constexpr Minisat::Lit::Lit(const Minisat::Lit&)
/usr/include/minisat/core/SolverTypes.h:51:8: note:   no known conversion for argument 1 from ‘int’ to ‘const Minisat::Lit&’
/usr/include/minisat/core/SolverTypes.h:51:8: note: candidate: constexpr Minisat::Lit::Lit(Minisat::Lit&&)
/usr/include/minisat/core/SolverTypes.h:51:8: note:   no known conversion for argument 1 from ‘int’ to ‘Minisat::Lit&&’
/var/tmp/portage/portage/dev-libs/link-grammar-5.3.11-r1/work/link-grammar-5.3.11/link-grammar/sat-solver/sat-encoder.cpp:370:70: error: no matching function for call to ‘Minisat::Lit::Lit(int)’
           generate_literal(~Lit(_variables->string_cost(var, e->cost)));
                                                                      ^
In file included from /usr/include/minisat/core/Solver.h:29:0,
                 from /var/tmp/portage/portage/dev-libs/link-grammar-5.3.11-r1/work/link-grammar-5.3.11/link-grammar/sat-solver/sat-encoder.cpp:20:
/usr/include/minisat/core/SolverTypes.h:51:8: note: candidate: Minisat::Lit::Lit()
 struct Lit {
        ^
/usr/include/minisat/core/SolverTypes.h:51:8: note:   candidate expects 0 arguments, 1 provided
/usr/include/minisat/core/SolverTypes.h:51:8: note: candidate: constexpr Minisat::Lit::Lit(const Minisat::Lit&)
/usr/include/minisat/core/SolverTypes.h:51:8: note:   no known conversion for argument 1 from ‘int’ to ‘const Minisat::Lit&’
/usr/include/minisat/core/SolverTypes.h:51:8: note: candidate: constexpr Minisat::Lit::Lit(Minisat::Lit&&)
/usr/include/minisat/core/SolverTypes.h:51:8: note:   no known conversion for argument 1 from ‘int’ to ‘Minisat::Lit&&’
/var/tmp/portage/portage/dev-libs/link-grammar-5.3.11-r1/work/link-grammar-5.3.11/link-grammar/sat-solver/sat-encoder.cpp:393:51: error: no matching function for call to ‘Minisat::Lit::Lit(int)’
           rhs.push(Lit(_variables->string(new_var)));
[...]

I can provide a more complete build.log if needed but you get the idea. If you have a reference minisat which is none of the ones I talked about, please point me to it, I'll forward that to our maintainers of minisat.

[ampli]

Hi, In order to solve the problem I would like to install Gentoo and reproduce it. I will need hints on how to install these two minisat versions, and how to build link-grammar under Gentoo (a reference to online material is fine, but a detailed "repeat by" is preferred).

Note that in the configure output you provided, the system minisat was used - not the bundled one. However, it seems as if the AC_CHECK_DECL([mkLit], ... check failed even though mkLit() is declared, so if you include the relevant portion of config.log (or all of it as attachment) it can help me to fix the problem even without trying it myself on Gentoo. (The relevant portion starts with checking whether mkLit is declared and ends with checking whether x.Solver::setPolarity is declared.)

[linas]

Amir, There is an easy explanation for what is happening: the configure script does not find the systems SAT (and that is OK, I guess, its not fatal, and doesn't need to be fixed) but then, during compile, the makefile uses the system-installed SAT header files, which obvious conflict with our in-tree heder files.

The obvious fix is to make sure that wee only use our in-tree header files when building in-tree. How hard can this be?

[ampli]

The current configure script (and also the earlier one one at at 5.3.11) indeed has such a problem. (I cannot be sure this is the problem before I see the configure output or config.log.) I will send a PR to fix that.

[ampli]

If the system minisat library is not found, then the current configure script sets use_minisat_bundled_library=yes. In that case, it doesn't perform the following:

 AC_SUBST(MINISAT_LIBS)
 AC_SUBST(MINISAT_INCLUDES)

So the system minsat includes cannot be used in that case due to their possible existence in MINISAT_INCLUDES.

Please note that the problem happens when compiling a sat-solver file using the systems headers, and this is totally fine (what is not fine is to compile the bundled library with the systems headers, a thing that doesn't happen in our case).

However, "-isystem /usr/include/minisat` is left in CPPFLAGS due to a bug. PR #443 fixes that. But this doesn't explain the problem.

To sum up - this PR is not expected to solve the problem here. I will need to look at the SolverTypes.h file that Gentoo uses in order to find the mismatch. Stay tuned...

[linas]

Why doesn't it explain the problem?

[ampli]

Why doesn't it explain the problem?

1) It seems the configure script finds both the system minisat files and the system minisat headers, because if one of them is not found, then use_minisat_bundled_library=yes and this is shown as:

   Boolean SAT parser:             yes (using the bundled minisat library)

2) SolverTypes.h as appear in GitHub (from which gentoo is supposed to take it) has mkLit() declared. However, from the compilation output it is apparent that it was not detected by the AC_CHECK_DECL([mkLit], ... check, because the corresponding "#define Lit" didn't get defined.

So I still need to see the configure outout and the config.log.

[Meanwhile I'm trying to install Gentoo. All had been going very well untill I tried to install Gnome3, which needs systemd, and from that point I'm fighting with the installation...]

[linas]

And some people talk about systemd as if its a good thing :-)

[ampli]

I now have an up-to-date working Gentoo/Gnome3 system, as an additional system to make LG tests on... It seems the problem is specific to the GCC version it uses (4.9.3) which is lower than what exists in the system in which the problem didn't happen.

We can issue a new library version, but maybe we can wait also to the resolution of the following problem: The Python2 bindings doesn't work on Gentoo (the Python3 works fine). Here is the error message:

...
    import _clinkgrammar
ImportError: dynamic module does not define init function (init_clinkgrammar)

And indeed nm -D doesn't show init_clinkgrammar (as on other systems) but instead shows Pyinit__clinkgrammar and _init, which don't exist on other systems. I have no clue yet regarding that.

[ampli]

The Python2 bindings doesn't work on Gentoo (the Python3 works fine).

The problem was that configure didn't take into account systems in which the "python" binary is Python3. PR #445 fixes that.

Now tests.py is sccessful when it is run by "make check".

But make installcheck reveals a fatal Gentoo problem in malloc.c (!!!), for both Python2 and Python3:

.................................python3.4: malloc.c:3716: _int_malloc: Assertion `(unsigned long) (size) >= (unsigned long) (nb)' failed.
Abort

This happens in the following test:

$ PYTHONPATH=/usr/local/lib/python3.4/site-packages ./bindings/python-examples/tests.py -v
...
test_that_parse_returns_empty_iterator_on_no_linkage_sat (__main__.DBasicParsingTestCase)
Parsing a bad sentence with no null-links shouldn't give any linkage (sat) ... python3.4: malloc.c:3716: _int_malloc: Assertion `(unsigned long) (size) >= (unsigned long) (nb)' failed.
Abort

So I propose to release now version 5.3.12. In any case, the Gentoo maintainers will have to fix malloc.c.

[ampli]

In any case, the Gentoo maintainers will have to fix malloc.c.

After lookit more at it, it is most probably a bindings bug... I am checking it further.

[ampli]

The failure is in sat-solver/word-tag.hpp:108 _match_possible[wj].insert(pj);, inside libsdtc++:

#5  0x00007ffff4e14728 in operator new(unsigned long) () from /usr/lib/gcc/x86_64-pc-linux-gnu/4.9.3/libstdc++.so.6

maybe due to a previous memory corruption.

However, I cannot reproduce it using the system minisat - only the bundled one. I didn't test it with valgrind because running valgrind on gentoo is too complicated. I ran valgrind in the same situation on Fedora, but it didn't find a problem.

To sum up: The problem happens only in Gentoo, in a certain test of the sat-solver when using the bundled minisat. I still don't have a clue where the problem is and will not continue to investigate this further for now. The problem for which this issue was opened has been fixed in PR 444. So this issue can eventually be closed.

[EvaSDK]

I'll try to get around to testing all this this weekend.

[ampli]

The problem happens only in Gentoo, in a certain test of the sat-solver when using the bundled minisat. I still don't have a clue where the problem is and will not continue to investigate this further for now.

It was too interesting so I continued to investigate it nevertheless... (I also succeeded to run valgrind on Gentoo after all.)

The reason of the crash when using the bundled library is that the system library got used instead on run time. The just added commit to PR #444 - to statically link the bundled library - solved that. This solves issue #431.

[linas]

this should be fixed in version 5.3.13

[ampli]

I think this is solved now. Please open a new issue in case such a problem still exists.