Adding more configs

meelgroup · Feb 28, 2024 · 935c9d2 · 935c9d2
1 parent e93dab3
commit 935c9d2
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 1 deletion.
diff --git a/src/main.cpp b/src/main.cpp
@@ -83,6 +83,12 @@ int main(int argc, char **argv) {
         .action([&](const auto&) {tiebreak = Tiebreak::None;})
         .flag()
         .help("Use original BVA tie-break. Runs BVA instead of SBVA");
+    program.add_argument("--clscutoff")
+        .action([&](const auto& a) {config.matched_cls_cutoff = std::atoi(a.c_str());})
+        .help("Matched clauses cutoff. The larger, the larger the gain must be to perform BVA");
+    program.add_argument("--litscutoff")
+        .action([&](const auto& a) {config.matched_lits_cutoff = std::atoi(a.c_str());})
+        .help("Matched literals cutoff. The larger, the larger the gain must be to perform BVA");
     program.add_argument("-c", "--countpreserve")
         .action([&](const auto&) {config.preserve_model_cnt = true;})
         .flag()

diff --git a/src/sbva.cpp b/src/sbva.cpp
@@ -730,7 +730,8 @@ class Formula {
                 continue;
             }
 
-            if (matched_lits.size() <= 2 && matched_clauses.size() <= 2) {
+            if (matched_lits.size() <= config.matched_lits_cutoff &&
+                    matched_clauses.size() <= config.matched_cls_cutoff) {
                 continue;
             }
 

diff --git a/src/sbva.h b/src/sbva.h
@@ -39,6 +39,8 @@ struct Config {
     int64_t steps = std::numeric_limits<int64_t>::max();
     unsigned int max_replacements = 0;
     bool preserve_model_cnt = 0;
+    uint32_t matched_lits_cutoff = 2; // the larger, the more strict
+    uint32_t matched_cls_cutoff = 2;  // the larger, the more strict
 };
 
 enum Tiebreak {