Commit 452ff186 authored by Kučera Petr RNDr. Ph.D.'s avatar Kučera Petr RNDr. Ph.D.
Browse files

seed as global parameter

parent 718d5a45
......@@ -26,6 +26,7 @@ struct config_t
{
std::string output_file{};
unsigned n{2};
unsigned long long random_seed{0};
};
void
......@@ -40,6 +41,8 @@ dump_config(const config_t &conf)
SUBool::logs.DumpValue("\t", level, "output_file", conf.output_file);
SUBool::logs.DumpVerbosity("\t", level);
SUBool::logs.DumpValue("\t", level, "n", conf.n);
SUBool::logs.TLog(level)
<< "\trandom seed: " << conf.random_seed << std::endl;
}
std::optional<config_t>
......@@ -56,6 +59,7 @@ parse_arguments(int argc, char *argv[])
{
return {};
}
conf.random_seed = opts.Seed();
return conf;
}
......
......@@ -48,6 +48,7 @@ struct config_t
std::string input_file{};
std::string output_file{};
PROCESS process{PROCESS::PRIME};
unsigned long long random_seed{0};
};
std::optional<config_t>
......@@ -66,6 +67,7 @@ parse_arguments(int argc, char *argv[])
{
return {};
}
conf.random_seed = opts.Seed();
return conf;
}
......@@ -84,6 +86,8 @@ dump_config(const config_t &conf)
SUBool::logs.TLog(level)
<< "\tprocess: " << process_names.at(static_cast<unsigned>(conf.process))
<< std::endl;
SUBool::logs.TLog(level)
<< "\trandom seed: " << conf.random_seed << std::endl;
SUBool::logs.DumpVerbosity("\t", level);
}
......
......@@ -57,6 +57,7 @@ struct config_t
std::string file_right{};
RELATION relation{RELATION::EQUAL};
COMPARE_KIND compare_kind{COMPARE_KIND::IMPLICATE};
unsigned long long random_seed{0};
};
void
......@@ -74,6 +75,8 @@ dump_config(const config_t &conf)
kRelationAnnotation.DumpValue("\t", level, "relation", conf.relation);
kCompareKindAnnotation.DumpValue(
"\t", level, "compare_kind", conf.compare_kind);
SUBool::logs.TLog(level)
<< "\trandom seed: " << conf.random_seed << std::endl;
}
std::optional<config_t>
......@@ -98,6 +101,7 @@ parse_arguments(int argc, char *argv[])
{
return {};
}
conf.random_seed = opts.Seed();
return conf;
}
......
......@@ -22,6 +22,7 @@ struct config_t
bool suppress_first{false};
bool suppress_second{false};
bool suppress_third{false};
unsigned long long random_seed{0};
};
void
......@@ -39,6 +40,8 @@ dump_config(const config_t &conf)
SUBool::logs.DumpValue("\t", level, "suppress_first", conf.suppress_first);
SUBool::logs.DumpValue("\t", level, "suppress_second", conf.suppress_second);
SUBool::logs.DumpValue("\t", level, "suppress_third", conf.suppress_third);
SUBool::logs.TLog(level)
<< "\trandom seed: " << conf.random_seed << std::endl;
}
std::optional<config_t>
......@@ -60,6 +63,7 @@ parse_arguments(int argc, char *argv[])
{
return {};
}
conf.random_seed = opts.Seed();
return conf;
}
......
......@@ -174,7 +174,7 @@ parse_arguments(int argc, char *argv[], config_t &conf)
conf.comp_base_config.impl_system = oneprove_opts->ImplSystem();
conf.comp_base_config.impl_system_rebuild =
oneprove_opts->ImplSystemRebuild();
conf.random_seed = pccheck_random_opts->Seed();
conf.random_seed = opts.Seed();
conf.pccheck_random_rounds = pccheck_random_opts->Rounds();
conf.pccheck_random_budget = pccheck_random_opts->Budget();
conf.pccheck_random_budget_inc = pccheck_random_opts->BudgetInc();
......@@ -346,7 +346,6 @@ main(int argc, char *argv[])
}
auto cnf = SUBool::input_or_die<SUBool::CNF>(
the_conf.input_file, 0, 2, "Failed to parse the input file");
SUBool::sub_rand.seed(the_conf.random_seed);
std::signal(SIGTERM, terminate);
std::signal(SIGQUIT, terminate);
......
......@@ -192,16 +192,12 @@ SUBool::PCOneProveOptions::ParseLogEncOpts()
}
SUBool::PCRandomPCChecksOptions::PCRandomPCChecksOptions()
: OptionsGroup("Random PC Checks"),
mSeed(std::chrono::system_clock::now().time_since_epoch().count())
: OptionsGroup("Random PC Checks")
{
AddOptions()("seed,S", po::value<unsigned long long>(&mSeed),
"Initial random seed. Current time is used if the seed is not provided "
"explicitly.") //
("pccheck-random-rounds",
po::value<unsigned>(&mRounds)->default_value(kDefaultRounds),
"Number of rounds during one random check of propagation "
"completeness.") //
AddOptions()("pccheck-random-rounds",
po::value<unsigned>(&mRounds)->default_value(kDefaultRounds),
"Number of rounds during one random check of propagation "
"completeness.") //
("pccheck-random-budget",
po::value<unsigned>(&mBudget)->default_value(kDefaultBudget),
"How many times an unsucessful random PC check should be repeated. "
......
......@@ -9,8 +9,6 @@
#ifndef __PC_OPT_H
#define __PC_OPT_H
#include <chrono>
#include "drenc.h"
#include "empower.h"
#include "enum_opt.h"
......@@ -154,7 +152,6 @@ namespace SUBool
static constexpr unsigned kDefaultBudgetInc = 1;
private:
unsigned long long mSeed{0};
unsigned mRounds{kDefaultRounds};
unsigned mBudget{kDefaultBudget};
unsigned mBudgetInc{kDefaultBudgetInc};
......@@ -164,7 +161,6 @@ namespace SUBool
virtual bool GetValues() override;
unsigned long long Seed() const;
unsigned Rounds() const;
unsigned Budget() const;
unsigned BudgetInc() const;
......@@ -301,12 +297,6 @@ SUBool::PCOneProveOptions::ImplSystemRebuild() const
return mImplSystemRebuild;
}
inline unsigned long long
SUBool::PCRandomPCChecksOptions::Seed() const
{
return mSeed;
}
inline unsigned
SUBool::PCRandomPCChecksOptions::Rounds() const
{
......
......@@ -7,6 +7,7 @@
*/
#include "prgutil.h"
#include "random_utils.h"
#include "version.h"
const std::string SUBool::kVersionInfo = SUBOOL_VERSION;
......@@ -60,6 +61,9 @@ SUBool::PrgOptions::InitCommon()
"Config file")("no-config", "Do not attempt to read a config file.");
mConfigOnly.add(std::move(opt_verbosity));
}
mCommon.add_options()("seed,S", po::value<unsigned long long>(&mSeed),
"Initial random seed. Current time is used if the seed is not provided "
"explicitly.");
}
void
......@@ -108,6 +112,7 @@ SUBool::PrgOptions::ProcessCommon() const
return false;
}
logs.mVerbLevel = mVerbosity;
SUBool::sub_rand.seed(mSeed);
return true;
}
......
......@@ -11,6 +11,7 @@
#include <algorithm>
#include <array>
#include <chrono>
#include <fstream>
#include <iostream>
#include <sstream>
......@@ -141,6 +142,7 @@ namespace SUBool
bool mUseConfigFile{false};
unsigned mVerbosity{LogStream::kDefaultLogLevel};
std::string mConfigFile{};
unsigned long long mSeed{0};
po::options_description mCommon{};
po::options_description mConfig{};
......@@ -167,7 +169,9 @@ namespace SUBool
PrgOptions(bool use_config_file = false,
const std::string &common_opts_label = kCommonOptsLabel)
: mPrgName(kPrgName), mPrgDesc(kPrgDesc),
mUseConfigFile(use_config_file), mCommon(common_opts_label)
mUseConfigFile(use_config_file),
mSeed(std::chrono::system_clock::now().time_since_epoch().count()),
mCommon(common_opts_label)
{
InitCommon();
}
......@@ -189,6 +193,7 @@ namespace SUBool
template <typename T, typename... Args>
std::shared_ptr<T> MakeOptionsGroup(Args &&...args);
bool HasValue(const std::string &opt_name) const;
unsigned long long Seed() const;
};
} // namespace SUBool
......@@ -258,4 +263,10 @@ SUBool::PrgOptions::MakeOptionsGroup(Args &&...args)
return opt_group;
}
inline unsigned long long
SUBool::PrgOptions::Seed() const
{
return mSeed;
}
#endif
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment