version 0.5.8

shnarazk · Apr 16, 2019 · d478ae6 · d478ae6
1 parent 73bb700
commit d478ae6
Show file tree

Hide file tree

Showing 6 changed files with 825 additions and 123 deletions.
diff --git a/Cargo.lock b/Cargo.lock
diff --git a/Cargo.toml b/Cargo.toml
@@ -1,6 +1,6 @@
 [package]
 name = "sat-bench"
-version = "0.5.7"
+version = "0.5.8"
 authors = ["Shuji Narazaki <[email protected]>"]
 edition = "2018"
 

diff --git a/LICENSE b/LICENSE
diff --git a/src/bench18.rs b/src/bench18.rs
@@ -1,103 +1,103 @@
 pub const SCB: [(usize, &str); 400] = [
-    (  1, "10-3-13.cnf"),
-    (  2, "10-4-10.cnf"),
-    (  3, "1mod8.rules.7-7.cnf"),
-    (  4, "20180321_110704973_p_cnf_320_1120.cnf"),
-    (  5, "20180321_110706599_p_cnf_320_1120.cnf"),
-    (  6, "20180321_110707239_p_cnf_320_1120.cnf"),
-    (  7, "20180321_140823961_p_cnf_320_1120.cnf"),
-    (  8, "20180321_140824282_p_cnf_320_1120.cnf"),
-    (  9, "20180321_140826713_p_cnf_320_1120.cnf"),
-    ( 10, "20180321_140827428_p_cnf_320_1120.cnf"),
-    ( 11, "20180321_140833987_p_cnf_320_1120.cnf"),
-    ( 12, "20180322_164223076_p_cnf_320_1120.cnf"),
-    ( 13, "20180322_164224543_p_cnf_320_1120.cnf"),
-    ( 14, "20180322_164226378_p_cnf_320_1120.cnf"),
-    ( 15, "20180322_164226661_p_cnf_320_1120.cnf"),
-    ( 16, "20180322_164238439_p_cnf_320_1120.cnf"),
-    ( 17, "20180322_164241329_p_cnf_320_1120.cnf"),
-    ( 18, "20180322_164241842_p_cnf_320_1120.cnf"),
-    ( 19, "20180322_164245263_p_cnf_320_1120.cnf"),
-    ( 20, "20180326_095801070_p_cnf_320_1120.cnf"),
-    ( 21, "20180326_095804286_p_cnf_320_1120.cnf"),
-    ( 22, "20180326_095804936_p_cnf_320_1120.cnf"),
-    ( 23, "20180326_095805836_p_cnf_320_1120.cnf"),
-    ( 24, "5or7mod8.rules.7-7.cnf"),
-    ( 25, "6-3-8.cnf"),
-    ( 26, "6-4-6.cnf"),
-    ( 27, "6-4-7.cnf"),
-    ( 28, "6-5-6.cnf"),
-    ( 29, "7-4-7.cnf"),
-    ( 30, "7-5-6.cnf"),
-    ( 31, "8-4-10.cnf"),
-    ( 32, "8-4-8.cnf"),
-    ( 33, "8-4-9.cnf"),
-    ( 34, "8-5-6.cnf"),
-    ( 35, "9-4-10.cnf"),
-    ( 36, "9-4-9.cnf"),
-    ( 37, "C3-2-31.cnf"),
-    ( 38, "CNP-5-0.cnf"),
-    ( 39, "CNP-5-100.cnf"),
-    ( 40, "CNP-5-1000.cnf"),
-    ( 41, "CNP-5-1100.cnf"),
-    ( 42, "CNP-5-1200.cnf"),
-    ( 43, "CNP-5-1300.cnf"),
-    ( 44, "CNP-5-1400.cnf"),
-    ( 45, "CNP-5-1500.cnf"),
-    ( 46, "CNP-5-1600.cnf"),
-    ( 47, "CNP-5-1700.cnf"),
-    ( 48, "CNP-5-1800.cnf"),
-    ( 49, "CNP-5-1900.cnf"),
-    ( 50, "CNP-5-200.cnf"),
-    ( 51, "CNP-5-300.cnf"),
-    ( 52, "CNP-5-400.cnf"),
-    ( 53, "CNP-5-500.cnf"),
-    ( 54, "CNP-5-600.cnf"),
-    ( 55, "CNP-5-700.cnf"),
-    ( 56, "CNP-5-800.cnf"),
-    ( 57, "CNP-5-900.cnf"),
-    ( 58, "Cake_8_16.cnf"),
-    ( 59, "Cake_9_19.cnf"),
-    ( 60, "Cake_9_20.cnf"),
-    ( 61, "Karatsuba4477457x5308417.cnf"),
-    ( 62, "Karatsuba6972593x13466917.cnf"),
-    ( 63, "Karatsuba7654321x1234567.cnf"),
-    ( 64, "Nb11T118.cnf"),
-    ( 65, "Nb13T165.cnf"),
-    ( 66, "Nb13T166.cnf"),
-    ( 67, "Nb14T194.cnf"),
-    ( 68, "Nb27T6.cnf"),
-    ( 69, "Nb29T6.cnf"),
-    ( 70, "Nb37T6.cnf"),
-    ( 71, "Nb39T6.cnf"),
-    ( 72, "Nb42T6.cnf"),
-    ( 73, "Nb44T6.cnf"),
-    ( 74, "Nb45T6.cnf"),
-    ( 75, "Nb49T6.cnf"),
-    ( 76, "Nb51T6.cnf"),
-    ( 77, "Nb52T6.cnf"),
-    ( 78, "Nb54T6.cnf"),
-    ( 79, "Nb8T60.cnf"),
-    ( 80, "Nb8T61.cnf"),
-    ( 81, "Nb8T62.cnf"),
-    ( 82, "Nb8T63.cnf"),
-    ( 83, "Problem11_label29_false-unreach-call.c.cnf"),
-    ( 84, "Problem11_label51_false-unreach-call.c.cnf"),
-    ( 85, "Problem14_label14_false-unreach-call.c.cnf"),
-    ( 86, "Problem14_label19_true-unreach-call.c.cnf"),
-    ( 87, "Problem14_label20_true-unreach-call.c.cnf"),
-    ( 88, "Problem14_label48_true-unreach-call.c.cnf"),
-    ( 89, "Problem14_label55_true-unreach-call.c.cnf"),
-    ( 90, "Problem14_label57_false-unreach-call.c.cnf"),
-    ( 91, "T103.2.0.cnf"),
-    ( 92, "T105.2.0.cnf"),
-    ( 93, "T107.2.0.cnf"),
-    ( 94, "T116.2.0.cnf"),
-    ( 95, "T117.2.0.cnf"),
-    ( 96, "T122.2.0.cnf"),
-    ( 97, "T125.2.0.cnf"),
-    ( 98, "T129.2.0.cnf"),
-    ( 99, "T56.2.0.cnf"),
+    (1, "10-3-13.cnf"),
+    (2, "10-4-10.cnf"),
+    (3, "1mod8.rules.7-7.cnf"),
+    (4, "20180321_110704973_p_cnf_320_1120.cnf"),
+    (5, "20180321_110706599_p_cnf_320_1120.cnf"),
+    (6, "20180321_110707239_p_cnf_320_1120.cnf"),
+    (7, "20180321_140823961_p_cnf_320_1120.cnf"),
+    (8, "20180321_140824282_p_cnf_320_1120.cnf"),
+    (9, "20180321_140826713_p_cnf_320_1120.cnf"),
+    (10, "20180321_140827428_p_cnf_320_1120.cnf"),
+    (11, "20180321_140833987_p_cnf_320_1120.cnf"),
+    (12, "20180322_164223076_p_cnf_320_1120.cnf"),
+    (13, "20180322_164224543_p_cnf_320_1120.cnf"),
+    (14, "20180322_164226378_p_cnf_320_1120.cnf"),
+    (15, "20180322_164226661_p_cnf_320_1120.cnf"),
+    (16, "20180322_164238439_p_cnf_320_1120.cnf"),
+    (17, "20180322_164241329_p_cnf_320_1120.cnf"),
+    (18, "20180322_164241842_p_cnf_320_1120.cnf"),
+    (19, "20180322_164245263_p_cnf_320_1120.cnf"),
+    (20, "20180326_095801070_p_cnf_320_1120.cnf"),
+    (21, "20180326_095804286_p_cnf_320_1120.cnf"),
+    (22, "20180326_095804936_p_cnf_320_1120.cnf"),
+    (23, "20180326_095805836_p_cnf_320_1120.cnf"),
+    (24, "5or7mod8.rules.7-7.cnf"),
+    (25, "6-3-8.cnf"),
+    (26, "6-4-6.cnf"),
+    (27, "6-4-7.cnf"),
+    (28, "6-5-6.cnf"),
+    (29, "7-4-7.cnf"),
+    (30, "7-5-6.cnf"),
+    (31, "8-4-10.cnf"),
+    (32, "8-4-8.cnf"),
+    (33, "8-4-9.cnf"),
+    (34, "8-5-6.cnf"),
+    (35, "9-4-10.cnf"),
+    (36, "9-4-9.cnf"),
+    (37, "C3-2-31.cnf"),
+    (38, "CNP-5-0.cnf"),
+    (39, "CNP-5-100.cnf"),
+    (40, "CNP-5-1000.cnf"),
+    (41, "CNP-5-1100.cnf"),
+    (42, "CNP-5-1200.cnf"),
+    (43, "CNP-5-1300.cnf"),
+    (44, "CNP-5-1400.cnf"),
+    (45, "CNP-5-1500.cnf"),
+    (46, "CNP-5-1600.cnf"),
+    (47, "CNP-5-1700.cnf"),
+    (48, "CNP-5-1800.cnf"),
+    (49, "CNP-5-1900.cnf"),
+    (50, "CNP-5-200.cnf"),
+    (51, "CNP-5-300.cnf"),
+    (52, "CNP-5-400.cnf"),
+    (53, "CNP-5-500.cnf"),
+    (54, "CNP-5-600.cnf"),
+    (55, "CNP-5-700.cnf"),
+    (56, "CNP-5-800.cnf"),
+    (57, "CNP-5-900.cnf"),
+    (58, "Cake_8_16.cnf"),
+    (59, "Cake_9_19.cnf"),
+    (60, "Cake_9_20.cnf"),
+    (61, "Karatsuba4477457x5308417.cnf"),
+    (62, "Karatsuba6972593x13466917.cnf"),
+    (63, "Karatsuba7654321x1234567.cnf"),
+    (64, "Nb11T118.cnf"),
+    (65, "Nb13T165.cnf"),
+    (66, "Nb13T166.cnf"),
+    (67, "Nb14T194.cnf"),
+    (68, "Nb27T6.cnf"),
+    (69, "Nb29T6.cnf"),
+    (70, "Nb37T6.cnf"),
+    (71, "Nb39T6.cnf"),
+    (72, "Nb42T6.cnf"),
+    (73, "Nb44T6.cnf"),
+    (74, "Nb45T6.cnf"),
+    (75, "Nb49T6.cnf"),
+    (76, "Nb51T6.cnf"),
+    (77, "Nb52T6.cnf"),
+    (78, "Nb54T6.cnf"),
+    (79, "Nb8T60.cnf"),
+    (80, "Nb8T61.cnf"),
+    (81, "Nb8T62.cnf"),
+    (82, "Nb8T63.cnf"),
+    (83, "Problem11_label29_false-unreach-call.c.cnf"),
+    (84, "Problem11_label51_false-unreach-call.c.cnf"),
+    (85, "Problem14_label14_false-unreach-call.c.cnf"),
+    (86, "Problem14_label19_true-unreach-call.c.cnf"),
+    (87, "Problem14_label20_true-unreach-call.c.cnf"),
+    (88, "Problem14_label48_true-unreach-call.c.cnf"),
+    (89, "Problem14_label55_true-unreach-call.c.cnf"),
+    (90, "Problem14_label57_false-unreach-call.c.cnf"),
+    (91, "T103.2.0.cnf"),
+    (92, "T105.2.0.cnf"),
+    (93, "T107.2.0.cnf"),
+    (94, "T116.2.0.cnf"),
+    (95, "T117.2.0.cnf"),
+    (96, "T122.2.0.cnf"),
+    (97, "T125.2.0.cnf"),
+    (98, "T129.2.0.cnf"),
+    (99, "T56.2.0.cnf"),
     (100, "T62.2.0.cnf"),
     (101, "T77.2.0.cnf"),
     (102, "T82.2.0.cnf"),
@@ -180,15 +180,24 @@ pub const SCB: [(usize, &str); 400] = [
     (179, "cms-scheel-md4-families-r24-c6-p0-5-10-11-17-18.cnf"),
     (180, "cms-scheel-md4-families-r24-c6-p1-9-13-16-18-19.cnf"),
     (181, "cms-scheel-md4-families-r24-c6-p2-4-9-16-17-19.cnf"),
-    (182, "cms-scheel-md4-families-r24-c8-p2-3-4-5-7-12-16-19.cnf"),
-    (183, "cms-scheel-md5-families-r24-c11-p1-4-6-9-10-11-13-15-17-18-19.cnf"),
+    (
+        182,
+        "cms-scheel-md4-families-r24-c8-p2-3-4-5-7-12-16-19.cnf",
+    ),
+    (
+        183,
+        "cms-scheel-md5-families-r24-c11-p1-4-6-9-10-11-13-15-17-18-19.cnf",
+    ),
     (184, "cms-scheel-md5-families-r24-c4-p1-3-4-16.cnf"),
     (185, "cms-scheel-md5-families-r24-c5-p2-7-8-15-19.cnf"),
     (186, "cms-scheel-md5-families-r24-c5-p6-11-15-16-19.cnf"),
     (187, "cms-scheel-md5-families-r24-c6-p1-4-6-13-14-18.cnf"),
     (188, "cms-scheel-md5-families-r24-c7-p1-3-6-10-11-14-15.cnf"),
     (189, "cms-scheel-md5-families-r24-c7-p1-5-6-12-16-18-19.cnf"),
-    (190, "cms-scheel-md5-families-r24-c8-p0-3-5-6-14-16-18-19.cnf"),
+    (
+        190,
+        "cms-scheel-md5-families-r24-c8-p0-3-5-6-14-16-18-19.cnf",
+    ),
     (191, "commutativity.c.cnf"),
     (192, "commutativity3.c.cnf"),
     (193, "course0.12_2018_3_1.cnf"),
@@ -312,10 +321,22 @@ pub const SCB: [(usize, &str); 400] = [
     (311, "newton_3_4_true-unreach-call.i.cnf"),
     (312, "newton_3_6_false-unreach-call.i.cnf"),
     (313, "ortholatin-7.cnf"),
-    (314, "pals_floodmax.5_overflow_false-unreach-call.ufo.UNBOUNDED.pals.c.cnf"),
-    (315, "pals_lcr-var-start-time.5_true-unreach-call.ufo.UNBOUNDED.pals.c.cnf"),
-    (316, "pals_lcr-var-start-time.6_true-unreach-call.ufo.UNBOUNDED.pals.c.cnf"),
-    (317, "pals_lcr.8_overflow_false-unreach-call.ufo.UNBOUNDED.pals.c.cnf"),
+    (
+        314,
+        "pals_floodmax.5_overflow_false-unreach-call.ufo.UNBOUNDED.pals.c.cnf",
+    ),
+    (
+        315,
+        "pals_lcr-var-start-time.5_true-unreach-call.ufo.UNBOUNDED.pals.c.cnf",
+    ),
+    (
+        316,
+        "pals_lcr-var-start-time.6_true-unreach-call.ufo.UNBOUNDED.pals.c.cnf",
+    ),
+    (
+        317,
+        "pals_lcr.8_overflow_false-unreach-call.ufo.UNBOUNDED.pals.c.cnf",
+    ),
     (318, "patat-08-comp-3.cnf"),
     (319, "prime_119218851371.cnf"),
     (320, "prime_200560490131.cnf"),
@@ -362,7 +383,10 @@ pub const SCB: [(usize, &str); 400] = [
     (361, "si2-m4Dr2-m256-08.cnf"),
     (362, "si2-r001-m200-00.cnf"),
     (363, "si2-r001-m200-09.cnf"),
-    (364, "sqrt_Householder_pseudoconstant_true-unreach-call.c.cnf"),
+    (
+        364,
+        "sqrt_Householder_pseudoconstant_true-unreach-call.c.cnf",
+    ),
     (365, "sqrt_ineq_2.c.cnf"),
     (366, "sqrt_ineq_3.c.cnf"),
     (367, "sted1_0x0-330.cnf"),
@@ -385,7 +409,10 @@ pub const SCB: [(usize, &str); 400] = [
     (384, "sted5_0x24204-50.cnf"),
     (385, "sted5_0x24204-60.cnf"),
     (386, "sted5_0x24204-70.cnf"),
-    (387, "terminator_03_true-unreach-call_true-termination.i.cnf"),
+    (
+        387,
+        "terminator_03_true-unreach-call_true-termination.i.cnf",
+    ),
     (388, "udiv35prop.cnf"),
     (389, "udiv40prop.cnf"),
     (390, "udiv45prop.cnf"),

diff --git a/src/bin/benchbot.rs b/src/bin/benchbot.rs
@@ -22,7 +22,7 @@ use std::sync::RwLock;
 use std::{env, process, thread, time};
 use structopt::StructOpt;
 
-const VERSION: &str = "benchbot 0.5.7";
+const VERSION: &str = "benchbot 0.5.8";
 
 lazy_static! {
     pub static ref CHID: RwLock<u64> = RwLock::new(0);
@@ -275,15 +275,13 @@ fn worker(config: Config) {
             // I'm the last one.
             state("");
             let (s, u) = report(&config).unwrap_or((0, 0));
-            if let Ok(processed) = PROCESSED.read() {
-                if let Ok(mut answered) = ANSWERED.write() {
-                    let sum = s + u;
-                    *answered = sum;
-                    post(&format!(
-                        "All {} problems were solved, answered {}.",
-                        processed, sum,
-                    ));
-                }
+            if let Ok(mut answered) = ANSWERED.write() {
+                let sum = s + u;
+                *answered = sum;
+                post(&format!(
+                    "All ({} + {}, {}) problems were solved, answered {}.",
+                    config.target_from, config.target_step, config.target_to, sum,
+                ));
             }
             let tarfile = config.sync_dir.join(&format!("{}.tar.xz", config.run_name));
             Command::new("tar")
@@ -343,8 +341,10 @@ fn worker(config: Config) {
                 || (num == 360 && 164 < ans)
                 || (num == 380 && 171 < ans)
             {
-                post(&format!("New record: {} solutions at {}-th problem.", ans, pro));
-
+                post(&format!(
+                    "New record: {} solutions at {}-th problem.",
+                    ans, pro
+                ));
             }
         }
     }

diff --git a/src/bin/sat-bench.rs b/src/bin/sat-bench.rs
@@ -23,7 +23,7 @@ pub enum SolverException {
     Abort,
 }
 
-const VERSION: &str = "sat-bench 0.5.7";
+const VERSION: &str = "sat-bench 0.5.8";
 const SAT_PROBLEMS: [(usize, &str); 18] = [
     (100, "3-SAT/UF100"),
     (125, "3-SAT/UF125"),