diff --git a/include/stp/Sat/UniSamp.h b/include/stp/Sat/UniSamp.h index 2f6d16c5..db63988c 100644 --- a/include/stp/Sat/UniSamp.h +++ b/include/stp/Sat/UniSamp.h @@ -60,7 +60,7 @@ class UniSamp : public SATSolver public: UniSamp(uint64_t unisamp_seed, uint64_t samples_needed, - uint64_t samples_generated); + uint64_t _samples_generated); ~UniSamp(); diff --git a/lib/STPManager/STP.cpp b/lib/STPManager/STP.cpp index ec630954..6e812fbc 100644 --- a/lib/STPManager/STP.cpp +++ b/lib/STPManager/STP.cpp @@ -115,7 +115,7 @@ SATSolver* STP::get_new_sat_solver() case UserDefinedFlags::UNIGEN_SOLVER: #ifdef USE_UNIGEN newS = new UniSamp(bm->UserFlags.unisamp_seed, bm->UserFlags.num_samples, - bm->UserFlags.samples_generated); + bm->UserFlags.samples_generated); #else std::cerr << "UniSamp support was not enabled at configure time." << std::endl; @@ -125,7 +125,7 @@ SATSolver* STP::get_new_sat_solver() case UserDefinedFlags::APPROXMC_SOLVER: #ifdef USE_UNIGEN newS = new UniSamp(bm->UserFlags.unisamp_seed, bm->UserFlags.num_samples, - bm->UserFlags.samples_generated); + bm->UserFlags.samples_generated); #else std::cerr << "UniSamp support was not enabled at configure time." << std::endl; diff --git a/lib/Sat/UniSamp.cpp b/lib/Sat/UniSamp.cpp index d5abae35..b79e4756 100644 --- a/lib/Sat/UniSamp.cpp +++ b/lib/Sat/UniSamp.cpp @@ -123,8 +123,10 @@ bool UniSamp::solve(bool& timeout_expired) // Search without assumptions. */ // CMSat::lbool ret = s->solve(); // TODO AS - samples_generated += 1; - if (unisamp_ran) + samples_generated++; + std::cout << "c [stp->unigen] Generating Sample number " << samples_generated + << std::endl; + if (samples_generated > 1) return true; std::cout << "c [stp->unigen] UniSamp solving instance with " << a->nVars() @@ -189,7 +191,7 @@ 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 - 1].at(x) > 0); + return (unigen_models[samples_generated].at(x) > 0); } uint32_t UniSamp::newVar() diff --git a/tools/stp/main.cpp b/tools/stp/main.cpp index f3bda208..37582eea 100644 --- a/tools/stp/main.cpp +++ b/tools/stp/main.cpp @@ -249,20 +249,19 @@ void ExtraMain::create_options() "(default)" #endif #endif - )("unisamp,u", "use unisamp as solver -- behave as a almost " - "uniform sampler")( - "cmsgen,s", - "use cmsgen as solver -- behave as a uniform like sampler")( - "approxmc,c", - "use approxmc as solver -- behave as a approximate counter")( - "seed", - po::value(&bm->UserFlags.unisamp_seed) - ->default_value(bm->UserFlags.unisamp_seed), - "Seed for counting and sampling")( - "num-samples,ns", - po::value(&bm->UserFlags.num_samples) - ->default_value(bm->UserFlags.num_samples), - "Number of samples to generate in case of sampling"); + )("unisamp,u", "use unisamp as solver -- behave as a almost-uniform sampler")( + "cmsgen,s", + "use cmsgen as solver -- behave as a uniform like sampler")( + "approxmc,c", + "use approxmc as solver -- behave as a approximate counter")( + "seed", + po::value(&bm->UserFlags.unisamp_seed) + ->default_value(bm->UserFlags.unisamp_seed), + "Seed for counting and sampling")( + "num-samples,ns", + po::value(&bm->UserFlags.num_samples) + ->default_value(bm->UserFlags.num_samples), + "Number of samples to generate in sampling mode"); ; po::options_description refinement_options("Refinement options");