diff --git a/src/approxmc.cpp b/src/approxmc.cpp index b5f3e87..49c2466 100644 --- 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& AppMC::get_sampling_set() const { return data->conf.sampling_set; diff --git a/src/approxmc.h b/src/approxmc.h index a13093b..b6b1470 100644 --- 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 index 0b1c270..a71d550 100644 --- a/src/config.h +++ b/src/config.h @@ -48,7 +48,6 @@ struct Config { int reuse_models = 1; std::vector 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 index efc5910..7699d51 100644 --- 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);