"undefined reference" with library usage

[DiIVIiCH]

Hi. I need to do a lot of tests, so i want to use this assumptions thing in cryptominisat. I'm under Linux Mint 17.3 now. Cryptominisat5 compiles well, i have all the files in directories usr/local/(bin,include,lib). I use gcc 4.8.4. Now i just copy your example of library usage and when i do "gcc prog.cpp -std=c++11" i get a lof of errors like this: /tmp/ccgQmMaP.o: In functionmain': prog.cpp:(.text+0x1f): undefined reference to CMSat::SATSolver::SATSolver(void*, std::atomic<bool>*)' prog.cpp:(.text+0x3c): undefined reference toCMSat::SATSolver::set_num_threads(unsigned int)' prog.cpp:(.text+0x4d): undefined reference to CMSat::SATSolver::new_vars(unsigned long)' prog.cpp:(.text+0x89): undefined reference toCMSat::SATSolver::add_clause(std::vector<CMSat::Lit, std::allocator > const&)' ... ` I'm more Windows user, so i definitely miss something. Can you help me?

P.S. is it possible to use cryptominisat as library in Visual Studio?

[a1880]

A correct compile & link command does look more complex than your attempt. Look here for an somewhat outdated example to illustrate the point: https://github.com/stp/stp/issues/221

[DiIVIiCH]

Well, i looked, and i still don't understand what i did wrong. I installed cryptominisat into system, i can perform Python example, but i need C. Why my program don't see cryptominisat.h file?

[a1880]

gcc is seeking include files along an include path. Use the -I parameter to tell gcc, where to look. Use gcc -v --help to get a full listing of options.

[DiIVIiCH]

But i have file in usr/local/include/cryptominisat5/cryptominisat.h, as much as i understand it's default path for include libraries for gcc.

[msoos]

Yes, all is good. You need to link in the library, though :) Also, try using g++, you'll have a lot less trouble. Can you please tell us the full exact command you are using to build your program along with the full error it gives? We can fix it then :) Thanks!

[DiIVIiCH]

Tried g++.

g++ prog.cpp -o prog -std=c++11

/tmp/cctF3DMi.o: In function `main':
prog.cpp:(.text+0x1f): undefined reference to `CMSat::SATSolver::SATSolver(void*, std::atomic<bool>*)'
prog.cpp:(.text+0x3c): undefined reference to `CMSat::SATSolver::set_num_threads(unsigned int)'
prog.cpp:(.text+0x4d): undefined reference to `CMSat::SATSolver::new_vars(unsigned long)'
prog.cpp:(.text+0x89): undefined reference to `CMSat::SATSolver::add_clause(std::vector<CMSat::Lit, std::allocator<CMSat::Lit> > const&)'
prog.cpp:(.text+0xd1): undefined reference to `CMSat::SATSolver::add_clause(std::vector<CMSat::Lit, std::allocator<CMSat::Lit> > const&)'
prog.cpp:(.text+0x16b): undefined reference to `CMSat::SATSolver::add_clause(std::vector<CMSat::Lit, std::allocator<CMSat::Lit> > const&)'
prog.cpp:(.text+0x17c): undefined reference to `CMSat::SATSolver::solve(std::vector<CMSat::Lit, std::allocator<CMSat::Lit> > const*)'
prog.cpp:(.text+0x1dc): undefined reference to `CMSat::SATSolver::get_model() const'
prog.cpp:(.text+0x231): undefined reference to `CMSat::SATSolver::get_model() const'
prog.cpp:(.text+0x286): undefined reference to `CMSat::SATSolver::get_model() const'
prog.cpp:(.text+0x2ca): undefined reference to `CMSat::SATSolver::get_model() const'
prog.cpp:(.text+0x2e6): undefined reference to `CMSat::SATSolver::get_model() const'
/tmp/cctF3DMi.o:prog.cpp:(.text+0x302): more undefined references to `CMSat::SATSolver::get_model() const' follow
/tmp/cctF3DMi.o: In function `main':
prog.cpp:(.text+0x38a): undefined reference to `CMSat::SATSolver::~SATSolver()'
prog.cpp:(.text+0x3ae): undefined reference to `CMSat::SATSolver::~SATSolver()'
collect2: error: ld returned 1 exit status

[msoos]

Hey! Cool! Can you please try to link in the Cryptominisat libray too? ;) Let's see what it days then.

On 21 Dec 2016 02:31, "DiIVIiCH" notifications@github.com wrote:

Tried g++.

g++ prog.cpp -o prog -std=c++11

/tmp/cctF3DMi.o: In function main': prog.cpp:(.text+0x1f): undefined reference toCMSat::SATSolver::SATSolver(void, std::atomic)' prog.cpp:(.text+0x3c): undefined reference to CMSat::SATSolver::set_num_threads(unsigned int)' prog.cpp:(.text+0x4d): undefined reference toCMSat::SATSolver::new_vars(unsigned long)' prog.cpp:(.text+0x89): undefined reference to CMSat::SATSolver::add_clause(std::vector<CMSat::Lit, std::allocator<CMSat::Lit> > const&)' prog.cpp:(.text+0xd1): undefined reference toCMSat::SATSolver::add_clause(std::vector<CMSat::Lit, std::allocator > const&)' prog.cpp:(.text+0x16b): undefined reference to CMSat::SATSolver::add_clause(std::vector<CMSat::Lit, std::allocator<CMSat::Lit> > const&)' prog.cpp:(.text+0x17c): undefined reference toCMSat::SATSolver::solve(std::vector<CMSat::Lit, std::allocator > const*)' prog.cpp:(.text+0x1dc): undefined reference to CMSat::SATSolver::get_model() const' prog.cpp:(.text+0x231): undefined reference toCMSat::SATSolver::get_model() const' prog.cpp:(.text+0x286): undefined reference to CMSat::SATSolver::get_model() const' prog.cpp:(.text+0x2ca): undefined reference toCMSat::SATSolver::get_model() const' prog.cpp:(.text+0x2e6): undefined reference to CMSat::SATSolver::get_model() const' /tmp/cctF3DMi.o:prog.cpp:(.text+0x302): more undefined references toCMSat::SATSolver::get_model() const' follow /tmp/cctF3DMi.o: In function main': prog.cpp:(.text+0x38a): undefined reference toCMSat::SATSolver::~SATSolver()' prog.cpp:(.text+0x3ae): undefined reference to `CMSat::SATSolver::~SATSolver()' collect2: error: ld returned 1 exit status

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/msoos/cryptominisat/issues/375#issuecomment-268417831, or mute the thread https://github.com/notifications/unsubscribe-auth/ABReOdKGyhPunzMXKCDI0iUubv2hVsi8ks5rKI-IgaJpZM4LQ9Vw .

[DiIVIiCH]

Oh...it's worked. Now I undestand what a1880 talked about. Well, there is logic in it, but not obvious for windows user. :)

g++ prog.cpp -o prog -lcryptominisat5 -std=c++11

Thanks for your help.

[msoos]

No worries at all, I'm glad it worked! We'll update the readme to reflect this so others maybe have a better chance :) Thanks for reporting!

Happy new year,

Mate

On 21 Dec 2016 15:23, "DiIVIiCH" notifications@github.com wrote:

Closed #375 https://github.com/msoos/cryptominisat/issues/375.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/msoos/cryptominisat/issues/375#event-901738129, or mute the thread https://github.com/notifications/unsubscribe-auth/ABReOcM9vwSf9wJMC23q8osBAiGUKYJlks5rKUSDgaJpZM4LQ9Vw .