LratInstruction inheritance (#2784)

While implementing and testing LRAT proof output as LFSC, I discovered
that my implementation of LratInstruction as a tagged union was subtly
broken for reasons related to move/copy assignment/constructors.

While I could have figured out how to fix it, I decided to stop fighting
the system and use inheritance.

This PR will be followed by one using the inheritance-based
LratInstruction to implement output to LFSC.

2 files changed, 83 insertions, 139 deletions

diff --git a/src/proof/lrat/lrat_proof.cpp b/src/proof/lrat/lrat_proof.cpp
index 6c2c5e2e8..01dfd145f 100644
--- a/src/proof/lrat/lrat_proof.cpp
+++ b/src/proof/lrat/lrat_proof.cpp
@@ -20,10 +20,13 @@
 #include <cstdlib>
 #include <fstream>
 #include <iostream>
+#include <memory>
+#include <sstream>
 #include <unordered_map>
 
 #include "base/cvc4_assert.h"
 #include "base/output.h"
+#include "proof/lfsc_proof_printer.h"
 
 #if CVC4_USE_DRAT2ER
 #include "drat2er_options.h"
@@ -72,107 +75,9 @@ std::ostream& operator<<(std::ostream& o, const LratUPTrace& trace)
   return o;
 }
 
-// Prints the LRAT addition line in textual format
-std::ostream& operator<<(std::ostream& o, const LratAdditionData& add)
-{
-  o << add.d_idxOfClause << " ";
-  textOut(o, add.d_clause) << " ";
-  o << add.d_atTrace;  // Inludes a space at the end.
-  for (const auto& rat : add.d_resolvants)
-  {
-    o << "-" << rat.first << " ";
-    o << rat.second;  // Includes a space at the end.
-  }
-  o << "0\n";
-  return o;
-}
+}  // namespace
 
 // Prints the LRAT addition line in textual format
-std::ostream& operator<<(std::ostream& o, const LratDeletionData& del)
-{
-  o << del.d_idxOfClause << " d ";
-  for (const auto& idx : del.d_clauses)
-  {
-    o << idx << " ";
-  }
-  return o << "0\n";
-}
-
-// Prints the LRAT line in textual format
-std::ostream& operator<<(std::ostream& o, const LratInstruction& i)
-{
-  switch (i.d_kind)
-  {
-    case LRAT_ADDITION: return o << i.d_data.d_addition;
-    case LRAT_DELETION: return o << i.d_data.d_deletion;
-    default: return o;
-  }
-}
-
-}
-
-LratInstruction::LratInstruction(LratInstruction&& instr) : d_kind(instr.d_kind)
-{
-  switch (d_kind)
-  {
-    case LRAT_ADDITION:
-    {
-      d_data.d_addition = instr.d_data.d_addition;
-      break;
-    }
-    case LRAT_DELETION:
-    {
-      d_data.d_deletion = instr.d_data.d_deletion;
-      break;
-    }
-  }
-}
-
-LratInstruction::LratInstruction(LratInstruction& instr) : d_kind(instr.d_kind)
-{
-  switch (d_kind)
-  {
-    case LRAT_ADDITION:
-    {
-      d_data.d_addition = instr.d_data.d_addition;
-      break;
-    }
-    case LRAT_DELETION:
-    {
-      d_data.d_deletion = instr.d_data.d_deletion;
-      break;
-    }
-  }
-}
-
-LratInstruction::LratInstruction(LratAdditionData&& addition)
-    : d_kind(LRAT_ADDITION)
-{
-  d_data.d_addition = std::move(addition);
-}
-
-LratInstruction::LratInstruction(LratDeletionData&& deletion)
-    : d_kind(LRAT_DELETION)
-{
-  d_data.d_deletion = std::move(deletion);
-}
-
-LratInstruction::~LratInstruction()
-{
-  switch (d_kind)
-  {
-    case LRAT_ADDITION:
-    {
-      d_data.d_addition.~LratAdditionData();
-      break;
-    }
-    case LRAT_DELETION:
-    {
-      d_data.d_deletion.~LratDeletionData();
-      break;
-    }
-  }
-}
 
 LratProof LratProof::fromDratProof(
     const std::unordered_map<ClauseId, SatClause*>& usedClauses,
@@ -284,8 +189,9 @@ LratProof::LratProof(std::istream& textualProof)
         clauses.push_back(di);
       }
       std::sort(clauses.begin(), clauses.end());
-      d_instructions.emplace_back(
-          LratDeletionData(clauseIdx, std::move(clauses)));
+      std::unique_ptr<LratInstruction> instr(
+          new LratDeletion(clauseIdx, std::move(clauses)));
+      d_instructions.push_back(std::move(instr));
     }
     else
     {
@@ -332,23 +238,54 @@ LratProof::LratProof(std::istream& textualProof)
       // Pairs compare based on the first element, so this sorts by the
       // resolution target index
       std::sort(resolvants.begin(), resolvants.end());
-      d_instructions.emplace_back(LratAdditionData(clauseIdx,
-                                                   std::move(clause),
-                                                   std::move(atTrace),
-                                                   std::move(resolvants)));
+      std::unique_ptr<LratInstruction> instr(
+          new LratAddition(clauseIdx,
+                           std::move(clause),
+                           std::move(atTrace),
+                           std::move(resolvants)));
+      d_instructions.push_back(std::move(instr));
     }
   }
 }
 
