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/prop | |
parent | afaf4413775ff7d6054a5893f1397ad908e0773c (diff) |
Rename namespace CVC5 to cvc5. (#6258)
Diffstat (limited to 'src/prop')
69 files changed, 207 insertions, 207 deletions
diff --git a/src/prop/README.minisat b/src/prop/README.minisat index 081e79191..b3e101a88 100644 --- a/src/prop/README.minisat +++ b/src/prop/README.minisat @@ -4,7 +4,7 @@ This is MiniSAT 2.2.0, downloaded from here: on 11 July 2010. -The code has been modified to put everything in the CVC5::MiniSat +The code has been modified to put everything in the cvc5::MiniSat namespace. The build process has been modified. Other parts have been modified to serve CVC4's purposes. diff --git a/src/prop/bv_sat_solver_notify.h b/src/prop/bv_sat_solver_notify.h index 1645a096a..fe95e7adb 100644 --- a/src/prop/bv_sat_solver_notify.h +++ b/src/prop/bv_sat_solver_notify.h @@ -21,7 +21,7 @@ #include "prop/sat_solver_types.h" #include "util/resource_manager.h" -namespace CVC5 { +namespace cvc5 { namespace prop { class BVSatSolverNotify { @@ -45,6 +45,6 @@ public: };/* class BVSatSolverInterface::Notify */ } -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp index fb764631f..ba1a7fc3b 100644 --- a/src/prop/bvminisat/bvminisat.cpp +++ b/src/prop/bvminisat/bvminisat.cpp @@ -20,7 +20,7 @@ #include "proof/clause_id.h" #include "util/statistics_registry.h" -namespace CVC5 { +namespace cvc5 { namespace prop { BVMinisatSatSolver::BVMinisatSatSolver(StatisticsRegistry* registry, context::Context* mainSatContext, const std::string& name) @@ -298,4 +298,4 @@ void BVMinisatSatSolver::Statistics::init(BVMinisat::SimpSolver* minisat){ } } // namespace prop -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h index 2a099ad21..1bc0eb237 100644 --- a/src/prop/bvminisat/bvminisat.h +++ b/src/prop/bvminisat/bvminisat.h @@ -28,7 +28,7 @@ #include "util/statistics_registry.h" #include "util/stats_timer.h" -namespace CVC5 { +namespace cvc5 { namespace prop { class BVMinisatSatSolver : public BVSatSolverInterface, @@ -148,4 +148,4 @@ public: }; } // namespace prop -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/prop/bvminisat/core/Dimacs.h b/src/prop/bvminisat/core/Dimacs.h index be82fb557..a660391f7 100644 --- a/src/prop/bvminisat/core/Dimacs.h +++ b/src/prop/bvminisat/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/bvminisat/core/SolverTypes.h" #include "prop/bvminisat/utils/ParseUtils.h" -namespace CVC5 { +namespace cvc5 { namespace BVMinisat { //================================================================================================= @@ -86,6 +86,6 @@ static void parse_DIMACS(gzFile input_stream, Solver& S) { //================================================================================================= } // namespace BVMinisat -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc index d7dc3f6d4..d154b5e7f 100644 --- a/src/prop/bvminisat/core/Solver.cc +++ b/src/prop/bvminisat/core/Solver.cc @@ -34,7 +34,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "theory/interrupted.h" #include "util/utility.h" -namespace CVC5 { +namespace cvc5 { namespace BVMinisat { #define OUTPUT_TAG "bvminisat: [a=" << assumptions.size() << ",l=" << decisionLevel() << "] " @@ -82,7 +82,7 @@ CRef Solver::TCRef_Lazy = CRef_Undef - 1; // no real lazy ref here //================================================================================================= // Constructor/Destructor: -Solver::Solver(CVC5::context::Context* context) +Solver::Solver(cvc5::context::Context* context) : // Parameters (user settable): @@ -976,7 +976,7 @@ lbool Solver::search(int nof_conflicts, UIP uip) return l_False; } - if (!CVC5::options::bvEagerExplanations()) + if (!cvc5::options::bvEagerExplanations()) { // check if uip leads to a conflict if (backtrack_level < assumptions.size()) @@ -1028,7 +1028,7 @@ lbool Solver::search(int nof_conflicts, UIP uip) isWithinBudget = withinBudget(ResourceManager::Resource::BvSatConflictsStep); } - catch (const CVC5::theory::Interrupted& e) + catch (const cvc5::theory::Interrupted& e) { // do some clean-up and rethrow cancelUntil(assumptions.size()); @@ -1418,4 +1418,4 @@ bool Solver::withinBudget(ResourceManager::Resource r) const } } // namespace BVMinisat -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h index 6386c33fa..3bd43f889 100644 --- a/src/prop/bvminisat/core/Solver.h +++ b/src/prop/bvminisat/core/Solver.h @@ -33,7 +33,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/bvminisat/utils/Options.h" #include "util/resource_manager.h" -namespace CVC5 { +namespace cvc5 { namespace BVMinisat { class Solver; @@ -80,7 +80,7 @@ private: Notify* d_notify; /** Cvc4 context */ - CVC5::context::Context* c; + cvc5::context::Context* c; /** True constant */ Var varTrue; @@ -92,7 +92,7 @@ public: // Constructor/Destructor: // - Solver(CVC5::context::Context* c); + Solver(cvc5::context::Context* c); virtual ~Solver(); void setNotify(Notify* toNotify); @@ -534,6 +534,6 @@ inline void Solver::toDimacs (const char* file, Lit p, Lit q, Lit r){ ve //================================================================================================= } // namespace BVMinisat -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/prop/bvminisat/core/SolverTypes.h b/src/prop/bvminisat/core/SolverTypes.h index 96022efbf..fd0e86116 100644 --- a/src/prop/bvminisat/core/SolverTypes.h +++ b/src/prop/bvminisat/core/SolverTypes.h @@ -28,15 +28,15 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/bvminisat/mtl/Map.h" #include "prop/bvminisat/mtl/Vec.h" -namespace CVC5 { +namespace cvc5 { namespace BVMinisat { class Solver; } template <class Solver> class TSatProof; -} // namespace CVC5 +} // namespace cvc5 -namespace CVC5 { +namespace cvc5 { namespace BVMinisat { @@ -430,6 +430,6 @@ inline void Clause::strengthen(Lit p) //================================================================================================= } // namespace BVMinisat -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/prop/bvminisat/mtl/Alg.h b/src/prop/bvminisat/mtl/Alg.h index 0b173eb08..ae72ca878 100644 --- a/src/prop/bvminisat/mtl/Alg.h +++ b/src/prop/bvminisat/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/bvminisat/mtl/Vec.h" -namespace CVC5 { +namespace cvc5 { namespace BVMinisat { //================================================================================================= @@ -82,6 +82,6 @@ static inline void append(const vec<T>& from, vec<T>& to){ copy(from, to, true); //================================================================================================= } // namespace BVMinisat -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/prop/bvminisat/mtl/Alloc.h b/src/prop/bvminisat/mtl/Alloc.h index 582db74f1..2697f13b9 100644 --- a/src/prop/bvminisat/mtl/Alloc.h +++ b/src/prop/bvminisat/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/bvminisat/mtl/Vec.h" #include "prop/bvminisat/mtl/XAlloc.h" -namespace CVC5 { +namespace cvc5 { namespace BVMinisat { //================================================================================================= @@ -149,6 +149,6 @@ RegionAllocator<T>::alloc(int size) //================================================================================================= } // namespace BVMinisat -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/prop/bvminisat/mtl/Heap.h b/src/prop/bvminisat/mtl/Heap.h index 7b04a5091..73c1f07d2 100644 --- a/src/prop/bvminisat/mtl/Heap.h +++ b/src/prop/bvminisat/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/bvminisat/mtl/Vec.h" -namespace CVC5 { +namespace cvc5 { namespace BVMinisat { //================================================================================================= @@ -156,6 +156,6 @@ class Heap { //================================================================================================= } // namespace BVMinisat -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/prop/bvminisat/mtl/Map.h b/src/prop/bvminisat/mtl/Map.h index fd64fc751..2d5db2561 100644 --- a/src/prop/bvminisat/mtl/Map.h +++ b/src/prop/bvminisat/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/bvminisat/mtl/IntTypes.h" #include "prop/bvminisat/mtl/Vec.h" -namespace CVC5 { +namespace cvc5 { namespace BVMinisat { //================================================================================================= @@ -191,6 +191,6 @@ class Map { //================================================================================================= } // namespace BVMinisat -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/prop/bvminisat/mtl/Queue.h b/src/prop/bvminisat/mtl/Queue.h index a72660337..8407fd7ee 100644 --- a/src/prop/bvminisat/mtl/Queue.h +++ b/src/prop/bvminisat/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/bvminisat/mtl/Vec.h" -namespace CVC5 { +namespace cvc5 { namespace BVMinisat { //================================================================================================= @@ -86,6 +86,6 @@ public: //================================================================================================= } // namespace BVMinisat -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/prop/bvminisat/mtl/Sort.h b/src/prop/bvminisat/mtl/Sort.h index 1cfa220ab..30b3b5396 100644 --- a/src/prop/bvminisat/mtl/Sort.h +++ b/src/prop/bvminisat/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 BVMinisat { template<class T> @@ -94,6 +94,6 @@ template <class T> void sort(vec<T>& v) { //================================================================================================= } // namespace BVMinisat -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/prop/bvminisat/mtl/Vec.h b/src/prop/bvminisat/mtl/Vec.h index c918fc4a0..047a89991 100644 --- a/src/prop/bvminisat/mtl/Vec.h +++ b/src/prop/bvminisat/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/bvminisat/mtl/IntTypes.h" #include "prop/bvminisat/mtl/XAlloc.h" -namespace CVC5 { +namespace cvc5 { namespace BVMinisat { //================================================================================================= @@ -147,6 +147,6 @@ void vec<T>::clear(bool dealloc) { //================================================================================================= } // namespace BVMinisat -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/prop/bvminisat/mtl/XAlloc.h b/src/prop/bvminisat/mtl/XAlloc.h index 1500114a2..581915d36 100644 --- a/src/prop/bvminisat/mtl/XAlloc.h +++ b/src/prop/bvminisat/mtl/XAlloc.h @@ -24,7 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include <errno.h> #include <stdlib.h> -namespace CVC5 { +namespace cvc5 { namespace BVMinisat { //================================================================================================= @@ -42,6 +42,6 @@ static inline void* xrealloc(void *ptr, size_t size) //================================================================================================= } // namespace BVMinisat -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/prop/bvminisat/simp/SimpSolver.cc b/src/prop/bvminisat/simp/SimpSolver.cc index b4f9bd354..96ab5b526 100644 --- a/src/prop/bvminisat/simp/SimpSolver.cc +++ b/src/prop/bvminisat/simp/SimpSolver.cc @@ -27,7 +27,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/bvminisat/mtl/Sort.h" #include "prop/bvminisat/utils/System.h" -namespace CVC5 { +namespace cvc5 { namespace BVMinisat { //================================================================================================= @@ -48,7 +48,7 @@ static DoubleOption opt_simp_garbage_frac(_cat, "simp-gc-frac", "The fraction of //================================================================================================= // Constructor/Destructor: -SimpSolver::SimpSolver(CVC5::context::Context* context) +SimpSolver::SimpSolver(cvc5::context::Context* context) : Solver(context), grow(opt_grow), clause_lim(opt_clause_lim), @@ -57,9 +57,9 @@ SimpSolver::SimpSolver(CVC5::context::Context* context) use_asymm(opt_use_asymm), use_rcheck(opt_use_rcheck), use_elim(opt_use_elim - && CVC5::options::bitblastMode() - == CVC5::options::BitblastMode::EAGER - && !CVC5::options::produceModels()), + && cvc5::options::bitblastMode() + == cvc5::options::BitblastMode::EAGER + && !cvc5::options::produceModels()), merges(0), asymm_lits(0), eliminated_vars(0), @@ -94,7 +94,7 @@ SimpSolver::SimpSolver(CVC5::context::Context* context) SimpSolver::~SimpSolver() { - // CVC5::StatisticsRegistry::unregisterStat(&total_eliminate_time); + // cvc5::StatisticsRegistry::unregisterStat(&total_eliminate_time); } @@ -644,7 +644,7 @@ void SimpSolver::extendModel() bool SimpSolver::eliminate(bool turn_off_elim) { - // CVC5::TimerStat::CodeTimer codeTimer(total_eliminate_time); + // cvc5::TimerStat::CodeTimer codeTimer(total_eliminate_time); if (!simplify()) return false; @@ -809,4 +809,4 @@ void SimpSolver::garbageCollect() } } // namespace BVMinisat -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/prop/bvminisat/simp/SimpSolver.h b/src/prop/bvminisat/simp/SimpSolver.h index 6afdc6ba7..b103243d3 100644 --- a/src/prop/bvminisat/simp/SimpSolver.h +++ b/src/prop/bvminisat/simp/SimpSolver.h @@ -26,7 +26,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/bvminisat/core/Solver.h" #include "prop/bvminisat/mtl/Queue.h" -namespace CVC5 { +namespace cvc5 { namespace context { class Context; @@ -41,7 +41,7 @@ class SimpSolver : public Solver { public: // Constructor/Destructor: // - SimpSolver(CVC5::context::Context* context); + SimpSolver(cvc5::context::Context* context); ~SimpSolver(); // Problem specification: @@ -115,7 +115,7 @@ class SimpSolver : public Solver { int merges; int asymm_lits; int eliminated_vars; - // CVC5::TimerStat total_eliminate_time; + // cvc5::TimerStat total_eliminate_time; protected: @@ -238,6 +238,6 @@ inline lbool SimpSolver::solveLimited (bool do_simp, bool turn_off_simp){ //================================================================================================= } // namespace BVMinisat -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/prop/bvminisat/utils/Options.cc b/src/prop/bvminisat/utils/Options.cc index 44c642441..0b05d5cf6 100644 --- a/src/prop/bvminisat/utils/Options.cc +++ b/src/prop/bvminisat/utils/Options.cc @@ -21,7 +21,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/bvminisat/mtl/Sort.h" #include "prop/bvminisat/utils/ParseUtils.h" -namespace CVC5 { +namespace cvc5 { namespace BVMinisat { void BVMinisat::parseOptions(int& argc, char** argv, bool strict) @@ -91,4 +91,4 @@ void BVMinisat::printUsageAndExit (int argc, char** argv, bool verbose) } } // namespace BVMinisat -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/prop/bvminisat/utils/Options.h b/src/prop/bvminisat/utils/Options.h index e7b6942bd..033ffb64f 100644 --- a/src/prop/bvminisat/utils/Options.h +++ b/src/prop/bvminisat/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/bvminisat/mtl/Vec.h" #include "prop/bvminisat/utils/ParseUtils.h" -namespace CVC5 { +namespace cvc5 { namespace BVMinisat { //================================================================================================== @@ -432,6 +432,6 @@ class BoolOption : public Option //================================================================================================= } // namespace BVMinisat -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/prop/bvminisat/utils/ParseUtils.h b/src/prop/bvminisat/utils/ParseUtils.h index a748651db..d69856ebb 100644 --- a/src/prop/bvminisat/utils/ParseUtils.h +++ b/src/prop/bvminisat/utils/ParseUtils.h @@ -27,7 +27,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA //#include <zlib.h> #include <unistd.h> -namespace CVC5 { +namespace cvc5 { namespace BVMinisat { //------------------------------------------------------------------------------------------------- @@ -120,6 +120,6 @@ static bool eagerMatch(B& in, const char* str) { //================================================================================================= } // namespace BVMinisat -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/prop/bvminisat/utils/System.cc b/src/prop/bvminisat/utils/System.cc index 9b9f99eb5..606fc5cbe 100644 --- a/src/prop/bvminisat/utils/System.cc +++ b/src/prop/bvminisat/utils/System.cc @@ -25,7 +25,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include <stdio.h> #include <stdlib.h> -namespace CVC5 { +namespace cvc5 { namespace BVMinisat { // TODO: split the memory reading functions into two: one for reading high-watermark of RSS, and @@ -95,5 +95,5 @@ double BVMinisat::memUsed() { return 0; } #endif -} /* CVC5::BVMinisat namespace */ +} /* cvc5::BVMinisat namespace */ } /* CVC4 namespace */ diff --git a/src/prop/bvminisat/utils/System.h b/src/prop/bvminisat/utils/System.h index 117fbfa3d..c805c232a 100644 --- a/src/prop/bvminisat/utils/System.h +++ b/src/prop/bvminisat/utils/System.h @@ -29,7 +29,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA //------------------------------------------------------------------------------------------------- -namespace CVC5 { +namespace cvc5 { namespace BVMinisat { static inline double cpuTime(void); // CPU-time in seconds. @@ -37,7 +37,7 @@ extern double memUsed(); // Memory in mega bytes (returns 0 for unsup extern double memUsedPeak(); // Peak-memory in mega bytes (returns 0 for unsupported architectures). } // namespace BVMinisat -} // namespace CVC5 +} // namespace cvc5 //------------------------------------------------------------------------------------------------- // Implementation of inline functions: @@ -45,7 +45,7 @@ extern double memUsedPeak(); // Peak-memory in mega bytes (returns 0 for #if defined(_MSC_VER) || defined(__MINGW32__) #include <time.h> -static inline double CVC5::BVMinisat::cpuTime(void) +static inline double cvc5::BVMinisat::cpuTime(void) { return (double)clock() / CLOCKS_PER_SEC; } @@ -55,7 +55,7 @@ static inline double CVC5::BVMinisat::cpuTime(void) #include <sys/resource.h> #include <unistd.h> -static inline double CVC5::BVMinisat::cpuTime(void) +static inline double cvc5::BVMinisat::cpuTime(void) { struct rusage ru; getrusage(RUSAGE_SELF, &ru); diff --git a/src/prop/cadical.cpp b/src/prop/cadical.cpp index 9bad7072a..cac015904 100644 --- a/src/prop/cadical.cpp +++ b/src/prop/cadical.cpp @@ -20,7 +20,7 @@ #include "base/check.h" -namespace CVC5 { +namespace cvc5 { namespace prop { using CadicalLit = int; @@ -200,6 +200,6 @@ CadicalSolver::Statistics::~Statistics() { } } // namespace prop -} // namespace CVC5 +} // namespace cvc5 #endif // CVC4_USE_CADICAL diff --git a/src/prop/cadical.h b/src/prop/cadical.h index c49aa8d03..910e5def5 100644 --- a/src/prop/cadical.h +++ b/src/prop/cadical.h @@ -26,7 +26,7 @@ #include <cadical.hpp> -namespace CVC5 { +namespace cvc5 { namespace prop { class CadicalSolver : public SatSolver @@ -103,7 +103,7 @@ class CadicalSolver : public SatSolver }; } // namespace prop -} // namespace CVC5 +} // namespace cvc5 #endif // CVC4_USE_CADICAL #endif // CVC4__PROP__CADICAL_H diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index bd23bad94..1caea7bb7 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -37,7 +37,7 @@ #include "theory/theory.h" #include "theory/theory_engine.h" -namespace CVC5 { +namespace cvc5 { namespace prop { CnfStream::CnfStream(SatSolver* satSolver, @@ -788,4 +788,4 @@ void CnfStream::convertAndAssert(TNode node, bool negated) } } // namespace prop -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index af86da746..b39423d71 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -34,7 +34,7 @@ #include "prop/registrar.h" #include "prop/sat_solver_types.h" -namespace CVC5 { +namespace cvc5 { class OutputManager; @@ -318,6 +318,6 @@ class CnfStream { }; /* class CnfStream */ } // namespace prop -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PROP__CNF_STREAM_H */ diff --git a/src/prop/cryptominisat.cpp b/src/prop/cryptominisat.cpp index 91fc12c6c..ce5e4e2b0 100644 --- a/src/prop/cryptominisat.cpp +++ b/src/prop/cryptominisat.cpp @@ -22,7 +22,7 @@ #include <cryptominisat5/cryptominisat.h> -namespace CVC5 { +namespace cvc5 { namespace prop { using CMSatVar = unsigned; @@ -244,5 +244,5 @@ CryptoMinisatSolver::Statistics::~Statistics() { } } // namespace prop -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/prop/cryptominisat.h b/src/prop/cryptominisat.h index fb118619c..65e1196f3 100644 --- a/src/prop/cryptominisat.h +++ b/src/prop/cryptominisat.h @@ -33,7 +33,7 @@ namespace CMSat { class SATSolver; } -namespace CVC5 { +namespace cvc5 { namespace prop { class CryptoMinisatSolver : public SatSolver @@ -106,7 +106,7 @@ class CryptoMinisatSolver : public SatSolver }; } // namespace prop -} // namespace CVC5 +} // namespace cvc5 #endif // CVC4_USE_CRYPTOMINISAT #endif // CVC4__PROP__CRYPTOMINISAT_H diff --git a/src/prop/kissat.cpp b/src/prop/kissat.cpp index ccca3a3b4..10b7b07de 100644 --- a/src/prop/kissat.cpp +++ b/src/prop/kissat.cpp @@ -20,7 +20,7 @@ #include "base/check.h" -namespace CVC5 { +namespace cvc5 { namespace prop { using KissatLit = int32_t; @@ -173,6 +173,6 @@ KissatSolver::Statistics::~Statistics() } } // namespace prop -} // namespace CVC5 +} // namespace cvc5 #endif // CVC4_USE_KISSAT diff --git a/src/prop/kissat.h b/src/prop/kissat.h index 7bfcbac68..6984a7e50 100644 --- a/src/prop/kissat.h +++ b/src/prop/kissat.h @@ -28,7 +28,7 @@ extern "C" { #include <kissat/kissat.h> } -namespace CVC5 { +namespace cvc5 { namespace prop { class KissatSolver : public SatSolver @@ -97,7 +97,7 @@ class KissatSolver : public SatSolver }; } // namespace prop -} // namespace CVC5 +} // namespace cvc5 #endif // CVC4_USE_KISSAT #endif // CVC4__PROP__KISSAT_H 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<Lit>& 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<Lit>& 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<Lit>& 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<Lit>& 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<Solver>* proof) + cvc5::TSatProof<Solver>* proof) { Debug("minisat") << "ClauseAllocator::reloc: cr " << cr << std::endl; // FIXME what is this CRef_lazy @@ -2398,4 +2398,4 @@ std::shared_ptr<ProofNode> 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 Solver> 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<Minisat::Solver>; + friend class cvc5::prop::PropEngine; + friend class cvc5::prop::TheoryProxy; + friend class cvc5::prop::SatProofManager; + friend class cvc5::TSatProof<Minisat::Solver>; 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<CVC5::prop::SatProofManager> d_pfManager; + std::unique_ptr<cvc5::prop::SatProofManager> d_pfManager; public: /** Returns the current user assertion level */ @@ -105,7 +105,7 @@ class Solver { vec<bool> lemmas_removable; /** Nodes being converted to CNF */ - std::vector<CVC5::Node> lemmas_cnf_assertion; + std::vector<cvc5::Node> 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<ProofNode> 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 Solver> 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<uint32_t> void reloc(CRef& cr, ClauseAllocator& to, - CVC5::TSatProof<Solver>* proof = NULL); + cvc5::TSatProof<Solver>* 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<CVC5::Minisat::Solver>(Minisat::Solver::TLit lit) +prop::SatLiteral toSatLiteral<cvc5::Minisat::Solver>(Minisat::Solver::TLit lit) { return prop::MinisatSatSolver::toSatLiteral(lit); } template <> -void toSatClause<CVC5::Minisat::Solver>( - const CVC5::Minisat::Solver::TClause& minisat_cl, prop::SatClause& sat_cl) +void toSatClause<cvc5::Minisat::Solver>( + 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<T>& from, vec<T>& 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<T>::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<class T> @@ -94,6 +94,6 @@ template <class T> void sort(vec<T>& 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<T>::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 <errno.h> #include <stdlib.h> -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 <zlib.h> #include <unistd.h> -namespace CVC5 { +namespace cvc5 { namespace Minisat { //------------------------------------------------------------------------------------------------- @@ -120,6 +120,6 @@ static bool eagerMatch(B& in, const char* str) { //================================================================================================= } -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/prop/proof_cnf_stream.cpp b/src/prop/proof_cnf_stream.cpp index ab5c59dd1..76421db9b 100644 --- a/src/prop/proof_cnf_stream.cpp +++ b/src/prop/proof_cnf_stream.cpp @@ -18,7 +18,7 @@ #include "prop/minisat/minisat.h" #include "theory/builtin/proof_checker.h" -namespace CVC5 { +namespace cvc5 { namespace prop { ProofCnfStream::ProofCnfStream(context::UserContext* u, @@ -1012,4 +1012,4 @@ SatLiteral ProofCnfStream::handleIte(TNode node) } } // namespace prop -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/prop/proof_cnf_stream.h b/src/prop/proof_cnf_stream.h index 7c97a2e8e..fcca2cb34 100644 --- a/src/prop/proof_cnf_stream.h +++ b/src/prop/proof_cnf_stream.h @@ -27,7 +27,7 @@ #include "theory/eager_proof_generator.h" #include "theory/theory_proof_step_buffer.h" -namespace CVC5 { +namespace cvc5 { namespace prop { class SatProofManager; @@ -170,6 +170,6 @@ class ProofCnfStream : public ProofGenerator }; } // namespace prop -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/prop/proof_post_processor.cpp b/src/prop/proof_post_processor.cpp index 7f075ab37..6b31e6053 100644 --- a/src/prop/proof_post_processor.cpp +++ b/src/prop/proof_post_processor.cpp @@ -17,7 +17,7 @@ #include "theory/builtin/proof_checker.h" -namespace CVC5 { +namespace cvc5 { namespace prop { ProofPostprocessCallback::ProofPostprocessCallback( @@ -105,4 +105,4 @@ void ProofPostproccess::process(std::shared_ptr<ProofNode> pf) } } // namespace prop -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/prop/proof_post_processor.h b/src/prop/proof_post_processor.h index c74cb540f..363970117 100644 --- a/src/prop/proof_post_processor.h +++ b/src/prop/proof_post_processor.h @@ -23,7 +23,7 @@ #include "expr/proof_node_updater.h" #include "prop/proof_cnf_stream.h" -namespace CVC5 { +namespace cvc5 { namespace prop { @@ -107,6 +107,6 @@ class ProofPostproccess }; } // namespace prop -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 9032dbb75..efe599106 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -42,7 +42,7 @@ #include "util/resource_manager.h" #include "util/result.h" -namespace CVC5 { +namespace cvc5 { namespace prop { /** Keeps a boolean flag scoped */ @@ -616,4 +616,4 @@ std::shared_ptr<ProofNode> PropEngine::getProof() bool PropEngine::isProofEnabled() const { return d_pfCnfStream != nullptr; } } // namespace prop -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 1145961a1..a01668913 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -27,7 +27,7 @@ #include "theory/trust_node.h" #include "util/result.h" -namespace CVC5 { +namespace cvc5 { class ResourceManager; class DecisionEngine; @@ -381,6 +381,6 @@ class PropEngine }; } // namespace prop -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PROP_ENGINE_H */ diff --git a/src/prop/prop_proof_manager.cpp b/src/prop/prop_proof_manager.cpp index cb380f92d..08c13fe5f 100644 --- a/src/prop/prop_proof_manager.cpp +++ b/src/prop/prop_proof_manager.cpp @@ -19,7 +19,7 @@ #include "prop/prop_proof_manager.h" #include "prop/sat_solver.h" -namespace CVC5 { +namespace cvc5 { namespace prop { PropPfManager::PropPfManager(context::UserContext* userContext, @@ -109,4 +109,4 @@ std::shared_ptr<ProofNode> PropPfManager::getProof() } } // namespace prop -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/prop/prop_proof_manager.h b/src/prop/prop_proof_manager.h index d8732c11a..9a080edc1 100644 --- a/src/prop/prop_proof_manager.h +++ b/src/prop/prop_proof_manager.h @@ -23,7 +23,7 @@ #include "prop/proof_post_processor.h" #include "prop/sat_proof_manager.h" -namespace CVC5 { +namespace cvc5 { namespace prop { @@ -92,6 +92,6 @@ class PropPfManager }; /* class PropPfManager */ } // namespace prop -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PROP__PROOF_MANAGER_H */ diff --git a/src/prop/registrar.h b/src/prop/registrar.h index d0fc0fe25..ae085b573 100644 --- a/src/prop/registrar.h +++ b/src/prop/registrar.h @@ -23,7 +23,7 @@ #ifndef CVC4__PROP__REGISTRAR_H #define CVC4__PROP__REGISTRAR_H -namespace CVC5 { +namespace cvc5 { namespace prop { class Registrar { @@ -40,6 +40,6 @@ public: };/* class NullRegistrar */ } // namespace prop -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PROP__REGISTRAR_H */ diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp index a11eeaa8a..da9354c2f 100644 --- a/src/prop/sat_proof_manager.cpp +++ b/src/prop/sat_proof_manager.cpp @@ -20,7 +20,7 @@ #include "prop/minisat/minisat.h" #include "theory/theory_proof_step_buffer.h" -namespace CVC5 { +namespace cvc5 { namespace prop { SatProofManager::SatProofManager(Minisat::Solver* solver, @@ -753,4 +753,4 @@ void SatProofManager::registerSatAssumptions(const std::vector<Node>& assumps) } } // namespace prop -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/prop/sat_proof_manager.h b/src/prop/sat_proof_manager.h index 514f0153b..4d45ce3b7 100644 --- a/src/prop/sat_proof_manager.h +++ b/src/prop/sat_proof_manager.h @@ -28,7 +28,7 @@ namespace Minisat { class Solver; } -namespace CVC5 { +namespace cvc5 { class ProofNodeManager; @@ -587,6 +587,6 @@ class SatProofManager }; /* class SatProofManager */ } // namespace prop -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__SAT_PROOF_MANAGER_H */ diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index f06171775..1f59a7bd6 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -30,7 +30,7 @@ #include "prop/sat_solver_types.h" #include "util/statistics_registry.h" -namespace CVC5 { +namespace cvc5 { namespace prop { @@ -150,7 +150,7 @@ class CDCLTSatSolverInterface : public SatSolver virtual void initialize(context::Context* context, prop::TheoryProxy* theoryProxy, - CVC5::context::UserContext* userContext, + cvc5::context::UserContext* userContext, ProofNodeManager* pnm) = 0; virtual void push() = 0; @@ -209,6 +209,6 @@ inline std::ostream& operator <<(std::ostream& out, prop::SatValue val) { } } // namespace prop -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PROP__SAT_MODULE_H */ diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp index 1d933dce8..117210431 100644 --- a/src/prop/sat_solver_factory.cpp +++ b/src/prop/sat_solver_factory.cpp @@ -22,7 +22,7 @@ #include "prop/kissat.h" #include "prop/minisat/minisat.h" -namespace CVC5 { +namespace cvc5 { namespace prop { BVSatSolverInterface* SatSolverFactory::createMinisat( @@ -76,4 +76,4 @@ SatSolver* SatSolverFactory::createKissat(StatisticsRegistry* registry, } } // namespace prop -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/prop/sat_solver_factory.h b/src/prop/sat_solver_factory.h index 97b018e09..71e28ac39 100644 --- a/src/prop/sat_solver_factory.h +++ b/src/prop/sat_solver_factory.h @@ -27,7 +27,7 @@ #include "prop/sat_solver.h" #include "util/statistics_registry.h" -namespace CVC5 { +namespace cvc5 { namespace prop { class SatSolverFactory @@ -50,6 +50,6 @@ class SatSolverFactory }; /* class SatSolverFactory */ } // namespace prop -} // namespace CVC5 +} // namespace cvc5 #endif // CVC4__PROP__SAT_SOLVER_FACTORY_H diff --git a/src/prop/sat_solver_types.cpp b/src/prop/sat_solver_types.cpp index 3380329c3..13494221e 100644 --- a/src/prop/sat_solver_types.cpp +++ b/src/prop/sat_solver_types.cpp @@ -18,11 +18,11 @@ #include <algorithm> -namespace CVC5 { +namespace cvc5 { namespace prop { bool SatClauseLessThan::operator()(const SatClause& l, const SatClause& r) const { return std::lexicographical_compare(l.begin(), l.end(), r.begin(), r.end()); } } // namespace prop -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/prop/sat_solver_types.h b/src/prop/sat_solver_types.h index 392dfb2b1..0ab0cba53 100644 --- a/src/prop/sat_solver_types.h +++ b/src/prop/sat_solver_types.h @@ -29,7 +29,7 @@ #include <unordered_set> #include <vector> -namespace CVC5 { +namespace cvc5 { namespace prop { /** @@ -235,4 +235,4 @@ enum SatSolverLifespan }; } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/prop/skolem_def_manager.cpp b/src/prop/skolem_def_manager.cpp index a0819e571..dbc640d8c 100644 --- a/src/prop/skolem_def_manager.cpp +++ b/src/prop/skolem_def_manager.cpp @@ -16,7 +16,7 @@ #include "expr/attribute.h" -namespace CVC5 { +namespace cvc5 { namespace prop { SkolemDefManager::SkolemDefManager(context::Context* context, @@ -170,4 +170,4 @@ void SkolemDefManager::getSkolems( } } // namespace prop -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/prop/skolem_def_manager.h b/src/prop/skolem_def_manager.h index 6f4ec031f..11b726c2a 100644 --- a/src/prop/skolem_def_manager.h +++ b/src/prop/skolem_def_manager.h @@ -26,7 +26,7 @@ #include "context/context.h" #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace prop { /** @@ -86,6 +86,6 @@ class SkolemDefManager }; } // namespace prop -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PROP__SKOLEM_DEF_MANAGER_H */ diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index ffec0c365..4a95591b4 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -28,7 +28,7 @@ #include "theory/theory_engine.h" #include "util/statistics_registry.h" -namespace CVC5 { +namespace cvc5 { namespace prop { TheoryProxy::TheoryProxy(PropEngine* propEngine, @@ -105,7 +105,7 @@ void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) { theory::TrustNode tte = d_theoryEngine->getExplanation(lNode); Node theoryExplanation = tte.getNode(); - if (CVC5::options::produceProofs()) + if (cvc5::options::produceProofs()) { d_propEngine->getProofCnfStream()->convertPropagation(tte); } @@ -233,4 +233,4 @@ void TheoryProxy::getSkolems(TNode node, void TheoryProxy::preRegister(Node n) { d_theoryEngine->preRegister(n); } } // namespace prop -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index dedd1fa49..3b21bde58 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -35,7 +35,7 @@ #include "theory/trust_node.h" #include "util/resource_manager.h" -namespace CVC5 { +namespace cvc5 { class DecisionEngine; class TheoryEngine; @@ -167,6 +167,6 @@ class TheoryProxy : public Registrar } // namespace prop -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PROP__SAT_H */ |