Skip to content

Commit

Permalink
Add support for MergeSat
Browse files Browse the repository at this point in the history 
MergeSat is a recent SAT solver that fits the MiniSat2 interface.

To use MergeSat as a proper SAT backend, some extensions might be dropped.
Especially being able to print memory usage is not helpful for CBMC, but
requires pulling in a new dependency.

Signed-off-by: Norbert Manthey <[email protected]>
  • Loading branch information
@conp-solutions @tautschnig
conp-solutions authored and tautschnig committed Apr 26, 2022
1 parent a5ce4e5 commit c1d9942
Show file tree
Hide file tree
Showing 5 changed files with 82 additions and 8 deletions.
9 changes: 9 additions & 0 deletions src/Makefile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -139,6 +139,15 @@ minisat2-download:
@(cd ../minisat-2.2.1; patch -p1 < ../scripts/minisat-2.2.1-patch)
@rm minisat2_2.2.1.orig.tar.gz

mergesat_version = 4.0-rc
mergesat-download:
@echo "Downloading MergeSat $(mergesat_version)"
@$(DOWNLOADER) https://github.com/conp-solutions/mergesat/archive/$(mergesat_version).tar.gz
@$(TAR) xfz $(mergesat_version).tar.gz
@rm -Rf ../mergesat
@mv mergesat-$(mergesat_version) ../mergesat
@$(RM) $(mergesat_version).tar.gz

cudd-download:
@echo "Downloading Cudd 3.0.0"
@$(DOWNLOADER) https://sourceforge.net/projects/cudd-mirror/files/cudd-3.0.0.tar.gz/download cudd-3.0.0.tar.gz
Expand Down
7 changes: 6 additions & 1 deletion src/config.inc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -30,12 +30,13 @@ endif
#BOOLEFORCE = ../../booleforce-0.4
#MINISAT = ../../MiniSat-p_v1.14
#MINISAT2 = ../../minisat-2.2.1
#MERGESAT = ../../mergesat-3.0

This comment has been minimized.

Sign in to view

Copy link
@nmanthey

nmanthey Apr 26, 2022

Contributor

nit: version "3.0" is not true
#IPASIR = ../../ipasir
#GLUCOSE = ../../glucose-syrup
#CADICAL = ../../cadical

# select default solver to be minisat2 if no other is specified
ifeq ($(BOOLEFORCE)$(CHAFF)$(GLUCOSE)$(IPASIR)$(LINGELING)$(MINISAT)$(MINISAT2)$(PICOSAT)$(CADICAL),)
ifeq ($(BOOLEFORCE)$(CHAFF)$(GLUCOSE)$(IPASIR)$(LINGELING)$(MINISAT)$(MINISAT2)$(MERGESAT)$(PICOSAT)$(CADICAL),)
MINISAT2 = ../../minisat-2.2.1
endif

Expand Down Expand Up @@ -63,6 +64,10 @@ ifneq ($(MINISAT2),)
CP_CXXFLAGS += -DSATCHECK_MINISAT2
endif

ifneq ($(MERGESAT),)
CP_CXXFLAGS += -DSATCHECK_MERGESAT
endif

ifneq ($(GLUCOSE),)
CP_CXXFLAGS += -DSATCHECK_GLUCOSE
endif
Expand Down
36 changes: 35 additions & 1 deletion src/solvers/Makefile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,16 @@ ifneq ($(MINISAT2),)
CLEANFILES += $(MINISAT2_LIB) $(patsubst %$(OBJEXT), %$(DEPEXT), $(MINISAT2_LIB))
endif

ifneq ($(MERGESAT),)
# MergeSat is based on MiniSat2 and is invoked (with suitable defines/ifdefs)
# via satcheck_minisat2.{h,cpp}
MERGESAT_SRC=sat/satcheck_minisat2.cpp
MERGESAT_INCLUDE=-I $(MERGESAT)
MERGESAT_LIB=$(MERGESAT)/minisat/simp/SimpSolver$(OBJEXT) $(MERGESAT)/minisat/core/Solver$(OBJEXT) $(MERGESAT)/minisat/utils/ccnr$(OBJEXT) $(MERGESAT)/minisat/utils/Options$(OBJEXT) $(MERGESAT)/minisat/utils/System$(OBJEXT)
CP_CXXFLAGS += -DHAVE_MERGESAT -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS
CLEANFILES += $(MERGESAT_LIB) $(patsubst %$(OBJEXT), %$(DEPEXT), $(MERGESAT_LIB))
endif

