marijnheule / march-SAT-solver

the march SAT solver
GNU General Public License v3.0
6 stars 0 forks source link

Compilation failes as some definitions are missing #1

Open msoos opened 5 years ago

msoos commented 5 years ago

Hi,

The compilation fails as e.g. look_fix_binary_implications seems to be missing. The compilation error is:

/usr/bin/ld: doublelook.o: in function `DL_IUP_wo_eq_3SAT':
doublelook.c:(.text+0x93): undefined reference to `look_fix_binary_implications'
/usr/bin/ld: doublelook.c:(.text+0xac): undefined reference to `look_fix_binary_implications'
/usr/bin/ld: doublelook.o: in function `DL_IUP_wo_eq_kSAT':
doublelook.c:(.text+0x191): undefined reference to `look_fix_binary_implications'
/usr/bin/ld: doublelook.o: in function `DL_IFIUP':
doublelook.c:(.text+0x26c): undefined reference to `look_fix_binary_implications'
/usr/bin/ld: doublelook.c:(.text+0x2a7): undefined reference to `look_backtrack'
/usr/bin/ld: doublelook.o: in function `DL_fix_forced_literal':
doublelook.c:(.text+0x302): undefined reference to `look_fix_binary_implications'
/usr/bin/ld: doublelook.c:(.text+0x363): undefined reference to `look_backtrack'
/usr/bin/ld: doublelook.o: in function `DL_treelook':
doublelook.c:(.text+0x3d1): undefined reference to `look_fix_binary_implications'
/usr/bin/ld: doublelook.c:(.text+0x423): undefined reference to `look_backtrack'
/usr/bin/ld: parser.o: in function `propagate_unary_clauses':
parser.c:(.text+0xbb3): undefined reference to `fixEq'
/usr/bin/ld: resolvent.o: in function `strengthen_big_clause':
resolvent.c:(.text+0x382): undefined reference to `restore_big_clauses'
/usr/bin/ld: resolvent.c:(.text+0x3c0): undefined reference to `restore_big_clauses'
/usr/bin/ld: solver.o: in function `DPLL_add_binary_implications':
solver.c:(.text+0x19bd): undefined reference to `look_fix_binary_implications'
/usr/bin/ld: solver.c:(.text+0x1bec): undefined reference to `look_fix_binary_implications'
/usr/bin/ld: solver.o: in function `IFIUP':
solver.c:(.text+0x1dae): undefined reference to `look_fix_binary_implications'
/usr/bin/ld: solver.c:(.text+0x1e32): undefined reference to `look_fix_binary_implications'
/usr/bin/ld: solver.c:(.text+0x2582): undefined reference to `look_fix_binary_implications'
/usr/bin/ld: solver.o: in function `DPLL_propagate_binary_equivalence':
solver.c:(.text+0x27ab): undefined reference to `fixEq'
/usr/bin/ld: solver.c:(.text+0x27e8): undefined reference to `fixEq'
/usr/bin/ld: solver.c:(.text+0x295e): undefined reference to `look_fix_binary_implications'
/usr/bin/ld: solver.o: in function `DPLL_add_binary_implications':
solver.c:(.text+0x1333): undefined reference to `look_fix_binary_implications'
collect2: error: ld returned 1 exit status
make: *** [Makefile:28: march_pa] Error 1

I couldn't find the definition of look_fix_binary_implications. Maybe the relevant source file was accidentally not added to the code?

aaw commented 4 years ago

gcc doesn't like functions tagged as inline in both their .h declaration and their .c definition. You can fix by either changing all of march's .c inline function definitions to extern inline:

sed -i 's/inline/extern inline/g' *.c

or just removing all of the inline specifiers (I don't see a performance difference in march with/without):

sed -i 's/inline//g' *.{h,c}

msoos commented 4 years ago

Ah, I see! Sorry, I probably mis-grepped the code then! Marijn -- do you wanna push the change? Or should I just apply this manually to my own code? :)