refactor: simplify compilation features and CLI argument parsing

cksystemsgroup · Mar 6, 2021 · 14eb74a · 14eb74a
1 parent e32947d
commit 14eb74a
Show file tree

Hide file tree

Showing 11 changed files with 247 additions and 273 deletions.
diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
@@ -20,15 +20,15 @@ jobs:
             os: [ubuntu-20.04, macos-10.15, windows-2019]
             include:
               - os: ubuntu-20.04
-                features: z3-solver,boolector-solver
+                features: z3,boolector
                 target: x86_64-unknown-linux-gnu
                 extension: ""
               - os: macos-10.15
-                features: z3-solver,boolector-solver
+                features: z3,boolector
                 target: x86_64-apple-darwin
                 extension: ""
               - os: windows-2019
-                features: z3-solver
+                features: z3
                 target: x86_64-pc-windows-msvc
                 extension: ".exe"
         steps:

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
@@ -24,15 +24,15 @@ jobs:
         experimental: [false]
         include:
           - os: ubuntu-20.04
-            features: z3-solver,boolector-solver
+            features: z3,boolector
           - os: macos-10.15
-            features: z3-solver,boolector-solver
+            features: z3,boolector
           - os: windows-2019
-            features: z3-solver
+            features: z3
           - toolchain: stable
             os: ubuntu-latest
             experimental: true
-            features: z3-solver,boolector-solver
+            features: z3,boolector
     steps:
       - name: Checkout
         uses: actions/checkout@v2

diff --git a/Cargo.lock b/Cargo.lock
diff --git a/Cargo.toml b/Cargo.toml
@@ -13,8 +13,6 @@ version ="0.2.0"
 
 [features]
 default = []
-boolector-solver = ["boolector"]
-z3-solver = ["z3"]
 
 [lib]
 name = "monster"
@@ -30,7 +28,8 @@ harness = false
 
 [dependencies]
 byteorder = "~1.4.2"
-clap = "3.0.0-beta.2"
+clap = "~2.33.3"
+strum = { version = "~0.20.0", features = ["derive"] }
 riscu = "~0.5.0"
 petgraph = "~0.5.1"
 rand = "~0.8.3"

diff --git a/README.md b/README.md
@@ -73,7 +73,7 @@ $ choco install git -y
 ```
 ### Build and Test from Source
 Tests can be executed on all platforms, alltough one
-feature is not supported on Windows: `boolector-solver`
+feature is not supported on Windows: `boolector`
 
 1. Test your toolchain setup by compiling monster:
 ```

diff --git a/benches/engine.rs b/benches/engine.rs
@@ -16,10 +16,10 @@ use std::{
 use tempfile::{tempdir, TempDir};
 use utils::compile_riscu;
 
-#[cfg(feature = "boolector-solver")]
+#[cfg(feature = "boolector")]
 use monster::solver::Boolector;
 
-#[cfg(feature = "z3-solver")]
+#[cfg(feature = "z3")]
 use monster::solver::Z3;
 
 const TEST_FILES: [&str; 4] = [
@@ -50,11 +50,11 @@ fn bench_demonstration(c: &mut Criterion) {
     group.bench_function("Monster", |b| {
         b.iter(|| execute_single::<MonsterSolver, &PathBuf>(&object_file))
     });
-    #[cfg(feature = "boolector-solver")]
+    #[cfg(feature = "boolector")]
     group.bench_function("Boolector", |b| {
         b.iter(|| execute_single::<Boolector, &PathBuf>(&object_file))
     });
-    #[cfg(feature = "z3-solver")]
+    #[cfg(feature = "z3")]
     group.bench_function("Z3", |b| {
         b.iter(|| execute_single::<Z3, &PathBuf>(&object_file))
     });
@@ -69,11 +69,11 @@ fn bench_solver_avg(c: &mut Criterion) {
     group.bench_function("Monster", |b| {
         b.iter(|| execute_all::<MonsterSolver>(&object_files))
     });
-    #[cfg(feature = "boolector-solver")]
+    #[cfg(feature = "boolector")]
     group.bench_function("Boolector", |b| {
         b.iter(|| execute_all::<Boolector>(&object_files))
     });
-    #[cfg(feature = "z3-solver")]
+    #[cfg(feature = "z3")]
     group.bench_function("Z3", |b| b.iter(|| execute_all::<Z3>(&object_files)));
 }
 
@@ -94,7 +94,7 @@ fn bench_solver_individual(c: &mut Criterion) {
         });
     }
 
-    #[cfg(feature = "boolector-solver")]
+    #[cfg(feature = "boolector")]
     {
         let mut boolector_grp = c.benchmark_group("Boolector");
         boolector_grp
@@ -108,7 +108,7 @@ fn bench_solver_individual(c: &mut Criterion) {
         });
     }
 
-    #[cfg(feature = "z3-solver")]
+    #[cfg(feature = "z3")]
     {
         let mut z3_grp = c.benchmark_group("Z3");
         z3_grp.warm_up_time(Duration::from_secs(2)).sample_size(30);
@@ -126,7 +126,7 @@ fn compile_test_files() -> Vec<PathBuf> {
             TEMP_DIR = Some(tmp_dir.clone());
 
             TEST_OBJECT_FILES = Some(
-                compile_riscu(tmp_dir.clone(), Some(&TEST_FILES))
+                compile_riscu(tmp_dir, Some(&TEST_FILES))
                     .map(|(_source, object)| object)
                     .collect(),
             );