PCCAlgorithmOptions -> PCCompAlgorithmOptions

bin/pccompile.cpp

@@ -43,8 +43,8 @@ struct config_t
    std::string output_file{};
    bool minimize{false};
    SUBool::MINIMIZE_METHOD minimize_method{SUBool::MINIMIZE_METHOD::FULL};
-   SUBool::PCCAlgorithmOptions::ALGORITHM algorithm{
-       SUBool::PCCAlgorithmOptions::kDefaultAlgorithm};
+   SUBool::PCCompAlgorithmOptions::ALGORITHM algorithm{
+       SUBool::PCCompAlgorithmOptions::kDefaultAlgorithm};
    bool level_simplify{true};                // simplification at level increase
    unsigned verbosity{3};                    // 0 means no output
    bool use_empty_initial_hypothesis{false}; // For PCLearnComp
@@ -106,7 +106,7 @@ dump_config(const config_t &conf, unsigned level)
        << "\tminimize: " << SUBool::bool_to_string(conf.minimize) << std::endl;
    SUBool::kMinimizeMethodAnnotation.DumpValue(
        "\t", level, "minimize_method", conf.comp_base_config.minimize_method);
-   SUBool::PCCAlgorithmOptions::kAlgorithmAnnotation.DumpValue(
+   SUBool::PCCompAlgorithmOptions::kAlgorithmAnnotation.DumpValue(
        "\t", level, "algorithm", conf.algorithm);
    SUBool::logs.TLog(level)
        << "\tcomp_base_config.up_empower: "
@@ -201,7 +201,7 @@ parse_arguments(int argc, char *argv[], config_t &conf)
    SUBool::PrgOptions opts(true);
    opts.SetHelpDesc(prg_help);
    opts.InputOutput(&conf.input_file, &conf.output_file);
-   auto algorithm_opts = std::make_shared<SUBool::PCCAlgorithmOptions>();
+   auto algorithm_opts = std::make_shared<SUBool::PCCompAlgorithmOptions>();
    opts.AddOptionsGroup(algorithm_opts);
    auto pclearncomp_opts = std::make_shared<SUBool::PCLearnCompOptions>();
    opts.AddOptionsGroup(pclearncomp_opts);
@@ -671,13 +671,13 @@ incremental_compiler(const config_t &conf, SUBool::CNF cnf)
 
    switch (conf.algorithm)
    {
-   case SUBool::PCCAlgorithmOptions::ALGORITHM::INCREMENT_PC:
+   case SUBool::PCCompAlgorithmOptions::ALGORITHM::INCREMENT_PC:
       return std::make_shared<SUBool::PCComp>(
           std::move(cnf), std::move(a_conf));
-   case SUBool::PCCAlgorithmOptions::ALGORITHM::INCREMENT_URC_PC:
+   case SUBool::PCCompAlgorithmOptions::ALGORITHM::INCREMENT_URC_PC:
       interleave_pc = true;
       [[fallthrough]];
-   case SUBool::PCCAlgorithmOptions::ALGORITHM::INCREMENT_URC:
+   case SUBool::PCCompAlgorithmOptions::ALGORITHM::INCREMENT_URC:
    {
       SUBool::UCComp::Config uc_conf(a_conf);
       uc_conf.interleave_pc = interleave_pc;
@@ -707,7 +707,7 @@ learning_compiler(const config_t &conf, SUBool::CNF cnf)
 std::shared_ptr<SUBool::AbsComp>
 compiler(const config_t &conf, SUBool::CNF cnf)
 {
-   if (conf.algorithm == SUBool::PCCAlgorithmOptions::ALGORITHM::LEARNING)
+   if (conf.algorithm == SUBool::PCCompAlgorithmOptions::ALGORITHM::LEARNING)
    {
       return learning_compiler(conf, std::move(cnf));
    }

lib/pc_opt.cpp

@@ -8,8 +8,8 @@
 
 #include "pc_opt.h"
 
-const SUBool::EnumAnnotation<SUBool::PCCAlgorithmOptions::ALGORITHM>
-    SUBool::PCCAlgorithmOptions::kAlgorithmAnnotation("ALGORITHM",
+const SUBool::EnumAnnotation<SUBool::PCCompAlgorithmOptions::ALGORITHM>
+    SUBool::PCCompAlgorithmOptions::kAlgorithmAnnotation("ALGORITHM",
         {//
             {ALGORITHM::INCREMENT_PC, "incremental_pc",
                 "heuristic algorithm based on incremental adding empowering "
@@ -37,7 +37,7 @@ SUBool::minimize_method_opt() -> EnumOption<MINIMIZE_METHOD>
        "Minimization method", kDefaultMinimizeMethod);
 }
 
-SUBool::PCCAlgorithmOptions::PCCAlgorithmOptions()
+SUBool::PCCompAlgorithmOptions::PCCAlgorithmOptions()
     : OptionsGroup("Algorithm Selection"),
       mAlgorithmOption(kAlgorithmAnnotation, "algorithm,a",
           "Algorithm used for compilation", kDefaultAlgorithm)
@@ -46,7 +46,7 @@ SUBool::PCCAlgorithmOptions::PCCAlgorithmOptions()
 }
 
 bool
-SUBool::PCCAlgorithmOptions::GetValues()
+SUBool::PCCompAlgorithmOptions::GetValues()
 {
    return mAlgorithmOption.GetValue(mAlgorithm);
 }

lib/pc_opt.h

@@ -20,7 +20,7 @@ namespace SUBool
    EnumOption<MINIMIZE_METHOD> minimize_method_opt();
 
    // Algorithm selection in pccompile
-   class PCCAlgorithmOptions : public OptionsGroup
+   class PCCompAlgorithmOptions : public OptionsGroup
    {
     public:
       enum class ALGORITHM
@@ -39,7 +39,7 @@ namespace SUBool
       ALGORITHM mAlgorithm{kDefaultAlgorithm};
 
     public:
-      PCCAlgorithmOptions();
+      PCCompAlgorithmOptions();
 
       virtual bool GetValues() override;
 
@@ -71,7 +71,7 @@ namespace SUBool
 } // namespace SUBool
 
 inline auto
-SUBool::PCCAlgorithmOptions::Algorithm() const -> ALGORITHM
+SUBool::PCCompAlgorithmOptions::Algorithm() const -> ALGORITHM
 {
    return mAlgorithm;
 }

pccompile.help

@@ -51,14 +51,31 @@ LEARNING ALGORITHM
                                 used as an initial list of negatives. (default:
                                 all_empowering)
 
+
+PREPROCESSING
+  -r, --preprocess arg          Method of preprocessing. 0 = No
+                                preprocessing. 1 = Minimize the formula before compilation.
+                                2 = First make CNF prime with respect to
+                                1-provability, then minimize. 3 = First make CNF
+                                prime and then minimize. 4 = Only make CNF
+                                prime with respect to 1-provability, no
+                                minimization. 5 = Only make CNF prime, no minimization. 
+                                (default: 3)
+      --no-backbone-propagation
+                                Do not perform backbone propagation before
+                                preprocessing.
+
 SOLVERS
 
       --pccheck-solver arg      Solver to be used for the PC check. glucose =
                                 use glucose, kissat = use kissat. (default:
                                 glucose)
 
-ONE PROVABILITY
+EMPOWEREMENT
 
+  -w, --empower arg             What kind of encoding should be used for
+                                empowerment.
+ONE PROVABILITY
 
   -1, --one-prove arg           What kind of encoding should be used for
                                 1-provability.
@@ -112,18 +129,6 @@ ONE PROVABILITY
                                 of the logarithmic encoding is bounded to the
                                 logarithm of the parameter rounded up.
                                 (default: 0)
-PREPROCESSING
-  -r, --preprocess arg          Method of preprocessing. 0 = No
-                                preprocessing. 1 = Minimize the formula before compilation.
-                                2 = First make CNF prime with respect to
-                                1-provability, then minimize. 3 = First make CNF
-                                prime and then minimize. 4 = Only make CNF
-                                prime with respect to 1-provability, no
-                                minimization. 5 = Only make CNF prime, no minimization. 
-                                (default: 3)
-      --no-backbone-propagation
-                                Do not perform backbone propagation before
-                                preprocessing.
 RANDOM PC CHECKS
 
   -S, --seed arg                Initial random seed. Current time is used, if
@@ -140,10 +145,6 @@ RANDOM PC CHECKS
                                 random negative example was successfully found. 0
                                 means no increase. (default: 1)
 
-EMPOWEREMENT
-
-  -w, --empower arg             What kind of encoding should be used for
-                                empowerment.
 
 
 SIMPLIFICATION