UPSCCBinary (continuing implementation)

lib/absenc.cpp

@@ -19,6 +19,7 @@
 #include "up_onelevel.h"
 #include "up_quad.h"
 #include "up_quad_impl.h"
+#include "up_scc_binary.h"
 #include "up_scc_unary.h"
 
 SUBool::AbsEncoder::AbsEncoder(const AbsConfig &conf)
@@ -29,9 +30,8 @@ SUBool::AbsEncoder::AbsEncoder(const AbsConfig &conf)
 
 void
 SUBool::AbsEncoder::BuildEncoding(const CNF &cnf,
-                                  const ClausesToLiterals &cl2lit,
-                                  const LitImplSystem &impl_system,
-                                  const LitISGraph &scc_graph)
+    const ClausesToLiterals &cl2lit, const LitImplSystem &impl_system,
+    const LitISGraph &scc_graph)
 {
    logs.TLog(4) << "Building encoding for (p cnf " << cnf.MaxVariable() << " "
                 << cnf.Size() << ")" << std::endl;
@@ -67,9 +67,8 @@ SUBool::AbsEncoder::RequiresSCCGraph() const
 
 void
 SUBool::AbsEncoder::InitOneProveEncoder(const CNF &cnf,
-                                        const ClausesToLiterals &cl2lit,
-                                        const LitImplSystem &impl_system,
-                                        const LitISGraph &scc_graph)
+    const ClausesToLiterals &cl2lit, const LitImplSystem &impl_system,
+    const LitISGraph &scc_graph)
 {
    auto &conf = GetConfig();
    switch (conf.up_one_prove)
@@ -93,7 +92,7 @@ SUBool::AbsEncoder::InitOneProveEncoder(const CNF &cnf,
    case UP_ONE_PROVE::MIN_LQ:
       mOneProveEncoder = std::unique_ptr<UPEncMinLQ>(
           new UPEncMinLQ(cnf, cl2lit, mVarStore, conf.log_conf,
-                         conf.min_lq_log_weights, conf.min_lq_quad_weights));
+              conf.min_lq_log_weights, conf.min_lq_quad_weights));
       break;
    case UP_ONE_PROVE::QUAD_IMPL_SYSTEM:
       mOneProveEncoder =
@@ -105,25 +104,25 @@ SUBool::AbsEncoder::InitOneProveEncoder(const CNF &cnf,
           mVarStore, impl_system);
       break;
    case UP_ONE_PROVE::SCC_UNARY:
-      mOneProveEncoder = std::make_unique<UPSCCUnary>(cnf, cl2lit, mVarStore,
-                                                      impl_system, scc_graph);
+      mOneProveEncoder = std::make_unique<UPSCCUnary>(
+          cnf, cl2lit, mVarStore, impl_system, scc_graph);
       break;
    case UP_ONE_PROVE::SCC_BINARY:
-      throw BadParameterException("AbsEncoder::InitOneProveEncoder",
-                                  "SCC_BINARY UP encoding not yet implemented");
+      mOneProveEncoder = std::make_unique<UPSCCBinary>(
+          UPSCCBinary::Config(conf.log_conf.use_bit_level), cnf, cl2lit,
+          mVarStore, impl_system, scc_graph);
+      break;
    default:
       throw BadParameterException("AbsEncoder::InitOneProveEncoder",
-                                  "Unknown UP encoding type for 1-provability");
+          "Unknown UP encoding type for 1-provability");
    }
    mMaxUPLevelBound = mOneProveEncoder->MaxLevelBound();
 }
 
 unsigned
 SUBool::AbsEncoder::NextUPLevelBound(const CNF &cnf,
-                                     const ClausesToLiterals &cl2lit,
-                                     const LitImplSystem &impl_system,
-                                     const LitISGraph &scc_graph,
-                                     unsigned level)
+    const ClausesToLiterals &cl2lit, const LitImplSystem &impl_system,
+    const LitISGraph &scc_graph, unsigned level)
 {
    InitOneProveEncoder(cnf, cl2lit, impl_system, scc_graph);
    return mOneProveEncoder->NextLevelBound(level);
@@ -157,8 +156,8 @@ SUBool::AbsEncoder::WriteMappingsOfVariable(std::ostream &out, unsigned i) const
 {
    if (i == 0)
    {
-      throw OutOfBoundsException("AbsEncoder::WriteMappingsOfVariable",
-                                 "Variable i is 0");
+      throw OutOfBoundsException(
+          "AbsEncoder::WriteMappingsOfVariable", "Variable i is 0");
    }
    out << "c Mappings of variable " << i << std::endl;
 }
@@ -196,11 +195,10 @@ SUBool::operator<<(std::ostream &out, const AbsEncoder &enc)
 }
 
 void