ifneq ($(IPASIR),)
IPASIR_SRC=sat/satcheck_ipasir.cpp
IPASIR_INCLUDE=-I $(IPASIR)
Expand Down Expand Up @@ -74,6 +84,7 @@ SRC = $(BOOLEFORCE_SRC) \
$(GLUCOSE_SRC) \
$(LINGELING_SRC) \
$(MINISAT2_SRC) \
$(MERGESAT_SRC) \
$(IPASIR_SRC) \
$(MINISAT_SRC) \
$(PICOSAT_SRC) \
Expand Down Expand Up @@ -226,6 +237,28 @@ $(MINISAT2)/minisat/core/Solver$(OBJEXT): $(MINISAT2)/minisat/core/Solver.cc
endif
endif

ifneq ($(MERGESAT),)
ifeq ($(BUILD_ENV_),MSVC)
sat/satcheck_minisat2$(OBJEXT): sat/satcheck_minisat2.cpp
$(CXX) $(CP_CXXFLAGS) /w /nologo /c /EHsc $< /Fo$@

$(MERGESAT)/minisat/utils/ccnr$(OBJEXT): $(MERGESAT)/minisat/utils/ccnr.cc
$(CXX) $(CP_CXXFLAGS) /w /nologo /c /EHsc $< /Fo$@

$(MERGESAT)/minisat/utils/Options$(OBJEXT): $(MERGESAT)/minisat/utils/Options.cc
$(CXX) $(CP_CXXFLAGS) /w /nologo /c /EHsc $< /Fo$@

$(MERGESAT)/minisat/utils/System$(OBJEXT): $(MERGESAT)/minisat/utils/System.cc
$(CXX) $(CP_CXXFLAGS) /w /nologo /c /EHsc $< /Fo$@

$(MERGESAT)/minisat/simp/SimpSolver$(OBJEXT): $(MERGESAT)/minisat/simp/SimpSolver.cc
$(CXX) $(CP_CXXFLAGS) /w /nologo /c /EHsc $< /Fo$@

$(MERGESAT)/minisat/core/Solver$(OBJEXT): $(MERGESAT)/minisat/core/Solver.cc
$(CXX) $(CP_CXXFLAGS) /w /nologo /c /EHsc $< /Fo$@

This comment has been minimized.

Sign in to view

Copy link
@nmanthey

nmanthey Apr 26, 2022

Contributor

nit: Is this configuration actually tested on Windows? I did not test this myself, and know for earlier versions that this compilation does not work without modifications to MergeSat.
endif
endif

ifneq ($(GLUCOSE),)
ifeq ($(BUILD_ENV_),MSVC)
sat/satcheck_glucose$(OBJEXT): sat/satcheck_glucose.cpp
Expand All @@ -241,6 +274,7 @@ endif

INCLUDES += -I .. \
$(CHAFF_INCLUDE) $(BOOLEFORCE_INCLUDE) $(MINISAT_INCLUDE) $(MINISAT2_INCLUDE) \
$(MERGESAT_INCLUDE) \
$(IPASIR_INCLUDE) \
$(SQUOLEM2_INC) $(CUDD_INCLUDE) $(GLUCOSE_INCLUDE) \
$(PICOSAT_INCLUDE) $(LINGELING_INCLUDE) $(CADICAL_INCLUDE)
Expand All @@ -259,7 +293,7 @@ endif
endif

SOLVER_LIB = $(CHAFF_LIB) $(BOOLEFORCE_LIB) $(MINISAT_LIB) \
$(MINISAT2_LIB) $(SQUOLEM2_LIB) $(CUDD_LIB) \
$(MINISAT2_LIB) $(MERGESAT_LIB) $(SQUOLEM2_LIB) $(CUDD_LIB) \
$(PICOSAT_LIB) $(LINGELING_LIB) $(GLUCOSE_LIB) $(CADICAL_LIB)

