Random PC Checks options in pccompile

bin/pccompile.cpp

@@ -166,35 +166,6 @@ dump_config(const config_t &conf, unsigned level)
 
 std::vector<std::string> log_enc_opt_strings = {"amf", "cex", "flm", "cml"};
 
-bool
-parse_log_enc_opts(
-    const std::string &opt_string, SUBool::UPEncLogarithmic::Config &conf)
-{
-   std::vector<bool> opt_values(log_enc_opt_strings.size(), false);
-   size_t start = 0;
-   size_t end = 0;
-   if (!opt_string.empty())
-   {
-      while (start != std::string::npos)
-      {
-         end = opt_string.find_first_of(',', start);
-         auto i = std::find(log_enc_opt_strings.begin(),
-             log_enc_opt_strings.end(), opt_string.substr(start, end - start));
-         if (i == log_enc_opt_strings.end())
-         {
-            return false;
-         }
-         opt_values[i - log_enc_opt_strings.begin()] = true;
-         start = end + static_cast<size_t>(end < std::string::npos);
-      }
-   }
-   conf.add_amo_on_fire_vars = opt_values[0];
-   conf.add_compare_exclusivity = opt_values[1];
-   conf.add_force_linear_order_on_max_level = opt_values[2];
-   conf.contradiction_has_max_level = opt_values[3];
-   return true;
-}
-
 int
 parse_arguments(int argc, char *argv[], config_t &conf)
 {
@@ -209,6 +180,8 @@ parse_arguments(int argc, char *argv[], config_t &conf)
    auto solver_opts = opts.MakeOptionsGroup<SUBool::PCSolverOptions>();
    auto empower_opts = opts.MakeOptionsGroup<SUBool::PCEmpowerOptions>();
    auto oneprove_opts = opts.MakeOptionsGroup<SUBool::PCOneProveOptions>();
+   auto pccheck_random_opts =
+       opts.MakeOptionsGroup<SUBool::PCRandomPCChecksOptions>();
    if (!opts.Parse(argc, argv))
    {
       return 1;
@@ -228,6 +201,10 @@ parse_arguments(int argc, char *argv[], config_t &conf)
    conf.comp_base_config.enc_conf.log_conf =
        oneprove_opts->EncLogarithmicConf();
    conf.comp_base_config.impl_system = oneprove_opts->ImplSystem();
+   conf.random_seed = pccheck_random_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();
    return 0;
 #if 0
    try

lib/pc_opt.cpp

@@ -190,3 +190,27 @@ SUBool::PCOneProveOptions::ParseLogEncOpts()
    mEncLogarithmicConf.contradiction_has_max_level = opt_values[3];
    return true;
 }
+
+SUBool::PCRandomPCChecksOptions::PCRandomPCChecksOptions()
+    : OptionsGroup("Random PC Checks"),
+      mSeed(std::chrono::system_clock::now().time_since_epoch().count())
+{
+   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),
+           "Number of rounds during one random check of propagation "
+           "completeness.") //
+       ("pccheck-random-budget", po::value<unsigned>(&mBudget),
+           "How many times an unsucessful random PC check should be repeated. "
+           "0 means no random check is ever performed.") //
+       ("pccheck-random-budget-inc", po::value<unsigned>(&mBudgetInc),
+           "Increase of the current budget in case a random negative example "
+           "is successfully found. 0 means no increase.");
+}
+
+bool
+SUBool::PCRandomPCChecksOptions::GetValues()
+{
+   return true;
+}

lib/pc_opt.h

@@ -159,6 +159,30 @@ namespace SUBool
       LIT_IMPL_SYSTEM ImplSystem() const;
       unsigned UPLevelBound() const;
    };
+
+   class PCRandomPCChecksOptions : public OptionsGroup
+   {
+    public:
+      static const unsigned kDefaultRounds = 100;
+      static const unsigned kDefaultBudget = 10;
+      static const unsigned kDefaultBudgetInc = 1;
+
+    private:
+      unsigned long long mSeed{0};
+      unsigned mRounds{kDefaultRounds};
+      unsigned mBudget{kDefaultBudget};
+      unsigned mBudgetInc{kDefaultBudgetInc};
+
+    public:
+      PCRandomPCChecksOptions();
+
+      virtual bool GetValues() override;
+
+      unsigned long long Seed() const;
+      unsigned Rounds() const;
+      unsigned Budget() const;
+      unsigned BudgetInc() const;
+   };
 } // namespace SUBool
 
 inline auto
@@ -228,4 +252,28 @@ SUBool::PCOneProveOptions::UPLevelBound() const
    return mUPLevelBound;
 }
 
+inline unsigned long long
+SUBool::PCRandomPCChecksOptions::Seed() const
+{
+   return mSeed;
+}
+
+inline unsigned
+SUBool::PCRandomPCChecksOptions::Rounds() const
+{
+   return mRounds;
+}
+
+inline unsigned
+SUBool::PCRandomPCChecksOptions::Budget() const
+{
+   return mBudget;
+}
+
+inline unsigned
+SUBool::PCRandomPCChecksOptions::BudgetInc() const
+{
+   return mBudgetInc;
+}
+
 #endif