#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"
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,
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
{
// 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
#ifndef __CVC4__PROOF__LRAT__LRAT_PROOF_H
#define __CVC4__PROOF__LRAT__LRAT_PROOF_H
+#include <iosfwd>
#include <string>
#include <unordered_map>
#include <vector>
// 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;
// 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),
// 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
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:
*/
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
projects / cvc5.git / commitdiff