.cproject

-<?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

@@ -4,9 +4,13 @@
 *.od
 *.or
 *.ox
-*.mk
 naps
 *_profile
 *_debug
 *_release
 *_static
+*.exe
+depend.mak
+.cproject
+.project
+.settings/

.project

-<?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.h

@@ -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

@@ -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

@@ -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);
 }

ccminisat/core/SolverTypes.h

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

+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

+ 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

+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

+/***************************************************************************************[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

+/***************************************************************************************[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

+/****************************************************************************************[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

+PHONY:
+	@echo "** Careful ** Since 4.0 you have to use the simp or parallel directory only for typing make"
+

manyglucose/mtl/Clone.cc

+/*
+ * Clone.cc
+ *
+ *  Created on: 2018/03/20
+ *      Author: nabesima
+ */
+#include "Clone.h"
+
+namespace Glucose {
+
+Clone::~Clone() {}
+
+};
+
+
+
+

manyglucose/mtl/Clone.h

+#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/config.mk

+##
+##  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/parallel/Makefile

+VERSION   = 4.1-27
+EXEC      = manyglucose-$(VERSION)
+DEPDIR    = mtl utils core simp
+MROOT = ..
+include $(MROOT)/mtl/template.mk