From 05a53a2ac405bcd18a84024247145f161809c3b0 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Thu, 1 Apr 2021 09:56:14 -0700 Subject: Rename namespace CVC5 to cvc5. (#6258) --- src/prop/minisat/core/Dimacs.h | 4 ++-- src/prop/minisat/core/Solver.cc | 38 ++++++++++++++++++------------------- src/prop/minisat/core/Solver.h | 34 ++++++++++++++++----------------- src/prop/minisat/core/SolverTypes.h | 14 +++++++------- src/prop/minisat/minisat.cpp | 14 +++++++------- src/prop/minisat/minisat.h | 6 +++--- src/prop/minisat/mtl/Alg.h | 4 ++-- src/prop/minisat/mtl/Alloc.h | 4 ++-- src/prop/minisat/mtl/Heap.h | 4 ++-- src/prop/minisat/mtl/Map.h | 4 ++-- src/prop/minisat/mtl/Queue.h | 4 ++-- src/prop/minisat/mtl/Sort.h | 4 ++-- src/prop/minisat/mtl/Vec.h | 4 ++-- src/prop/minisat/mtl/XAlloc.h | 4 ++-- src/prop/minisat/simp/SimpSolver.cc | 10 +++++----- src/prop/minisat/simp/SimpSolver.h | 14 +++++++------- src/prop/minisat/utils/Options.h | 4 ++-- src/prop/minisat/utils/ParseUtils.h | 4 ++-- 18 files changed, 87 insertions(+), 87 deletions(-) (limited to 'src/prop/minisat') diff --git a/src/prop/minisat/core/Dimacs.h b/src/prop/minisat/core/Dimacs.h index b48044457..02182fde3 100644 --- a/src/prop/minisat/core/Dimacs.h +++ b/src/prop/minisat/core/Dimacs.h @@ -26,7 +26,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/minisat/utils/ParseUtils.h" #include "prop/minisat/core/SolverTypes.h" -namespace CVC5 { +namespace cvc5 { namespace Minisat { //================================================================================================= @@ -86,6 +86,6 @@ static void parse_DIMACS(gzFile input_stream, Solver& S) { //================================================================================================= } -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 9dbcada15..cd3ae5edf 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -39,9 +39,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/minisat/mtl/Sort.h" #include "prop/theory_proxy.h" -using namespace CVC5::prop; +using namespace cvc5::prop; -namespace CVC5 { +namespace cvc5 { namespace Minisat { namespace { @@ -83,7 +83,7 @@ static inline void dtviewPropagationHeaderHelper(size_t level) // Writes to Trace macro for propagation tracing static inline void dtviewBoolPropagationHelper(size_t level, Lit& l, - CVC5::prop::TheoryProxy* proxy) + cvc5::prop::TheoryProxy* proxy) { Trace("dtview::prop") << std::string( level + 1 - (options::incrementalSolving() ? 1 : 0), ' ') @@ -95,7 +95,7 @@ static inline void dtviewBoolPropagationHelper(size_t level, // Writes to Trace macro for conflict tracing static inline void dtviewPropConflictHelper(size_t level, Clause& confl, - CVC5::prop::TheoryProxy* proxy) + cvc5::prop::TheoryProxy* proxy) { Trace("dtview::conflict") << std::string(level + 1 - (options::incrementalSolving() ? 1 : 0), ' ') @@ -148,9 +148,9 @@ class ScopedBool //================================================================================================= // Constructor/Destructor: -Solver::Solver(CVC5::prop::TheoryProxy* proxy, - CVC5::context::Context* context, - CVC5::context::UserContext* userContext, +Solver::Solver(cvc5::prop::TheoryProxy* proxy, + cvc5::context::Context* context, + cvc5::context::UserContext* userContext, ProofNodeManager* pnm, bool enableIncremental) : d_proxy(proxy), @@ -548,7 +548,7 @@ bool Solver::addClause_(vec& ps, bool removable, ClauseId& id) ProofManager::getCnfProof()->registerConvertedClause(id); } ProofManager::getSatProof()->finalizeProof( - CVC5::Minisat::CRef_Lazy); + cvc5::Minisat::CRef_Lazy); } if (isProofEnabled()) { @@ -648,7 +648,7 @@ bool Solver::addClause_(vec& ps, bool removable, ClauseId& id) id = ProofManager::getSatProof()->storeUnitConflict( ca[confl][0], LEARNT); ProofManager::getSatProof()->finalizeProof( - CVC5::Minisat::CRef_Lazy); + cvc5::Minisat::CRef_Lazy); } else { @@ -1030,7 +1030,7 @@ int Solver::analyze(CRef confl, vec& out_learnt, int& out_btlevel) Trace("pf::sat") << "\n"; } - Trace("pf::sat") << CVC5::push; + Trace("pf::sat") << cvc5::push; for (int j = (p == lit_Undef) ? 0 : 1, size = ca[confl].size(); j < size; j++) @@ -1073,7 +1073,7 @@ int Solver::analyze(CRef confl, vec& out_learnt, int& out_btlevel) } } } - Trace("pf::sat") << CVC5::pop; + Trace("pf::sat") << cvc5::pop; // Select next clause to look at: while (!seen[var(trail[index--])]); @@ -1326,7 +1326,7 @@ CRef Solver::propagate(TheoryCheckType type) // theory propagation if (type == CHECK_FINAL) { // Do the theory check - theoryCheck(CVC5::theory::Theory::EFFORT_FULL); + theoryCheck(cvc5::theory::Theory::EFFORT_FULL); // Pick up the theory propagated literals (there could be some, // if new lemmas are added) propagateTheory(); @@ -1350,9 +1350,9 @@ CRef Solver::propagate(TheoryCheckType type) if (confl == CRef_Undef && type != CHECK_WITHOUT_THEORY) { // Do the theory check if (type == CHECK_FINAL_FAKE) { - theoryCheck(CVC5::theory::Theory::EFFORT_FULL); + theoryCheck(cvc5::theory::Theory::EFFORT_FULL); } else { - theoryCheck(CVC5::theory::Theory::EFFORT_STANDARD); + theoryCheck(cvc5::theory::Theory::EFFORT_STANDARD); } // Pick up the theory propagated literals propagateTheory(); @@ -1439,7 +1439,7 @@ void Solver::propagateTheory() { | | Note: the propagation queue might be NOT empty |________________________________________________________________________________________________@*/ -void Solver::theoryCheck(CVC5::theory::Theory::Effort effort) +void Solver::theoryCheck(cvc5::theory::Theory::Effort effort) { d_proxy->theoryCheck(effort); } @@ -2145,7 +2145,7 @@ void Solver::pop() --assertionLevel; Debug("minisat") << "in user pop, decreasing assertion level to " << assertionLevel << "\n" - << CVC5::push; + << cvc5::push; while (true) { Debug("minisat") << "== unassigning " << trail.last() << std::endl; Var x = var(trail.last()); @@ -2167,7 +2167,7 @@ void Solver::pop() // Remove the clauses removeClausesAboveLevel(clauses_persistent, assertionLevel); removeClausesAboveLevel(clauses_removable, assertionLevel); - Debug("minisat") << CVC5::pop; + Debug("minisat") << cvc5::pop; // Pop the SAT context to notify everyone d_context->pop(); // SAT context for CVC4 @@ -2347,7 +2347,7 @@ CRef Solver::updateLemmas() { void ClauseAllocator::reloc(CRef& cr, ClauseAllocator& to, - CVC5::TSatProof* proof) + cvc5::TSatProof* proof) { Debug("minisat") << "ClauseAllocator::reloc: cr " << cr << std::endl; // FIXME what is this CRef_lazy @@ -2398,4 +2398,4 @@ std::shared_ptr Solver::getProof() bool Solver::isProofEnabled() const { return d_pfManager != nullptr; } } // namespace Minisat -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index 53f7a828c..9da0e2f89 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -38,16 +38,16 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "theory/theory.h" #include "util/resource_manager.h" -namespace CVC5 { +namespace cvc5 { template class TSatProof; namespace prop { class PropEngine; class TheoryProxy; } // namespace prop -} // namespace CVC5 +} // namespace cvc5 -namespace CVC5 { +namespace cvc5 { namespace Minisat { //================================================================================================= @@ -56,10 +56,10 @@ namespace Minisat { class Solver { /** The only two CVC4 entry points to the private solver data */ - friend class CVC5::prop::PropEngine; - friend class CVC5::prop::TheoryProxy; - friend class CVC5::prop::SatProofManager; - friend class CVC5::TSatProof; + friend class cvc5::prop::PropEngine; + friend class cvc5::prop::TheoryProxy; + friend class cvc5::prop::SatProofManager; + friend class cvc5::TSatProof; public: static CRef TCRef_Undef; @@ -73,10 +73,10 @@ class Solver { protected: /** The pointer to the proxy that provides interfaces to the SMT engine */ - CVC5::prop::TheoryProxy* d_proxy; + cvc5::prop::TheoryProxy* d_proxy; /** The context from the SMT solver */ - CVC5::context::Context* d_context; + cvc5::context::Context* d_context; /** The current assertion level (user) */ int assertionLevel; @@ -88,7 +88,7 @@ class Solver { Var varFalse; /** The resolution proof manager */ - std::unique_ptr d_pfManager; + std::unique_ptr d_pfManager; public: /** Returns the current user assertion level */ @@ -105,7 +105,7 @@ class Solver { vec lemmas_removable; /** Nodes being converted to CNF */ - std::vector lemmas_cnf_assertion; + std::vector lemmas_cnf_assertion; /** Do a another check if FULL_EFFORT was the last one */ bool recheck; @@ -134,9 +134,9 @@ public: // Constructor/Destructor: // - Solver(CVC5::prop::TheoryProxy* proxy, - CVC5::context::Context* context, - CVC5::context::UserContext* userContext, + Solver(cvc5::prop::TheoryProxy* proxy, + cvc5::context::Context* context, + cvc5::context::UserContext* userContext, ProofNodeManager* pnm, bool enableIncremental = false); virtual ~Solver(); @@ -153,7 +153,7 @@ public: Var falseVar() const { return varFalse; } /** Retrive the SAT proof manager */ - CVC5::prop::SatProofManager* getProofManager(); + cvc5::prop::SatProofManager* getProofManager(); /** Retrive the refutation proof */ std::shared_ptr getProof(); @@ -438,7 +438,7 @@ protected: CRef propagateBool (); // Perform Boolean propagation. Returns possibly conflicting clause. void propagateTheory (); // Perform Theory propagation. void theoryCheck( - CVC5::theory::Theory::Effort + cvc5::theory::Theory::Effort effort); // Perform a theory satisfiability check. Adds lemmas. CRef updateLemmas (); // Add the lemmas, backtraking if necessary and return a conflict if there is one void cancelUntil (int level); // Backtrack until a certain level. @@ -666,6 +666,6 @@ inline void Solver::toDimacs (const char* file, Lit p, Lit q, Lit r){ ve //================================================================================================= } // namespace Minisat -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/prop/minisat/core/SolverTypes.h b/src/prop/minisat/core/SolverTypes.h index 4d9dd682d..c3f4279cb 100644 --- a/src/prop/minisat/core/SolverTypes.h +++ b/src/prop/minisat/core/SolverTypes.h @@ -31,15 +31,15 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/minisat/mtl/Map.h" #include "prop/minisat/mtl/Vec.h" -namespace CVC5 { +namespace cvc5 { namespace Minisat { class Solver; } template class TSatProof; -} // namespace CVC5 +} // namespace cvc5 -namespace CVC5 { +namespace cvc5 { namespace Minisat { //================================================================================================= @@ -183,9 +183,9 @@ inline std::ostream& operator <<(std::ostream& out, Minisat::lbool val) { } } // namespace Minisat -} // namespace CVC5 +} // namespace cvc5 -namespace CVC5 { +namespace cvc5 { namespace Minisat{ //================================================================================================= @@ -322,7 +322,7 @@ class ClauseAllocator : public RegionAllocator void reloc(CRef& cr, ClauseAllocator& to, - CVC5::TSatProof* proof = NULL); + cvc5::TSatProof* proof = NULL); // Implementation moved to Solver.cc. }; @@ -500,6 +500,6 @@ inline void Clause::strengthen(Lit p) //================================================================================================= } -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index e95677d57..07b345eda 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -25,7 +25,7 @@ #include "proof/sat_proof.h" #include "util/statistics_registry.h" -namespace CVC5 { +namespace cvc5 { namespace prop { //// DPllMinisatSatSolver @@ -301,20 +301,20 @@ void MinisatSatSolver::Statistics::init(Minisat::SimpSolver* minisat){ } } // namespace prop -} // namespace CVC5 +} // namespace cvc5 -namespace CVC5 { +namespace cvc5 { template <> -prop::SatLiteral toSatLiteral(Minisat::Solver::TLit lit) +prop::SatLiteral toSatLiteral(Minisat::Solver::TLit lit) { return prop::MinisatSatSolver::toSatLiteral(lit); } template <> -void toSatClause( - const CVC5::Minisat::Solver::TClause& minisat_cl, prop::SatClause& sat_cl) +void toSatClause( + const cvc5::Minisat::Solver::TClause& minisat_cl, prop::SatClause& sat_cl) { prop::MinisatSatSolver::toSatClause(minisat_cl, sat_cl); } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h index 7dfeb6aa2..0a36b6297 100644 --- a/src/prop/minisat/minisat.h +++ b/src/prop/minisat/minisat.h @@ -20,7 +20,7 @@ #include "prop/minisat/simp/SimpSolver.h" #include "util/statistics_registry.h" -namespace CVC5 { +namespace cvc5 { namespace prop { class MinisatSatSolver : public CDCLTSatSolverInterface @@ -40,7 +40,7 @@ class MinisatSatSolver : public CDCLTSatSolverInterface static void toSatClause (const Minisat::Clause& clause, SatClause& sat_clause); void initialize(context::Context* context, TheoryProxy* theoryProxy, - CVC5::context::UserContext* userContext, + cvc5::context::UserContext* userContext, ProofNodeManager* pnm) override; ClauseId addClause(SatClause& clause, bool removable) override; @@ -119,4 +119,4 @@ class MinisatSatSolver : public CDCLTSatSolverInterface }; /* class MinisatSatSolver */ } // namespace prop -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/prop/minisat/mtl/Alg.h b/src/prop/minisat/mtl/Alg.h index 37bc4b7b6..69b782da9 100644 --- a/src/prop/minisat/mtl/Alg.h +++ b/src/prop/minisat/mtl/Alg.h @@ -24,7 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "base/check.h" #include "prop/minisat/mtl/Vec.h" -namespace CVC5 { +namespace cvc5 { namespace Minisat { //================================================================================================= @@ -82,6 +82,6 @@ static inline void append(const vec& from, vec& to){ copy(from, to, true); //================================================================================================= } -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/prop/minisat/mtl/Alloc.h b/src/prop/minisat/mtl/Alloc.h index 850aaeb73..f6e6d64b2 100644 --- a/src/prop/minisat/mtl/Alloc.h +++ b/src/prop/minisat/mtl/Alloc.h @@ -25,7 +25,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/minisat/mtl/Vec.h" #include "prop/minisat/mtl/XAlloc.h" -namespace CVC5 { +namespace cvc5 { namespace Minisat { //================================================================================================= @@ -149,6 +149,6 @@ RegionAllocator::alloc(int size) //================================================================================================= } -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/prop/minisat/mtl/Heap.h b/src/prop/minisat/mtl/Heap.h index e2ad1513f..7a88c874d 100644 --- a/src/prop/minisat/mtl/Heap.h +++ b/src/prop/minisat/mtl/Heap.h @@ -24,7 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "base/check.h" #include "prop/minisat/mtl/Vec.h" -namespace CVC5 { +namespace cvc5 { namespace Minisat { //================================================================================================= @@ -156,6 +156,6 @@ class Heap { //================================================================================================= } -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/prop/minisat/mtl/Map.h b/src/prop/minisat/mtl/Map.h index 2efed4433..1c48f3962 100644 --- a/src/prop/minisat/mtl/Map.h +++ b/src/prop/minisat/mtl/Map.h @@ -24,7 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/minisat/mtl/IntTypes.h" #include "prop/minisat/mtl/Vec.h" -namespace CVC5 { +namespace cvc5 { namespace Minisat { //================================================================================================= @@ -191,6 +191,6 @@ class Map { //================================================================================================= } -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/prop/minisat/mtl/Queue.h b/src/prop/minisat/mtl/Queue.h index ef30591bf..cdbc22600 100644 --- a/src/prop/minisat/mtl/Queue.h +++ b/src/prop/minisat/mtl/Queue.h @@ -24,7 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "base/check.h" #include "prop/minisat/mtl/Vec.h" -namespace CVC5 { +namespace cvc5 { namespace Minisat { //================================================================================================= @@ -86,6 +86,6 @@ public: //================================================================================================= } -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/prop/minisat/mtl/Sort.h b/src/prop/minisat/mtl/Sort.h index 7cf393847..2b9550d48 100644 --- a/src/prop/minisat/mtl/Sort.h +++ b/src/prop/minisat/mtl/Sort.h @@ -26,7 +26,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA //================================================================================================= // Some sorting algorithms for vec's -namespace CVC5 { +namespace cvc5 { namespace Minisat { template @@ -94,6 +94,6 @@ template void sort(vec& v) { //================================================================================================= } -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/prop/minisat/mtl/Vec.h b/src/prop/minisat/mtl/Vec.h index e17e320d2..5410981f9 100644 --- a/src/prop/minisat/mtl/Vec.h +++ b/src/prop/minisat/mtl/Vec.h @@ -27,7 +27,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/minisat/mtl/IntTypes.h" #include "prop/minisat/mtl/XAlloc.h" -namespace CVC5 { +namespace cvc5 { namespace Minisat { //================================================================================================= @@ -147,6 +147,6 @@ void vec::clear(bool dealloc) { //================================================================================================= } -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/prop/minisat/mtl/XAlloc.h b/src/prop/minisat/mtl/XAlloc.h index 6bd8c02e8..300dbb16b 100644 --- a/src/prop/minisat/mtl/XAlloc.h +++ b/src/prop/minisat/mtl/XAlloc.h @@ -24,7 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include #include -namespace CVC5 { +namespace cvc5 { namespace Minisat { //================================================================================================= @@ -42,6 +42,6 @@ static inline void* xrealloc(void *ptr, size_t size) //================================================================================================= } -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc index 52162776b..e29c1032a 100644 --- a/src/prop/minisat/simp/SimpSolver.cc +++ b/src/prop/minisat/simp/SimpSolver.cc @@ -27,8 +27,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/minisat/mtl/Sort.h" #include "prop/minisat/utils/System.h" -using namespace CVC5; -using namespace CVC5::Minisat; +using namespace cvc5; +using namespace cvc5::Minisat; //================================================================================================= // Options: @@ -48,9 +48,9 @@ static DoubleOption opt_simp_garbage_frac(_cat, "simp-gc-frac", "The fraction of //================================================================================================= // Constructor/Destructor: -SimpSolver::SimpSolver(CVC5::prop::TheoryProxy* proxy, - CVC5::context::Context* context, - CVC5::context::UserContext* userContext, +SimpSolver::SimpSolver(cvc5::prop::TheoryProxy* proxy, + cvc5::context::Context* context, + cvc5::context::UserContext* userContext, ProofNodeManager* pnm, bool enableIncremental) : Solver(proxy, context, userContext, pnm, enableIncremental), diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h index 6c8a87d5e..63a5a93fd 100644 --- a/src/prop/minisat/simp/SimpSolver.h +++ b/src/prop/minisat/simp/SimpSolver.h @@ -27,13 +27,13 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/minisat/core/Solver.h" #include "prop/minisat/mtl/Queue.h" -namespace CVC5 { +namespace cvc5 { namespace prop { class TheoryProxy; } -} // namespace CVC5 +} // namespace cvc5 -namespace CVC5 { +namespace cvc5 { namespace Minisat { //================================================================================================= @@ -42,9 +42,9 @@ class SimpSolver : public Solver { public: // Constructor/Destructor: // - SimpSolver(CVC5::prop::TheoryProxy* proxy, - CVC5::context::Context* context, - CVC5::context::UserContext* userContext, + SimpSolver(cvc5::prop::TheoryProxy* proxy, + cvc5::context::Context* context, + cvc5::context::UserContext* userContext, ProofNodeManager* pnm, bool enableIncremental = false); ~SimpSolver(); @@ -271,6 +271,6 @@ inline lbool SimpSolver::solve (Lit p, Lit q, Lit r, bool do_simp, bool t //================================================================================================= } // namespace Minisat - } // namespace CVC5 + } // namespace cvc5 #endif diff --git a/src/prop/minisat/utils/Options.h b/src/prop/minisat/utils/Options.h index f37b6305e..22e4cd6ee 100644 --- a/src/prop/minisat/utils/Options.h +++ b/src/prop/minisat/utils/Options.h @@ -29,7 +29,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/minisat/mtl/Vec.h" #include "prop/minisat/utils/ParseUtils.h" -namespace CVC5 { +namespace cvc5 { namespace Minisat { //================================================================================================== @@ -432,6 +432,6 @@ class BoolOption : public Option //================================================================================================= } -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/prop/minisat/utils/ParseUtils.h b/src/prop/minisat/utils/ParseUtils.h index 27e454d00..ae8783e96 100644 --- a/src/prop/minisat/utils/ParseUtils.h +++ b/src/prop/minisat/utils/ParseUtils.h @@ -27,7 +27,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA //#include #include -namespace CVC5 { +namespace cvc5 { namespace Minisat { //------------------------------------------------------------------------------------------------- @@ -120,6 +120,6 @@ static bool eagerMatch(B& in, const char* str) { //================================================================================================= } -} // namespace CVC5 +} // namespace cvc5 #endif -- cgit v1.2.3