Fixing build with newer CMS

meelgroup · Jan 3, 2024 · 0dd6b51 · 0dd6b51
1 parent 35feb97
commit 0dd6b51
Show file tree

Hide file tree

Showing 4 changed files with 0 additions and 22 deletions.
diff --git a/src/approxmc.cpp b/src/approxmc.cpp
@@ -59,7 +59,6 @@ DLL_PUBLIC AppMC::AppMC()
     data->counter.solver = new SATSolver();
     data->counter.solver->set_up_for_scalmc();
     data->counter.solver->set_allow_otf_gauss();
-    data->counter.solver->set_xor_detach(data->conf.cms_detach_xor);
 }
 
 DLL_PUBLIC AppMC::~AppMC()
@@ -164,12 +163,6 @@ DLL_PUBLIC void AppMC::set_var_elim_ratio(double var_elim_ratio)
     data->conf.var_elim_ratio = var_elim_ratio;
 }
 
-DLL_PUBLIC void AppMC::set_detach_xors(uint32_t detach_xors)
-{
-    data->conf.cms_detach_xor = detach_xors;
-    data->counter.solver->set_xor_detach(data->conf.cms_detach_xor);
-}
-
 DLL_PUBLIC void AppMC::set_reuse_models(uint32_t reuse_models)
 {
     data->conf.reuse_models = reuse_models;
@@ -295,17 +288,11 @@ DLL_PUBLIC bool AppMC::add_bnn_clause(
     return data->counter.solver->add_bnn_clause(lits, cutoff, out);
 }
 
-DLL_PUBLIC void AppMC::set_detach_warning()
-{
-    data->counter.solver->set_verbosity_detach_warning(true);
-}
-
 DLL_PUBLIC CMSat::SATSolver* AppMC::get_solver()
 {
     return data->counter.solver;
 }
 
-
 DLL_PUBLIC const std::vector<uint32_t>& AppMC::get_sampling_set() const
 {
     return data->conf.sampling_set;

diff --git a/src/approxmc.h b/src/approxmc.h
@@ -90,7 +90,6 @@ class AppMC
     //Main options
     void set_up_log(std::string log_file_name);
     void set_verbosity(uint32_t verb);
-    void set_detach_warning();
     void set_seed(uint32_t seed);
     void set_epsilon(double epsilon);
     void set_delta(double delta);

diff --git a/src/config.h b/src/config.h
@@ -48,7 +48,6 @@ struct Config {
     int reuse_models = 1;
     std::vector<uint32_t> sampling_set;
     std::string logfilename = "";
-    int cms_detach_xor = 1;
     int dump_intermediary_cnf = 0;
     int debug = 0;
     int force_sol_extension = false;

diff --git a/src/main.cpp b/src/main.cpp
@@ -67,7 +67,6 @@ uint32_t start_iter = 0;
 uint32_t verb_cls = 0;
 uint32_t simplify;
 double var_elim_ratio;
-uint32_t detach_xors = 1;
 uint32_t reuse_models = 1;
 uint32_t force_sol_extension = 0;
 uint32_t sparse = 0;
@@ -130,8 +129,6 @@ void add_appmc_options()
     improvement_options.add_options()
     ("sparse", po::value(&sparse)->default_value(sparse)
         , "0 = (default) Do not use sparse method. 1 = Generate sparse XORs when possible.")
-    ("detachxor", po::value(&detach_xors)->default_value(detach_xors)
-        , "Detach XORs in CMS")
     ("reusemodels", po::value(&reuse_models)->default_value(reuse_models)
         , "Reuse models while counting solutions")
     ("forcesolextension", po::value(&force_sol_extension)->default_value(force_sol_extension)
@@ -461,15 +458,11 @@ void set_approxmc_options()
 {
     //Main options
     appmc->set_verbosity(verbosity);
-    if (verbosity >= 2) {
-        appmc->set_detach_warning();
-    }
     appmc->set_seed(seed);
     appmc->set_epsilon(epsilon);
     appmc->set_delta(delta);
 
     //Improvement options
-    appmc->set_detach_xors(detach_xors);
     appmc->set_reuse_models(reuse_models);
     appmc->set_sparse(sparse);