pccompile empowerement options

bin/pccheck.cpp

@@ -93,9 +93,9 @@ dump_config(const config_t &conf, unsigned level)
        << "\tencode_only: " << SUBool::bool_to_string(conf.encode_only)
        << std::endl;
    SUBool::logs.DumpValue("\t", level, "no_up_backbones", conf.no_up_backbones);
-   SUBool::logs.TLog(level)
-       << "\tup_empower: " << static_cast<unsigned>(conf.up_empower)
-       << std::endl;
+
+   SUBool::PCEncoder::kUPEmpowerAnnotation.DumpValue(
+       "\t", level, "up_empower", conf.up_empower);
    SUBool::logs.TLog(level) << "\tenc_conf:" << std::endl;
    conf.enc_conf.Dump("\t\t", level);
    SUBool::logs.TLog(level)

bin/pccompile.cpp

@@ -108,9 +108,8 @@ dump_config(const config_t &conf, unsigned level)
        "\t", level, "minimize_method", conf.comp_base_config.minimize_method);
    SUBool::PCCompAlgorithmOptions::kAlgorithmAnnotation.DumpValue(
        "\t", level, "algorithm", conf.algorithm);
-   SUBool::logs.TLog(level)
-       << "\tcomp_base_config.up_empower: "
-       << static_cast<unsigned>(conf.comp_base_config.up_empower) << std::endl;
+   SUBool::PCEncoder::kUPEmpowerAnnotation.DumpValue("\t", level,
+       "comp_base_config.up_empower", conf.comp_base_config.up_empower);
    SUBool::logs.TLog(level)
        << "\tcomp_base_config.simp_steps: " << conf.comp_base_config.simp_steps
        << (conf.comp_base_config.simp_steps > 0
@@ -206,6 +205,7 @@ parse_arguments(int argc, char *argv[], config_t &conf)
    auto preprocess_opts =
        opts.MakeOptionsGroup<SUBool::PCCompPreprocessOptions>();
    auto solver_opts = opts.MakeOptionsGroup<SUBool::PCSolverOptions>();
+   auto empower_opts = opts.MakeOptionsGroup<SUBool::PCEmpowerOptions>();
    if (!opts.Parse(argc, argv))
    {
       return 1;
@@ -219,6 +219,7 @@ parse_arguments(int argc, char *argv[], config_t &conf)
    conf.comp_base_config.propagate_backbones =
        !preprocess_opts->NoBackbonePropagation();
    conf.comp_base_config.solver_type = solver_opts->SolverType();
+   conf.comp_base_config.up_empower = empower_opts->Empower();
    return 0;
 #if 0
    try

lib/pc_opt.cpp

@@ -105,3 +105,17 @@ SUBool::PCSolverOptions::GetValues()
 {
    return mSolverTypeOption.GetValue(mSolverType);
 }
+
+SUBool::PCEmpowerOptions::PCEmpowerOptions()
+    : OptionsGroup("Empowerment Encoding"),
+      mEmpowerOption(PCEncoder::kUPEmpowerAnnotation, "empower,w",
+          "Encoding used to encode empowerment.", kDefaultEmpower)
+{
+   Add(mEmpowerOption);
+}
+
+bool
+SUBool::PCEmpowerOptions::GetValues()
+{
+   return mEmpowerOption.GetValue(mEmpower);
+}

lib/pc_opt.h

@@ -106,6 +106,25 @@ namespace SUBool
 
       SOLVER_TYPE SolverType() const;
    };
+
+   // Empowerement
+   class PCEmpowerOptions : public OptionsGroup
+   {
+    public:
+      static const PCEncoder::UP_EMPOWER kDefaultEmpower =
+          PCEncoder::UP_EMPOWER::ONE_LEVEL;
+
+    private:
+      EnumOption<PCEncoder::UP_EMPOWER> mEmpowerOption;
+      PCEncoder::UP_EMPOWER mEmpower{kDefaultEmpower};
+
+    public:
+      PCEmpowerOptions();
+
+      virtual bool GetValues() override;
+
+      PCEncoder::UP_EMPOWER Empower() const;
+   };
 } // namespace SUBool
 
 inline auto
