diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-03-31 15:23:17 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-03-31 22:23:17 +0000 |
commit | a1466978fbc328507406d4a121dab4d1a1047e1d (patch) | |
tree | 12b40f161bb4d7a6ee40c20c78a15d6cda3c1995 /src/smt | |
parent | f9a9af855fb65804ff0b36e764ccd9d0fa9f87f8 (diff) |
Rename namespace CVC4 to CVC5. (#6249)
Diffstat (limited to 'src/smt')
77 files changed, 204 insertions, 204 deletions
diff --git a/src/smt/abduction_solver.cpp b/src/smt/abduction_solver.cpp index 46410755a..cd4228eed 100644 --- a/src/smt/abduction_solver.cpp +++ b/src/smt/abduction_solver.cpp @@ -23,9 +23,9 @@ #include "theory/quantifiers/sygus/sygus_grammar_cons.h" #include "theory/smt_engine_subsolver.h" -using namespace CVC4::theory; +using namespace CVC5::theory; -namespace CVC4 { +namespace CVC5 { namespace smt { AbductionSolver::AbductionSolver(SmtEngine* parent) : d_parent(parent) {} @@ -195,4 +195,4 @@ void AbductionSolver::checkAbduct(Node a) } } // namespace smt -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/smt/abduction_solver.h b/src/smt/abduction_solver.h index dcae290b4..c7328a9a8 100644 --- a/src/smt/abduction_solver.h +++ b/src/smt/abduction_solver.h @@ -20,7 +20,7 @@ #include "expr/node.h" #include "expr/type_node.h" -namespace CVC4 { +namespace CVC5 { class SmtEngine; @@ -115,6 +115,6 @@ class AbductionSolver }; } // namespace smt -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__SMT__ABDUCTION_SOLVER_H */ diff --git a/src/smt/abstract_values.cpp b/src/smt/abstract_values.cpp index 90a61f8bb..e4c7f2668 100644 --- a/src/smt/abstract_values.cpp +++ b/src/smt/abstract_values.cpp @@ -16,7 +16,7 @@ #include "options/smt_options.h" -namespace CVC4 { +namespace CVC5 { namespace smt { AbstractValues::AbstractValues(NodeManager* nm) @@ -52,4 +52,4 @@ Node AbstractValues::mkAbstractValue(TNode n) } } // namespace smt -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/smt/abstract_values.h b/src/smt/abstract_values.h index 27d522203..be4a0c7a3 100644 --- a/src/smt/abstract_values.h +++ b/src/smt/abstract_values.h @@ -23,7 +23,7 @@ #include "expr/node.h" #include "theory/substitutions.h" -namespace CVC4 { +namespace CVC5 { namespace smt { /** @@ -75,6 +75,6 @@ class AbstractValues }; } // namespace smt -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp index 38a424731..f82d0769b 100644 --- a/src/smt/assertions.cpp +++ b/src/smt/assertions.cpp @@ -24,10 +24,10 @@ #include "smt/abstract_values.h" #include "smt/smt_engine.h" -using namespace CVC4::theory; -using namespace CVC4::kind; +using namespace CVC5::theory; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace smt { Assertions::Assertions(context::UserContext* u, AbstractValues& absv) @@ -243,4 +243,4 @@ bool Assertions::isProofEnabled() const } } // namespace smt -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/smt/assertions.h b/src/smt/assertions.h index 15f1d140e..135fe8974 100644 --- a/src/smt/assertions.h +++ b/src/smt/assertions.h @@ -23,7 +23,7 @@ #include "expr/node.h" #include "preprocessing/assertion_pipeline.h" -namespace CVC4 { +namespace CVC5 { namespace smt { class AbstractValues; @@ -172,6 +172,6 @@ class Assertions }; } // namespace smt -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/smt/check_models.cpp b/src/smt/check_models.cpp index 07493d0b9..0c21002af 100644 --- a/src/smt/check_models.cpp +++ b/src/smt/check_models.cpp @@ -23,9 +23,9 @@ #include "theory/substitutions.h" #include "theory/theory_engine.h" -using namespace CVC4::theory; +using namespace CVC5::theory; -namespace CVC4 { +namespace CVC5 { namespace smt { CheckModels::CheckModels(SmtSolver& s) : d_smt(s) {} @@ -148,4 +148,4 @@ void CheckModels::checkModel(Model* m, } } // namespace smt -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/smt/check_models.h b/src/smt/check_models.h index 4843eea8d..d12a33ee5 100644 --- a/src/smt/check_models.h +++ b/src/smt/check_models.h @@ -20,7 +20,7 @@ #include "context/cdlist.h" #include "expr/node.h" -namespace CVC4 { +namespace CVC5 { namespace smt { class Model; @@ -48,6 +48,6 @@ class CheckModels }; } // namespace smt -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 5d27c2eb8..f29b67d6d 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -43,7 +43,7 @@ using namespace std; -namespace CVC4 { +namespace CVC5 { std::string sexprToString(api::Term sexpr) { @@ -2811,4 +2811,4 @@ void DatatypeDeclarationCommand::toStream(std::ostream& out, out, api::Sort::sortVectorToTypeNodes(d_datatypes)); } -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/smt/command.h b/src/smt/command.h index 1017a74c9..6d169ce5e 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -31,7 +31,7 @@ #include "cvc4_export.h" #include "options/language.h" -namespace CVC4 { +namespace CVC5 { namespace api { class Solver; @@ -1509,6 +1509,6 @@ class CVC4_EXPORT DeclarationSequence : public CommandSequence OutputLanguage language = language::output::LANG_AUTO) const override; }; -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__COMMAND_H */ diff --git a/src/smt/defined_function.h b/src/smt/defined_function.h index a5c9f8d96..7f3007975 100644 --- a/src/smt/defined_function.h +++ b/src/smt/defined_function.h @@ -21,7 +21,7 @@ #include "expr/node.h" -namespace CVC4 { +namespace CVC5 { namespace smt { /** @@ -55,6 +55,6 @@ class DefinedFunction }; /* class DefinedFunction */ } // namespace smt -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__SMT__DEFINED_FUNCTION_H */ diff --git a/src/smt/dump.cpp b/src/smt/dump.cpp index bb0bff1d7..76973ec32 100644 --- a/src/smt/dump.cpp +++ b/src/smt/dump.cpp @@ -23,7 +23,7 @@ #include "smt/command.h" #include "smt/node_command.h" -namespace CVC4 { +namespace CVC5 { #if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) @@ -58,12 +58,14 @@ CVC4dumpstream& CVC4dumpstream::operator<<(const NodeCommand& nc) DumpC DumpChannel; std::ostream& DumpC::setStream(std::ostream* os) { - ::CVC4::DumpOutChannel.setStream(os); + ::CVC5::DumpOutChannel.setStream(os); return *os; } -std::ostream& DumpC::getStream() { return ::CVC4::DumpOutChannel.getStream(); } -std::ostream* DumpC::getStreamPointer() { return ::CVC4::DumpOutChannel.getStreamPointer(); } - +std::ostream& DumpC::getStream() { return ::CVC5::DumpOutChannel.getStream(); } +std::ostream* DumpC::getStreamPointer() +{ + return ::CVC5::DumpOutChannel.getStreamPointer(); +} void DumpC::setDumpFromString(const std::string& optarg) { if (Configuration::isDumpingBuild()) @@ -241,4 +243,4 @@ pipe to perform on-line checking. The --dump-to option can be used to dump\n\ to a file.\n\ "; -}/* CVC4 namespace */ +} // namespace CVC5 diff --git a/src/smt/dump.h b/src/smt/dump.h index d8c2e5b4e..be146470a 100644 --- a/src/smt/dump.h +++ b/src/smt/dump.h @@ -21,7 +21,7 @@ #include "base/output.h" -namespace CVC4 { +namespace CVC5 { class Command; class NodeCommand; @@ -110,8 +110,8 @@ class DumpC /** The dump singleton */ extern DumpC DumpChannel; -#define Dump ::CVC4::DumpChannel +#define Dump ::CVC5::DumpChannel -}/* CVC4 namespace */ +} // namespace CVC5 #endif /* CVC4__DUMP_H */ diff --git a/src/smt/dump_manager.cpp b/src/smt/dump_manager.cpp index 81993f3d5..6b81d5594 100644 --- a/src/smt/dump_manager.cpp +++ b/src/smt/dump_manager.cpp @@ -18,7 +18,7 @@ #include "smt/dump.h" #include "smt/node_command.h" -namespace CVC4 { +namespace CVC5 { namespace smt { DumpManager::DumpManager(context::UserContext* u) @@ -72,4 +72,4 @@ void DumpManager::setPrintFuncInModel(Node f, bool p) } } // namespace smt -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/smt/dump_manager.h b/src/smt/dump_manager.h index 1a8a6e3d0..519b93110 100644 --- a/src/smt/dump_manager.h +++ b/src/smt/dump_manager.h @@ -22,7 +22,7 @@ #include "expr/node.h" -namespace CVC4 { +namespace CVC5 { class NodeCommand; @@ -75,6 +75,6 @@ class DumpManager }; } // namespace smt -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/smt/env.cpp b/src/smt/env.cpp index 55afcadf7..6440c29d3 100644 --- a/src/smt/env.cpp +++ b/src/smt/env.cpp @@ -25,9 +25,9 @@ #include "theory/rewriter.h" #include "util/resource_manager.h" -using namespace CVC4::smt; +using namespace CVC5::smt; -namespace CVC4 { +namespace CVC5 { Env::Env(NodeManager* nm) : d_context(new context::Context()), @@ -101,4 +101,4 @@ const Printer& Env::getPrinter() std::ostream& Env::getDumpOut() { return *d_options.getOut(); } -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/smt/env.h b/src/smt/env.h index 18f0de0b5..3ceefdd34 100644 --- a/src/smt/env.h +++ b/src/smt/env.h @@ -25,7 +25,7 @@ #include "util/statistics.h" #include "util/statistics_registry.h" -namespace CVC4 { +namespace CVC5 { class NodeManager; class StatisticsRegistry; @@ -182,6 +182,6 @@ class Env std::unique_ptr<ResourceManager> d_resourceManager; }; /* class Env */ -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__SMT__ENV_H */ diff --git a/src/smt/expand_definitions.cpp b/src/smt/expand_definitions.cpp index 62779dbba..599f57747 100644 --- a/src/smt/expand_definitions.cpp +++ b/src/smt/expand_definitions.cpp @@ -24,11 +24,11 @@ #include "smt/smt_engine_stats.h" #include "theory/theory_engine.h" -using namespace CVC4::preprocessing; -using namespace CVC4::theory; -using namespace CVC4::kind; +using namespace CVC5::preprocessing; +using namespace CVC5::theory; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace smt { ExpandDefs::ExpandDefs(SmtEngine& smt, @@ -367,4 +367,4 @@ void ExpandDefs::setProofNodeManager(ProofNodeManager* pnm) } } // namespace smt -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/smt/expand_definitions.h b/src/smt/expand_definitions.h index 5f21e8f0c..035e7989d 100644 --- a/src/smt/expand_definitions.h +++ b/src/smt/expand_definitions.h @@ -22,7 +22,7 @@ #include "expr/node.h" #include "theory/trust_node.h" -namespace CVC4 { +namespace CVC5 { class ProofNodeManager; class ResourceManager; @@ -95,6 +95,6 @@ class ExpandDefs }; } // namespace smt -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/smt/interpolation_solver.cpp b/src/smt/interpolation_solver.cpp index 616014992..d14b87901 100644 --- a/src/smt/interpolation_solver.cpp +++ b/src/smt/interpolation_solver.cpp @@ -23,9 +23,9 @@ #include "theory/quantifiers/sygus/sygus_interpol.h" #include "theory/smt_engine_subsolver.h" -using namespace CVC4::theory; +using namespace CVC5::theory; -namespace CVC4 { +namespace CVC5 { namespace smt { InterpolationSolver::InterpolationSolver(SmtEngine* parent) : d_parent(parent) @@ -136,4 +136,4 @@ void InterpolationSolver::checkInterpol(Node interpol, } } // namespace smt -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/smt/interpolation_solver.h b/src/smt/interpolation_solver.h index e4c8faecd..1c9b65d85 100644 --- a/src/smt/interpolation_solver.h +++ b/src/smt/interpolation_solver.h @@ -20,7 +20,7 @@ #include "expr/node.h" #include "expr/type_node.h" -namespace CVC4 { +namespace CVC5 { class SmtEngine; @@ -81,6 +81,6 @@ class InterpolationSolver }; } // namespace smt -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__SMT__INTERPOLATION_SOLVER_H */ diff --git a/src/smt/listeners.cpp b/src/smt/listeners.cpp index 7f85e2f98..c686e4115 100644 --- a/src/smt/listeners.cpp +++ b/src/smt/listeners.cpp @@ -25,7 +25,7 @@ #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" -namespace CVC4 { +namespace CVC5 { namespace smt { ResourceOutListener::ResourceOutListener(SmtEngine& smt) : d_smt(smt) {} @@ -103,4 +103,4 @@ void SmtNodeManagerListener::nmNotifyNewSkolem(TNode n, } } // namespace smt -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/smt/listeners.h b/src/smt/listeners.h index d3dc04ebc..1705b9126 100644 --- a/src/smt/listeners.h +++ b/src/smt/listeners.h @@ -22,7 +22,7 @@ #include "base/listener.h" #include "expr/node.h" -namespace CVC4 { +namespace CVC5 { class OutputManager; class SmtEngine; @@ -75,6 +75,6 @@ class SmtNodeManagerListener : public NodeManagerListener }; } // namespace smt -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/smt/logic_exception.h b/src/smt/logic_exception.h index bb1d274ae..91f2d3723 100644 --- a/src/smt/logic_exception.h +++ b/src/smt/logic_exception.h @@ -24,9 +24,9 @@ #include "base/exception.h" -namespace CVC4 { +namespace CVC5 { -class LogicException : public CVC4::Exception +class LogicException : public CVC5::Exception { public: LogicException() : @@ -43,6 +43,6 @@ class LogicException : public CVC4::Exception } }; /* class LogicException */ -}/* CVC4 namespace */ +} // namespace CVC5 #endif /* CVC4__SMT__LOGIC_EXCEPTION_H */ diff --git a/src/smt/managed_ostreams.cpp b/src/smt/managed_ostreams.cpp index dcf90228c..6baabe0e5 100644 --- a/src/smt/managed_ostreams.cpp +++ b/src/smt/managed_ostreams.cpp @@ -24,7 +24,7 @@ #include "options/smt_options.h" #include "smt/update_ostream.h" -namespace CVC4 { +namespace CVC5 { ManagedOstream::ManagedOstream() : d_managed(NULL) {} @@ -164,4 +164,4 @@ void ManagedDiagnosticOutputChannel::addSpecialCases(OstreamOpener* opener) opener->addSpecialCase("stderr", &std::cerr); } -}/* CVC4 namespace */ +} // namespace CVC5 diff --git a/src/smt/managed_ostreams.h b/src/smt/managed_ostreams.h index 55ca15dcb..ba56bcfa3 100644 --- a/src/smt/managed_ostreams.h +++ b/src/smt/managed_ostreams.h @@ -22,7 +22,7 @@ #include <ostream> -namespace CVC4 { +namespace CVC5 { class OstreamOpener; @@ -141,6 +141,6 @@ class ManagedDiagnosticOutputChannel : public ManagedOstream { void addSpecialCases(OstreamOpener* opener) const override; };/* class ManagedRegularOutputChannel */ -}/* CVC4 namespace */ +} // namespace CVC5 #endif /* CVC4__MANAGED_OSTREAMS_H */ diff --git a/src/smt/model.cpp b/src/smt/model.cpp index 93459a2b5..c1b9b7c12 100644 --- a/src/smt/model.cpp +++ b/src/smt/model.cpp @@ -23,7 +23,7 @@ #include "smt/smt_engine_scope.h" #include "theory/theory_model.h" -namespace CVC4 { +namespace CVC5 { namespace smt { Model::Model(theory::TheoryModel* tm) : d_isKnownSat(false), d_tmodel(tm) @@ -68,4 +68,4 @@ const std::vector<Node>& Model::getDeclaredTerms() const } } // namespace smt -}/* CVC4 namespace */ +} // namespace CVC5 diff --git a/src/smt/model.h b/src/smt/model.h index 063116de8..f43ba6eec 100644 --- a/src/smt/model.h +++ b/src/smt/model.h @@ -22,7 +22,7 @@ #include "expr/node.h" -namespace CVC4 { +namespace CVC5 { class SmtEngine; @@ -46,7 +46,7 @@ std::ostream& operator<<(std::ostream&, const Model&); */ class Model { friend std::ostream& operator<<(std::ostream&, const Model&); - friend class ::CVC4::SmtEngine; + friend class ::CVC5::SmtEngine; public: /** construct */ @@ -118,6 +118,6 @@ class Model { }; } // namespace smt -}/* CVC4 namespace */ +} // namespace CVC5 #endif /* CVC4__MODEL_H */ diff --git a/src/smt/model_blocker.cpp b/src/smt/model_blocker.cpp index 6ae09b27c..964a59b2f 100644 --- a/src/smt/model_blocker.cpp +++ b/src/smt/model_blocker.cpp @@ -21,9 +21,9 @@ #include "theory/rewriter.h" #include "theory/theory_model.h" -using namespace CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { Node ModelBlocker::getModelBlocker(const std::vector<Node>& assertions, theory::TheoryModel* m, @@ -278,4 +278,4 @@ Node ModelBlocker::getModelBlocker(const std::vector<Node>& assertions, return blocker; } -} /* namespace CVC4 */ +} // namespace CVC5 diff --git a/src/smt/model_blocker.h b/src/smt/model_blocker.h index 52389480e..3ec28758f 100644 --- a/src/smt/model_blocker.h +++ b/src/smt/model_blocker.h @@ -22,7 +22,7 @@ #include "expr/node.h" #include "options/smt_options.h" -namespace CVC4 { +namespace CVC5 { namespace theory { class TheoryModel; @@ -69,6 +69,6 @@ class ModelBlocker const std::vector<Node>& exprToBlock = std::vector<Node>()); }; /* class TheoryModelCoreBuilder */ -} // namespace CVC4 +} // namespace CVC5 #endif /* __CVC4__THEORY__MODEL_BLOCKER_H */ diff --git a/src/smt/model_core_builder.cpp b/src/smt/model_core_builder.cpp index 9bd531a1f..b68797f61 100644 --- a/src/smt/model_core_builder.cpp +++ b/src/smt/model_core_builder.cpp @@ -16,9 +16,9 @@ #include "theory/subs_minimize.h" -using namespace CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { bool ModelCoreBuilder::setModelCore(const std::vector<Node>& assertions, theory::TheoryModel* m, @@ -104,4 +104,4 @@ bool ModelCoreBuilder::setModelCore(const std::vector<Node>& assertions, return false; } -} /* namespace CVC4 */ +} // namespace CVC5 diff --git a/src/smt/model_core_builder.h b/src/smt/model_core_builder.h index 229eaf8e9..6075b528f 100644 --- a/src/smt/model_core_builder.h +++ b/src/smt/model_core_builder.h @@ -23,7 +23,7 @@ #include "options/smt_options.h" #include "theory/theory_model.h" -namespace CVC4 { +namespace CVC5 { /** * A utility for building model cores. @@ -59,6 +59,6 @@ class ModelCoreBuilder options::ModelCoresMode mode); }; /* class TheoryModelCoreBuilder */ -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__THEORY__MODEL_CORE_BUILDER_H */ diff --git a/src/smt/node_command.cpp b/src/smt/node_command.cpp index 98f73d34d..487a65ddf 100644 --- a/src/smt/node_command.cpp +++ b/src/smt/node_command.cpp @@ -20,7 +20,7 @@ #include "printer/printer.h" -namespace CVC4 { +namespace CVC5 { /* -------------------------------------------------------------------------- */ /* class NodeCommand */ @@ -158,4 +158,4 @@ NodeCommand* DefineFunctionNodeCommand::clone() const return new DefineFunctionNodeCommand(d_id, d_fun, d_formals, d_formula); } -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/smt/node_command.h b/src/smt/node_command.h index faef7aca3..0820ea807 100644 --- a/src/smt/node_command.h +++ b/src/smt/node_command.h @@ -25,7 +25,7 @@ #include "expr/type_node.h" #include "options/language.h" -namespace CVC4 { +namespace CVC5 { /** * A node version of Command. DO NOT use this version unless there is a need @@ -142,6 +142,6 @@ class DefineFunctionNodeCommand : public NodeCommand Node d_formula; }; -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__SMT__NODE_COMMAND_H */ diff --git a/src/smt/optimization_solver.cpp b/src/smt/optimization_solver.cpp index 1d92a5591..2143b9467 100644 --- a/src/smt/optimization_solver.cpp +++ b/src/smt/optimization_solver.cpp @@ -19,9 +19,9 @@ #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/smt_engine_subsolver.h" -using namespace CVC4::theory; +using namespace CVC5::theory; -namespace CVC4 { +namespace CVC5 { namespace smt { /** @@ -134,4 +134,4 @@ ObjectiveType Objective::getType() { return d_type; } Node Objective::getNode() { return d_node; } } // namespace smt -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/smt/optimization_solver.h b/src/smt/optimization_solver.h index 6117b9df5..c24a4ae52 100644 --- a/src/smt/optimization_solver.h +++ b/src/smt/optimization_solver.h @@ -22,7 +22,7 @@ #include "smt/assertions.h" #include "util/result.h" -namespace CVC4 { +namespace CVC5 { class SmtEngine; @@ -114,6 +114,6 @@ class Objective }; } // namespace smt -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__SMT__OPTIMIZATION_SOLVER_H */ diff --git a/src/smt/options_manager.cpp b/src/smt/options_manager.cpp index 8cab87b9f..d78435754 100644 --- a/src/smt/options_manager.cpp +++ b/src/smt/options_manager.cpp @@ -24,7 +24,7 @@ #include "smt/set_defaults.h" #include "util/resource_manager.h" -namespace CVC4 { +namespace CVC5 { namespace smt { OptionsManager::OptionsManager(Options* opts, ResourceManager* rm) @@ -143,4 +143,4 @@ void OptionsManager::finishInit(LogicInfo& logic, bool isInternalSubsolver) } } // namespace smt -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/smt/options_manager.h b/src/smt/options_manager.h index 12a1689a1..29e222296 100644 --- a/src/smt/options_manager.h +++ b/src/smt/options_manager.h @@ -18,7 +18,7 @@ #include "options/options_listener.h" #include "smt/managed_ostreams.h" -namespace CVC4 { +namespace CVC5 { class LogicInfo; class Options; @@ -75,6 +75,6 @@ class OptionsManager : public OptionsListener }; } // namespace smt -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__SMT__OPTIONS_MANAGER_H */ diff --git a/src/smt/output_manager.cpp b/src/smt/output_manager.cpp index e01d5879e..6d01643ab 100644 --- a/src/smt/output_manager.cpp +++ b/src/smt/output_manager.cpp @@ -18,7 +18,7 @@ #include "smt/smt_engine.h" -namespace CVC4 { +namespace CVC5 { OutputManager::OutputManager(SmtEngine* smt) : d_smt(smt) {} @@ -29,4 +29,4 @@ std::ostream& OutputManager::getDumpOut() const return *d_smt->getOptions().getOut(); } -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/smt/output_manager.h b/src/smt/output_manager.h index 88759e66d..76db5d19b 100644 --- a/src/smt/output_manager.h +++ b/src/smt/output_manager.h @@ -20,7 +20,7 @@ #include <ostream> -namespace CVC4 { +namespace CVC5 { class Printer; class SmtEngine; @@ -52,6 +52,6 @@ class OutputManager SmtEngine* d_smt; }; -} // namespace CVC4 +} // namespace CVC5 #endif // CVC4__SMT__OUTPUT_MANAGER_H diff --git a/src/smt/preprocess_proof_generator.cpp b/src/smt/preprocess_proof_generator.cpp index 9ee01b2ef..0fd3d9ce6 100644 --- a/src/smt/preprocess_proof_generator.cpp +++ b/src/smt/preprocess_proof_generator.cpp @@ -23,7 +23,7 @@ #include "options/proof_options.h" #include "theory/rewriter.h" -namespace CVC4 { +namespace CVC5 { namespace smt { PreprocessProofGenerator::PreprocessProofGenerator(ProofNodeManager* pnm, @@ -254,4 +254,4 @@ void PreprocessProofGenerator::checkEagerPedantic(PfRule r) } } // namespace smt -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/smt/preprocess_proof_generator.h b/src/smt/preprocess_proof_generator.h index ed19549c9..338397488 100644 --- a/src/smt/preprocess_proof_generator.h +++ b/src/smt/preprocess_proof_generator.h @@ -24,7 +24,7 @@ #include "expr/proof_generator.h" #include "theory/trust_node.h" -namespace CVC4 { +namespace CVC5 { class LazyCDProof; class ProofNodeManager; @@ -144,6 +144,6 @@ class PreprocessProofGenerator : public ProofGenerator }; } // namespace smt -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp index e5dd7869c..c2ebdbcd0 100644 --- a/src/smt/preprocessor.cpp +++ b/src/smt/preprocessor.cpp @@ -24,10 +24,10 @@ #include "smt/smt_engine.h" using namespace std; -using namespace CVC4::theory; -using namespace CVC4::kind; +using namespace CVC5::theory; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace smt { Preprocessor::Preprocessor(SmtEngine& smt, @@ -159,4 +159,4 @@ void Preprocessor::setProofGenerator(PreprocessProofGenerator* pppg) } } // namespace smt -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/smt/preprocessor.h b/src/smt/preprocessor.h index eadbbedc5..6bb0ef5d6 100644 --- a/src/smt/preprocessor.h +++ b/src/smt/preprocessor.h @@ -23,7 +23,7 @@ #include "smt/process_assertions.h" #include "theory/booleans/circuit_propagator.h" -namespace CVC4 { +namespace CVC5 { namespace preprocessing { class PreprocessingPassContext; } @@ -128,6 +128,6 @@ class Preprocessor }; } // namespace smt -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp index 3c7d88fe8..7ff4e54b5 100644 --- a/src/smt/process_assertions.cpp +++ b/src/smt/process_assertions.cpp @@ -39,11 +39,11 @@ #include "theory/theory_engine.h" using namespace std; -using namespace CVC4::preprocessing; -using namespace CVC4::theory; -using namespace CVC4::kind; +using namespace CVC5::preprocessing; +using namespace CVC5::theory; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace smt { /** Useful for counting the number of recursive calls. */ @@ -462,4 +462,4 @@ void ProcessAssertions::dumpAssertions(const char* key, } } // namespace smt -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/smt/process_assertions.h b/src/smt/process_assertions.h index f1c0aed3b..3844daafb 100644 --- a/src/smt/process_assertions.h +++ b/src/smt/process_assertions.h @@ -23,7 +23,7 @@ #include "expr/node.h" #include "util/resource_manager.h" -namespace CVC4 { +namespace CVC5 { class SmtEngine; @@ -124,6 +124,6 @@ class ProcessAssertions }; } // namespace smt -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp index 765beb9a2..d3b650612 100644 --- a/src/smt/proof_manager.cpp +++ b/src/smt/proof_manager.cpp @@ -25,7 +25,7 @@ #include "smt/preprocess_proof_generator.h" #include "smt/proof_post_processor.h" -namespace CVC4 { +namespace CVC5 { namespace smt { PfManager::PfManager(context::UserContext* u, SmtEngine* smte) @@ -190,4 +190,4 @@ void PfManager::getAssertions(Assertions& as, } } // namespace smt -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/smt/proof_manager.h b/src/smt/proof_manager.h index bf2078396..f0f384b7c 100644 --- a/src/smt/proof_manager.h +++ b/src/smt/proof_manager.h @@ -20,7 +20,7 @@ #include "context/cdhashmap.h" #include "expr/node.h" -namespace CVC4 { +namespace CVC5 { class ProofChecker; class ProofNode; @@ -117,6 +117,6 @@ class PfManager }; /* class SmtEngine */ } // namespace smt -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__SMT__PROOF_MANAGER_H */ diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index ff437e7e6..7e48c5c48 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -25,10 +25,10 @@ #include "theory/rewriter.h" #include "theory/theory.h" -using namespace CVC4::kind; -using namespace CVC4::theory; +using namespace CVC5::kind; +using namespace CVC5::theory; -namespace CVC4 { +namespace CVC5 { namespace smt { ProofPostprocessCallback::ProofPostprocessCallback(ProofNodeManager* pnm, @@ -1185,4 +1185,4 @@ void ProofPostproccess::setEliminateRule(PfRule rule) } } // namespace smt -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/smt/proof_post_processor.h b/src/smt/proof_post_processor.h index 78c367881..3c0d1e841 100644 --- a/src/smt/proof_post_processor.h +++ b/src/smt/proof_post_processor.h @@ -25,7 +25,7 @@ #include "util/statistics_registry.h" #include "util/stats_histogram.h" -namespace CVC4 { +namespace CVC5 { class SmtEngine; @@ -303,6 +303,6 @@ class ProofPostproccess }; } // namespace smt -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/smt/quant_elim_solver.cpp b/src/smt/quant_elim_solver.cpp index ba11319d3..08b69af81 100644 --- a/src/smt/quant_elim_solver.cpp +++ b/src/smt/quant_elim_solver.cpp @@ -23,10 +23,10 @@ #include "theory/rewriter.h" #include "theory/theory_engine.h" -using namespace CVC4::theory; -using namespace CVC4::kind; +using namespace CVC5::theory; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace smt { QuantElimSolver::QuantElimSolver(SmtSolver& sms) : d_smtSolver(sms) {} @@ -130,4 +130,4 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as, } } // namespace smt -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/smt/quant_elim_solver.h b/src/smt/quant_elim_solver.h index 9c3ee5a3f..80f67371b 100644 --- a/src/smt/quant_elim_solver.h +++ b/src/smt/quant_elim_solver.h @@ -20,7 +20,7 @@ #include "expr/node.h" #include "smt/assertions.h" -namespace CVC4 { +namespace CVC5 { namespace smt { class SmtSolver; @@ -99,6 +99,6 @@ class QuantElimSolver }; } // namespace smt -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__SMT__QUANT_ELIM_SOLVER_H */ diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index f8476b734..dd76de313 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -41,9 +41,9 @@ #include "smt/logic_exception.h" #include "theory/theory.h" -using namespace CVC4::theory; +using namespace CVC5::theory; -namespace CVC4 { +namespace CVC5 { namespace smt { void setDefaults(LogicInfo& logic, bool isInternalSubsolver) @@ -1480,4 +1480,4 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } } // namespace smt -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/smt/set_defaults.h b/src/smt/set_defaults.h index a4513c0e1..220314b0d 100644 --- a/src/smt/set_defaults.h +++ b/src/smt/set_defaults.h @@ -17,7 +17,7 @@ #include "theory/logic_info.h" -namespace CVC4 { +namespace CVC5 { namespace smt { /** @@ -36,6 +36,6 @@ namespace smt { void setDefaults(LogicInfo& logic, bool isInternalSubsolver); } // namespace smt -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__SMT__SET_DEFAULTS_H */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index f10439156..a7e464008 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -72,13 +72,13 @@ #include "base/configuration_private.h" using namespace std; -using namespace CVC4::smt; -using namespace CVC4::preprocessing; -using namespace CVC4::prop; -using namespace CVC4::context; -using namespace CVC4::theory; +using namespace CVC5::smt; +using namespace CVC5::preprocessing; +using namespace CVC5::prop; +using namespace CVC5::context; +using namespace CVC5::theory; -namespace CVC4 { +namespace CVC5 { SmtEngine::SmtEngine(NodeManager* nm, Options* optr) : d_env(new Env(nm)), @@ -505,7 +505,7 @@ bool SmtEngine::isValidGetInfoFlag(const std::string& key) const return false; } -CVC4::SExpr SmtEngine::getInfo(const std::string& key) const +CVC5::SExpr SmtEngine::getInfo(const std::string& key) const { SmtScope smts(this); @@ -2047,4 +2047,4 @@ OutputManager& SmtEngine::getOutputManager() { return d_outMgr; } theory::Rewriter* SmtEngine::getRewriter() { return d_env->getRewriter(); } -}/* CVC4 namespace */ +} // namespace CVC5 diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index de3a64ff6..21250dc30 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -34,7 +34,7 @@ #include "util/sexpr.h" #include "util/statistics.h" -namespace CVC4 { +namespace CVC5 { template <bool ref_count> class NodeTemplate; typedef NodeTemplate<true> Node; @@ -63,7 +63,7 @@ class Solver; namespace context { class Context; class UserContext; -}/* CVC4::context namespace */ + } // namespace context /* -------------------------------------------------------------------------- */ @@ -75,7 +75,7 @@ class PreprocessingPassContext; namespace prop { class PropEngine; -}/* CVC4::prop namespace */ + } // namespace prop /* -------------------------------------------------------------------------- */ @@ -111,24 +111,23 @@ class PfManager; class UnsatCoreManager; ProofManager* currentProofManager(); -}/* CVC4::smt namespace */ +} // namespace smt /* -------------------------------------------------------------------------- */ namespace theory { class Rewriter; class QuantifiersEngine; -}/* CVC4::theory namespace */ - + } // namespace theory /* -------------------------------------------------------------------------- */ class CVC4_EXPORT SmtEngine { - friend class ::CVC4::api::Solver; - friend class ::CVC4::smt::SmtEngineState; - friend class ::CVC4::smt::SmtScope; - friend class ::CVC4::LogicRequest; + friend class ::CVC5::api::Solver; + friend class ::CVC5::smt::SmtEngineState; + friend class ::CVC5::smt::SmtScope; + friend class ::CVC5::LogicRequest; /* ....................................................................... */ public: @@ -220,7 +219,7 @@ class CVC4_EXPORT SmtEngine bool isValidGetInfoFlag(const std::string& key) const; /** Query information about the SMT environment. */ - CVC4::SExpr getInfo(const std::string& key) const; + CVC5::SExpr getInfo(const std::string& key) const; /** * Set an aspect of the current SMT execution environment. @@ -1168,6 +1167,6 @@ class CVC4_EXPORT SmtEngine /* -------------------------------------------------------------------------- */ -}/* CVC4 namespace */ +} // namespace CVC5 #endif /* CVC4__SMT_ENGINE_H */ diff --git a/src/smt/smt_engine_scope.cpp b/src/smt/smt_engine_scope.cpp index 2aa96dfbb..d3dff72ce 100644 --- a/src/smt/smt_engine_scope.cpp +++ b/src/smt/smt_engine_scope.cpp @@ -22,7 +22,7 @@ #include "base/output.h" #include "smt/smt_engine.h" -namespace CVC4 { +namespace CVC5 { namespace smt { thread_local SmtEngine* s_smtEngine_current = NULL; @@ -65,5 +65,5 @@ StatisticsRegistry* SmtScope::currentStatisticsRegistry() { return s_smtEngine_current->getStatisticsRegistry(); } -}/* CVC4::smt namespace */ -}/* CVC4 namespace */ +} // namespace smt +} // namespace CVC5 diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h index 746abe1df..e45679f79 100644 --- a/src/smt/smt_engine_scope.h +++ b/src/smt/smt_engine_scope.h @@ -24,7 +24,7 @@ #include "options/options.h" -namespace CVC4 { +namespace CVC5 { class ProofManager; class SmtEngine; @@ -59,8 +59,7 @@ class SmtScope : public NodeManagerScope Options::OptionsScope d_optionsScope; };/* class SmtScope */ - -}/* CVC4::smt namespace */ -}/* CVC4 namespace */ +} // namespace smt +} // namespace CVC5 #endif /* CVC4__SMT__SMT_ENGINE_SCOPE_H */ diff --git a/src/smt/smt_engine_state.cpp b/src/smt/smt_engine_state.cpp index 504709942..fcf02784f 100644 --- a/src/smt/smt_engine_state.cpp +++ b/src/smt/smt_engine_state.cpp @@ -17,7 +17,7 @@ #include "options/smt_options.h" #include "smt/smt_engine.h" -namespace CVC4 { +namespace CVC5 { namespace smt { SmtEngineState::SmtEngineState(context::Context* c, @@ -308,4 +308,4 @@ void SmtEngineState::doPendingPops() } } // namespace smt -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/smt/smt_engine_state.h b/src/smt/smt_engine_state.h index 3c3075bf5..b5d98832f 100644 --- a/src/smt/smt_engine_state.h +++ b/src/smt/smt_engine_state.h @@ -23,7 +23,7 @@ #include "smt/smt_mode.h" #include "util/result.h" -namespace CVC4 { +namespace CVC5 { class SmtEngine; @@ -261,6 +261,6 @@ class SmtEngineState }; } // namespace smt -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/smt/smt_engine_stats.cpp b/src/smt/smt_engine_stats.cpp index 382dcba1f..1becdc8c2 100644 --- a/src/smt/smt_engine_stats.cpp +++ b/src/smt/smt_engine_stats.cpp @@ -16,7 +16,7 @@ #include "smt/smt_statistics_registry.h" -namespace CVC4 { +namespace CVC5 { namespace smt { SmtEngineStatistics::SmtEngineStatistics() @@ -70,4 +70,4 @@ SmtEngineStatistics::~SmtEngineStatistics() } } // namespace smt -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/smt/smt_engine_stats.h b/src/smt/smt_engine_stats.h index 9e3e7989e..e0923ec3e 100644 --- a/src/smt/smt_engine_stats.h +++ b/src/smt/smt_engine_stats.h @@ -20,7 +20,7 @@ #include "util/statistics_registry.h" #include "util/stats_timer.h" -namespace CVC4 { +namespace CVC5 { namespace smt { struct SmtEngineStatistics @@ -60,6 +60,6 @@ struct SmtEngineStatistics }; /* struct SmtEngineStatistics */ } // namespace smt -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__SMT__SMT_ENGINE_STATS_H */ diff --git a/src/smt/smt_mode.cpp b/src/smt/smt_mode.cpp index 49a8822dc..f25607249 100644 --- a/src/smt/smt_mode.cpp +++ b/src/smt/smt_mode.cpp @@ -16,7 +16,7 @@ #include <iostream> -namespace CVC4 { +namespace CVC5 { std::ostream& operator<<(std::ostream& out, SmtMode m) { @@ -34,4 +34,4 @@ std::ostream& operator<<(std::ostream& out, SmtMode m) return out; } -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/smt/smt_mode.h b/src/smt/smt_mode.h index dd8e13c72..91c35fc1f 100644 --- a/src/smt/smt_mode.h +++ b/src/smt/smt_mode.h @@ -19,7 +19,7 @@ #include <iosfwd> -namespace CVC4 { +namespace CVC5 { /** * The mode of the solver, which is an extension of Figure 4.1 on @@ -52,6 +52,6 @@ enum class SmtMode */ std::ostream& operator<<(std::ostream& out, SmtMode m); -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 89e75d892..e8ac58fe7 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -27,7 +27,7 @@ using namespace std; -namespace CVC4 { +namespace CVC5 { namespace smt { SmtSolver::SmtSolver(SmtEngine& smt, @@ -287,4 +287,4 @@ theory::QuantifiersEngine* SmtSolver::getQuantifiersEngine() Preprocessor* SmtSolver::getPreprocessor() { return &d_pp; } } // namespace smt -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/smt/smt_solver.h b/src/smt/smt_solver.h index e93cc63b8..db4871381 100644 --- a/src/smt/smt_solver.h +++ b/src/smt/smt_solver.h @@ -23,7 +23,7 @@ #include "theory/logic_info.h" #include "util/result.h" -namespace CVC4 { +namespace CVC5 { class SmtEngine; class TheoryEngine; @@ -151,6 +151,6 @@ class SmtSolver }; } // namespace smt -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__SMT__SMT_SOLVER_H */ diff --git a/src/smt/smt_statistics_registry.cpp b/src/smt/smt_statistics_registry.cpp index 7757d5b1b..a916aae7b 100644 --- a/src/smt/smt_statistics_registry.cpp +++ b/src/smt/smt_statistics_registry.cpp @@ -19,10 +19,10 @@ #include "smt/smt_engine_scope.h" #include "util/statistics_registry.h" -namespace CVC4 { +namespace CVC5 { StatisticsRegistry* smtStatisticsRegistry() { return smt::SmtScope::currentStatisticsRegistry(); } -}/* CVC4 namespace */ +} // namespace CVC5 diff --git a/src/smt/smt_statistics_registry.h b/src/smt/smt_statistics_registry.h index 38ff6fcc3..31d151544 100644 --- a/src/smt/smt_statistics_registry.h +++ b/src/smt/smt_statistics_registry.h @@ -20,7 +20,7 @@ #include "util/statistics_registry.h" -namespace CVC4 { +namespace CVC5 { /** * This returns the StatisticsRegistry attached to the currently in scope @@ -28,4 +28,4 @@ namespace CVC4 { */ StatisticsRegistry* smtStatisticsRegistry(); -}/* CVC4 namespace */ +} // namespace CVC5 diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp index ea74f7a1e..2bb38ea98 100644 --- a/src/smt/sygus_solver.cpp +++ b/src/smt/sygus_solver.cpp @@ -29,10 +29,10 @@ #include "theory/quantifiers_engine.h" #include "theory/smt_engine_subsolver.h" -using namespace CVC4::theory; -using namespace CVC4::kind; +using namespace CVC5::theory; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace smt { SygusSolver::SygusSolver(SmtSolver& sms, @@ -412,4 +412,4 @@ void SygusSolver::setSygusConjectureStale() } } // namespace smt -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/smt/sygus_solver.h b/src/smt/sygus_solver.h index 5cdf26fce..a1ffa195d 100644 --- a/src/smt/sygus_solver.h +++ b/src/smt/sygus_solver.h @@ -23,7 +23,7 @@ #include "smt/assertions.h" #include "util/result.h" -namespace CVC4 { +namespace CVC5 { class OutputManager; @@ -189,6 +189,6 @@ class SygusSolver }; } // namespace smt -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__SMT__SYGUS_SOLVER_H */ diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp index 6202ab80c..4d726b64e 100644 --- a/src/smt/term_formula_removal.cpp +++ b/src/smt/term_formula_removal.cpp @@ -28,7 +28,7 @@ using namespace std; -namespace CVC4 { +namespace CVC5 { RemoveTermFormulas::RemoveTermFormulas(context::UserContext* u, ProofNodeManager* pnm) @@ -544,4 +544,4 @@ ProofGenerator* RemoveTermFormulas::getTConvProofGenerator() bool RemoveTermFormulas::isProofEnabled() const { return d_pnm != nullptr; } -}/* CVC4 namespace */ +} // namespace CVC5 diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h index 22d5870b7..0f80fb8a4 100644 --- a/src/smt/term_formula_removal.h +++ b/src/smt/term_formula_removal.h @@ -28,7 +28,7 @@ #include "theory/trust_node.h" #include "util/hash.h" -namespace CVC4 { +namespace CVC5 { class LazyCDProof; class ProofNodeManager; @@ -209,4 +209,4 @@ class RemoveTermFormulas { bool isProofEnabled() const; };/* class RemoveTTE */ -}/* CVC4 namespace */ +} // namespace CVC5 diff --git a/src/smt/unsat_core_manager.cpp b/src/smt/unsat_core_manager.cpp index f1bc1065b..4d17c7414 100644 --- a/src/smt/unsat_core_manager.cpp +++ b/src/smt/unsat_core_manager.cpp @@ -17,7 +17,7 @@ #include "expr/proof_node_algorithm.h" #include "smt/assertions.h" -namespace CVC4 { +namespace CVC5 { namespace smt { void UnsatCoreManager::getUnsatCore(std::shared_ptr<ProofNode> pfn, @@ -89,4 +89,4 @@ void UnsatCoreManager::getRelevantInstantiations( } } // namespace smt -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/smt/unsat_core_manager.h b/src/smt/unsat_core_manager.h index daa83ed54..92e6018df 100644 --- a/src/smt/unsat_core_manager.h +++ b/src/smt/unsat_core_manager.h @@ -21,7 +21,7 @@ #include "expr/node.h" #include "expr/proof_node.h" -namespace CVC4 { +namespace CVC5 { namespace smt { @@ -67,6 +67,6 @@ class UnsatCoreManager }; /* class UnsatCoreManager */ } // namespace smt -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__SMT__UNSAT_CORE_MANAGER_H */ diff --git a/src/smt/update_ostream.h b/src/smt/update_ostream.h index ef2ea03e4..691da984f 100644 --- a/src/smt/update_ostream.h +++ b/src/smt/update_ostream.h @@ -30,7 +30,7 @@ #include "options/set_language.h" #include "smt/dump.h" -namespace CVC4 { +namespace CVC5 { class ChannelSettings { public: @@ -116,6 +116,6 @@ class TraceOstreamUpdate : public OstreamUpdate { void set(std::ostream* setTo) override { Trace.setStream(setTo); } }; /* class TraceOstreamUpdate */ -}/* CVC4 namespace */ +} // namespace CVC5 #endif /* CVC4__UPDATE_OSTREAM_H */ diff --git a/src/smt/witness_form.cpp b/src/smt/witness_form.cpp index a339210c0..959a6a6c3 100644 --- a/src/smt/witness_form.cpp +++ b/src/smt/witness_form.cpp @@ -17,7 +17,7 @@ #include "expr/skolem_manager.h" #include "theory/rewriter.h" -namespace CVC4 { +namespace CVC5 { namespace smt { WitnessFormGenerator::WitnessFormGenerator(ProofNodeManager* pnm) @@ -152,4 +152,4 @@ ProofGenerator* WitnessFormGenerator::convertExistsInternal(Node exists) } } // namespace smt -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/smt/witness_form.h b/src/smt/witness_form.h index c48948ade..905b0624b 100644 --- a/src/smt/witness_form.h +++ b/src/smt/witness_form.h @@ -23,7 +23,7 @@ #include "expr/proof_generator.h" #include "expr/term_conversion_proof_generator.h" -namespace CVC4 { +namespace CVC5 { namespace smt { /** @@ -97,6 +97,6 @@ class WitnessFormGenerator : public ProofGenerator }; } // namespace smt -} // namespace CVC4 +} // namespace CVC5 #endif |