diff --git a/CMakeLists.txt b/CMakeLists.txt index d4f9ecd6..0d02ff06 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -853,3 +853,4 @@ install(FILES install(EXPORT ${STP_EXPORT_NAME} DESTINATION "${STP_INSTALL_CMAKE_DIR}" ) + diff --git a/include/stp/STPManager/UserDefinedFlags.h b/include/stp/STPManager/UserDefinedFlags.h index ee354557..66dba8f8 100644 --- a/include/stp/STPManager/UserDefinedFlags.h +++ b/include/stp/STPManager/UserDefinedFlags.h @@ -70,7 +70,7 @@ struct UserDefinedFlags int64_t AIG_rewrites_iterations = 0; // Number of iterations of AIG rewrites. int64_t bitblast_simplification = 0; int64_t size_reducing_fixed_point = 0; - + bool simplify_to_constants_only = false; @@ -141,7 +141,7 @@ struct UserDefinedFlags int64_t timeout_max_conflicts = -1; int num_solver_threads = 1; uint64_t unisamp_seed = 12345; - uint64_t num_samples = 500; + uint64_t num_samples = 10; uint64_t samples_generated = 0; int64_t timeout_max_time = -1; // seconds diff --git a/include/stp/Sat/UniSamp.h b/include/stp/Sat/UniSamp.h index db63988c..db78c2b3 100644 --- a/include/stp/Sat/UniSamp.h +++ b/include/stp/Sat/UniSamp.h @@ -50,8 +50,9 @@ class UniSamp : public SATSolver #endif { - ApproxMC::AppMC* a; - UniGen::UniG* s; + vector> unigen_models; + ApproxMC::AppMC* appmc; + UniGen::UniG* unigen; ArjunNS::Arjun* arjun; uint64_t seed; uint64_t samples_generated = 0; diff --git a/lib/Sat/ApxMC.cpp b/lib/Sat/ApxMC.cpp index 567fe6e0..b29ee260 100644 --- a/lib/Sat/ApxMC.cpp +++ b/lib/Sat/ApxMC.cpp @@ -133,6 +133,7 @@ bool ApxMC::solve(bool& timeout_expired) // Search without assumptions. sampling_vars_orig = sampling_vars; arjun->set_sampl_vars(sampling_vars_orig); sampling_vars = arjun->run_backwards(); + auto empty_sampl_vars = arjun->get_empty_sampl_vars(); const auto ret = arjun->get_fully_simplified_renumbered_cnf(sc); sampling_vars = ret.sampl_vars; a->new_vars(ret.nvars); @@ -154,6 +155,7 @@ bool ApxMC::solve(bool& timeout_expired) // Search without assumptions. a->set_sampl_vars(sampling_vars); auto sol_count = a->count(); + sol_count.hashCount += empty_sampl_vars.size(); // use gmp to get the absolute count of solutions mpz_class result; diff --git a/lib/Sat/UniSamp.cpp b/lib/Sat/UniSamp.cpp index 149604d1..8341f8ae 100644 --- a/lib/Sat/UniSamp.cpp +++ b/lib/Sat/UniSamp.cpp @@ -32,14 +32,19 @@ using std::vector; using namespace CMSat; using namespace UniGen; // namespace in UniGen library +using std::cout; +using std::endl; + namespace stp { -static vector> unigen_models; -void mycallback(const std::vector& solution, void*) +void mycallback(const std::vector& solution, void* data) { - unigen_models.push_back(solution); + vector>* unigen_models = (vector>*)data; + /* for (auto s : solution) std::cout << (s>0 ? "1" : "0"); */ + /* std::cout << std::endl; */ + unigen_models->push_back(solution); } void UniSamp::enableRefinement(const bool enable) @@ -55,19 +60,18 @@ UniSamp::UniSamp(uint64_t unisamp_seed, uint64_t _samples_needed, uint64_t _samples_generated) { - a = new ApproxMC::AppMC; - s = new UniG(a); + appmc = new ApproxMC::AppMC; + unigen = new UniG(appmc); arjun = new ArjunNS::Arjun; seed = unisamp_seed; samples_needed = _samples_needed; samples_generated = _samples_generated; // unisamp_ran = false; - s->set_callback(mycallback, NULL); - a->set_verbosity(0); + unigen->set_callback(mycallback, &unigen_models); + appmc->set_verbosity(0); arjun->set_verbosity(0); - s->set_verbosity(0); - - a->set_seed(seed); + unigen->set_verbosity(0); + appmc->set_seed(seed); // s->log_to_file("stp.cnf"); //s->set_num_threads(num_threads); @@ -78,7 +82,7 @@ UniSamp::UniSamp(uint64_t unisamp_seed, uint64_t _samples_needed, UniSamp::~UniSamp() { - delete s; + delete unigen; vector* real_temp_cl = (vector*)temp_cl; delete real_temp_cl; } @@ -95,15 +99,13 @@ void UniSamp::setMaxTime(int64_t _max_time) bool UniSamp::addClause(const vec_literals& ps) // Add a clause to the solver. { - // Cryptominisat uses a slightly different vec class. - // Cryptominisat uses a slightly different Lit class too. - vector& real_temp_cl = *(vector*)temp_cl; real_temp_cl.clear(); for (int i = 0; i < ps.size(); i++) { real_temp_cl.push_back(CMSat::Lit(var(ps[i]), sign(ps[i]))); } + /* cout << "c Adding clause to arjun " << real_temp_cl << " 0" << endl; */ return arjun->add_clause(real_temp_cl); } @@ -129,62 +131,64 @@ bool UniSamp::solve(bool& timeout_expired) // Search without assumptions. if (samples_generated > 1) return true; - std::cout << "c [stp->unigen] UniSamp solving instance with " << a->nVars() + std::cout << "c [stp->unigen] UniSamp solving instance with " << arjun->nVars() << " variables." << std::endl; vector sampling_vars, sampling_vars_orig; - for (uint32_t i = 0; i < a->nVars(); i++) - sampling_vars.push_back(i); - - arjun->set_seed(5); - + for (uint32_t i = 0; i < arjun->nVars(); i++) sampling_vars.push_back(i); sampling_vars_orig = sampling_vars; arjun->set_sampl_vars(sampling_vars_orig); + + const uint32_t orig_num_vars = arjun->nVars(); + appmc->new_vars(orig_num_vars); + bool ret = true; - const uint32_t orig_num_vars = arjun->get_orig_num_vars(); - a->new_vars(orig_num_vars); arjun->start_getting_constraints(false); vector clause; - while (ret) - { + while (ret) { bool is_xor, rhs; ret = arjun->get_next_constraint(clause, is_xor, rhs); assert(rhs); assert(!is_xor); - if (!ret) - break; + if (!ret) break; bool ok = true; - for (auto l : clause) - { - if (l.var() >= orig_num_vars) - { + for (auto l : clause) { + if (l.var() >= orig_num_vars) { ok = false; break; } } - - if (ok) - { - a->add_clause(clause); + if (ok) { + /* cout << "adding clause to appmc " << clause << endl; */ + appmc->add_clause(clause); } } arjun->end_getting_constraints(); sampling_vars = arjun->run_backwards(); + auto empty_sampl_vars = arjun->get_empty_sampl_vars(); delete arjun; - a->set_sampl_vars(sampling_vars); + + appmc->set_sampl_vars(sampling_vars); std::cout << "c [unigen->arjun] sampling var size [from arjun] " << sampling_vars.size() << " orig size " << sampling_vars_orig.size() << "\n"; - auto sol_count = a->count(); - s->set_full_sampling_vars(sampling_vars_orig); + auto sol_count = appmc->count(); + cout << "c Sol count: " << sol_count.cellSolCount + << "*2**" << (sol_count.hashCount+empty_sampl_vars.size()) << endl; // std::cout << "c [stp->unigen] ApproxMC got count " << sol_count.cellSolCount // << "*2**" << sol_count.hashCount << std::endl; - - s->sample(&sol_count, samples_needed); + unigen->set_verbosity(0); + unigen->set_verb_sampler_cls(0); + unigen->set_kappa(0.1); + unigen->set_multisample(false); + unigen->set_full_sampling_vars(sampling_vars_orig); +unigen->set_empty_sampling_vars(empty_sampl_vars); + + unigen->sample(&sol_count, samples_needed); unisamp_ran = true; return true; } @@ -193,25 +197,29 @@ uint8_t UniSamp::modelValue(uint32_t x) const { // if (unigen_models[0].size() < sampling_vars.size()) // std::cout << "c [stp->unigen] ERROR! found model size is not large enough\n"; - return (unigen_models[samples_generated].at(x) > 0); + if (samples_generated >= unigen_models.size()) + { + std::cout << "c [stp->unigen] ERROR! samples_generated: " << samples_generated + << " but unigen_models.size(): " << unigen_models.size() << std::endl; + exit(-1); + } + return (unigen_models.at(samples_generated).at(x) > 0); } uint32_t UniSamp::newVar() { - a->new_var(); arjun->new_var(); - return a->nVars() - 1; + return arjun->nVars() - 1; } void UniSamp::setVerbosity(int v) { - a->set_verbosity(0); arjun->set_verbosity(0); } unsigned long UniSamp::nVars() const { - return a->nVars(); + return arjun->nVars(); } void UniSamp::printStats() const