Commit 214bc7fb authored by Kučera Petr RNDr. Ph.D.'s avatar Kučera Petr RNDr. Ph.D.
Browse files

CMakeLists for optional glucose support

parent ad17cbe9
......@@ -39,22 +39,30 @@ endfunction(su_add_pthread)
find_package(Boost 1.64.0 COMPONENTS program_options REQUIRED)
# Glucose related part
if(DEFINED ENV{GLUCOSE_HOME})
set (GLUCOSE_HOME $ENV{GLUCOSE_HOME})
message(STATUS "Using GLUCOSE_HOME=${GLUCOSE_HOME}")
option(USE_KISSAT "If the project should compile with kissat support" ON)
if(USE_KISSAT)
if(DEFINED ENV{GLUCOSE_HOME})
set (GLUCOSE_HOME $ENV{GLUCOSE_HOME})
message(STATUS "Using GLUCOSE_HOME=${GLUCOSE_HOME}")
else()
set (GLUCOSE_HOME ${SUBool_SOURCE_DIR}/solvers/glucose)
message(STATUS "GLUCOSE_HOME not defined, using default GLUCOSE_HOME=${GLUCOSE_HOME}")
endif()
# find_library(GLUCOSE_LIB glucose_debug /usr/local/glucose/simp)
# find_library(GLUCOSE_LIB glucose_release /usr/local/glucose/simp)
find_library(GLUCOSE_LIB _release ${GLUCOSE_HOME}/simp)
message(STATUS "Using GLUCOSE_LIB: ${GLUCOSE_LIB}")
include_directories (SYSTEM ${GLUCOSE_HOME})
else()
set (GLUCOSE_HOME ${SUBool_SOURCE_DIR}/solvers/glucose)
message(STATUS "GLUCOSE_HOME not defined, using default GLUCOSE_HOME=${GLUCOSE_HOME}")
message(STATUS "Glucose support will not be available")
endif()
# find_library(GLUCOSE_LIB glucose_debug /usr/local/glucose/simp)
# find_library(GLUCOSE_LIB glucose_release /usr/local/glucose/simp)
find_library(GLUCOSE_LIB _release ${GLUCOSE_HOME}/simp)
message(STATUS "Using GLUCOSE_LIB: ${GLUCOSE_LIB}")
# END of Glusoce related part
function(su_add_glucose_lib libs)
set(${libs} ${${libs}} ${GLUCOSE_LIB} PARENT_SCOPE)
if(USE_GLUCOSE)
set(${libs} ${${libs}} ${GLUCOSE_LIB} PARENT_SCOPE)
endif()
endfunction(su_add_glucose_lib)
# END of Glusoce related part
# KISSAT related part
option(USE_KISSAT "If the project should compile with kissat support" ON)
......@@ -122,7 +130,6 @@ endfunction(su_add_cadical_lib)
include_directories (BEFORE SYSTEM ${Boost_INCLUDE_DIRS})
include_directories (${SUBool_SOURCE_DIR}/lib)
include_directories (SYSTEM ${GLUCOSE_HOME})
include_directories (/usr/local/include/)
add_subdirectory (lib)
......
......@@ -221,7 +221,9 @@ SUBool::CadicalBind::LearntsSize() const
{
if (!mLearner || !mCollectLearnts)
{
return 0;
throw InvariantFailedException("CadicalBind::LearntsSize",
"Learnts are not being collected by the solver");
// return 0;
}
return mLearner->LearntsSize();
}
......@@ -231,7 +233,9 @@ SUBool::CadicalBind::Learnts() const
{
if (!mLearner || !mCollectLearnts)
{
return {};
throw InvariantFailedException("CadicalBind::Learnts",
"Learnts are not being collected by the solver");
// return {};
}
return mLearner->Learnts();
}
......@@ -241,7 +245,9 @@ SUBool::CadicalBind::ExtractLearnts()
{
if (!mLearner || !mCollectLearnts)
{
return {};
throw InvariantFailedException("CadicalBind::ExtractLearnts",
"Learnts are not being collected by the solver");
// return {};
}
return mLearner->ExtractLearnts();
}
......@@ -277,7 +283,7 @@ SUBool::CBLearner::LearntsSize() const
return mLearnts.size();
}
std::vector<SUBool::Clause>
const std::vector<SUBool::Clause> &
SUBool::CBLearner::Learnts() const
{
return mLearnts;
......
......@@ -28,7 +28,7 @@ namespace SUBool
void Clear();
size_t LearntsSize() const;
std::vector<Clause> Learnts() const;
const std::vector<Clause> &Learnts() const;
std::vector<Clause> ExtractLearnts();
};
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment