Skip to content
Commits on Source (56)
Show whitespace changes
Inline Side-by-side
.cproject deleted 100644 → 0
View file @ f1ab401e
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<?fileVersion 4.0.0?>
<cproject storage_type_id="org.eclipse.cdt.core.XmlProjectDescriptionStorage">
<storageModule moduleId="org.eclipse.cdt.core.settings">
<cconfiguration id="0.114514924">
<storageModule buildSystemId="org.eclipse.cdt.managedbuilder.core.configurationDataProvider" id="0.114514924" moduleId="org.eclipse.cdt.core.settings" name="デフォルト">
<externalSettings/>
<extensions>
<extension id="org.eclipse.cdt.core.VCErrorParser" point="org.eclipse.cdt.core.ErrorParser"/>
<extension id="org.eclipse.cdt.core.GmakeErrorParser" point="org.eclipse.cdt.core.ErrorParser"/>
<extension id="org.eclipse.cdt.core.CWDLocator" point="org.eclipse.cdt.core.ErrorParser"/>
<extension id="org.eclipse.cdt.core.GCCErrorParser" point="org.eclipse.cdt.core.ErrorParser"/>
<extension id="org.eclipse.cdt.core.GASErrorParser" point="org.eclipse.cdt.core.ErrorParser"/>
<extension id="org.eclipse.cdt.core.GLDErrorParser" point="org.eclipse.cdt.core.ErrorParser"/>
</extensions>
</storageModule>
<storageModule moduleId="cdtBuildSystem" version="4.0.0">
<configuration buildProperties="" description="" id="0.114514924" name="デフォルト" parent="org.eclipse.cdt.build.core.prefbase.cfg">
<folderInfo id="0.114514924." name="/" resourcePath="">
<toolChain id="org.eclipse.cdt.build.core.prefbase.toolchain.725442348" name="ツールチェーンなし" resourceTypeBasedDiscovery="false" superClass="org.eclipse.cdt.build.core.prefbase.toolchain">
<targetPlatform id="org.eclipse.cdt.build.core.prefbase.toolchain.725442348.436375175" name=""/>
<builder id="org.eclipse.cdt.build.core.settings.default.builder.1165131656" keepEnvironmentInBuildfile="false" managedBuildOn="false" name="Gnu Make ビルダー" superClass="org.eclipse.cdt.build.core.settings.default.builder"/>
<tool id="org.eclipse.cdt.build.core.settings.holder.libs.1258053810" name="ライブラリー設定フォルダー" superClass="org.eclipse.cdt.build.core.settings.holder.libs"/>
<tool id="org.eclipse.cdt.build.core.settings.holder.1047628829" name="アセンブリー" superClass="org.eclipse.cdt.build.core.settings.holder">
<inputType id="org.eclipse.cdt.build.core.settings.holder.inType.440652964" languageId="org.eclipse.cdt.core.assembly" languageName="アセンブリー" sourceContentType="org.eclipse.cdt.core.asmSource" superClass="org.eclipse.cdt.build.core.settings.holder.inType"/>
</tool>
<tool id="org.eclipse.cdt.build.core.settings.holder.1368023086" name="GNU C++" superClass="org.eclipse.cdt.build.core.settings.holder">
<inputType id="org.eclipse.cdt.build.core.settings.holder.inType.1795190116" languageId="org.eclipse.cdt.core.g++" languageName="GNU C++" sourceContentType="org.eclipse.cdt.core.cxxSource,org.eclipse.cdt.core.cxxHeader" superClass="org.eclipse.cdt.build.core.settings.holder.inType"/>
</tool>
<tool id="org.eclipse.cdt.build.core.settings.holder.1368816036" name="GNU C" superClass="org.eclipse.cdt.build.core.settings.holder">
<inputType id="org.eclipse.cdt.build.core.settings.holder.inType.2011086387" languageId="org.eclipse.cdt.core.gcc" languageName="GNU C" sourceContentType="org.eclipse.cdt.core.cSource,org.eclipse.cdt.core.cHeader" superClass="org.eclipse.cdt.build.core.settings.holder.inType"/>
</tool>
</toolChain>
</folderInfo>
</configuration>
</storageModule>
<storageModule moduleId="org.eclipse.cdt.core.externalSettings"/>
</cconfiguration>
</storageModule>
<storageModule moduleId="cdtBuildSystem" version="4.0.0">
<project id="gpw-solver-2.12.null.1091620089" name="gpw-solver-2.12"/>
</storageModule>
<storageModule moduleId="scannerConfiguration">
<autodiscovery enabled="true" problemReportingEnabled="true" selectedProfileId=""/>
<scannerConfigBuildInfo instanceId="0.114514924">
<autodiscovery enabled="true" problemReportingEnabled="true" selectedProfileId=""/>
</scannerConfigBuildInfo>
</storageModule>
</cproject>
.gitignore
View file @ f9829216
......@@ -4,9 +4,13 @@
*.od
*.or
*.ox
*.mk
naps
*_profile
*_debug
*_release
*_static
*.exe
depend.mak
.cproject
.project
.settings/
.project deleted 100644 → 0
View file @ f1ab401e
<?xml version="1.0" encoding="UTF-8"?>
<projectDescription>
<name>gpw-solver-2.11a</name>
<comment></comment>
<projects>
</projects>
<buildSpec>
<buildCommand>
<name>org.eclipse.cdt.managedbuilder.core.genmakebuilder</name>
<triggers>clean,full,incremental,</triggers>
<arguments>
<dictionary>
<key>?name?</key>
<value></value>
</dictionary>
<dictionary>
<key>org.eclipse.cdt.make.core.append_environment</key>
<value>true</value>
</dictionary>
<dictionary>
<key>org.eclipse.cdt.make.core.autoBuildTarget</key>
<value>all</value>
</dictionary>
<dictionary>
<key>org.eclipse.cdt.make.core.buildArguments</key>
<value></value>
</dictionary>
<dictionary>
<key>org.eclipse.cdt.make.core.buildCommand</key>
<value>make</value>
</dictionary>
<dictionary>
<key>org.eclipse.cdt.make.core.cleanBuildTarget</key>
<value>clean</value>
</dictionary>
<dictionary>
<key>org.eclipse.cdt.make.core.contents</key>
<value>org.eclipse.cdt.make.core.activeConfigSettings</value>
</dictionary>
<dictionary>
<key>org.eclipse.cdt.make.core.enableAutoBuild</key>
<value>false</value>
</dictionary>
<dictionary>
<key>org.eclipse.cdt.make.core.enableCleanBuild</key>
<value>true</value>
</dictionary>
<dictionary>
<key>org.eclipse.cdt.make.core.enableFullBuild</key>
<value>true</value>
</dictionary>
<dictionary>
<key>org.eclipse.cdt.make.core.fullBuildTarget</key>
<value>all</value>
</dictionary>
<dictionary>
<key>org.eclipse.cdt.make.core.stopOnError</key>
<value>true</value>
</dictionary>
<dictionary>
<key>org.eclipse.cdt.make.core.useDefaultBuildCmd</key>
<value>true</value>
</dictionary>
</arguments>
</buildCommand>
<buildCommand>
<name>org.eclipse.cdt.managedbuilder.core.ScannerConfigBuilder</name>
<triggers>full,incremental,</triggers>
<arguments>
</arguments>
</buildCommand>
</buildSpec>
<natures>
<nature>org.eclipse.cdt.core.cnature</nature>
<nature>org.eclipse.cdt.core.ccnature</nature>
<nature>org.eclipse.cdt.managedbuilder.core.managedBuildNature</nature>
<nature>org.eclipse.cdt.managedbuilder.core.ScannerConfigNature</nature>
</natures>
</projectDescription>
Main.C
View file @ f9829216
......@@ -61,6 +61,7 @@ bool opt_maxsat = false; // MaxSat mode
SolverT opt_solver = st_GlueMiniSat;
bool opt_simp_solver = true;
int opt_num_threads = 0;
ConvertT opt_convert = ct_Mixed;
ConvertT opt_convert_goal = ct_Sorters; //ct_Undef;
bool opt_convert_goal_reusing = true;
......@@ -129,7 +130,7 @@ cchar* doc =
"~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~\n"
"Naps 1.00 by Masahiko Sakai, 2015, an extension of\n"
"MiniSat+ 1.0 by Niklas Een and Niklas Sorensson, 2005.\n"
"This sofrware contains GlueMiniSat 2.2.6 by Hidetomo Nabeshima.\n"
"This sofrware contains GlueMiniSat 2.2.6 and ManyGlucose 4.1 by Hidetomo Nabeshima.\n"
"~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~\n"
"USAGE: naps <input-file> [<result-file>] [-<option> ...]\n"
"\n"
......@@ -137,12 +138,15 @@ cchar* doc =
" -M -minisat Use MiniSat v1.13 as backend\n"
// " -S -satelite Use SatELite v1.0 as backend\n"
" -GM -glueminisat Use GlueMiniSat v2.2.6 as backend (default)\n"
" -G4 -glucose4.1 Use Glucose v4.1 as backend\n"
" -MG -manyglucose Use ManyGlucose v4.1 as backend\n"
" -M2 -minisat2.2 Use MiniSat v2.2 as backend\n"
" -GL -glucose1.0 Use Glucose v1.0 as backend\n"
" -E -es1sat Use ES1Sat v1.0 as backend\n"
" -C -ccminisat Use CCMiniSat v1.0 as backend\n"
" -Simp Use Simplification facility if possible (default)\n"
" -noSimp Don't use Simplification facility\n"
" -nthreads= Number of SAT solver threads\n"
"\n"
" -ca -adders Convert PB-constrs to clauses through adders.\n"
" -cs -sorters Convert PB-constrs to clauses through sorters.\n"
......@@ -255,12 +259,16 @@ void parseOptions(int argc, char** argv)
else if (oneof(arg, "M,minisat" )) opt_solver = st_MiniSat;
// else if (oneof(arg, "S,satelite" )) opt_solver = st_SatELite;
else if (oneof(arg, "GM,glueminisat")) opt_solver = st_GlueMiniSat;
else if (oneof(arg, "G4,glucose4.1" )) opt_solver = st_Glucose41;
else if (oneof(arg, "MG,manyglucose")) opt_solver = st_ManyGlucose;
else if (oneof(arg, "M2,minisat2.2" )) opt_solver = st_MiniSat22;
else if (oneof(arg, "GL,glucose1.0" )) opt_solver = st_Glucose10;
else if (oneof(arg, "E,es1sat" )) opt_solver = st_ES1Sat;
else if (oneof(arg, "C,ccminisat" )) opt_solver = st_CCMiniSat;
else if (oneof(arg, "Simp" )) opt_simp_solver = true; // default
else if (oneof(arg, "noSimp" )) opt_simp_solver = false;
else if (strncmp(arg, "-nthreads=", 10) == 0) opt_num_threads = atoi(arg+10);
else if (oneof(arg, "ca,adders" )) opt_convert = ct_Adders;
else if (oneof(arg, "cs,sorters")) opt_convert = ct_Sorters;
......
Main.h
View file @ f9829216
......@@ -27,7 +27,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
//=================================================================================================
enum SolverT { st_MiniSat, st_SatELite, st_GlueMiniSat, st_MiniSat22, st_Glucose10, st_ES1Sat, st_CCMiniSat};
enum SolverT { st_MiniSat, st_SatELite, st_GlueMiniSat, st_Glucose41, st_ManyGlucose, st_MiniSat22, st_Glucose10, st_ES1Sat, st_CCMiniSat};
enum ConvertT { ct_Sorters, ct_Adders, ct_BDDs, ct_Mixed, ct_Mixed2, ct_Undef };
enum Command { cmd_Minimize, cmd_FirstSolution, cmd_AllSolutions, cmd_InterestSolutions, cmd_Soft };
enum GpwT { gt_none, gt_positive, gt_negative, gt_low, gt_high, gt_both };
......@@ -50,6 +50,7 @@ extern bool opt_eager_cl;
// -- solver options:
extern SolverT opt_solver;
extern bool opt_simp_solver;
extern int opt_num_threads;
extern ConvertT opt_convert;
extern ConvertT opt_convert_goal;
extern bool opt_convert_goal_reusing;
......
Makefile
View file @ f9829216
......@@ -12,7 +12,11 @@ DCOBJSPB = $(addsuffix d, $(COBJSPB))
RCOBJSPB = $(addsuffix r, $(COBJSPB))
R64COBJSPB= $(addsuffix x, $(COBJSPB))
COBJS = $(COBJSPB) glueminisat/core/Solver.o glueminisat/simp/SimpSolver.o glueminisat/utils/System.o es1sat/core/Solver.o es1sat/simp/SimpSolver.o ccminisat/core/Solver.o ccminisat/simp/SimpSolver.o
COBJS = $(COBJSPB) \
glueminisat/core/Solver.o glueminisat/simp/SimpSolver.o glueminisat/utils/System.o \
manyglucose/parallel/MultiSolvers.o manyglucose/parallel/ParallelSolver.o manyglucose/parallel/PrdClausesQueue.o manyglucose/parallel/SolverConfiguration.o manyglucose/parallel/PeriodClausesBuffer.o manyglucose/parallel/SharedCompanion.o manyglucose/parallel/SolverCompanion.o manyglucose/parallel/PrdClausesQueueMgr.o manyglucose/parallel/PrdClauses.o manyglucose/simp/SimpSolver.o manyglucose/core/Solver.o manyglucose/mtl/Clone.o manyglucose/utils/System.o manyglucose/utils/Chronometer.o \
es1sat/core/Solver.o es1sat/simp/SimpSolver.o \
ccminisat/core/Solver.o ccminisat/simp/SimpSolver.o
PCOBJS = $(addsuffix p, $(COBJS))
DCOBJS = $(addsuffix d, $(COBJS))
RCOBJS = $(addsuffix r, $(COBJS))
......@@ -20,20 +24,21 @@ R64COBJS = $(addsuffix x, $(COBJS))
EXEC = naps
#CXX = g++6
#LDFLAGS += -Wl,-rpath=/usr/local/lib/gcc6
CXX = g++
#CXX = g++10
LDFLAGS += -L/usr/local/lib/g++8
#CXX = icpc
CXX ?= g++
CFLAGS = -Wall -ffloat-store
#CFLAGS += -IADTs -include Global.h -include Main.h -D_FILE_OFFSET_BITS=64
#CFLAGS += -IADTs -Iglueminisat -include Global.h -include Main.h -D_FILE_OFFSET_BITS=64
#CFLAGS += -IADTs -Iglueminisat -include Global.h -include Main.h -D_FILE_OFFSET_BITS=64 -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS -D NDEBUG
CFLAGS += -IADTs -Iglueminisat -include Main.h -D_FILE_OFFSET_BITS=64 -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS # modified by nabesima
CFLAGS += -IADTs -Iglueminisat -Imanyglucose -include Main.h -D_FILE_OFFSET_BITS=64 -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS # modified by nabesima
CFLAGS += -I/usr/local/include -fno-strict-aliasing
COPTIMIZE = -O3 -fomit-frame-pointer -falign-loops=4 -falign-functions=16 -foptimize-sibling-calls -finline-functions -fcse-follow-jumps -fcse-skip-blocks -frerun-cse-after-loop -frerun-loop-opt -fgcse
LDFLAGS += -L/usr/local/lib -L/opt/local/lib
LDFLAGS += -L/usr/lib
LDFLAGS += -lpthread
.PHONY : s p d r x build clean cleanPB depend
......@@ -76,6 +81,7 @@ clean:
$(MAKE) cleanPB
MROOT=$(CURDIR)/glueminisat $(MAKE) -C $(CURDIR)/glueminisat/core clean
MROOT=$(CURDIR)/glueminisat $(MAKE) -C $(CURDIR)/glueminisat/simp clean
$(MAKE) -C $(CURDIR)/manyglucose/parallel clean
MROOT=$(CURDIR)/es1sat $(MAKE) -C $(CURDIR)/es1sat/core clean
MROOT=$(CURDIR)/es1sat $(MAKE) -C $(CURDIR)/es1sat/simp clean
MROOT=$(CURDIR)/ccminisat $(MAKE) -C $(CURDIR)/ccminisat/core clean
......@@ -84,7 +90,7 @@ clean:
## Build rule
%.o %.op %.od %.or %.ox: %.C
@echo Compiling: $<
@$(CXX) $(CFLAGS) -c -o $@ $<
$(CXX) $(CFLAGS) -c -o $@ $<
glueminisat/core/Solver.o:
MROOT=$(CURDIR)/glueminisat $(MAKE) -C $(CURDIR)/glueminisat/core
......@@ -110,6 +116,18 @@ glueminisat/simp/SimpSolver.od:
glueminisat/simp/SimpSolver.ox:
MROOT=$(CURDIR)/glueminisat $(MAKE) -C $(CURDIR)/glueminisat/simp rx
manyglucose/parallel/MultiSolvers.o:
$(MAKE) -C $(CURDIR)/manyglucose/parallel CXX=$(CXX)
manyglucose/parallel/MultiSolvers.or:
$(MAKE) -C $(CURDIR)/manyglucose/parallel CXX=$(CXX) rs
manyglucose/parallel/MultiSolvers.od:
$(MAKE) -C $(CURDIR)/manyglucose/parallel CXX=$(CXX) d
manyglucose/parallel/MultiSolvers.ox:
$(MAKE) -C $(CURDIR)/manyglucose/parallel CXX=$(CXX) rx
es1sat/core/Solver.o: es1sat/core/Solver.cc
MROOT=$(CURDIR)/es1sat $(MAKE) -C $(CURDIR)/es1sat/core
......@@ -161,27 +179,27 @@ ccminisat/simp/SimpSolver.ox: ccminisat/simp/SimpSolver.cc
## Linking rules (standard/profile/debug/release)
$(EXEC): $(COBJS)
@echo Linking $(EXEC)
@$(CXX) $(COBJS) $(LDFLAGS) -lz -lgmp -Wall -o $@
$(CXX) $(COBJS) $(LDFLAGS) -lz -lgmp -Wall -o $@
$(EXEC)_profile: $(PCOBJS)
@echo Linking $@
@$(CXX) $(PCOBJS) $(LDFLAGS) -lz -lgmp -Wall -pg -o $@
$(CXX) $(PCOBJS) $(LDFLAGS) -lz -lgmp -Wall -pg -o $@
$(EXEC)_debug: $(DCOBJS)
@echo Linking $@
@$(CXX) $(DCOBJS) $(LDFLAGS) -lz -lgmp -Wall -o $@
$(CXX) $(DCOBJS) $(LDFLAGS) -lz -lgmp -Wall -o $@
$(EXEC)_release: $(RCOBJS)
@echo Linking $@
@$(CXX) $(RCOBJS) $(LDFLAGS) -lz -Wall -o $@
$(CXX) $(RCOBJS) $(LDFLAGS) -lz -Wall -o $@
$(EXEC)_bignum_static: $(RCOBJS)
@echo Linking $@
@$(CXX) --static $(RCOBJS) $(LDFLAGS) -lz -lgmp -Wall -o $@
$(CXX) --static $(RCOBJS) $(LDFLAGS) -lz -lgmp -Wall -o $@
$(EXEC)_64-bit_static: $(R64COBJS)
@echo Linking $@
@$(CXX) --static $(R64COBJS) $(LDFLAGS) -lz -Wall -o $@
$(CXX) --static $(R64COBJS) $(LDFLAGS) -lz -Wall -o $@
## Make dependencies
......
Solver.h
View file @ f9829216
......@@ -26,6 +26,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
//#include "SatELite.h"
#include "glueminisat/core/Solver.h"
#include "glueminisat/simp/SimpSolver.h"
#include "manyglucose/parallel/MultiSolvers.h"
#include "es1sat/core/Solver.h"
#include "es1sat/simp/SimpSolver.h"
#include "ccminisat/core/Solver.h"
......@@ -39,6 +40,8 @@ class Solver {
// SatELite::Solver* satelite;
GlueMiniSat::Solver* glueminisat;
GlueMiniSat::SimpSolver* simp_glueminisat;
Glucose::SimpSolver* glucose;
Glucose::MultiSolvers* manyglucose;
ES1Sat::Solver* es1sat;
ES1Sat::SimpSolver* simp_es1sat;
CCMiniSat::Solver* ccminisat;
......@@ -69,6 +72,23 @@ class Solver {
return(ll_Undef);
}
Glucose::Lit lit2glit(const Lit lit) {
return Glucose::mkLit(var(lit), sign(lit));
}
void vec2vec(const vec<Lit>& in, Glucose::vec<Glucose::Lit>& out) {
for (int i=0; i < in.size(); i++)
out.push(lit2glit(in[i]));
}
lbool lbool2lbool(Glucose::lbool v) const {
switch (Glucose::toInt(v)) {
case 0: return toLbool(+1);
case 1: return toLbool(-1);
case 2: return toLbool( 0);
}
assert(false);
return(ll_Undef);
}
ES1Sat::Lit elit2lit(const Lit lit) {
return ES1Sat::mkLit(var(lit), sign(lit));
}
......@@ -122,6 +142,8 @@ public:
// if (satelite) return satelite->ok;
if (glueminisat) return glueminisat->getOK();
if (simp_glueminisat) return simp_glueminisat->getOK();
if (glucose) return glucose->getOK();
if (manyglucose) return manyglucose->getOK();
if (es1sat) return es1sat->getOK();
if (simp_es1sat) return simp_es1sat->getOK();
if (ccminisat) return ccminisat->getOK();
......@@ -136,7 +158,7 @@ public:
if (minisat ) return (BasicSolverStats&)minisat->stats;
// if (satelite) return (BasicSolverStats&)satelite->stats;
// if (glueminisat||es1sat) return basicStats;
if (glueminisat||simp_glueminisat
if (glueminisat||simp_glueminisat||glucose||manyglucose
||es1sat||simp_es1sat
||ccminisat||simp_ccminisat) return basicStats;
assert(false);
......@@ -148,6 +170,8 @@ public:
// if (satelite != NULL) return satelite->assigns[v];
if (glueminisat != NULL) return lbool2lbool(glueminisat->getAssign(v)).toInt();
if (simp_glueminisat != NULL) return lbool2lbool(simp_glueminisat->getAssign(v)).toInt();
if (glucose != NULL) return lbool2lbool(glucose ->getAssign(v)).toInt();
if (manyglucose != NULL) return lbool2lbool(manyglucose->getAssign(v)).toInt();
if (es1sat != NULL) return lbool2lbool(es1sat ->getAssign(v)).toInt();
if (simp_es1sat != NULL) return lbool2lbool(simp_es1sat->getAssign(v)).toInt();
......@@ -162,6 +186,8 @@ public:
// if (satelite != NULL) return satelite->trail.size();
if (glueminisat != NULL) return glueminisat->getTrailSize();
if (simp_glueminisat != NULL) return simp_glueminisat->getTrailSize();
if (glucose != NULL) return glucose->getTrailSize();
if (manyglucose != NULL) return manyglucose->getTrailSize();
if (es1sat != NULL) return es1sat->getTrailSize();
if (simp_es1sat != NULL) return simp_es1sat->getTrailSize();
if (ccminisat != NULL) return ccminisat->getTrailSize();
......@@ -174,6 +200,8 @@ public:
// if (satelite != NULL) return satelite->trail[index];
if (glueminisat != NULL) return Lit(GlueMiniSat::var(glueminisat->getTrail(index)), GlueMiniSat::sign(glueminisat->getTrail(index)));
if (simp_glueminisat != NULL) return Lit(GlueMiniSat::var(simp_glueminisat->getTrail(index)), GlueMiniSat::sign(simp_glueminisat->getTrail(index)));
if (glucose != NULL) return Lit(Glucose::var(glucose->getTrail(index)), Glucose::sign(glucose->getTrail(index)));
if (manyglucose != NULL) return Lit(Glucose::var(manyglucose->getTrail(index)), Glucose::sign(manyglucose->getTrail(index)));
if (es1sat != NULL) return Lit(ES1Sat::var(es1sat->getTrail(index)), ES1Sat::sign(es1sat->getTrail(index)));
if (simp_es1sat != NULL) return Lit(ES1Sat::var(simp_es1sat->getTrail(index)), ES1Sat::sign(simp_es1sat->getTrail(index)));
if (ccminisat != NULL) return Lit(CCMiniSat::var(ccminisat->getTrail(index)), CCMiniSat::sign(ccminisat->getTrail(index)));
......@@ -186,6 +214,8 @@ public:
// if (satelite ) satelite->verbosity = level;
if (glueminisat) glueminisat->verbosity = level;
if (simp_glueminisat) simp_glueminisat->verbosity = level;
if (glucose) glucose->verbosity = level;
if (manyglucose) manyglucose->setVerbosity(level);
if (es1sat ) es1sat->verbosity = level;
if (simp_es1sat) simp_es1sat->verbosity = level;
if (ccminisat ) ccminisat->verbosity = level;
......@@ -217,6 +247,8 @@ public:
// if (satelite) return satelite ->newVar(dvar);
if (glueminisat) return glueminisat->newVar(true, dvar);
if (simp_glueminisat) return simp_glueminisat->newVar(true, dvar);
if (glucose) return glucose ->newVar(true, dvar);
if (manyglucose) return manyglucose ->newVar(true, dvar);
if (es1sat) return es1sat ->newVar(true, dvar);
if (simp_es1sat) return simp_es1sat ->newVar(true, dvar);
if (ccminisat) return ccminisat ->newVar(true, dvar);
......@@ -243,6 +275,16 @@ public:
}
return simp_glueminisat->addClause_(ps_);
}
if (glucose) {
Glucose::vec<Glucose::Lit> ps_;
vec2vec(ps, ps_);
return glucose->addClause(ps_);
}
if (manyglucose) {
Glucose::vec<Glucose::Lit> ps_;
vec2vec(ps, ps_);
return manyglucose->addClause(ps_);
}
if (es1sat) {
ES1Sat::vec<ES1Sat::Lit> ps_;
vec2vec(ps, ps_);
......@@ -306,6 +348,8 @@ public:
reportf("Out of Memory in adding unit to glueminisat\n");
raise(SIGTERM);
}
if (glucose) return glucose ->addClause(lit2glit(p));
if (manyglucose) return manyglucose->addClause(lit2glit(p));
if (es1sat) return es1sat ->addClause(elit2lit(p));
if (simp_es1sat) return simp_es1sat ->addClause(elit2lit(p));
if (ccminisat) return ccminisat ->addClause(clit2lit(p));
......@@ -319,6 +363,8 @@ public:
if (simp_glueminisat) {
simp_glueminisat->setFrozen(x, true); // printf("variable %d is frozen\n", x);
}
if (glucose ) glucose ->setFrozen(x, true);
if (manyglucose) manyglucose->setFrozen(x, true);
if (simp_es1sat) simp_es1sat->setFrozen(x, true);
if (simp_ccminisat) simp_ccminisat->setFrozen(x, true);
// else assert(false);
......@@ -363,6 +409,29 @@ public:
basicStats.starts += simp_glueminisat->starts;
return ret;
}
if (glucose) {
Glucose::vec<Glucose::Lit> assumps_;
vec2vec(assumps, assumps_);
bool ret = glucose->solve(assumps_, opt_simp_solver);
basicStats.conflicts += glucose->conflicts;
basicStats.decisions += glucose->decisions;
basicStats.propagations += glucose->propagations;
basicStats.starts += glucose->starts;
return ret;
}
if (manyglucose) {
Glucose::vec<Glucose::Lit> assumps_;
vec2vec(assumps, assumps_);
manyglucose->setNumThreads(opt_num_threads);
lbool lret = lbool2lbool(manyglucose->solve(assumps_, opt_simp_solver));
assert(lret != ll_Undef);
bool ret = (lret == ll_True);
basicStats.conflicts += manyglucose->getNumConflicts();
basicStats.decisions += manyglucose->getNumDecisions();
basicStats.propagations += manyglucose->getNumPropagations();
basicStats.starts += manyglucose->getNumRestarts();
return ret;
}
if (es1sat) {
ES1Sat::vec<ES1Sat::Lit> assumps_;
vec2vec(assumps, assumps_);
......@@ -421,6 +490,8 @@ public:
// if (satelite) return satelite->model[v];
if (glueminisat) return lbool2lbool(glueminisat->model[v]);
if (simp_glueminisat) return lbool2lbool(simp_glueminisat->model[v]);
if (glucose) return lbool2lbool(glucose->model[v]);
if (manyglucose) return lbool2lbool(manyglucose->model[v]);
if (es1sat) return lbool2lbool(es1sat->model[v]);
if (simp_es1sat) return lbool2lbool(simp_es1sat->model[v]);
if (ccminisat) return lbool2lbool(ccminisat->model[v]);
......@@ -430,6 +501,8 @@ public:
}
bool varElimed(Var x) {
if (simp_glueminisat) return simp_glueminisat->isEliminated(x);
if (glucose ) return glucose ->isEliminated(x);
if (manyglucose) return manyglucose->isEliminated(x);
if (simp_es1sat) return simp_es1sat->isEliminated(x);
if (simp_ccminisat) return simp_ccminisat->isEliminated(x);
// if (satelite) return satelite->var_elimed[x];
......@@ -470,6 +543,8 @@ public:
bool okay() {
if (glueminisat) return glueminisat->okay();
if (simp_glueminisat) return simp_glueminisat->okay();
if (glucose) return glucose->okay();
if (manyglucose) return manyglucose->okay();
if (es1sat) return es1sat->okay();
if (simp_es1sat) return simp_es1sat->okay();
if (ccminisat) return ccminisat->okay();
......@@ -485,6 +560,8 @@ public:
// satelite ? satelite->nVars() :
glueminisat ? glueminisat->nVars() :
simp_glueminisat ? simp_glueminisat->nVars() :
glucose ? glucose->nVars() :
manyglucose ? manyglucose->nVars() :
es1sat ? es1sat->nVars() :
simp_es1sat ? simp_es1sat->nVars() :
ccminisat ? ccminisat->nVars() :
......@@ -507,6 +584,10 @@ public:
glueminisat->toDimacs(filename, out_max);
} else if (simp_glueminisat) {
simp_glueminisat->toDimacs(filename, out_max);
} else if (glucose) {
glucose->toDimacs(filename);
} else if (manyglucose) {
manyglucose->toDimacs(filename);
} else
reportf("-cnf: unsupported option.\n"),exit(1);
// assert(false);
......@@ -519,6 +600,8 @@ public:
// satelite (type == st_SatELite ? new SatELite::Solver : NULL),
glueminisat(!opt_simp_solver && (type == st_GlueMiniSat || type == st_MiniSat22 || type == st_Glucose10) ? new GlueMiniSat::Solver : NULL),
// simp_glueminisat(opt_simp_solver && (type == st_GlueMiniSat || type == st_MiniSat22 || type == st_Glucose10) ? new GlueMiniSat::SimpSolver : NULL),
glucose (type == st_Glucose41 ? new Glucose::SimpSolver : NULL),
manyglucose(type == st_ManyGlucose ? new Glucose::MultiSolvers : NULL),
es1sat (!opt_simp_solver && type == st_ES1Sat ? new ES1Sat::Solver : NULL),
simp_es1sat (opt_simp_solver && type == st_ES1Sat ? new ES1Sat::SimpSolver : NULL),
ccminisat (!opt_simp_solver && type == st_CCMiniSat? new CCMiniSat::Solver : NULL),
......
ccminisat/core/SolverTypes.h
View file @ f9829216
......@@ -118,6 +118,10 @@ public:
inline int toInt (lbool l) { return l.value; }
inline lbool toLbool(int v) { return lbool((uint8_t)v); }
//const lbool l_True = lbool((uint8_t)0);
//const lbool l_False = lbool((uint8_t)1);
//const lbool l_Undef = lbool((uint8_t)2);
//=================================================================================================
// Clause -- a simple class for representing a clause:
......
ccminisat/utils/System.cc
View file @ f9829216
......@@ -20,13 +20,13 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include "utils/System.h"
#if defined(__linux__)
#include <stdio.h>
#include <stdlib.h>
using namespace CCMiniSat;
#if defined(__linux__)
// TODO: split the memory reading functions into two: one for reading high-watermark of RSS, and
// one for reading the current virtual memory size.
......
es1-glueminisat-1.0a/utils/System.cc
View file @ f9829216
......@@ -20,13 +20,13 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include "utils/System.h"
#if defined(__linux__)
#include <stdio.h>
#include <stdlib.h>
using namespace GlueMiniSat;
#if defined(__linux__)
// TODO: split the memory reading functions into two: one for reading high-watermark of RSS, and
// one for reading the current virtual memory size.
......
es1sat/core/SolverTypes.h
View file @ f9829216
......@@ -119,6 +119,9 @@ public:
//static lbool l_True = lbool((uint8_t)0); // gcc does not do constant propagation if these are real constants.
//static lbool l_False = lbool((uint8_t)1);
//static lbool l_Undef = lbool((uint8_t)2);
//const lbool l_True = lbool((uint8_t)0);
//const lbool l_False = lbool((uint8_t)1);
//const lbool l_Undef = lbool((uint8_t)2);
inline int toInt (lbool l) { return l.value; }
inline lbool toLbool(int v) { return lbool((uint8_t)v); }
......
es1sat/utils/System.cc
View file @ f9829216
......@@ -20,13 +20,13 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include "utils/System.h"
#if defined(__linux__)
#include <stdio.h>
#include <stdlib.h>
using namespace ES1Sat;
#if defined(__linux__)
// TODO: split the memory reading functions into two: one for reading high-watermark of RSS, and
// one for reading the current virtual memory size.
......
glueminisat/core/SolverTypes.h
View file @ f9829216
......@@ -84,9 +84,11 @@ const Lit lit_Error = { -1 }; // }
// does enough constant propagation to produce sensible code, and this appears to be somewhat
// fragile unfortunately.
#ifndef l_True
#define l_True (lbool((uint8_t)0)) // gcc does not do constant propagation if these are real constants.
#define l_False (lbool((uint8_t)1))
#define l_Undef (lbool((uint8_t)2))
#endif
class lbool {
uint8_t value;
......
glueminisat/utils/System.cc
View file @ f9829216
......@@ -17,16 +17,16 @@ NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FO
DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
**************************************************************************************************/
#include "utils/System.h"
#if defined(__linux__)
#include <stdio.h>
#include <stdlib.h>
#include <assert.h>
#include "utils/System.h"
using namespace GlueMiniSat;
#if defined(__linux__)
// TODO: split the memory reading functions into two: one for reading high-watermark of RSS, and
// one for reading the current virtual memory size.
......@@ -76,7 +76,8 @@ double GlueMiniSat::memUsedPeak() {
double GlueMiniSat::memUsed(void) {
struct rusage ru;
getrusage(RUSAGE_SELF, &ru);
if(getrusage(RUSAGE_SELF, &ru) != 0)
printf("ERROR! gitrusage failed\n"), exit(1);
return (double)ru.ru_maxrss / 1024; }
// modified by nabesima
//double GlueMiniSat::memUsedPeak(void) { return memUsed(); }
......
manyglucose/Changelog 0 → 100644
View file @ f9829216
Version 4.1
- Adaptative (activated by default) strategies. See SAT 2016 paper.
Version 4.0
- Add a Multithread version, called syrup (many glucose ;-)
See SAT14 paper: Lazy Clause Exchange Policy for parallel SAT solvers.
- Can work indepentently in sequential or with many cores
Version 3.0 (2013)
- Add incremental features.
See SAT13 paper: Improving Glucose for Incremental SAT Solving with Assumptions: Application to MUS Extraction
- Add certified UNSAT proof.
Version 2.3 (2012)
- Add new restart strategy
See CP12 paper: Refining Restarts Strategies For SAT and UNSAT
- Add additionnal features to speed the search
Version 2.0 (2011)
- Add additionnal features (freeze potential good clauses for one turn)
- Based on Minisat 2.2
Version 1.0 (2009)
- Based on Minisat 2.0
First release of glucose.
See ijcai 2009 paper: Predicting Learnt Clauses Quality in Modern SAT Solver
manyglucose/LICENCE 0 → 100644
View file @ f9829216
Glucose -- Copyright (c) 2009-2017, Gilles Audemard, Laurent Simon
CRIL - Univ. Artois, France
LRI - Univ. Paris Sud, France (2009-2013)
Labri - Univ. Bordeaux, France
Syrup (Glucose Parallel) -- Copyright (c) 2013-2014, Gilles Audemard, Laurent Simon
CRIL - Univ. Artois, France
Labri - Univ. Bordeaux, France
Glucose sources are based on MiniSat (see below MiniSat copyrights). Permissions and copyrights of
Glucose (sources until 2013, Glucose 3.0, single core) are exactly the same as Minisat on which it
is based on. (see below).
Glucose-Syrup sources are based on another copyright. Permissions and copyrights for the parallel
version of Glucose-Syrup (the "Software") are granted, free of charge, to deal with the Software
without restriction, including the rights to use, copy, modify, merge, publish, distribute,
sublicence, and/or sell copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:
- The above and below copyrights notices and this permission notice shall be included in all
copies or substantial portions of the Software;
- The parallel version of Glucose (all files modified since Glucose 3.0 releases, 2013) cannot
be used in any competitive event (sat competitions/evaluations) without the express permission of
the authors (Gilles Audemard / Laurent Simon). This is also the case for any competitive event
using Glucose Parallel as an embedded SAT engine (single core or not).
--------------- Original Minisat Copyrights
Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
Copyright (c) 2007-2010, Niklas Sorensson
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
associated documentation files (the "Software"), to deal in the Software without restriction,
including without limitation the rights to use, copy, modify, merge, publish, distribute,
sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in all copies or
substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
manyglucose/README 0 → 100644
View file @ f9829216
Directory overview:
==================
mtl/ Minisat Template Library
core/ A core version of the solver glucose (no main here)
simp/ An extended solver with simplification capabilities
parallel/ A multicore version of glucose
README
LICENSE
Changelog
To build (release version: without assertions, statically linked, etc):
======================================================================
Like minisat....
cd { simp | parallel }
make rs
Usage:
======
in simp directory: ./glucose --help
in parallel directory: ./glucose-syrup --help
\ No newline at end of file
manyglucose/api/ipasir.h 0 → 100644
View file @ f9829216
/* Part of the generic incremental SAT API called 'ipasir'.
* See 'LICENSE' for rights to use this software.
*/
#ifndef ipasir_h_INCLUDED
#define ipasir_h_INCLUDED
/**
* Return the name and the version of the incremental SAT
* solving library.
*/
const char * ipasir_signature ();
/**
* Construct a new solver and return a pointer to it.
* Use the returned pointer as the first parameter in each
* of the following functions.
*
* Required state: N/A
* State after: INPUT
*/
void * ipasir_init ();
/**
* Release the solver, i.e., all its resoruces and
* allocated memory (destructor). The solver pointer
* cannot be used for any purposes after this call.
*
* Required state: INPUT or SAT or UNSAT
* State after: undefined
*/
void ipasir_release (void * solver);
/**
* Add the given literal into the currently added clause
* or finalize the clause with a 0. Clauses added this way
* cannot be removed. The addition of removable clauses
* can be simulated using activation literals and assumptions.
*
* Required state: INPUT or SAT or UNSAT
* State after: INPUT
*
* Literals are encoded as (non-zero) integers as in the
* DIMACS formats. They have to be smaller or equal to
* INT_MAX and strictly larger than INT_MIN (to avoid
* negation overflow). This applies to all the literal
* arguments in API functions.
*/
void ipasir_add (void * solver, int lit_or_zero);
/**
* Add an assumption for the next SAT search (the next call
* of ipasir_solve). After calling ipasir_solve all the
* previously added assumptions are cleared.
*
* Required state: INPUT or SAT or UNSAT
* State after: INPUT
*/
void ipasir_assume (void * solver, int lit);
/**
* Solve the formula with specified clauses under the specified assumptions.
* If the formula is satisfiable the function returns 10 and the state of the solver is changed to SAT.
* If the formula is unsatisfiable the function returns 20 and the state of the solver is changed to UNSAT.
* If the search is interrupted (see ipasir_set_terminate) the function returns 0 and the state of the solver remains INPUT.
* This function can be called in any defined state of the solver.
*
* Required state: INPUT or SAT or UNSAT
* State after: INPUT or SAT or UNSAT
*/
int ipasir_solve (void * solver);
/**
* Get the truth value of the given literal in the found satisfying
* assignment. Return 'lit' if True, '-lit' if False, and 0 if not important.
* This function can only be used if ipasir_solve has returned 10
* and no 'ipasir_add' nor 'ipasir_assume' has been called
* since then, i.e., the state of the solver is SAT.
*
* Required state: SAT
* State after: SAT
*/
int ipasir_val (void * solver, int lit);
/**
* Check if the given assumption literal was used to prove the
* unsatisfiability of the formula under the assumptions
* used for the last SAT search. Return 1 if so, 0 otherwise.
* This function can only be used if ipasir_solve has returned 20 and
* no ipasir_add or ipasir_assume has been called since then, i.e.,
* the state of the solver is UNSAT.
*
* Required state: UNSAT
* State after: UNSAT
*/
int ipasir_failed (void * solver, int lit);
/**
* Set a callback function used to indicate a termination requirement to the
* solver. The solver will periodically call this function and check its return
* value during the search. The ipasir_set_terminate function can be called in any
* state of the solver, the state remains unchanged after the call.
* The callback function is of the form "int terminate(void * state)"
* - it returns a non-zero value if the solver should terminate.
* - the solver calls the callback function with the parameter "state"
* having the value passed in the ipasir_set_terminate function (2nd parameter).
*
* Required state: INPUT or SAT or UNSAT
* State after: INPUT or SAT or UNSAT
*/
void ipasir_set_terminate (void * solver, void * state, int (*terminate)(void * state));
#endif
manyglucose/api/ipasirmanyglucose.cc 0 → 100644
View file @ f9829216
//#define __STDC_LIMIT_MACROS
//#define __STDC_FORMAT_MACROS
#include "parallel/MultiSolvers.h"
//#include "utils/System.h"
#include <cassert>
#include <cstdio>
#include <cstdlib>
#include <cstring>
#include <climits>
using namespace std;
using namespace Glucose;
extern "C" {
static const char * sig = "manyglucose-4.1.27";
};
class IPAsirManyGlucose: public MultiSolvers {
vec<Lit> assumptions, clause;
int szfmap;
unsigned char * fmap;
bool nomodel;
unsigned long long calls;
double total_time;
void reset() {
if (fmap)
delete[] fmap, fmap = 0, szfmap = 0;
}
Lit import(int lit) {
while (abs(lit) > nVars())
(void) newVar();
return mkLit(Var(abs(lit) - 1), (lit > 0));
}
void ana() {
fmap = new unsigned char[szfmap = nVars()];
memset(fmap, 0, szfmap);
for (int i = 0; i < conflict.size(); i++) {
int tmp = var(conflict[i]);
assert(0 <= tmp && tmp < szfmap);
fmap[tmp] = 1;
}
}
double ps(double s, double t) {
return t ? s / t : 0;
}
public:
IPAsirManyGlucose() :
szfmap(0), fmap(0), nomodel(false), calls(0), total_time(0.0) {
// MiniSAT by default produces non standard conforming messages.
// So either we have to set this to '0' or patch the sources.
setVerbosity(1);
}
~IPAsirManyGlucose() {
reset();
}
void printStatistics() {
printStats();
}
void add(int lit) {
reset();
nomodel = true;
if (lit)
clause.push(import(lit));
else
addClause(clause), clause.clear();
}
void assume(int lit) {
reset();
nomodel = true;
assumptions.push(import(lit));
}
int solve() {
double start = realTime();
setvbuf(stdout, (char *) NULL, _IONBF, 0);
calls++;
reset();
lbool res = MultiSolvers::solve(assumptions, false);
assumptions.clear();
nomodel = (res != l_True);
printStatistics();
total_time += realTime() - start;
return (res == l_Undef) ? 0 : (res == l_True ? 10 : 20);
}
int val(int lit) {
if (nomodel)
return 0;
lbool res = getModelValue(import(lit));
return (res == l_True) ? lit : -lit;
}
int failed(int lit) {
if (!fmap)
ana();
int tmp = var(import(lit));
assert(0 <= tmp && tmp < nVars());
return fmap[tmp] != 0;
}
double get_time() {
return total_time;
}
void stats() {
printStats();
}
};
extern "C" {
#include "ipasir.h"
static IPAsirManyGlucose * import(void * s) {
return (IPAsirManyGlucose*) s;
}
const char * ipasir_signature() {
return sig;
}
void * ipasir_init() {
return new IPAsirManyGlucose();
}
void ipasir_release(void * s) {
import(s)->stats();
delete import(s);
}
int ipasir_solve(void * s) {
return import(s)->solve();
}
void ipasir_add(void * s, int l) {
import(s)->add(l);
}
void ipasir_assume(void * s, int l) {
import(s)->assume(l);
}
int ipasir_val(void * s, int l) {
return import(s)->val(l);
}
int ipasir_failed(void * s, int l) {
return import(s)->failed(l);
}
void ipasir_set_terminate(void * s, void * state,
int (*callback)(void * state)) {
import(s)->setTermCallback(state, callback);
}
}