+void LratAddition::outputAsText(std::ostream& o) const
+{
+  o << d_idxOfClause << " ";
+  textOut(o, d_clause) << " ";
+  o << d_atTrace;  // Inludes a space at the end.
+  for (const auto& rat : d_resolvants)
+  {
+    o << "-" << rat.first << " ";
+    o << rat.second;  // Includes a space at the end.
+  }
+  o << "0\n";
+}
+
+void LratDeletion::outputAsText(std::ostream& o) const
+{
+  o << d_idxOfClause << " d ";
+  for (const auto& idx : d_clauses)
+  {
+    o << idx << " ";
+  }
+  o << "0\n";
+}
+
 std::ostream& operator<<(std::ostream& o, const LratProof& p)
 {
   for (const auto& instr : p.getInstructions())
   {
-    o << instr;
+    o << *instr;
   }
   return o;
 }
 
+std::ostream& operator<<(std::ostream& o, const LratInstruction& i)
+{
+  i.outputAsText(o);
+  return o;
+}
+
 }  // namespace lrat
 }  // namespace proof
 }  // namespace CVC4
diff --git a/src/proof/lrat/lrat_proof.h b/src/proof/lrat/lrat_proof.h
index 384fbbdf4..d976c1279 100644
--- a/src/proof/lrat/lrat_proof.h
+++ b/src/proof/lrat/lrat_proof.h
@@ -26,6 +26,7 @@
 #ifndef __CVC4__PROOF__LRAT__LRAT_PROOF_H
 #define __CVC4__PROOF__LRAT__LRAT_PROOF_H
 
+#include <iosfwd>
 #include <string>
 #include <unordered_map>
 #include <vector>
@@ -41,22 +42,33 @@ namespace lrat {
 // Refers to clause position within an LRAT proof
 using ClauseIdx = size_t;
 
-enum LratInstructionKind
+// This is conceptually an Either<Addition,Deletion>
+class LratInstruction
 {
-  LRAT_DELETION,
-  LRAT_ADDITION,
+ public:
+  /**
+   * Write this LRAT instruction in textual format
+   *
+   * @param out the stream to write to
+   */
+  virtual void outputAsText(std::ostream& out) const = 0;
+  virtual ~LratInstruction() = default;
 };
 
-struct LratDeletionData
+class LratDeletion : public LratInstruction
 {
-  LratDeletionData(ClauseIdx idxOfClause, std::vector<ClauseIdx>&& clauses)
+ public:
+  LratDeletion(ClauseIdx idxOfClause, std::vector<ClauseIdx>&& clauses)
       : d_idxOfClause(idxOfClause), d_clauses(clauses)
   {
     // Nothing left to do
   }
 
-  ~LratDeletionData() = default;
+  LratDeletion() = default;
 
+  void outputAsText(std::ostream& out) const override;
+
+ private:
   // This idx doesn't really matter, but it's in the format anyway, so we parse
   // it.
   ClauseIdx d_idxOfClause;
@@ -69,12 +81,13 @@ struct LratDeletionData
 // propegation
 using LratUPTrace = std::vector<ClauseIdx>;
 
-struct LratAdditionData
+class LratAddition : public LratInstruction
 {
-  LratAdditionData(ClauseIdx idxOfClause,
-                   prop::SatClause&& clause,
-                   LratUPTrace&& atTrace,
-                   std::vector<std::pair<ClauseIdx, LratUPTrace>> resolvants)
+ public:
+  LratAddition(ClauseIdx idxOfClause,
+               prop::SatClause&& clause,
+               LratUPTrace&& atTrace,
+               std::vector<std::pair<ClauseIdx, LratUPTrace>> resolvants)
       : d_idxOfClause(idxOfClause),
         d_clause(clause),
         d_atTrace(atTrace),
@@ -83,8 +96,9 @@ struct LratAdditionData
     // Nothing left to do
   }
 
-  ~LratAdditionData() = default;
+  void outputAsText(std::ostream& out) const override;
 
+ private:
   // The idx for the new clause
   ClauseIdx d_idxOfClause;
   // The new clause
@@ -98,25 +112,6 @@ struct LratAdditionData
   std::vector<std::pair<ClauseIdx, LratUPTrace>> d_resolvants;
 };
 
-// This is conceptually an Either<Addition,Deletion>
-struct LratInstruction
-{
-  LratInstructionKind d_kind;
-  union LratInstructionData
-  {
-    LratAdditionData d_addition;
-    LratDeletionData d_deletion;
-    ~LratInstructionData(){/* Empty destructor */};
-    LratInstructionData(){/* Empty constructor */};
-  } d_data;
-
-  LratInstruction(LratInstruction&& instr);
-  LratInstruction(LratInstruction& instr);
-  LratInstruction(LratAdditionData&& addition);
-  LratInstruction(LratDeletionData&& deletion);
-  ~LratInstruction();
-};
-
 class LratProof
 {
  public:
@@ -142,18 +137,30 @@ class LratProof
    */
   LratProof(std::istream& textualProof);
 
-  const std::vector<LratInstruction>& getInstructions() const
+  /**
+   * Construct a LRAT proof from an explicit instruction list
+   *
+   * @param instructions
+   */
+  LratProof(std::vector<std::unique_ptr<LratInstruction>>&& instructions)
+      : d_instructions(std::move(instructions))
+  {
+    // Nothing else
+  }
+
+  const std::vector<std::unique_ptr<LratInstruction>>& getInstructions() const
   {
     return d_instructions;
   }
 
  private:
   // The instructions in the proof. Each is a deletion or addition.
-  std::vector<LratInstruction> d_instructions;
+  std::vector<std::unique_ptr<LratInstruction>> d_instructions;
 };
 
 // Prints the LRAT proof in textual format
 std::ostream& operator<<(std::ostream& o, const LratProof& p);
+std::ostream& operator<<(std::ostream& o, const LratInstruction& i);
 
 }  // namespace lrat
 }  // namespace proof