Skip to content

N
naps
Source
Select Git revision
...
Target
Select Git revision
 
Commits (51)
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 13996 additions and 359 deletions
.cproject deleted 100644 → 0
View file @ d7e17b14
<?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 @ 589102ab
......@@ -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 @ d7e17b14
<?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 @ 589102ab
This diff is collapsed.
Main.h
View file @ 589102ab
......@@ -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 };
......@@ -35,7 +35,7 @@ enum GpwT { gt_none, gt_positive, gt_negative, gt_low, gt_high, gt_both };
// Controlling optimization
extern bool minimization_mode; // turned on after first SAT-solver execution
extern std::map<Pair< int, Pair< Interval<Int> , Interval<Int> > >, Pair<Pair< Interval<Int> , Interval<Int> >, Formula> > memo_bdd_conv_int_in_min_mode;
extern Map<Pair<int,Int>, Formula> memo_bdd_conv_in_min_mode;
extern Map<Pair<int,Int>, Formula> memo_bdd_conv_in_min_mode;
// -- output options:
extern bool opt_satlive;
......@@ -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 @ 589102ab
......@@ -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 \
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++8
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
......
SatELite.h
View file @ 589102ab
......@@ -505,26 +505,26 @@ struct Solver {
macro void dump(Clause c, bool newline = true, FILE* out = stdout) {
fprintf(out, "{");
for (int i = 0; i < c.size(); i++) fprintf(out, " "L_LIT, L_lit(c[i]));
for (int i = 0; i < c.size(); i++) fprintf(out, " " L_LIT, L_lit(c[i]));
fprintf(out, " }%s", newline ? "\n" : "");
fflush(out);
}
macro void dump(Solver& S, Clause c, bool newline = true, FILE* out = stdout) {
fprintf(out, "{");
for (int i = 0; i < c.size(); i++) fprintf(out, " "L_LIT":%c", L_lit(c[i]), name(S.value(c[i])));
for (int i = 0; i < c.size(); i++) fprintf(out, " " L_LIT":%c", L_lit(c[i]), name(S.value(c[i])));
fprintf(out, " }%s", newline ? "\n" : "");
fflush(out);
}
macro void dump(const vec<Lit>& c, bool newline = true, FILE* out = stdout) {
fprintf(out, "{");
for (int i = 0; i < c.size(); i++) fprintf(out, " "L_LIT, L_lit(c[i]));
for (int i = 0; i < c.size(); i++) fprintf(out, " " L_LIT, L_lit(c[i]));
fprintf(out, " }%s", newline ? "\n" : "");
fflush(out);
}
macro void dump(Solver& S, vec<Lit>& c, bool newline = true, FILE* out = stdout) {
fprintf(out, "{");
for (int i = 0; i < c.size(); i++) fprintf(out, " "L_LIT":%c", L_lit(c[i]), name(S.value(c[i])));
for (int i = 0; i < c.size(); i++) fprintf(out, " " L_LIT":%c", L_lit(c[i]), name(S.value(c[i])));
fprintf(out, " }%s", newline ? "\n" : "");
fflush(out);
}
......
Solver.h
View file @ 589102ab
This diff is collapsed.
ccminisat/core/SolverTypes.h
View file @ 589102ab
......@@ -44,7 +44,7 @@ typedef int Var;
struct Lit;
Lit mkLit(Var var, bool sign = false);
struct Lit {
int x;
......@@ -64,9 +64,9 @@ inline bool sign (Lit p) { return p.x & 1; }
inline int var (Lit p) { return p.x >> 1; }
// Mapping Literals to and from compact integers suitable for array indexing:
inline int toInt (Var v) { return v; }
inline int toInt (Lit p) { return p.x; }
inline Lit toLit (int i) { Lit p; p.x = i; return p; }
inline int toInt (Var v) { return v; }
inline int toInt (Lit p) { return p.x; }
inline Lit toLit (int i) { Lit p; p.x = i; return p; }
//const Lit lit_Undef = mkLit(var_Undef, false); // }- Useful special constants.
//const Lit lit_Error = mkLit(var_Undef, true ); // }
......@@ -79,7 +79,7 @@ const Lit lit_Error = { -1 }; // }
// Lifted booleans:
//
// NOTE: this implementation is optimized for the case when comparisons between values are mostly
// between one variable and one constant. Some care had to be taken to make sure that gcc
// between one variable and one constant. Some care had to be taken to make sure that gcc
// does enough constant propagation to produce sensible code, and this appears to be somewhat
// fragile unfortunately.
......@@ -102,7 +102,7 @@ public:
bool operator != (lbool b) const { return !(*this == b); }
lbool operator ^ (bool b) const { return lbool((uint8_t)(value^(uint8_t)b)); }
lbool operator && (lbool b) const {
lbool operator && (lbool b) const {
uint8_t sel = (this->value << 1) | (b.value << 3);
uint8_t v = (0xF7F755F4 >> sel) & 3;
return lbool(v); }
......@@ -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:
......@@ -130,7 +134,7 @@ class Clause {
unsigned learnt : 1;
unsigned has_extra : 1;
unsigned reloced : 1;
unsigned size : 27;
unsigned size : 27;
unsigned cc_const : 31;
unsigned lcc : 1;
} header;
......@@ -146,16 +150,16 @@ class Clause {
header.has_extra = use_extra;
header.reloced = 0;
header.size = ps.size();
header.cc_const = k;
header.lcc = 0;
header.cc_const = k;
header.lcc = 0;
for (int i = 0; i < ps.size(); i++)
for (int i = 0; i < ps.size(); i++)
data[i].lit = ps[i];
if (header.has_extra){
if (header.learnt)
data[header.size].act = 0;
else
data[header.size].act = 0;
else
calcAbstraction(); }
}
/*
......@@ -168,21 +172,21 @@ class Clause {
header.has_extra = use_extra;
header.reloced = 0;
header.size = ps.size();
header.cc_const = k;
header.lcc = 0;
header.cc_const = k;
header.lcc = 0;
// printf("cck = %d", header.cc_const);
for (int i = 0; i < ps.size(); i++)
// printf("cck = %d", header.cc_const);
for (int i = 0; i < ps.size(); i++)
data[i].lit = ps[i];
if (header.has_extra){
if (header.learnt)
data[header.size].act = 0;
else
data[header.size].act = 0;
else
calcAbstraction(); }
}
*/
public:
void calcAbstraction() {
assert(header.has_extra);
......@@ -260,9 +264,9 @@ class ClauseAllocator : public RegionAllocator<uint32_t>
{
assert(sizeof(Lit) == sizeof(uint32_t));
assert(sizeof(float) == sizeof(uint32_t));
bool learnt = learn;
bool learnt = learn;
bool use_extra = learnt | extra_clause_field;
int Cc_Const = k;
int Cc_Const = k;
CRef cid = RegionAllocator<uint32_t>::alloc(clauseWord32Size(ps.size(), use_extra));
new (lea(cid)) Clause(ps, use_extra, learnt, Cc_Const);
......@@ -287,45 +291,45 @@ class ClauseAllocator : public RegionAllocator<uint32_t>
void reloc(CRef& cr, ClauseAllocator& to)
{
Clause& c = operator[](cr);
if (c.reloced()) { cr = c.relocation(); return; }
/*
if(c.cc_const() > 1 && c.learnt()){
fprintf(stderr,"CNum%d ",cr);
for(int i = 0; i < c.size(); i++){
fprintf(stderr,"%d ",toInt(c[i]));
}
fprintf(stderr,"Const %d/%d l %d \n",c.cc_const(),c.size(),c.learnt());
}
*/
/*
if(c.cc_const() > 1 && c.learnt()){
fprintf(stderr,"CNum%d ",cr);
for(int i = 0; i < c.size(); i++){
fprintf(stderr,"%d ",toInt(c[i]));
}
fprintf(stderr,"Const %d/%d l %d \n",c.cc_const(),c.size(),c.learnt());
}
*/
assert(c.cc_const() == 1 || !c.learnt());
/*
if(c.cc_const() == 1){
cr = to.alloc(c, c.learnt());
}
else {
cr = to.ccalloc(c, c.learnt(), c.cc_const());
}
c.relocate(cr);
*/
/*
if(c.cc_const() == 1){
cr = to.alloc(c, c.learnt());
}
else {
cr = to.ccalloc(c, c.learnt(), c.cc_const());
}
c.relocate(cr);
*/
cr = to.alloc(c, c.learnt());
c.relocate(cr);
// Copy extra data-fields:
// Copy extra data-fields:
// (This could be cleaned-up. Generalize Clause-constructor to be applicable here instead?)
to[cr].mark(c.mark());
assert(to[cr].cc_const() == 1 || !to[cr].learnt());
if (to[cr].learnt()){
// fprintf(stderr,"C%d",c.cc_const());
to[cr].activity() = c.activity();}
if (to[cr].learnt()){
// fprintf(stderr,"C%d",c.cc_const());
to[cr].activity() = c.activity();}
else if (to[cr].has_extra()) to[cr].calcAbstraction();
to[cr].cc_const(c.cc_const());
// printf("reloc is end \n");
to[cr].cc_const(c.cc_const());
// printf("reloc is end \n");
}
};
......@@ -343,7 +347,7 @@ class OccLists
public:
OccLists(const Deleted& d) : deleted(d) {}
void init (const Idx& idx){ occs.growTo(toInt(idx)+1); dirty.growTo(toInt(idx)+1, 0); }
// Vec& operator[](const Idx& idx){ return occs[toInt(idx)]; }
Vec& operator[](const Idx& idx){ return occs[toInt(idx)]; }
......@@ -402,13 +406,13 @@ class CMap
typedef Map<CRef, T, CRefHash> HashTable;
HashTable map;
public:
// Size-operations:
void clear () { map.clear(); }
int size () const { return map.elems(); }
// Insert/Remove/Test mapping:
void insert (CRef cr, const T& t){ map.insert(cr, t); }
void growTo (CRef cr, const T& t){ map.insert(cr, t); } // NOTE: for compatibility
......@@ -435,11 +439,11 @@ class CMap
/*_________________________________________________________________________________________________
|
| subsumes : (other : const Clause&) -> Lit
|
|
| Description:
| Checks if clause subsumes 'other', and at the same time, if it can be used to simplify 'other'
| by subsumption resolution.
|
|
| Result:
| lit_Error - No subsumption or simplification
| lit_Undef - Clause subsumes 'other'
......@@ -462,18 +466,18 @@ inline Lit Clause::subsumes(const Clause& other) const
for (unsigned i = 0; i < header.size; i++) {
// search for c[i] or ~c[i]
for (unsigned j = 0; j < other.header.size; j++)
if (c[i] == d[j]){
goto ok;
}
else if (ret == lit_Undef && c[i] == ~d[j]){
count_diff++;
ret = c[i];
goto ok;
if (c[i] == d[j]){
goto ok;
}
else if (ret == lit_Undef && c[i] == ~d[j]){
count_diff++;
ret = c[i];
goto ok;
}
else if(header.cc_const - count_diff > other.header.cc_const){
count_diff++;
goto ok;
}
else if(header.cc_const - count_diff > other.header.cc_const){
count_diff++;
goto ok;
}
// did not find it
return lit_Error;
ok:;
......@@ -483,12 +487,12 @@ inline Lit Clause::subsumes(const Clause& other) const
printf("count_diff = %d \n", count_diff);
printf("this :");
for (unsigned i = 0; i < header.size; i++){
printf("%d ",toInt(c[i]));
printf("%d ",toInt(c[i]));
}
printf("const = %d/%d \n",header.cc_const,header.size);
printf("other :");
for (unsigned i = 0; i < other.header.size; i++){
printf("%d ",toInt(d[i]));
printf("%d ",toInt(d[i]));
}
printf(" const = %d/%d \n",other.header.cc_const,other.header.size);
}
......@@ -510,8 +514,8 @@ inline Lit Clause::subsumes(const Clause& other) const
return lit_Undef;
}
else{ printf();return ret;}
// return ret;
*/
// return ret;
*/
}
inline void Clause::strengthen(Lit p)
......
ccminisat/utils/System.cc
View file @ 589102ab
......@@ -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 @ 589102ab
......@@ -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 @ 589102ab
......@@ -44,7 +44,7 @@ typedef int Var;
struct Lit;
Lit mkLit(Var var, bool sign = false);
struct Lit {
int x;
......@@ -64,9 +64,9 @@ inline bool sign (Lit p) { return p.x & 1; }
inline int var (Lit p) { return p.x >> 1; }
// Mapping Literals to and from compact integers suitable for array indexing:
inline int toInt (Var v) { return v; }
inline int toInt (Lit p) { return p.x; }
inline Lit toLit (int i) { Lit p; p.x = i; return p; }
inline int toInt (Var v) { return v; }
inline int toInt (Lit p) { return p.x; }
inline Lit toLit (int i) { Lit p; p.x = i; return p; }
//const Lit lit_Undef = mkLit(var_Undef, false); // }- Useful special constants.
//const Lit lit_Error = mkLit(var_Undef, true ); // }
......@@ -79,7 +79,7 @@ const Lit lit_Error = { -1 }; // }
// Lifted booleans:
//
// NOTE: this implementation is optimized for the case when comparisons between values are mostly
// between one variable and one constant. Some care had to be taken to make sure that gcc
// between one variable and one constant. Some care had to be taken to make sure that gcc
// does enough constant propagation to produce sensible code, and this appears to be somewhat
// fragile unfortunately.
......@@ -102,7 +102,7 @@ public:
bool operator != (lbool b) const { return !(*this == b); }
lbool operator ^ (bool b) const { return lbool((uint8_t)(value^(uint8_t)b)); }
lbool operator && (lbool b) const {
lbool operator && (lbool b) const {
uint8_t sel = (this->value << 1) | (b.value << 3);
uint8_t v = (0xF7F755F4 >> sel) & 3;
return lbool(v); }
......@@ -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); }
......@@ -148,13 +151,13 @@ class Clause {
header.reloced = 0;
header.size = ps.size();
for (int i = 0; i < ps.size(); i++)
for (int i = 0; i < ps.size(); i++)
data[i].lit = ps[i];
if (header.has_extra){
if (header.learnt)
data[header.size].act = 0;
else
data[header.size].act = 0;
else
calcAbstraction(); }
}
......@@ -242,13 +245,13 @@ class ClauseAllocator : public RegionAllocator<uint32_t>
void reloc(CRef& cr, ClauseAllocator& to)
{
Clause& c = operator[](cr);
if (c.reloced()) { cr = c.relocation(); return; }
cr = to.alloc(c, c.learnt());
c.relocate(cr);
// Copy extra data-fields:
// Copy extra data-fields:
// (This could be cleaned-up. Generalize Clause-constructor to be applicable here instead?)
to[cr].mark(c.mark());
if (to[cr].learnt()) to[cr].activity() = c.activity();
......@@ -270,7 +273,7 @@ class OccLists
public:
OccLists(const Deleted& d) : deleted(d) {}
void init (const Idx& idx){ occs.growTo(toInt(idx)+1); dirty.growTo(toInt(idx)+1, 0); }
// Vec& operator[](const Idx& idx){ return occs[toInt(idx)]; }
Vec& operator[](const Idx& idx){ return occs[toInt(idx)]; }
......@@ -329,13 +332,13 @@ class CMap
typedef Map<CRef, T, CRefHash> HashTable;
HashTable map;
public:
// Size-operations:
void clear () { map.clear(); }
int size () const { return map.elems(); }
// Insert/Remove/Test mapping:
void insert (CRef cr, const T& t){ map.insert(cr, t); }
void growTo (CRef cr, const T& t){ map.insert(cr, t); } // NOTE: for compatibility
......@@ -361,11 +364,11 @@ class CMap
/*_________________________________________________________________________________________________
|
| subsumes : (other : const Clause&) -> Lit
|
|
| Description:
| Checks if clause subsumes 'other', and at the same time, if it can be used to simplify 'other'
| by subsumption resolution.
|
|
| Result:
| lit_Error - No subsumption or simplification
| lit_Undef - Clause subsumes 'other'
......
es1sat/utils/System.cc
View file @ 589102ab
......@@ -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 @ 589102ab
......@@ -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 @ 589102ab
......@@ -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 @ 589102ab
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 @ 589102ab
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 @ 589102ab
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/core/BoundedQueue.h 0 → 100644
View file @ 589102ab
/***************************************************************************************[BoundedQueue.h]
Glucose -- Copyright (c) 2009-2014, 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.
**************************************************************************************************/
#ifndef BoundedQueue_h
#define BoundedQueue_h
#include "../mtl/Vec.h"
//=================================================================================================
namespace Glucose {
template <class T>
class bqueue {
vec<T> elems;
int first;
int last;
unsigned long long sumofqueue;
int maxsize;
int queuesize; // Number of current elements (must be < maxsize !)
bool expComputed;
double exp,value;
public:
bqueue(void) :
first(0), last(0), sumofqueue(0), maxsize(0), queuesize(0),expComputed(false)
, exp(0.0), value(0.0) // added by nabesima
{ }
void initSize(int size) {growTo(size);exp = 2.0/(size+1);} // Init size of bounded size queue
void push(T x) {
expComputed = false;
if (queuesize==maxsize) {
assert(last==first); // The queue is full, next value to enter will replace oldest one
sumofqueue -= elems[last];
if ((++last) == maxsize) last = 0;
} else
queuesize++;
sumofqueue += x;
elems[first] = x;
if ((++first) == maxsize) {first = 0;last = 0;}
}
T peek() { assert(queuesize>0); return elems[last]; }
void pop() {sumofqueue-=elems[last]; queuesize--; if ((++last) == maxsize) last = 0;}
unsigned long long getsum() const {return sumofqueue;}
unsigned int getavg() const {return (unsigned int)(sumofqueue/((unsigned long long)queuesize));}
int maxSize() const {return maxsize;}
double getavgDouble() const {
double tmp = 0;
for(int i=0;i<elems.size();i++) {
tmp+=elems[i];
}
return tmp/elems.size();
}
int isvalid() const {return (queuesize==maxsize);}
void growTo(int size) {
elems.growTo(size);
first=0; maxsize=size; queuesize = 0;last = 0;
for(int i=0;i<size;i++) elems[i]=0;
}
double getAvgExp() {
if(expComputed) return value;
double a=exp;
value = elems[first];
for(int i = first;i<maxsize;i++) {
value+=a*((double)elems[i]);
a=a*exp;
}
for(int i = 0;i<last;i++) {
value+=a*((double)elems[i]);
a=a*exp;
}
value = value*(1-exp)/(1-a);
expComputed = true;
return value;
}
void fastclear() {first = 0; last = 0; queuesize=0; sumofqueue=0;} // to be called after restarts... Discard the queue
int size(void) { return queuesize; }
void clear(bool dealloc = false) { elems.clear(dealloc); first = 0; maxsize=0; queuesize=0;sumofqueue=0;}
void copyTo(bqueue &dest) const {
dest.last = last;
dest.sumofqueue = sumofqueue;
dest.maxsize = maxsize;
dest.queuesize = queuesize;
dest.expComputed = expComputed;
dest.exp = exp;
dest.value = value;
dest.first = first;
elems.copyTo(dest.elems);
}
};
}
//=================================================================================================
#endif
manyglucose/core/Constants.h 0 → 100644
View file @ 589102ab
/***************************************************************************************[Constants.h]
Glucose -- Copyright (c) 2009-2014, 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.
**************************************************************************************************/
#define DYNAMICNBLEVEL
#define CONSTANTREMOVECLAUSE
// Constants for clauses reductions
#define RATIOREMOVECLAUSES 2
// Constants for restarts
#define LOWER_BOUND_FOR_BLOCKING_RESTART 10000
manyglucose/core/Dimacs.h 0 → 100644
View file @ 589102ab
/****************************************************************************************[Dimacs.h]
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.
**************************************************************************************************/
#ifndef Glucose_Dimacs_h
#define Glucose_Dimacs_h
#include <stdio.h>
#include "../utils/ParseUtils.h"
#include "../core/SolverTypes.h"
namespace Glucose {
//=================================================================================================
// DIMACS Parser:
template<class B, class Solver>
static void readClause(B& in, Solver& S, vec<Lit>& lits) {
int parsed_lit, var;
lits.clear();
for (;;){
parsed_lit = parseInt(in);
if (parsed_lit == 0) break;
var = abs(parsed_lit)-1;
while (var >= S.nVars()) S.newVar();
lits.push( (parsed_lit > 0) ? mkLit(var) : ~mkLit(var) );
}
}
template<class B, class Solver>
static void parse_DIMACS_main(B& in, Solver& S) {
vec<Lit> lits;
int vars = 0;
int clauses = 0;
int cnt = 0;
for (;;){
skipWhitespace(in);
if (*in == EOF) break;
else if (*in == 'p'){
if (eagerMatch(in, "p cnf")){
vars = parseInt(in);
clauses = parseInt(in);
// SATRACE'06 hack
// if (clauses > 4000000)
// S.eliminate(true);
}else{
printf("PARSE ERROR! Unexpected char: %c\n", *in), exit(3);
}
} else if (*in == 'c' || *in == 'p')
skipLine(in);
else{
cnt++;
readClause(in, S, lits);
S.addClause_(lits); }
}
if (vars != S.nVars())
fprintf(stderr, "WARNING! DIMACS header mismatch: wrong number of variables.\n");
if (cnt != clauses)
fprintf(stderr, "WARNING! DIMACS header mismatch: wrong number of clauses.\n");
}
// Inserts problem into solver.
//
template<class Solver>
static void parse_DIMACS(gzFile input_stream, Solver& S) {
StreamBuffer in(input_stream);
parse_DIMACS_main(in, S); }
//=================================================================================================
}
#endif
manyglucose/core/Makefile 0 → 100644
View file @ 589102ab
PHONY:
@echo "** Careful ** Since 4.0 you have to use the simp or parallel directory only for typing make"
manyglucose/core/Solver.cc 0 → 100644
View file @ 589102ab
This diff is collapsed.
manyglucose/core/Solver.h 0 → 100644
View file @ 589102ab
This diff is collapsed.
manyglucose/core/SolverStats.h 0 → 100644
View file @ 589102ab
This diff is collapsed.
manyglucose/core/SolverTypes.h 0 → 100644
View file @ 589102ab
This diff is collapsed.
manyglucose/mtl/Alg.h 0 → 100644
View file @ 589102ab
This diff is collapsed.
manyglucose/mtl/Alloc.h 0 → 100644
View file @ 589102ab
This diff is collapsed.
manyglucose/mtl/CSV.h 0 → 100644
View file @ 589102ab
This diff is collapsed.
manyglucose/mtl/Clone.cc 0 → 100644
View file @ 589102ab
/*
* Clone.cc
*
* Created on: 2018/03/20
* Author: nabesima
*/
#include "Clone.h"
namespace Glucose {
Clone::~Clone() {}
};
manyglucose/mtl/Clone.h 0 → 100644
View file @ 589102ab
#ifndef Glucose_Clone_h
#define Glucose_Clone_h
namespace Glucose {
class Clone {
public:
virtual Clone* clone() const = 0;
virtual ~Clone() = 0; // added by nabesima
};
};
#endif
manyglucose/mtl/Heap.h 0 → 100644
View file @ 589102ab
This diff is collapsed.
manyglucose/mtl/IntSet.h 0 → 100644
View file @ 589102ab
This diff is collapsed.
manyglucose/mtl/IntTypes.h 0 → 100644
View file @ 589102ab
This diff is collapsed.
manyglucose/mtl/Map.h 0 → 100644
View file @ 589102ab
This diff is collapsed.
manyglucose/mtl/Queue.h 0 → 100644
View file @ 589102ab
This diff is collapsed.
manyglucose/mtl/Sort.h 0 → 100644
View file @ 589102ab
This diff is collapsed.
manyglucose/mtl/Stopwatch.h 0 → 100644
View file @ 589102ab
This diff is collapsed.
manyglucose/mtl/Vec.h 0 → 100644
View file @ 589102ab
This diff is collapsed.
manyglucose/mtl/VecThreads.h 0 → 100644
View file @ 589102ab
This diff is collapsed.
manyglucose/mtl/XAlloc.h 0 → 100644
View file @ 589102ab
This diff is collapsed.
manyglucose/mtl/config.mk 0 → 100644
View file @ 589102ab
##
## This file is for system specific configurations. For instance, on
## some systems the path to zlib needs to be added. Example:
##
## CFLAGS += -I/usr/local/include
## LFLAGS += -L/usr/local/lib
manyglucose/mtl/template.mk 0 → 100644
View file @ 589102ab
This diff is collapsed.
manyglucose/parallel/ClausesBuffer.cc 0 → 100644
View file @ 589102ab
This diff is collapsed.
manyglucose/parallel/ClausesBuffer.h 0 → 100644
View file @ 589102ab
This diff is collapsed.
manyglucose/parallel/Main.cc 0 → 100644
View file @ 589102ab
This diff is collapsed.
manyglucose/parallel/Makefile 0 → 100644
View file @ 589102ab
VERSION = 4.1-27
EXEC = manyglucose-$(VERSION)
DEPDIR = mtl utils core simp
MROOT = ..
include $(MROOT)/mtl/template.mk
manyglucose/parallel/MultiSolvers.cc 0 → 100644
View file @ 589102ab
This diff is collapsed.
manyglucose/parallel/MultiSolvers.h 0 → 100644
View file @ 589102ab
This diff is collapsed.
manyglucose/parallel/ParallelSolver.cc 0 → 100644
View file @ 589102ab
This diff is collapsed.
manyglucose/parallel/ParallelSolver.h 0 → 100644
View file @ 589102ab
This diff is collapsed.
manyglucose/parallel/PeriodClausesBuffer.cc 0 → 100644
View file @ 589102ab
This diff is collapsed.
manyglucose/parallel/PeriodClausesBuffer.h 0 → 100644
View file @ 589102ab
This diff is collapsed.
manyglucose/parallel/PrdClauses.cc 0 → 100644
View file @ 589102ab
This diff is collapsed.