0

I get the following error:

/home/eran/CLionProjects/lambda-PDR2/minisat/minisat/core/Solver.h:339: undefined reference to `Minisat::Solver::addClause_(Minisat::vec<Minisat::Lit, int>&)'

which fits to the code from here: https://github.com/niklasso/minisat/blob/master/minisat/core/Solver.h#L339

It seems it is unable to recognize the minisat library. The cmakelists.txt is:


cmake_minimum_required(VERSION 3.10)

project(LambdaPDR)

set(CMAKE_CXX_STANDARD 11)
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wall -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS -O3 -g -fpermissive -DPEDANTIC")

include_directories(minisat minisat/minisat/core minisat/minisat/mtl minisat/minisat/simp aiger utils core tests)

##add reference to /home/eran/CLionProjects/lambda-PDR2/minisat/lib/libminisat.a which is already compile
add_library(minisat STATIC minisat/minisat/core/Solver.cc minisat/minisat/simp/SimpSolver.cc minisat/minisat/utils/Options.cc minisat/minisat/utils/System.cc)
add_library(aiger STATIC aiger/aiger.c)
add_library(common STATIC utils/common.cpp)
add_library(model STATIC utils/Model.cpp)
add_library(simp_model STATIC utils/SimpModel.cpp)
add_library(monotonization STATIC core/monotonization.cpp)
add_library(lambda_pdr STATIC core/LambdaPDR.cpp)
add_library(tests STATIC tests/test.cpp tests/MonotonizationTest.cpp tests/LambdaPDRTest.cpp)
add_executable(LambdaPDR main.cpp)
include_directories(utils)


target_link_libraries(LambdaPDR  aiger common model simp_model monotonization lambda_pdr tests)

I believe this is some kind of reference problem.

I expect the code to be compile successfully with minisat library.

edward
  • 1
  • 1
    where are you linking your executable to the minisat target? I don't see it. Maybe that's all you're missing? – starball Mar 20 '23 at 23:17

0 Answers0