fixed maple bug

run.sh

@@ -21,9 +21,9 @@
 # - 367c25ad50259a685a25b86d6dd171b2-GP_100_950_33.cnf
 
 # 这个存在问题
-DIR=/pub/data/chenzh/data/sat2021
+DIR=/pub/data/chenzh/data/sat2022
 # INSTANCE=tseitingrid7x165_shuffled.cnf
-INSTANCE=WS_500_16_70_10.apx_0.cnf
+INSTANCE=a44fce1796383ea31df08af3b0f65db3-soelberg_unit_159.cnf
 
 make -j && mpirun --bind-to none -np 9 --allow-run-as-root ./light -i $DIR/$INSTANCE --shuffle=1 --share=1 --threads=16 --times=3600 --share_method=0
 

run2.sh

@@ -0,0 +1,31 @@
+#!/bin/bash
+
+# cd kissat-inc
+# make clean
+# ./configure
+# make -j 64
+# cd ..
+# make clean
+
+# buglist
+# - fe96b630b3e761821308b544368dd521-GP_100_950_34.cnf
+# - 0d4970edf84353e5a5798bca3f7f270e-SAT_H_instances_childsnack_p10.hddl_2.cnf
+
+
+# 退出慢
+# - 00aefd1fc30c425075166ca051e57218-barman-pfile10-038.sas.ex.15.cnf
+# - 23e61c50ee2ac5cad1d337572abdebcf-aws-encryption-sdk-c:aws_cryptosdk_priv_hdr_parse_edks.cnf
+
+# 解不出来
+# - 72329bc80f5f55dcc356a22f3f11ebec-GP_200_313_5.cnf
+# - 367c25ad50259a685a25b86d6dd171b2-GP_100_950_33.cnf
+
+# 这个存在问题
+DIR=/pub/data/chenzh/data/sat2022
+# INSTANCE=tseitingrid7x165_shuffled.cnf
+INSTANCE=a44fce1796383ea31df08af3b0f65db3-soelberg_unit_159.cnf
+
+make -j && mpirun --bind-to none -np 9 --allow-run-as-root ./light -i $DIR/$INSTANCE --shuffle=1 --share=0 --threads=16 --times=3600 --share_method=0
+
+# make -j 16 && mpirun --mca btl_tcp_if_include 192.168.100.0/24 --hostfile ./experiment/hostfile --bind-to none -np 65 --allow-run-as-root ./light -i $DIR/$INSTANCE --share=1 --threads=16 --times=3600 --share_method=0
+#./light -i $DIR/$INSTANCE --share=1 --threads=16 --times=3600

src/solve.cpp

@@ -28,7 +28,7 @@ void * solve_worker(void *arg) {
    while (!terminated) {
         int res = sq->solve();
         if (res && !terminated) {
-            printf("c result: %d, winner is %d, winner run %d confs\n", res, sq->id, sq->get_conflicts());
+            // printf("c result: %d, winner is %d, winner run %d confs\n", res, sq->id, sq->get_conflicts());
 
             // terminated = 1;
             // sq->controller->terminate_workers();
@@ -41,7 +41,7 @@ void * solve_worker(void *arg) {
             terminated = 1;
             sq->controller->terminate_workers();
         }
-        printf("get result %d with res %d\n", sq->id, res);
+        // printf("get result %d with res %d\n", sq->id, res);
    }
    return NULL;
 }

src/solver_api/basemaple.cpp

@@ -43,7 +43,7 @@ int basemaple::val(int l) {
       int lit = solver->model[l] == (MapleCOMSPS::lbool((uint8_t)0)) ? l + 1 : -(l + 1);
       return lit;
    }
-   return l;
+   return l + 1;
 }
 
 void basemaple::terminate() {