-SUBool::AbsEncoder::AbsConfig::Dump(const std::string &line_prefix,
-                                    unsigned level) const
+SUBool::AbsEncoder::AbsConfig::Dump(
+    const std::string &line_prefix, unsigned level) const
 {
-   dump_value(
-       line_prefix, level, "up_one_prove",
+   dump_value(line_prefix, level, "up_one_prove",
        AbsEncoder::kUPOneProveNames.at(static_cast<unsigned>(up_one_prove))
            + " (" + std::to_string(static_cast<unsigned>(up_one_prove)) + ")");
    dump_value(line_prefix, level, "optimize", optimize);

lib/pcenc.cpp

@@ -19,7 +19,7 @@
 #include "up_quad.h"
 
 // On only for debugging
-//#define ONLY_UP_ONE_PROVE
+#define ONLY_UP_ONE_PROVE
 
 SUBool::PCEncoder::PCEncoder(const Config &conf)
     : AbsEncoder(conf), mConf(conf), mOneProveInputs(), mOneProveOutputs(),
@@ -29,8 +29,8 @@ SUBool::PCEncoder::PCEncoder(const Config &conf)
 }
 
 void
-SUBool::PCEncoder::InitEmpEncoder(const CNF &cnf,
-                                  const ClausesToLiterals &cl2lit)
+SUBool::PCEncoder::InitEmpEncoder(
+    const CNF &cnf, const ClausesToLiterals &cl2lit)
 {
    switch (mConf.up_empower)
    {
@@ -48,13 +48,13 @@ SUBool::PCEncoder::InitEmpEncoder(const CNF &cnf,
       break;
    default:
       throw BadParameterException("PCEncoder::InitEmpEncoder",
-                                  "Unknown UP encoding type for empowerement");
+          "Unknown UP encoding type for empowerement");
    }
 }
 
 void
-SUBool::PCEncoder::AddClauses(const CNF &cnf, const ClausesToLiterals &cl2lit,
-                              const LitImplSystem &)
+SUBool::PCEncoder::AddClauses(
+    const CNF &cnf, const ClausesToLiterals &cl2lit, const LitImplSystem &)
 {
    InitEmpEncoder(cnf, cl2lit);
    AddOneProvability();
@@ -76,14 +76,14 @@ SUBool::PCEncoder::EmpowerOutput(unsigned i) const
 }
 
 unsigned
-SUBool::PCEncoder::ExtractClause(const SolverInterface &solver,
-                                 Clause *clause) const
+SUBool::PCEncoder::ExtractClause(
+    const SolverInterface &solver, Clause *clause) const
 {
 
    if (clause == nullptr)
    {
-      throw NullPointerException("PCEncoder::ExtractClause",
-                                 "clause == nullptr");
+      throw NullPointerException(
+          "PCEncoder::ExtractClause", "clause == nullptr");
    }
    std::vector<Literal> literals;
    for (unsigned i = 0; i < mOneProveInputs.size(); ++i)
@@ -121,7 +121,7 @@ SUBool::PCEncoder::AddOneProveNoInputConflict()
       Literal pos(i, true);
       Literal neg(i, false);
       mClauses.emplace_back(Literal(mOneProveInputs[pos.Index()], false),
-                            Literal(mOneProveInputs[neg.Index()], false));
+          Literal(mOneProveInputs[neg.Index()], false));
    }
 }
 
@@ -146,7 +146,7 @@ SUBool::PCEncoder::AddOneProveOutputConflict()
       if (!mConf.optimize)
       {
          mClauses.emplace_back(Literal(t, true), Literal(pos_var, false),
-                               Literal(neg_var, false));
+             Literal(neg_var, false));
       }
    }
    mClauses.emplace_back(t_literals);
