diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-04-01 09:56:14 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-01 16:56:14 +0000 |
commit | 05a53a2ac405bcd18a84024247145f161809c3b0 (patch) | |
tree | 34241c0a82f79d717ddbfbb0c294f9a09c7edb0c /src/proof | |
parent | afaf4413775ff7d6054a5893f1397ad908e0773c (diff) |
Rename namespace CVC5 to cvc5. (#6258)
Diffstat (limited to 'src/proof')
-rw-r--r-- | src/proof/clause_id.h | 4 | ||||
-rw-r--r-- | src/proof/cnf_proof.cpp | 4 | ||||
-rw-r--r-- | src/proof/cnf_proof.h | 8 | ||||
-rw-r--r-- | src/proof/dot/dot_printer.cpp | 4 | ||||
-rw-r--r-- | src/proof/dot/dot_printer.h | 4 | ||||
-rw-r--r-- | src/proof/proof_manager.cpp | 4 | ||||
-rw-r--r-- | src/proof/proof_manager.h | 10 | ||||
-rw-r--r-- | src/proof/sat_proof.h | 8 | ||||
-rw-r--r-- | src/proof/sat_proof_implementation.h | 12 | ||||
-rw-r--r-- | src/proof/unsat_core.cpp | 4 | ||||
-rw-r--r-- | src/proof/unsat_core.h | 4 |
11 files changed, 33 insertions, 33 deletions
diff --git a/src/proof/clause_id.h b/src/proof/clause_id.h index 6f3caaf19..7ce8a384a 100644 --- a/src/proof/clause_id.h +++ b/src/proof/clause_id.h @@ -20,7 +20,7 @@ #ifndef CVC4__PROOF__CLAUSE_ID_H #define CVC4__PROOF__CLAUSE_ID_H -namespace CVC5 { +namespace cvc5 { /** * A ClauseId is a shared identifier between the proofs module and the sat @@ -35,6 +35,6 @@ const ClauseId ClauseIdEmpty(-1); const ClauseId ClauseIdUndef(-2); const ClauseId ClauseIdError(-3); -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PROOF__CLAUSE_ID_H */ diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp index dc1a6dd61..fbe87c267 100644 --- a/src/proof/cnf_proof.cpp +++ b/src/proof/cnf_proof.cpp @@ -23,7 +23,7 @@ #include "prop/minisat/minisat.h" #include "prop/sat_solver_types.h" -namespace CVC5 { +namespace cvc5 { CnfProof::CnfProof(prop::CnfStream* stream, context::Context* ctx, @@ -113,4 +113,4 @@ bool CnfProof::getCurrentAssertionKind() return d_currentAssertionStack.back().second; } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h index 1319b83d6..88eb885aa 100644 --- a/src/proof/cnf_proof.h +++ b/src/proof/cnf_proof.h @@ -28,7 +28,7 @@ #include "proof/clause_id.h" #include "proof/proof_manager.h" -namespace CVC5 { +namespace cvc5 { namespace prop { class CnfStream; } // namespace prop @@ -46,7 +46,7 @@ typedef std::unordered_set<Node, NodeHashFunction> NodeSet; class CnfProof { protected: - CVC5::prop::CnfStream* d_cnfStream; + cvc5::prop::CnfStream* d_cnfStream; /** Map from ClauseId to the assertion that lead to adding this clause **/ ClauseIdToNode d_clauseToAssertion; @@ -67,7 +67,7 @@ protected: std::string d_name; public: - CnfProof(CVC5::prop::CnfStream* cnfStream, + CnfProof(cvc5::prop::CnfStream* cnfStream, context::Context* ctx, const std::string& name); ~CnfProof(); @@ -95,6 +95,6 @@ public: Node getAssertionForClause(ClauseId clause); };/* class CnfProof */ -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__CNF_PROOF_H */ diff --git a/src/proof/dot/dot_printer.cpp b/src/proof/dot/dot_printer.cpp index 8ecec8484..c2e8bd863 100644 --- a/src/proof/dot/dot_printer.cpp +++ b/src/proof/dot/dot_printer.cpp @@ -17,7 +17,7 @@ #include <sstream> #include "expr/proof_node_manager.h" -namespace CVC5 { +namespace cvc5 { namespace proof { void DotPrinter::cleanQuotes(std::string& s) @@ -91,4 +91,4 @@ void DotPrinter::ruleArguments(std::ostringstream& currentArguments, } } // namespace proof -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/proof/dot/dot_printer.h b/src/proof/dot/dot_printer.h index 173495780..3bcc1cd73 100644 --- a/src/proof/dot/dot_printer.h +++ b/src/proof/dot/dot_printer.h @@ -21,7 +21,7 @@ #include "expr/proof_node.h" -namespace CVC5 { +namespace cvc5 { namespace proof { class DotPrinter @@ -69,6 +69,6 @@ class DotPrinter }; } // namespace proof -} // namespace CVC5 +} // namespace cvc5 #endif
\ No newline at end of file diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index 8b3dfd17a..d9fd9c37a 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -36,7 +36,7 @@ #include "theory/valuation.h" #include "util/hash.h" -namespace CVC5 { +namespace cvc5 { ProofManager::ProofManager(context::Context* context) : d_context(context), @@ -217,4 +217,4 @@ void ProofManager::addUnsatCore(Node formula) d_outputCoreFormulas.insert(formula); } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h index b303b996f..b6e6c1b2c 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -28,7 +28,7 @@ #include "expr/node.h" #include "proof/clause_id.h" -namespace CVC5 { +namespace cvc5 { // forward declarations namespace Minisat { @@ -42,11 +42,11 @@ namespace prop { class SmtEngine; template <class Solver> class TSatProof; -typedef TSatProof<CVC5::Minisat::Solver> CoreSatProof; +typedef TSatProof<cvc5::Minisat::Solver> CoreSatProof; class CnfProof; -typedef TSatProof<CVC5::Minisat::Solver> CoreSatProof; +typedef TSatProof<cvc5::Minisat::Solver> CoreSatProof; namespace prop { typedef uint64_t SatVariable; @@ -81,7 +81,7 @@ public: // initialization void initSatProof(Minisat::Solver* solver); - void initCnfProof(CVC5::prop::CnfStream* cnfStream, context::Context* ctx); + void initCnfProof(cvc5::prop::CnfStream* cnfStream, context::Context* ctx); // getting various proofs static CoreSatProof* getSatProof(); @@ -120,6 +120,6 @@ private: };/* class ProofManager */ -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PROOF_MANAGER_H */ diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h index 298b82624..a66ca2d00 100644 --- a/src/proof/sat_proof.h +++ b/src/proof/sat_proof.h @@ -34,11 +34,11 @@ #include "util/stats_histogram.h" // Forward declarations. -namespace CVC5 { +namespace cvc5 { class CnfProof; -} // namespace CVC5 +} // namespace cvc5 -namespace CVC5 { +namespace cvc5 { /** * Helper debugging functions */ @@ -369,6 +369,6 @@ template <class Solver> void toSatClause(const typename Solver::TClause& minisat_cl, prop::SatClause& sat_cl); -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__SAT__PROOF_H */ diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h index 6049c4876..c2bbf6f11 100644 --- a/src/proof/sat_proof_implementation.h +++ b/src/proof/sat_proof_implementation.h @@ -26,7 +26,7 @@ #include "prop/sat_solver_types.h" #include "smt/smt_statistics_registry.h" -namespace CVC5 { +namespace cvc5 { template <class Solver> void printLit(typename Solver::TLit l) { @@ -1040,12 +1040,12 @@ TSatProof<Solver>::Statistics::~Statistics() { smtStatisticsRegistry()->unregisterStat(&d_usedClauseGlue); } -inline std::ostream& operator<<(std::ostream& out, CVC5::ClauseKind k) +inline std::ostream& operator<<(std::ostream& out, cvc5::ClauseKind k) { switch (k) { - case CVC5::INPUT: out << "INPUT"; break; - case CVC5::THEORY_LEMMA: out << "THEORY_LEMMA"; break; - case CVC5::LEARNT: out << "LEARNT"; break; + case cvc5::INPUT: out << "INPUT"; break; + case cvc5::THEORY_LEMMA: out << "THEORY_LEMMA"; break; + case cvc5::LEARNT: out << "LEARNT"; break; default: out << "ClauseKind Unknown! [" << unsigned(k) << "]"; } @@ -1053,6 +1053,6 @@ inline std::ostream& operator<<(std::ostream& out, CVC5::ClauseKind k) return out; } -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__SAT__PROOF_IMPLEMENTATION_H */ diff --git a/src/proof/unsat_core.cpp b/src/proof/unsat_core.cpp index 2415daf98..e13db65d0 100644 --- a/src/proof/unsat_core.cpp +++ b/src/proof/unsat_core.cpp @@ -20,7 +20,7 @@ #include "printer/printer.h" #include "smt/smt_engine_scope.h" -namespace CVC5 { +namespace cvc5 { UnsatCore::UnsatCore(const std::vector<Node>& core) : d_useNames(false), d_core(core), d_names() @@ -58,4 +58,4 @@ std::ostream& operator<<(std::ostream& out, const UnsatCore& core) { return out; } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/proof/unsat_core.h b/src/proof/unsat_core.h index 46dd7bf69..7d7688347 100644 --- a/src/proof/unsat_core.h +++ b/src/proof/unsat_core.h @@ -22,7 +22,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { /** * An unsat core, which can optionally be initialized as a list of names @@ -68,6 +68,6 @@ class UnsatCore /** Print the unsat core to stream out */ std::ostream& operator<<(std::ostream& out, const UnsatCore& core); -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__UNSAT_CORE_H */ |