@@ -145,4 +164,10 @@ SUBool::PCSolverOptions::SolverType() const
    return mSolverType;
 }
 
+inline SUBool::PCEncoder::UP_EMPOWER
+SUBool::PCEmpowerOptions::Empower() const
+{
+   return mEmpower;
+}
+
 #endif

lib/pcenc.cpp

@@ -21,6 +21,17 @@
 // On only for debugging
 //#define ONLY_UP_ONE_PROVE
 
+const SUBool::EnumAnnotation<SUBool::PCEncoder::UP_EMPOWER>
+    SUBool::PCEncoder::kUPEmpowerAnnotation("UP_EMPOWER",
+        {
+            //
+            {UP_EMPOWER::QUADRATIC_EQUIV, "quadratic_equiv",
+                "quadratic size encoding with equivalences"}, //
+            {UP_EMPOWER::QUADRATIC_ONE_SIDED, "quadratic_one_sided",
+                "quadratic size encoding with implications"},           //
+            {UP_EMPOWER::ONE_LEVEL, "one_level", "one level encoding"}, //
+        });
+
 SUBool::PCEncoder::PCEncoder(const Config &conf)
     : AbsEncoder(conf), mConf(conf), mOneProveInputs(), mOneProveOutputs(),
       mEmpowerInputs(), mEmpowerOutputs(), mSelectionLits(),

lib/pcenc.h

@@ -16,6 +16,7 @@
 
 #include "absenc.h"
 #include "cl2lit.h"
+#include "enum.h"
 #include "glucose_bind.h"
 #include "normalform.h"
 #include "upenc.h"
@@ -30,10 +31,11 @@ namespace SUBool
       {
          QUADRATIC_EQUIV,
          QUADRATIC_ONE_SIDED,
-         ONE_LEVEL,
-         Last = ONE_LEVEL
+         ONE_LEVEL
       };
 
+      static const EnumAnnotation<UP_EMPOWER> kUPEmpowerAnnotation;
+
       struct Config : AbsConfig
       {
          UP_EMPOWER up_empower = UP_EMPOWER::ONE_LEVEL;
@@ -53,13 +55,13 @@ namespace SUBool
       std::vector<Literal> mSelectionLits;
 
       virtual void AddClauses(const CNF &cnf, const ClausesToLiterals &cl2lit,
-                              const LitImplSystem &impl_system) override;
+          const LitImplSystem &impl_system) override;
 
       unsigned NewAuxVar(const std::string &name);
-      unsigned NewAuxComparisonVar(const std::string &left,
-                                   const std::string &right, unsigned bit);
-      unsigned NewFireVar(unsigned c_index, unsigned c_subindex,
-                          const Literal &lit);
+      unsigned NewAuxComparisonVar(
+          const std::string &left, const std::string &right, unsigned bit);
+      unsigned NewFireVar(
+          unsigned c_index, unsigned c_subindex, const Literal &lit);
       unsigned NewFireVar(unsigned c_index, const Literal &lit);
       unsigned EmpowerOutput(unsigned i) const;
 
@@ -92,8 +94,8 @@ namespace SUBool
 
       void InitEmpEncoder(const CNF &cnf, const ClausesToLiterals &cl2lit);
 
-      virtual void WriteMappingsOfVariable(std::ostream &out,
-                                           unsigned i) const override;
+      virtual void WriteMappingsOfVariable(
+          std::ostream &out, unsigned i) const override;
 
       virtual std::string Name() const override;
 
@@ -104,8 +106,8 @@ namespace SUBool
       PCEncoder(const Config &conf = Config());
 
       // Returns empowering variable.
-      virtual unsigned ExtractClause(const SolverInterface &solver,
-                                     Clause *clause) const override;
+      virtual unsigned ExtractClause(
+          const SolverInterface &solver, Clause *clause) const override;
 
       static UP_EMPOWER UpEmpowerOfInt(unsigned emp);
    };