@@ -156,8 +156,8 @@ void
 SUBool::PCEncoder::AddOneProveBlock()
 {
    mVarStore.SetPrefix("v");
-   mOneProveEncoder->Encode(mConf.up_level_bound, &mOneProveInputs,
-                            &mOneProveOutputs, &mClauses);
+   mOneProveEncoder->Encode(
+       mConf.up_level_bound, &mOneProveInputs, &mOneProveOutputs, &mClauses);
    mVarStore.SetPrefix("");
 }
 
@@ -174,13 +174,12 @@ SUBool::PCEncoder::AddPassValuesToEmpower()
 {
    for (unsigned i = 0; i < mOneProveInputs.size(); ++i)
    {
-      mClauses.emplace_back(Literal(mEmpowerInputs[i], false),
-                            mSelectionLits[i / 2].Negation());
-      mClauses.emplace_back(Literal(mEmpowerInputs[i], false),
-                            Literal(mOneProveInputs[i], true));
+      mClauses.emplace_back(
+          Literal(mEmpowerInputs[i], false), mSelectionLits[i / 2].Negation());
+      mClauses.emplace_back(
+          Literal(mEmpowerInputs[i], false), Literal(mOneProveInputs[i], true));
       mClauses.emplace_back(Literal(mEmpowerInputs[i], true),
-                            mSelectionLits[i / 2],
-                            Literal(mOneProveInputs[i], false));
+          mSelectionLits[i / 2], Literal(mOneProveInputs[i], false));
       /* XXX */
       // mClauses.emplace_back(
       //     Literal(mEmpowerInputs[i], false),
@@ -206,7 +205,7 @@ SUBool::PCEncoder::AddEmpNoConflict()
       Literal pos(i, true);
       Literal neg(i, false);
       mClauses.emplace_back(Literal(EmpowerOutput(pos.Index()), false),
-                            Literal(EmpowerOutput(neg.Index()), false));
+          Literal(EmpowerOutput(neg.Index()), false));
    }
 }
 
@@ -218,9 +217,9 @@ SUBool::PCEncoder::AddEmpNotDerived()
       Literal pos(i, true);
       Literal neg(i, false);
       mClauses.emplace_back(mSelectionLits[i - 1].Negation(),
-                            Literal(EmpowerOutput(pos.Index()), false));
+          Literal(EmpowerOutput(pos.Index()), false));
       mClauses.emplace_back(mSelectionLits[i - 1].Negation(),
-                            Literal(EmpowerOutput(neg.Index()), false));
+          Literal(EmpowerOutput(neg.Index()), false));
    }
 }
 
