WIP

.github/workflows/test.yml

@@ -12,15 +12,19 @@ jobs:
       fail-fast: false
       matrix:
         os: ['ubuntu-latest', 'macos-latest', 'windows-latest']
+        build_threads: ['On']
+        build_type: ['Debug']
         include:
           - os: 'ubuntu-latest'
+            build_threads: 'On'
             generator: 'Ninja'
-            build_type: 'Debug'
           - os: 'macos-latest'
             generator: 'Ninja'
-            build_type: 'Debug'
           - os: 'windows-latest'
             generator: 'Visual Studio 17 2022'
+          - os: 'ubuntu-latest'
+            build_threads: 'Off'
+            generator: 'Ninja'
             build_type: 'Debug'
 
     steps:
@@ -46,6 +50,7 @@ jobs:
         -B "${{github.workspace}}/build"
         -DCMAKE_BUILD_TYPE="${{matrix.build_type}}"
         -DCLASP_BUILD_TESTS="On"
+        -DCLASP_BUILD_WITH_THREADS="${{matrix.build_threads}}"
         -DLIB_POTASSCO_BUILD_TESTS="On"
         -DCMAKE_CXX_STANDARD="14"
 

clasp/solver_strategies.h

@@ -396,7 +396,7 @@ struct DynamicLimit {
  * \see A. Biere, A. Froehlich "Evaluating CDCL Restart Schemes"
  */
 struct BlockLimit {
-	explicit BlockLimit(uint32 windowSize, double R = 1.4, MovingAvg::Type t = MovingAvg::Type::avg_ema);
+	explicit BlockLimit(uint32 windowSize, double R = 1.4, MovingAvg::Type t = MovingAvg::avg_ema);
 	bool push(uint32 nAssign) {
 		avg.push(nAssign);
 		return ++n >= next;

src/clasp_options.cpp

@@ -301,8 +301,8 @@ static int xconvert(const char* x, RestartSchedule& out, const char** errPos, in
 	using Potassco::xconvert;
 	std::pair<uint32, double> req(0, 0);
 	uint32             lim  = 0, sWin = 0;
-	MovingAvg::Type    fast = MovingAvg::Type::avg_sma;
-	MovingAvg::Type    slow = MovingAvg::Type::avg_sma;
+	MovingAvg::Type    fast = MovingAvg::avg_sma;
+	MovingAvg::Type    slow = MovingAvg::avg_sma;
 	DynamicLimit::Keep keep = RestartSchedule::keep_never;
 	const char*        next = 0;
 	if (x[1] != ',' || !xconvert(x + 2, req, &x, e) || req.first == 0 || req.second <= 0.0)
@@ -311,11 +311,11 @@ static int xconvert(const char* x, RestartSchedule& out, const char** errPos, in
 		return convertRet(0, x, errPos);
 	if (*x == ',' && !xconvert(x + 1, fast, &x, e))
 		return convertRet(0, x, errPos);
-	if (*x == ',' && fast != MovingAvg::Type::avg_sma && xconvert(x + 1, keep, &next, e))
+	if (*x == ',' && fast != MovingAvg::avg_sma && xconvert(x + 1, keep, &next, e))
 		x = next;
 	if (*x == ',' && !xconvert(x + 1, slow, &x, e))
 		return convertRet(0, x, errPos);
-	if (*x == ',' && slow != MovingAvg::Type::avg_sma && !xconvert(x + 1, sWin, &x, e))
+	if (*x == ',' && slow != MovingAvg::avg_sma && !xconvert(x + 1, sWin, &x, e))
 		return convertRet(0, x, errPos);
 	out = RestartSchedule::dynamic(req.first, static_cast<float>(req.second), lim, fast, keep, slow, sWin);
 	return convertRet(1, x, errPos);

src/solver_strategies.cpp

@@ -201,7 +201,7 @@ void DynamicLimit::resetAdjust(float k, Type t, uint32 uLimit, bool resetAvg) {
 	}
 }
 void DynamicLimit::block() {
-	resetRun(Keep::keep_block);
+	resetRun(RestartSchedule::keep_block);
 }
 
 void DynamicLimit::resetRun(Keep k) {
@@ -211,7 +211,7 @@ void DynamicLimit::resetRun(Keep k) {
 }
 void DynamicLimit::reset() {
 	global_.reset();
-	resetRun(Keep::keep_never);
+	resetRun(RestartSchedule::keep_never);
 }
 void DynamicLimit::update(uint32 dl, uint32 lbd) {
 	// update global avg
@@ -240,7 +240,7 @@ uint32 DynamicLimit::restart(uint32 maxLBD, float k) {
 		}
 		resetAdjust(rk, nt, uLim);
 	}
-	resetRun(Keep::keep_restart);
+	resetRun(RestartSchedule::keep_restart);
 	return adjust.limit;
 }
 BlockLimit::BlockLimit(uint32 windowSize, double R, MovingAvg::Type at)

tests/cli_test.cpp

@@ -567,16 +567,16 @@ TEST_CASE("Cli options", "[cli]") {
 		const RestartSchedule& rs = config.search(0).restart.rsSched;
 		REQUIRE(rs.isDynamic());
 		REQUIRE(rs.lbdLim() == 0);
-		REQUIRE(rs.fastAvg() == MovingAvg::Type::avg_ema_smooth);
+		REQUIRE(rs.fastAvg() == MovingAvg::avg_ema_smooth);
 		REQUIRE(rs.keepAvg() == RestartSchedule::keep_restart);
 
 		REQUIRE(config.setValue("solver.restarts", "D,100,0.9,255,ls,rb,e,1234"));
 		REQUIRE(config.getValue("solver.restarts") == "d,100,0.9,255,ls,br,e,1234");
 		REQUIRE(rs.isDynamic());
 		REQUIRE(rs.lbdLim() == 255);
-		REQUIRE(rs.fastAvg() == MovingAvg::Type::avg_ema_log_smooth);
+		REQUIRE(rs.fastAvg() == MovingAvg::avg_ema_log_smooth);
 		REQUIRE(rs.keepAvg() == RestartSchedule::keep_always);
-		REQUIRE(rs.slowAvg() == MovingAvg::Type::avg_ema);
+		REQUIRE(rs.slowAvg() == MovingAvg::avg_ema);
 		REQUIRE(rs.slowWin() == 1234);
 
 		REQUIRE_FALSE(config.setValue("solver.restarts", "D,100,0.9,255,ls,rb,e,1234,12"));
@@ -585,9 +585,9 @@ TEST_CASE("Cli options", "[cli]") {
 		REQUIRE(config.getValue("solver.restarts") == "d,50,0.8,0,ls,es,10000");
 		REQUIRE(rs.isDynamic());
 		REQUIRE(rs.lbdLim() == 0);
-		REQUIRE(rs.fastAvg() == MovingAvg::Type::avg_ema_log_smooth);
+		REQUIRE(rs.fastAvg() == MovingAvg::avg_ema_log_smooth);
 		REQUIRE(rs.keepAvg() == RestartSchedule::keep_never);
-		REQUIRE(rs.slowAvg() == MovingAvg::Type::avg_ema_smooth);
+		REQUIRE(rs.slowAvg() == MovingAvg::avg_ema_smooth);
 		REQUIRE(rs.slowWin() == 10000);
 	}
 
@@ -601,7 +601,7 @@ TEST_CASE("Cli options", "[cli]") {
 		REQUIRE(b.window == 5000);
 		REQUIRE(b.first == 10000);
 		REQUIRE(b.scale() == 1.4f);
-		REQUIRE(b.avg == uint32(MovingAvg::Type::avg_ema));
+		REQUIRE(b.avg == uint32(MovingAvg::avg_ema));
 
 		REQUIRE_FALSE(config.setValue("solver.block_restarts", "5000,0.8"));
 		REQUIRE_FALSE(config.setValue("solver.block_restarts", "5000,5.1"));
@@ -611,7 +611,7 @@ TEST_CASE("Cli options", "[cli]") {
 		REQUIRE(b.window == 10000);
 		REQUIRE(b.scale() == 1.1f);
 		REQUIRE(b.first == 0);
-		REQUIRE(b.avg == uint32(MovingAvg::Type::avg_sma));
+		REQUIRE(b.avg == uint32(MovingAvg::avg_sma));
 	}
 
 	SECTION("test opt-stop option")	{