diff options
Diffstat (limited to 'src/smt')
77 files changed, 195 insertions, 195 deletions
diff --git a/src/smt/abduction_solver.cpp b/src/smt/abduction_solver.cpp index cd4228eed..804a93401 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 CVC5::theory; +using namespace cvc5::theory; -namespace CVC5 { +namespace cvc5 { namespace smt { AbductionSolver::AbductionSolver(SmtEngine* parent) : d_parent(parent) {} @@ -195,4 +195,4 @@ void AbductionSolver::checkAbduct(Node a) } } // namespace smt -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/smt/abduction_solver.h b/src/smt/abduction_solver.h index c7328a9a8..03b300a7a 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 CVC5 { +namespace cvc5 { class SmtEngine; @@ -115,6 +115,6 @@ class AbductionSolver }; } // namespace smt -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__SMT__ABDUCTION_SOLVER_H */ diff --git a/src/smt/abstract_values.cpp b/src/smt/abstract_values.cpp index e4c7f2668..fc978d39b 100644 --- a/src/smt/abstract_values.cpp +++ b/src/smt/abstract_values.cpp @@ -16,7 +16,7 @@ #include "options/smt_options.h" -namespace CVC5 { +namespace cvc5 { namespace smt { AbstractValues::AbstractValues(NodeManager* nm) @@ -52,4 +52,4 @@ Node AbstractValues::mkAbstractValue(TNode n) } } // namespace smt -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/smt/abstract_values.h b/src/smt/abstract_values.h index be4a0c7a3..5a7ce7ba1 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 CVC5 { +namespace cvc5 { namespace smt { /** @@ -75,6 +75,6 @@ class AbstractValues }; } // namespace smt -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp index f82d0769b..07d072751 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 CVC5::theory; -using namespace CVC5::kind; +using namespace cvc5::theory; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace smt { Assertions::Assertions(context::UserContext* u, AbstractValues& absv) @@ -243,4 +243,4 @@ bool Assertions::isProofEnabled() const } } // namespace smt -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/smt/assertions.h b/src/smt/assertions.h index 135fe8974..687c9b742 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 CVC5 { +namespace cvc5 { namespace smt { class AbstractValues; @@ -172,6 +172,6 @@ class Assertions }; } // namespace smt -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/smt/check_models.cpp b/src/smt/check_models.cpp index 0c21002af..b84bc3e64 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 CVC5::theory; +using namespace cvc5::theory; -namespace CVC5 { +namespace cvc5 { namespace smt { CheckModels::CheckModels(SmtSolver& s) : d_smt(s) {} @@ -148,4 +148,4 @@ void CheckModels::checkModel(Model* m, } } // namespace smt -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/smt/check_models.h b/src/smt/check_models.h index d12a33ee5..2d9f4cf1b 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 CVC5 { +namespace cvc5 { namespace smt { class Model; @@ -48,6 +48,6 @@ class CheckModels }; } // namespace smt -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 6d9b1a5ec..e4b179cf4 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -43,7 +43,7 @@ using namespace std; -namespace CVC5 { +namespace cvc5 { std::string sexprToString(api::Term sexpr) { @@ -2819,4 +2819,4 @@ void DatatypeDeclarationCommand::toStream(std::ostream& out, out, api::Sort::sortVectorToTypeNodes(d_datatypes)); } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/smt/command.h b/src/smt/command.h index 6d169ce5e..2d13a2246 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -31,7 +31,7 @@ #include "cvc4_export.h" #include "options/language.h" -namespace CVC5 { +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 CVC5 +} // namespace cvc5 #endif /* CVC4__COMMAND_H */ diff --git a/src/smt/defined_function.h b/src/smt/defined_function.h index 7f3007975..2a7332297 100644 --- a/src/smt/defined_function.h +++ b/src/smt/defined_function.h @@ -21,7 +21,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace smt { /** @@ -55,6 +55,6 @@ class DefinedFunction }; /* class DefinedFunction */ } // namespace smt -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__SMT__DEFINED_FUNCTION_H */ diff --git a/src/smt/dump.cpp b/src/smt/dump.cpp index 76973ec32..e00ed907f 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 CVC5 { +namespace cvc5 { #if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) @@ -58,13 +58,13 @@ CVC4dumpstream& CVC4dumpstream::operator<<(const NodeCommand& nc) DumpC DumpChannel; std::ostream& DumpC::setStream(std::ostream* os) { - ::CVC5::DumpOutChannel.setStream(os); + ::cvc5::DumpOutChannel.setStream(os); return *os; } -std::ostream& DumpC::getStream() { return ::CVC5::DumpOutChannel.getStream(); } +std::ostream& DumpC::getStream() { return ::cvc5::DumpOutChannel.getStream(); } std::ostream* DumpC::getStreamPointer() { - return ::CVC5::DumpOutChannel.getStreamPointer(); + return ::cvc5::DumpOutChannel.getStreamPointer(); } void DumpC::setDumpFromString(const std::string& optarg) { @@ -243,4 +243,4 @@ pipe to perform on-line checking. The --dump-to option can be used to dump\n\ to a file.\n\ "; -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/smt/dump.h b/src/smt/dump.h index be146470a..e4fe15aa7 100644 --- a/src/smt/dump.h +++ b/src/smt/dump.h @@ -21,7 +21,7 @@ #include "base/output.h" -namespace CVC5 { +namespace cvc5 { class Command; class NodeCommand; @@ -110,8 +110,8 @@ class DumpC /** The dump singleton */ extern DumpC DumpChannel; -#define Dump ::CVC5::DumpChannel +#define Dump ::cvc5::DumpChannel -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__DUMP_H */ diff --git a/src/smt/dump_manager.cpp b/src/smt/dump_manager.cpp index 6b81d5594..4b7f0b056 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 CVC5 { +namespace cvc5 { namespace smt { DumpManager::DumpManager(context::UserContext* u) @@ -72,4 +72,4 @@ void DumpManager::setPrintFuncInModel(Node f, bool p) } } // namespace smt -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/smt/dump_manager.h b/src/smt/dump_manager.h index 519b93110..c1bd7e898 100644 --- a/src/smt/dump_manager.h +++ b/src/smt/dump_manager.h @@ -22,7 +22,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { class NodeCommand; @@ -75,6 +75,6 @@ class DumpManager }; } // namespace smt -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/smt/env.cpp b/src/smt/env.cpp index 6440c29d3..fc19299d4 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 CVC5::smt; +using namespace cvc5::smt; -namespace CVC5 { +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 CVC5 +} // namespace cvc5 diff --git a/src/smt/env.h b/src/smt/env.h index 3ceefdd34..79377206a 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 CVC5 { +namespace cvc5 { class NodeManager; class StatisticsRegistry; @@ -182,6 +182,6 @@ class Env std::unique_ptr<ResourceManager> d_resourceManager; }; /* class Env */ -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__SMT__ENV_H */ diff --git a/src/smt/expand_definitions.cpp b/src/smt/expand_definitions.cpp index 599f57747..85a2732c9 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 CVC5::preprocessing; -using namespace CVC5::theory; -using namespace CVC5::kind; +using namespace cvc5::preprocessing; +using namespace cvc5::theory; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace smt { ExpandDefs::ExpandDefs(SmtEngine& smt, @@ -367,4 +367,4 @@ void ExpandDefs::setProofNodeManager(ProofNodeManager* pnm) } } // namespace smt -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/smt/expand_definitions.h b/src/smt/expand_definitions.h index 035e7989d..7d99445d5 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 CVC5 { +namespace cvc5 { class ProofNodeManager; class ResourceManager; @@ -95,6 +95,6 @@ class ExpandDefs }; } // namespace smt -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/smt/interpolation_solver.cpp b/src/smt/interpolation_solver.cpp index d14b87901..7b75ea2ed 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 CVC5::theory; +using namespace cvc5::theory; -namespace CVC5 { +namespace cvc5 { namespace smt { InterpolationSolver::InterpolationSolver(SmtEngine* parent) : d_parent(parent) @@ -136,4 +136,4 @@ void InterpolationSolver::checkInterpol(Node interpol, } } // namespace smt -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/smt/interpolation_solver.h b/src/smt/interpolation_solver.h index 1c9b65d85..bae777a16 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 CVC5 { +namespace cvc5 { class SmtEngine; @@ -81,6 +81,6 @@ class InterpolationSolver }; } // namespace smt -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__SMT__INTERPOLATION_SOLVER_H */ diff --git a/src/smt/listeners.cpp b/src/smt/listeners.cpp index c686e4115..e322531a7 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 CVC5 { +namespace cvc5 { namespace smt { ResourceOutListener::ResourceOutListener(SmtEngine& smt) : d_smt(smt) {} @@ -103,4 +103,4 @@ void SmtNodeManagerListener::nmNotifyNewSkolem(TNode n, } } // namespace smt -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/smt/listeners.h b/src/smt/listeners.h index 1705b9126..6857f7e6b 100644 --- a/src/smt/listeners.h +++ b/src/smt/listeners.h @@ -22,7 +22,7 @@ #include "base/listener.h" #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { class OutputManager; class SmtEngine; @@ -75,6 +75,6 @@ class SmtNodeManagerListener : public NodeManagerListener }; } // namespace smt -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/smt/logic_exception.h b/src/smt/logic_exception.h index 91f2d3723..0809d83e8 100644 --- a/src/smt/logic_exception.h +++ b/src/smt/logic_exception.h @@ -24,9 +24,9 @@ #include "base/exception.h" -namespace CVC5 { +namespace cvc5 { -class LogicException : public CVC5::Exception +class LogicException : public cvc5::Exception { public: LogicException() : @@ -43,6 +43,6 @@ class LogicException : public CVC5::Exception } }; /* class LogicException */ -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__SMT__LOGIC_EXCEPTION_H */ diff --git a/src/smt/managed_ostreams.cpp b/src/smt/managed_ostreams.cpp index 6baabe0e5..09b454cf2 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 CVC5 { +namespace cvc5 { ManagedOstream::ManagedOstream() : d_managed(NULL) {} @@ -164,4 +164,4 @@ void ManagedDiagnosticOutputChannel::addSpecialCases(OstreamOpener* opener) opener->addSpecialCase("stderr", &std::cerr); } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/smt/managed_ostreams.h b/src/smt/managed_ostreams.h index ba56bcfa3..f79eecc23 100644 --- a/src/smt/managed_ostreams.h +++ b/src/smt/managed_ostreams.h @@ -22,7 +22,7 @@ #include <ostream> -namespace CVC5 { +namespace cvc5 { class OstreamOpener; @@ -141,6 +141,6 @@ class ManagedDiagnosticOutputChannel : public ManagedOstream { void addSpecialCases(OstreamOpener* opener) const override; };/* class ManagedRegularOutputChannel */ -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__MANAGED_OSTREAMS_H */ diff --git a/src/smt/model.cpp b/src/smt/model.cpp index c1b9b7c12..a3742b652 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 CVC5 { +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 -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/smt/model.h b/src/smt/model.h index f43ba6eec..5eb1e45a4 100644 --- a/src/smt/model.h +++ b/src/smt/model.h @@ -22,7 +22,7 @@ #include "expr/node.h" -namespace CVC5 { +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 ::CVC5::SmtEngine; + friend class ::cvc5::SmtEngine; public: /** construct */ @@ -118,6 +118,6 @@ class Model { }; } // namespace smt -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__MODEL_H */ diff --git a/src/smt/model_blocker.cpp b/src/smt/model_blocker.cpp index 964a59b2f..64769a2ad 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 CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +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 CVC5 +} // namespace cvc5 diff --git a/src/smt/model_blocker.h b/src/smt/model_blocker.h index 3ec28758f..6d03a64c6 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 CVC5 { +namespace cvc5 { namespace theory { class TheoryModel; @@ -69,6 +69,6 @@ class ModelBlocker const std::vector<Node>& exprToBlock = std::vector<Node>()); }; /* class TheoryModelCoreBuilder */ -} // namespace CVC5 +} // 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 b68797f61..f16c93e62 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 CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +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 CVC5 +} // namespace cvc5 diff --git a/src/smt/model_core_builder.h b/src/smt/model_core_builder.h index 6075b528f..38a9e51ed 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 CVC5 { +namespace cvc5 { /** * A utility for building model cores. @@ -59,6 +59,6 @@ class ModelCoreBuilder options::ModelCoresMode mode); }; /* class TheoryModelCoreBuilder */ -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__MODEL_CORE_BUILDER_H */ diff --git a/src/smt/node_command.cpp b/src/smt/node_command.cpp index 487a65ddf..61d380b72 100644 --- a/src/smt/node_command.cpp +++ b/src/smt/node_command.cpp @@ -20,7 +20,7 @@ #include "printer/printer.h" -namespace CVC5 { +namespace cvc5 { /* -------------------------------------------------------------------------- */ /* class NodeCommand */ @@ -158,4 +158,4 @@ NodeCommand* DefineFunctionNodeCommand::clone() const return new DefineFunctionNodeCommand(d_id, d_fun, d_formals, d_formula); } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/smt/node_command.h b/src/smt/node_command.h index 0820ea807..9ba2b316d 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 CVC5 { +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 CVC5 +} // namespace cvc5 #endif /* CVC4__SMT__NODE_COMMAND_H */ diff --git a/src/smt/optimization_solver.cpp b/src/smt/optimization_solver.cpp index 2143b9467..ae1ce7057 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 CVC5::theory; +using namespace cvc5::theory; -namespace CVC5 { +namespace cvc5 { namespace smt { /** @@ -134,4 +134,4 @@ ObjectiveType Objective::getType() { return d_type; } Node Objective::getNode() { return d_node; } } // namespace smt -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/smt/optimization_solver.h b/src/smt/optimization_solver.h index c24a4ae52..b79a4a823 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 CVC5 { +namespace cvc5 { class SmtEngine; @@ -114,6 +114,6 @@ class Objective }; } // namespace smt -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__SMT__OPTIMIZATION_SOLVER_H */ diff --git a/src/smt/options_manager.cpp b/src/smt/options_manager.cpp index d78435754..0a7a0c54a 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 CVC5 { +namespace cvc5 { namespace smt { OptionsManager::OptionsManager(Options* opts, ResourceManager* rm) @@ -143,4 +143,4 @@ void OptionsManager::finishInit(LogicInfo& logic, bool isInternalSubsolver) } } // namespace smt -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/smt/options_manager.h b/src/smt/options_manager.h index 29e222296..62ad37eb0 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 CVC5 { +namespace cvc5 { class LogicInfo; class Options; @@ -75,6 +75,6 @@ class OptionsManager : public OptionsListener }; } // namespace smt -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__SMT__OPTIONS_MANAGER_H */ diff --git a/src/smt/output_manager.cpp b/src/smt/output_manager.cpp index 6d01643ab..a01c7a6a9 100644 --- a/src/smt/output_manager.cpp +++ b/src/smt/output_manager.cpp @@ -18,7 +18,7 @@ #include "smt/smt_engine.h" -namespace CVC5 { +namespace cvc5 { OutputManager::OutputManager(SmtEngine* smt) : d_smt(smt) {} @@ -29,4 +29,4 @@ std::ostream& OutputManager::getDumpOut() const return *d_smt->getOptions().getOut(); } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/smt/output_manager.h b/src/smt/output_manager.h index 76db5d19b..de21dc2b5 100644 --- a/src/smt/output_manager.h +++ b/src/smt/output_manager.h @@ -20,7 +20,7 @@ #include <ostream> -namespace CVC5 { +namespace cvc5 { class Printer; class SmtEngine; @@ -52,6 +52,6 @@ class OutputManager SmtEngine* d_smt; }; -} // namespace CVC5 +} // 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 0fd3d9ce6..016f60cfc 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 CVC5 { +namespace cvc5 { namespace smt { PreprocessProofGenerator::PreprocessProofGenerator(ProofNodeManager* pnm, @@ -254,4 +254,4 @@ void PreprocessProofGenerator::checkEagerPedantic(PfRule r) } } // namespace smt -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/smt/preprocess_proof_generator.h b/src/smt/preprocess_proof_generator.h index 338397488..8e3882b2a 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 CVC5 { +namespace cvc5 { class LazyCDProof; class ProofNodeManager; @@ -144,6 +144,6 @@ class PreprocessProofGenerator : public ProofGenerator }; } // namespace smt -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp index c2ebdbcd0..9f1f71bd7 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 CVC5::theory; -using namespace CVC5::kind; +using namespace cvc5::theory; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace smt { Preprocessor::Preprocessor(SmtEngine& smt, @@ -159,4 +159,4 @@ void Preprocessor::setProofGenerator(PreprocessProofGenerator* pppg) } } // namespace smt -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/smt/preprocessor.h b/src/smt/preprocessor.h index 6bb0ef5d6..0d307d734 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 CVC5 { +namespace cvc5 { namespace preprocessing { class PreprocessingPassContext; } @@ -128,6 +128,6 @@ class Preprocessor }; } // namespace smt -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp index 7ff4e54b5..29651211c 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 CVC5::preprocessing; -using namespace CVC5::theory; -using namespace CVC5::kind; +using namespace cvc5::preprocessing; +using namespace cvc5::theory; +using namespace cvc5::kind; -namespace CVC5 { +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 CVC5 +} // namespace cvc5 diff --git a/src/smt/process_assertions.h b/src/smt/process_assertions.h index 3844daafb..0409e181b 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 CVC5 { +namespace cvc5 { class SmtEngine; @@ -124,6 +124,6 @@ class ProcessAssertions }; } // namespace smt -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp index d3b650612..5b938ab64 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 CVC5 { +namespace cvc5 { namespace smt { PfManager::PfManager(context::UserContext* u, SmtEngine* smte) @@ -190,4 +190,4 @@ void PfManager::getAssertions(Assertions& as, } } // namespace smt -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/smt/proof_manager.h b/src/smt/proof_manager.h index f0f384b7c..e1177ca83 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 CVC5 { +namespace cvc5 { class ProofChecker; class ProofNode; @@ -117,6 +117,6 @@ class PfManager }; /* class SmtEngine */ } // namespace smt -} // namespace CVC5 +} // 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 7e48c5c48..dedb686c3 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 CVC5::kind; -using namespace CVC5::theory; +using namespace cvc5::kind; +using namespace cvc5::theory; -namespace CVC5 { +namespace cvc5 { namespace smt { ProofPostprocessCallback::ProofPostprocessCallback(ProofNodeManager* pnm, @@ -1185,4 +1185,4 @@ void ProofPostproccess::setEliminateRule(PfRule rule) } } // namespace smt -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/smt/proof_post_processor.h b/src/smt/proof_post_processor.h index 3c0d1e841..9f3e7e55b 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 CVC5 { +namespace cvc5 { class SmtEngine; @@ -303,6 +303,6 @@ class ProofPostproccess }; } // namespace smt -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/smt/quant_elim_solver.cpp b/src/smt/quant_elim_solver.cpp index 08b69af81..ddc20ee8d 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 CVC5::theory; -using namespace CVC5::kind; +using namespace cvc5::theory; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace smt { QuantElimSolver::QuantElimSolver(SmtSolver& sms) : d_smtSolver(sms) {} @@ -130,4 +130,4 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as, } } // namespace smt -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/smt/quant_elim_solver.h b/src/smt/quant_elim_solver.h index 80f67371b..e59d6c7ff 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 CVC5 { +namespace cvc5 { namespace smt { class SmtSolver; @@ -99,6 +99,6 @@ class QuantElimSolver }; } // namespace smt -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__SMT__QUANT_ELIM_SOLVER_H */ diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index dd76de313..5fed0d664 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 CVC5::theory; +using namespace cvc5::theory; -namespace CVC5 { +namespace cvc5 { namespace smt { void setDefaults(LogicInfo& logic, bool isInternalSubsolver) @@ -1480,4 +1480,4 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } } // namespace smt -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/smt/set_defaults.h b/src/smt/set_defaults.h index 220314b0d..eb7cc3910 100644 --- a/src/smt/set_defaults.h +++ b/src/smt/set_defaults.h @@ -17,7 +17,7 @@ #include "theory/logic_info.h" -namespace CVC5 { +namespace cvc5 { namespace smt { /** @@ -36,6 +36,6 @@ namespace smt { void setDefaults(LogicInfo& logic, bool isInternalSubsolver); } // namespace smt -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__SMT__SET_DEFAULTS_H */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index db67af2f0..724c5d48f 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 CVC5::smt; -using namespace CVC5::preprocessing; -using namespace CVC5::prop; -using namespace CVC5::context; -using namespace CVC5::theory; +using namespace cvc5::smt; +using namespace cvc5::preprocessing; +using namespace cvc5::prop; +using namespace cvc5::context; +using namespace cvc5::theory; -namespace CVC5 { +namespace cvc5 { SmtEngine::SmtEngine(NodeManager* nm, Options* optr) : d_env(new Env(nm)), @@ -503,7 +503,7 @@ bool SmtEngine::isValidGetInfoFlag(const std::string& key) const return false; } -CVC5::SExpr SmtEngine::getInfo(const std::string& key) const +cvc5::SExpr SmtEngine::getInfo(const std::string& key) const { SmtScope smts(this); @@ -2027,4 +2027,4 @@ OutputManager& SmtEngine::getOutputManager() { return d_outMgr; } theory::Rewriter* SmtEngine::getRewriter() { return d_env->getRewriter(); } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index dd23ac949..909c1cc50 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 CVC5 { +namespace cvc5 { template <bool ref_count> class NodeTemplate; typedef NodeTemplate<true> Node; @@ -124,10 +124,10 @@ namespace theory { class CVC4_EXPORT SmtEngine { - friend class ::CVC5::api::Solver; - friend class ::CVC5::smt::SmtEngineState; - friend class ::CVC5::smt::SmtScope; - friend class ::CVC5::LogicRequest; + friend class ::cvc5::api::Solver; + friend class ::cvc5::smt::SmtEngineState; + friend class ::cvc5::smt::SmtScope; + friend class ::cvc5::LogicRequest; /* ....................................................................... */ public: @@ -219,7 +219,7 @@ class CVC4_EXPORT SmtEngine bool isValidGetInfoFlag(const std::string& key) const; /** Query information about the SMT environment. */ - CVC5::SExpr getInfo(const std::string& key) const; + cvc5::SExpr getInfo(const std::string& key) const; /** * Set an aspect of the current SMT execution environment. @@ -1154,6 +1154,6 @@ class CVC4_EXPORT SmtEngine /* -------------------------------------------------------------------------- */ -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__SMT_ENGINE_H */ diff --git a/src/smt/smt_engine_scope.cpp b/src/smt/smt_engine_scope.cpp index d3dff72ce..cbb6a9679 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 CVC5 { +namespace cvc5 { namespace smt { thread_local SmtEngine* s_smtEngine_current = NULL; @@ -66,4 +66,4 @@ StatisticsRegistry* SmtScope::currentStatisticsRegistry() { } } // namespace smt -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h index e45679f79..8bb010cec 100644 --- a/src/smt/smt_engine_scope.h +++ b/src/smt/smt_engine_scope.h @@ -24,7 +24,7 @@ #include "options/options.h" -namespace CVC5 { +namespace cvc5 { class ProofManager; class SmtEngine; @@ -60,6 +60,6 @@ class SmtScope : public NodeManagerScope };/* class SmtScope */ } // namespace smt -} // namespace CVC5 +} // 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 fcf02784f..b33f1e13c 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 CVC5 { +namespace cvc5 { namespace smt { SmtEngineState::SmtEngineState(context::Context* c, @@ -308,4 +308,4 @@ void SmtEngineState::doPendingPops() } } // namespace smt -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/smt/smt_engine_state.h b/src/smt/smt_engine_state.h index b5d98832f..b90778b67 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 CVC5 { +namespace cvc5 { class SmtEngine; @@ -261,6 +261,6 @@ class SmtEngineState }; } // namespace smt -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/smt/smt_engine_stats.cpp b/src/smt/smt_engine_stats.cpp index 1becdc8c2..b0de2d8b3 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 CVC5 { +namespace cvc5 { namespace smt { SmtEngineStatistics::SmtEngineStatistics() @@ -70,4 +70,4 @@ SmtEngineStatistics::~SmtEngineStatistics() } } // namespace smt -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/smt/smt_engine_stats.h b/src/smt/smt_engine_stats.h index e0923ec3e..4ec06e99b 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 CVC5 { +namespace cvc5 { namespace smt { struct SmtEngineStatistics @@ -60,6 +60,6 @@ struct SmtEngineStatistics }; /* struct SmtEngineStatistics */ } // namespace smt -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__SMT__SMT_ENGINE_STATS_H */ diff --git a/src/smt/smt_mode.cpp b/src/smt/smt_mode.cpp index f25607249..db21e53c4 100644 --- a/src/smt/smt_mode.cpp +++ b/src/smt/smt_mode.cpp @@ -16,7 +16,7 @@ #include <iostream> -namespace CVC5 { +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 CVC5 +} // namespace cvc5 diff --git a/src/smt/smt_mode.h b/src/smt/smt_mode.h index 91c35fc1f..ce8babc2b 100644 --- a/src/smt/smt_mode.h +++ b/src/smt/smt_mode.h @@ -19,7 +19,7 @@ #include <iosfwd> -namespace CVC5 { +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 CVC5 +} // namespace cvc5 #endif diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index e8ac58fe7..3f663726c 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -27,7 +27,7 @@ using namespace std; -namespace CVC5 { +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 CVC5 +} // namespace cvc5 diff --git a/src/smt/smt_solver.h b/src/smt/smt_solver.h index db4871381..7d9d06ad9 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 CVC5 { +namespace cvc5 { class SmtEngine; class TheoryEngine; @@ -151,6 +151,6 @@ class SmtSolver }; } // namespace smt -} // namespace CVC5 +} // 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 a916aae7b..dd5ed470c 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 CVC5 { +namespace cvc5 { StatisticsRegistry* smtStatisticsRegistry() { return smt::SmtScope::currentStatisticsRegistry(); } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/smt/smt_statistics_registry.h b/src/smt/smt_statistics_registry.h index 31d151544..97bdde703 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 CVC5 { +namespace cvc5 { /** * This returns the StatisticsRegistry attached to the currently in scope @@ -28,4 +28,4 @@ namespace CVC5 { */ StatisticsRegistry* smtStatisticsRegistry(); -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp index 2bb38ea98..27e16ccc6 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 CVC5::theory; -using namespace CVC5::kind; +using namespace cvc5::theory; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace smt { SygusSolver::SygusSolver(SmtSolver& sms, @@ -412,4 +412,4 @@ void SygusSolver::setSygusConjectureStale() } } // namespace smt -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/smt/sygus_solver.h b/src/smt/sygus_solver.h index a1ffa195d..ffce2ff06 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 CVC5 { +namespace cvc5 { class OutputManager; @@ -189,6 +189,6 @@ class SygusSolver }; } // namespace smt -} // namespace CVC5 +} // 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 4d726b64e..262c46870 100644 --- a/src/smt/term_formula_removal.cpp +++ b/src/smt/term_formula_removal.cpp @@ -28,7 +28,7 @@ using namespace std; -namespace CVC5 { +namespace cvc5 { RemoveTermFormulas::RemoveTermFormulas(context::UserContext* u, ProofNodeManager* pnm) @@ -544,4 +544,4 @@ ProofGenerator* RemoveTermFormulas::getTConvProofGenerator() bool RemoveTermFormulas::isProofEnabled() const { return d_pnm != nullptr; } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h index 0f80fb8a4..d2d3bf6fd 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 CVC5 { +namespace cvc5 { class LazyCDProof; class ProofNodeManager; @@ -209,4 +209,4 @@ class RemoveTermFormulas { bool isProofEnabled() const; };/* class RemoveTTE */ -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/smt/unsat_core_manager.cpp b/src/smt/unsat_core_manager.cpp index 4d17c7414..976e7ea6c 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 CVC5 { +namespace cvc5 { namespace smt { void UnsatCoreManager::getUnsatCore(std::shared_ptr<ProofNode> pfn, @@ -89,4 +89,4 @@ void UnsatCoreManager::getRelevantInstantiations( } } // namespace smt -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/smt/unsat_core_manager.h b/src/smt/unsat_core_manager.h index 92e6018df..c41638222 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 CVC5 { +namespace cvc5 { namespace smt { @@ -67,6 +67,6 @@ class UnsatCoreManager }; /* class UnsatCoreManager */ } // namespace smt -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__SMT__UNSAT_CORE_MANAGER_H */ diff --git a/src/smt/update_ostream.h b/src/smt/update_ostream.h index 691da984f..c8f5d639b 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 CVC5 { +namespace cvc5 { class ChannelSettings { public: @@ -116,6 +116,6 @@ class TraceOstreamUpdate : public OstreamUpdate { void set(std::ostream* setTo) override { Trace.setStream(setTo); } }; /* class TraceOstreamUpdate */ -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__UPDATE_OSTREAM_H */ diff --git a/src/smt/witness_form.cpp b/src/smt/witness_form.cpp index 959a6a6c3..2ae39a664 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 CVC5 { +namespace cvc5 { namespace smt { WitnessFormGenerator::WitnessFormGenerator(ProofNodeManager* pnm) @@ -152,4 +152,4 @@ ProofGenerator* WitnessFormGenerator::convertExistsInternal(Node exists) } } // namespace smt -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/smt/witness_form.h b/src/smt/witness_form.h index 905b0624b..e30f165e5 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 CVC5 { +namespace cvc5 { namespace smt { /** @@ -97,6 +97,6 @@ class WitnessFormGenerator : public ProofGenerator }; } // namespace smt -} // namespace CVC5 +} // namespace cvc5 #endif |