@@ -249,8 +248,8 @@ SUBool::PCEncoder::WriteMappingsOfVariable(std::ostream &out, unsigned i) const
 {
    if (i == 0)
    {
-      throw OutOfBoundsException("PCEncoder::WriteMappingsOfVariable",
-                                 "Variable i is 0");
+      throw OutOfBoundsException(
+          "PCEncoder::WriteMappingsOfVariable", "Variable i is 0");
    }
    out << "c Mappings of variable " << i << std::endl;
    // s variables

lib/up_scc_binary.cpp

@@ -13,11 +13,29 @@ void
 SUBool::UPSCCBinary::Encode(unsigned max_level, std::vector<unsigned> *inputs,
     std::vector<unsigned> *outputs, std::vector<Clause> *clauses) const
 {
-   throw NotImplementedException("UPSCCBinary::Encode", "Not yet implemented");
+   assert(inputs != nullptr);
+   assert(outputs != nullptr);
+   assert(clauses != nullptr);
+
+   unsigned max_level_bound = MaxLevelBound();
+   if (max_level == 0 || max_level > max_level_bound)
+   {
+      max_level = max_level_bound;
+   }
+
+   Context ctx{max_level, VarInfoList(2 * mCnf.MaxVariable()),
+       mVarStore.VarArray(mCnf.MaxVariable(), true, ":in(", ")"),
+       mVarStore.VarArray(mCnf.MaxVariable(), true, ":out(", ")"), {}};
+   InitOutClauses(ctx);
+
+   AddClauses(ctx, *clauses);
+   *inputs = std::move(ctx.inputs);
+   *outputs = std::move(ctx.outputs);
 }
 
 auto
-SUBool::UPSCCBinary::EstimateSize(unsigned max_level) const -> NFSize
+SUBool::UPSCCBinary::EstimateSize(unsigned max_level [[maybe_unused]]) const
+    -> NFSize
 {
    throw NotImplementedException(
        "UPSCCBinary::EstimateSize", "Not yet implemented");
@@ -26,14 +44,124 @@ SUBool::UPSCCBinary::EstimateSize(unsigned max_level) const -> NFSize
 unsigned
 SUBool::UPSCCBinary::MaxLevelBound() const
 {
-   return mSCCGraph.MaxEffSCCVarSize();
-   throw NotImplementedException(
-       "UPSCCBinary::MaxLevelBound", "Not yet implemented");
+   return mConf.use_bit_level ? BitSizeForLevel(0)
+                              : mSCCGraph.MaxEffSCCVarSize();
 }
 
 unsigned
 SUBool::UPSCCBinary::NextLevelBound(unsigned level) const
 {
-   throw NotImplementedException(
-       "UPSCCBinary::NextLevelBound", "Not yet implemented");
+   if (level == 0 || level >= MaxLevelBound())
+   {
+      return 0;
+   }
+   if (mConf.use_bit_level)
+   {
+      return level + 1;
+   }
+   unsigned bits = BitSizeForLevel(level++);
+   while (BitSizeForLevel(level) == bits)
+   {
+      ++level;
+   }
+   return (level >= MaxLevelBound() ? 0 : level);
+}
+
+void
+SUBool::UPSCCBinary::AddClauses(
+    Context &ctx, std::vector<Clause> &clauses) const
+{
+   for (unsigned impl_index = 0; impl_index < mImplSystem.Size(); ++impl_index)
+   {
+      FireClauses(ctx, mImplSystem[impl_index], impl_index, clauses);
+   }
+   MoveOutClauses(ctx, clauses);
+}
+
+void
+SUBool::UPSCCBinary::InitOutClauses(Context &ctx) const
+{
+   for (unsigned i = 0; i < ctx.vars.size(); ++i)
+   {
+      auto &out_clause = ctx.vars[i].out_clause;
+      out_clause.push_back(make_negative_literal(ctx.outputs[i]));
+      out_clause.push_back(make_positive_literal(ctx.inputs[i]));
+   }
+}
+
+void
+SUBool::UPSCCBinary::FireClauses(Context &ctx, const LitImpl &impl,
+    unsigned impl_index, std::vector<Clause> &clauses) const
+{
+   unsigned simple_fire_var = 0;
+   ctx.scc_buffer.assign(mSCCGraph.SCCCount(), false);
+   for (const auto &lit : impl.Body())
+   {
+      ctx.scc_buffer[mSCCGraph.SCC(lit)] = true;
+   }
+   for (const auto &lit : impl.Cons())
+   {
+      if (ctx.scc_buffer[mSCCGraph.SCC(lit)])
+      {
+         FireVariableInMainSCC(ctx, impl, impl_index, lit, clauses);
+         continue;
+      }
+      simple_fire_var = FireVariableNotInMainSCC(
+          ctx, impl, impl_index, lit, simple_fire_var, clauses);
+   }
+}
+
+void
+SUBool::UPSCCBinary::MoveOutClauses(
+    Context &ctx, std::vector<Clause> &clauses) const
+{
+   for (auto &var_info : ctx.vars)
+   {
+      clauses.emplace_back(std::move(var_info.out_clause));
+   }
+}
+
+void
+SUBool::UPSCCBinary::FireVariableInMainSCC(Context &ctx, const LitImpl &impl,
+    unsigned impl_index, const Literal &lit, std::vector<Clause> &clauses) const
+{
+   // Literal in the main SCC
+   // - Init fire variable f[impl_index, lit]
+   // - Add implications to the output variables of the body
+   // - Add implications to the inequalities
+   // - Add to the out clause
+}
+
+unsigned
+SUBool::UPSCCBinary::FireVariableNotInMainSCC(Context &ctx, const LitImpl &impl,
+    unsigned impl_index, const Literal &lit, unsigned simple_fire_var,
+    std::vector<Clause> &clauses) const
+{
+   // Literal out of the main SCC
+   if (simple_fire_var == 0)
+   {
+      simple_fire_var = SimpleFireVar(ctx, impl, impl_index, clauses);
+   }
+   ctx.vars[lit.Index()].out_clause.push_back(
+       make_positive_literal(simple_fire_var));
+   return simple_fire_var;
+}
+
+unsigned
+SUBool::UPSCCBinary::SimpleFireVar(const Context &ctx, const LitImpl &impl,
+    unsigned impl_index, std::vector<Clause> &clauses) const
+{
+   if (impl.BodySize() == 1)
+   {
+      return ctx.outputs[impl.Body().front().Index()];
+   }
+   mVarStore.NameStream() << "f[" << impl_index << "]";
+   unsigned fv = mVarStore.NewVariable();
+   auto neg_fv = make_negative_literal(fv);
+   for (const auto &lit : impl.Body())
+   {
+      clauses.emplace_back(
+          neg_fv, make_positive_literal(ctx.outputs[lit.Index()]));
+   }
+   return fv;
 }

lib/up_scc_binary.h

@@ -29,12 +29,40 @@ namespace SUBool
          void Dump(const std::string &line_prefix, unsigned level) const;
       };
 
+      struct VarInfo
+      {
+         std::vector<unsigned> level_vars;
+         std::vector<Literal> out_clause;
+      };
+      using VarInfoList = std::vector<VarInfo>;
+      struct Context
+      {
+         unsigned max_level;
+         VarInfoList vars;
+         std::vector<unsigned> inputs;
+         std::vector<unsigned> outputs;
+         std::vector<bool> scc_buffer;
+      };
+
     private:
       const LitImplSystem &mImplSystem;
       const LitISGraph &mSCCGraph;
       Config mConf;
 
       unsigned BitSizeForLevel(unsigned level) const;
+      void InitOutClauses(Context &ctx) const;
+      void AddClauses(Context &ctx, std::vector<Clause> &clauses) const;
+      void FireClauses(Context &ctx, const LitImpl &impl, unsigned impl_index,
+          std::vector<Clause> &clauses) const;
+      void MoveOutClauses(Context &ctx, std::vector<Clause> &clauses) const;
+      void FireVariableInMainSCC(Context &ctx, const LitImpl &impl,
+          unsigned impl_index, const Literal &lit,
+          std::vector<Clause> &clauses) const;
+      unsigned FireVariableNotInMainSCC(Context &ctx, const LitImpl &impl,
+          unsigned impl_index, const Literal &lit, unsigned simple_fire_var,
+          std::vector<Clause> &clauses) const;
+      unsigned SimpleFireVar(const Context &ctx, const LitImpl &impl,
+          unsigned impl_index, std::vector<Clause> &clauses) const;
 
     public:
       UPSCCBinary(const Config &conf, const CNF &cnf,
@@ -57,7 +85,7 @@ namespace SUBool
 inline unsigned
 SUBool::UPSCCBinary::BitSizeForLevel(unsigned level) const
 {
-   return bit_size_for_level(level, mCnf.MaxVariable());
+   return bit_size_for_level(level, mSCCGraph.MaxEffSCCVarSize());
 }
 
 #endif

lib/up_scc_unary.cpp

@@ -270,8 +270,7 @@ SUBool::UPSCCUnary::AddOutImplications(
 std::pair<unsigned, bool>
 SUBool::UPSCCUnary::InspectImplSCC(Context &ctx, const LitImpl &impl) const
 {
-   ctx.scc_buffer.clear();
-   ctx.scc_buffer.resize(mSCCGraph.SCCCount(), false);
+   ctx.scc_buffer.assign(mSCCGraph.SCCCount(), false);
    for (const auto &lit : impl.Body())
    {
       ctx.scc_buffer[mSCCGraph.SCC(lit)] = true;