SOLVER_OBJS = $(filter %$(OBJEXT), $(SOLVER_LIB))
Expand Down
11 changes: 9 additions & 2 deletions src/solvers/sat/satcheck.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,7 @@ Author: Daniel Kroening, [email protected]
// #define SATCHECK_ZCHAFF
// #define SATCHECK_MINISAT1
// #define SATCHECK_MINISAT2
// #define SATCHECK_MERGESAT
// #define SATCHECK_GLUCOSE
// #define SATCHECK_BOOLEFORCE
// #define SATCHECK_PICOSAT
Expand All @@ -39,6 +40,10 @@ Author: Daniel Kroening, [email protected]
#define SATCHECK_MINISAT2
#endif

#if defined(HAVE_MERGESAT) && !defined(SATCHECK_MERGESAT)
# define SATCHECK_MERGESAT
#endif

#if defined(HAVE_GLUCOSE) && !defined(SATCHECK_GLUCOSE)
#define SATCHECK_GLUCOSE
#endif
Expand Down Expand Up @@ -80,9 +85,11 @@ typedef satcheck_booleforcet satcheck_no_simplifiert;
typedef satcheck_minisat1t satcheckt;
typedef satcheck_minisat1t satcheck_no_simplifiert;

#elif defined SATCHECK_MINISAT2
#elif defined SATCHECK_MINISAT2 || defined SATCHECK_MERGESAT
// MergeSat is based on MiniSat2 and is invoked (with suitable defines/ifdefs)
// via satcheck_minisat2.{h,cpp}

#include "satcheck_minisat2.h"
# include "satcheck_minisat2.h"

typedef satcheck_minisat_simplifiert satcheckt;
typedef satcheck_minisat_no_simplifiert satcheck_no_simplifiert;
Expand Down
27 changes: 23 additions & 4 deletions src/solvers/sat/satcheck_minisat2.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,17 +13,20 @@ Author: Daniel Kroening, [email protected]
# include <unistd.h>
#endif

#include <limits>

#include <util/invariant.h>
#include <util/make_unique.h>
#include <util/threeval.h>

#include <minisat/core/Solver.h>
#include <minisat/simp/SimpSolver.h>

#ifndef HAVE_MINISAT2
#error "Expected HAVE_MINISAT2"
#include <cstdlib>
#include <limits>

// MergeSat is based on MiniSat2; variations in their API are handled via
// #ifdefs
#if !defined(HAVE_MINISAT2) && !defined(HAVE_MERGESAT)
# error "Expected HAVE_MINISAT2 or HAVE_MERGESAT"
#endif

void convert(const bvt &bv, Minisat::vec<Minisat::Lit> &dest)
Expand Down Expand Up @@ -77,7 +80,11 @@ void satcheck_minisat2_baset<T>::set_polarity(literalt a, bool value)
try
{
add_variables();
#ifdef HAVE_MERGESAT
solver->setPolarity(a.var_no(), value);
#else
solver->setPolarity(a.var_no(), value ? l_True : l_False);
#endif
}
catch(Minisat::OutOfMemoryException)
{
Expand All @@ -101,12 +108,20 @@ void satcheck_minisat2_baset<T>::clear_interrupt()

const std::string satcheck_minisat_no_simplifiert::solver_text()
{
#ifdef HAVE_MERGESAT
return "MergeSat 4.0-rc without simplifier";
#else
return "MiniSAT 2.2.1 without simplifier";
#endif
}

const std::string satcheck_minisat_simplifiert::solver_text()
{
#ifdef HAVE_MERGESAT
return "MergeSat 4.0-rc with simplifier";
#else
return "MiniSAT 2.2.1 with simplifier";
#endif
}

template<typename T>
Expand Down Expand Up @@ -314,6 +329,10 @@ satcheck_minisat2_baset<T>::satcheck_minisat2_baset(
solver(util_make_unique<T>()),
time_limit_seconds(0)
{
#ifdef HAVE_MERGESAT
int ret = setenv(MINISAT_RUNTIME_ARGS, "-no-grow-iter", 0);

This comment has been minimized.

Sign in to view

Copy link
@nmanthey

nmanthey Apr 26, 2022

Contributor

IIUC, this variable needs to be set before the solver object is created. Have you checked whether this setting is actually passed through to the solver?

It might be simpler to always start from the SimpSolver object, and set the "use_simplification" parameter right after constructing the object, to indicate whether you want to have simplification or not. Then, you can also set the member behind the option you use in setenv, as this is always available as well. That would be member 'grow_iterations'
CHECK_RETURN(ret == 0);
#endif
}

template <typename T>
Expand Down

0 comments on commit c1d9942

Please sign in to comment.