diff options
Diffstat (limited to 'src/proof/lrat/lrat_proof.h')
-rw-r--r-- | src/proof/lrat/lrat_proof.h | 184 |
1 files changed, 0 insertions, 184 deletions
diff --git a/src/proof/lrat/lrat_proof.h b/src/proof/lrat/lrat_proof.h deleted file mode 100644 index 1c065a08e..000000000 --- a/src/proof/lrat/lrat_proof.h +++ /dev/null @@ -1,184 +0,0 @@ -/********************* */ -/*! \file lrat_proof.h - ** \verbatim - ** Top contributors (to current version): - ** Alex Ozdemir, Mathias Preiner - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief LRAT Proof Format - ** - ** Declares C++ types that represent a LRAT proof. - ** Defines serialization for these types. - ** - ** Represents an **abstract** LRAT proof. - ** Does **not** represent an LFSC LRAT proof, or an LRAT proof being used to - ** prove things about bit-vectors. - ** - ** Paper on LRAT: https://www.cs.utexas.edu/~marijn/publications/lrat.pdf - **/ - -#include "cvc4_private.h" - -#ifndef CVC4__PROOF__LRAT__LRAT_PROOF_H -#define CVC4__PROOF__LRAT__LRAT_PROOF_H - -#include <iosfwd> -#include <string> -#include <unordered_map> -#include <utility> -#include <vector> - -#include "proof/clause_id.h" -// Included because we need operator<< for the SAT types -#include "prop/sat_solver.h" -#include "util/statistics_registry.h" - -namespace CVC4 { -namespace proof { -namespace lrat { - -// Refers to clause position within an LRAT proof -using ClauseIdx = size_t; - -// This is conceptually an Either<Addition,Deletion> -class LratInstruction -{ - public: - /** - * Write this LRAT instruction in textual format - * - * @param out the stream to write to - */ - virtual void outputAsText(std::ostream& out) const = 0; - /** - * Write this LRAT instruction as an LFSC value - * - * @param out the stream to write to - * @param closeParen the stream to write any closing parentheses to - * - */ - virtual void outputAsLfsc(std::ostream& o, - std::ostream& closeParen) const = 0; - virtual ~LratInstruction() = default; -}; - -class LratDeletion : public LratInstruction -{ - public: - LratDeletion(ClauseIdx idxOfClause, std::vector<ClauseIdx>&& clauses) - : d_idxOfClause(idxOfClause), d_clauses(clauses) - { - // Nothing left to do - } - - LratDeletion() = default; - - void outputAsText(std::ostream& out) const override; - void outputAsLfsc(std::ostream& o, std::ostream& closeParen) const override; - - private: - // This idx doesn't really matter, but it's in the format anyway, so we parse - // it. - ClauseIdx d_idxOfClause; - - // Clauses to delete - std::vector<ClauseIdx> d_clauses; -}; - -// A sequence of locations that will contain unit clauses during unit -// propegation -using LratUPTrace = std::vector<ClauseIdx>; - -class LratAddition : public LratInstruction -{ - 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), - d_resolvants(resolvants) - { - // Nothing left to do - } - - void outputAsText(std::ostream& out) const override; - void outputAsLfsc(std::ostream& o, std::ostream& closeParen) const override; - - private: - // The idx for the new clause - ClauseIdx d_idxOfClause; - // The new clause - prop::SatClause d_clause; - // UP trace based on the negation of that clause - LratUPTrace d_atTrace; - - // Clauses that can resolve with `clause` on its first variable, - // together with a UP trace after that resolution. - // Used for RAT checks. - std::vector<std::pair<ClauseIdx, LratUPTrace>> d_resolvants; -}; - -class LratProof -{ - public: - /** - * @brief Construct an LRAT proof from a DRAT proof, using drat-trim - * - * @param clauses A store of clauses that might be in our formula - * @param usedIds the ids of clauses that are actually in our formula - * @param dratBinary The DRAT proof from the SAT solver, as a binary stream. - * - * @return an LRAT proof an a timer for how long it took to run drat-trim - */ - static LratProof fromDratProof( - const std::unordered_map<ClauseId, prop::SatClause>& clauses, - const std::vector<ClauseId> usedIds, - const std::string& dratBinary, - TimerStat& toolTimer); - /** - * @brief Construct an LRAT proof from its textual representation - * - * @param textualProof the textual encoding of the LRAT proof. See the paper - * in the file's header comment. - */ - LratProof(std::istream& textualProof); - - /** - * 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; - } - - void outputAsLfsc(std::ostream& o) const; - - private: - // The instructions in the proof. Each is a deletion or addition. - 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 -} // namespace CVC4 - -#endif |