diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-04-15 13:04:55 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-15 20:04:55 +0000 |
commit | 77bca094a140b35341257f125a55212ff0108250 (patch) | |
tree | 1d3369b9be5fc4c3e8cb279ae5ea662e59cbcb3e /src/smt | |
parent | 63647b1d79df6f287ea6599958b16fce44b8271d (diff) |
Rename occurrences of CVC4 to CVC5. (#6351)
This renames everything but GitHub links and build system related
macros. Switching the build system to cvc5 will be the last step in the
renaming process.
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/command.cpp | 22 | ||||
-rw-r--r-- | src/smt/dump.cpp | 12 | ||||
-rw-r--r-- | src/smt/dump.h | 38 | ||||
-rw-r--r-- | src/smt/logic_exception.h | 2 | ||||
-rw-r--r-- | src/smt/managed_ostreams.cpp | 6 | ||||
-rw-r--r-- | src/smt/model.h | 2 | ||||
-rw-r--r-- | src/smt/options_manager.cpp | 6 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 5 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 14 | ||||
-rw-r--r-- | src/smt/update_ostream.h | 4 |
10 files changed, 56 insertions, 55 deletions
diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 5585ab48f..f27ed6e1f 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -1602,7 +1602,7 @@ void GetValueCommand::invoke(api::Solver* solver, SymbolManager* sm) d_result = solver->mkTerm(api::SEXPR, result); d_commandStatus = CommandSuccess::instance(); } - catch (api::CVC4ApiRecoverableException& e) + catch (api::CVC5ApiRecoverableException& e) { d_commandStatus = new CommandRecoverableFailure(e.what()); } @@ -1680,7 +1680,7 @@ void GetAssignmentCommand::invoke(api::Solver* solver, SymbolManager* sm) d_result = solver->mkTerm(api::SEXPR, sexprs); d_commandStatus = CommandSuccess::instance(); } - catch (api::CVC4ApiRecoverableException& e) + catch (api::CVC5ApiRecoverableException& e) { d_commandStatus = new CommandRecoverableFailure(e.what()); } @@ -1813,7 +1813,7 @@ void BlockModelCommand::invoke(api::Solver* solver, SymbolManager* sm) solver->blockModel(); d_commandStatus = CommandSuccess::instance(); } - catch (api::CVC4ApiRecoverableException& e) + catch (api::CVC5ApiRecoverableException& e) { d_commandStatus = new CommandRecoverableFailure(e.what()); } @@ -1867,7 +1867,7 @@ void BlockModelValuesCommand::invoke(api::Solver* solver, SymbolManager* sm) solver->blockModelValues(d_terms); d_commandStatus = CommandSuccess::instance(); } - catch (api::CVC4ApiRecoverableException& e) + catch (api::CVC5ApiRecoverableException& e) { d_commandStatus = new CommandRecoverableFailure(e.what()); } @@ -1913,7 +1913,7 @@ void GetProofCommand::invoke(api::Solver* solver, SymbolManager* sm) d_result = solver->getSmtEngine()->getProof(); d_commandStatus = CommandSuccess::instance(); } - catch (api::CVC4ApiRecoverableException& e) + catch (api::CVC5ApiRecoverableException& e) { d_commandStatus = new CommandRecoverableFailure(e.what()); } @@ -2318,7 +2318,7 @@ void GetUnsatAssumptionsCommand::invoke(api::Solver* solver, SymbolManager* sm) d_result = solver->getUnsatAssumptions(); d_commandStatus = CommandSuccess::instance(); } - catch (api::CVC4ApiRecoverableException& e) + catch (api::CVC5ApiRecoverableException& e) { d_commandStatus = new CommandRecoverableFailure(e.what()); } @@ -2380,7 +2380,7 @@ void GetUnsatCoreCommand::invoke(api::Solver* solver, SymbolManager* sm) d_commandStatus = CommandSuccess::instance(); } - catch (api::CVC4ApiRecoverableException& e) + catch (api::CVC5ApiRecoverableException& e) { d_commandStatus = new CommandRecoverableFailure(e.what()); } @@ -2615,7 +2615,7 @@ void SetInfoCommand::invoke(api::Solver* solver, SymbolManager* sm) solver->setInfo(d_flag, d_value); d_commandStatus = CommandSuccess::instance(); } - catch (api::CVC4ApiRecoverableException&) + catch (api::CVC5ApiRecoverableException&) { // As per SMT-LIB spec, silently accept unknown set-info keys d_commandStatus = CommandSuccess::instance(); @@ -2657,7 +2657,7 @@ void GetInfoCommand::invoke(api::Solver* solver, SymbolManager* sm) d_result = sexprToString(solver->mkTerm(api::SEXPR, v)); d_commandStatus = CommandSuccess::instance(); } - catch (api::CVC4ApiRecoverableException& e) + catch (api::CVC5ApiRecoverableException& e) { d_commandStatus = new CommandRecoverableFailure(e.what()); } @@ -2716,7 +2716,7 @@ void SetOptionCommand::invoke(api::Solver* solver, SymbolManager* sm) solver->setOption(d_flag, d_value); d_commandStatus = CommandSuccess::instance(); } - catch (api::CVC4ApiRecoverableException&) + catch (api::CVC5ApiRecoverableException&) { d_commandStatus = new CommandUnsupported(); } @@ -2754,7 +2754,7 @@ void GetOptionCommand::invoke(api::Solver* solver, SymbolManager* sm) d_result = solver->getOption(d_flag); d_commandStatus = CommandSuccess::instance(); } - catch (api::CVC4ApiRecoverableException&) + catch (api::CVC5ApiRecoverableException&) { d_commandStatus = new CommandUnsupported(); } diff --git a/src/smt/dump.cpp b/src/smt/dump.cpp index f5ebd3c5b..9dbbba7d3 100644 --- a/src/smt/dump.cpp +++ b/src/smt/dump.cpp @@ -27,7 +27,7 @@ namespace cvc5 { #if defined(CVC5_DUMPING) && !defined(CVC5_MUZZLE) -CVC4dumpstream& CVC4dumpstream::operator<<(const Command& c) +CVC5dumpstream& CVC5dumpstream::operator<<(const Command& c) { if (d_os != nullptr) { @@ -36,7 +36,7 @@ CVC4dumpstream& CVC4dumpstream::operator<<(const Command& c) return *this; } -CVC4dumpstream& CVC4dumpstream::operator<<(const NodeCommand& nc) +CVC5dumpstream& CVC5dumpstream::operator<<(const NodeCommand& nc) { if (d_os != nullptr) { @@ -47,8 +47,8 @@ CVC4dumpstream& CVC4dumpstream::operator<<(const NodeCommand& nc) #else -CVC4dumpstream& CVC4dumpstream::operator<<(const Command& c) { return *this; } -CVC4dumpstream& CVC4dumpstream::operator<<(const NodeCommand& nc) +CVC5dumpstream& CVC5dumpstream::operator<<(const Command& c) { return *this; } +CVC5dumpstream& CVC5dumpstream::operator<<(const NodeCommand& nc) { return *this; } @@ -175,7 +175,7 @@ void DumpC::setDumpFromString(const std::string& optarg) { else { throw OptionException( - "The dumping feature was disabled in this build of CVC4."); + "The dumping feature was disabled in this build of cvc5."); } } @@ -238,7 +238,7 @@ other modes for checking correctness and completeness of decision procedure\n\ implementations.\n\ \n\ The --output-language option controls the language used for dumping, and\n\ -this allows you to connect CVC4 to another solver implementation via a UNIX\n\ +this allows you to connect cvc5 to another solver implementation via a UNIX\n\ pipe to perform on-line checking. The --dump-to option can be used to dump\n\ to a file.\n\ "; diff --git a/src/smt/dump.h b/src/smt/dump.h index 7a2b0146b..3038d8996 100644 --- a/src/smt/dump.h +++ b/src/smt/dump.h @@ -27,24 +27,24 @@ class NodeCommand; #if defined(CVC5_DUMPING) && !defined(CVC5_MUZZLE) -class CVC4dumpstream +class CVC5dumpstream { public: - CVC4dumpstream() : d_os(nullptr) {} - CVC4dumpstream(std::ostream& os) : d_os(&os) {} + CVC5dumpstream() : d_os(nullptr) {} + CVC5dumpstream(std::ostream& os) : d_os(&os) {} - CVC4dumpstream& operator<<(const Command& c); + CVC5dumpstream& operator<<(const Command& c); /** A convenience function for dumping internal commands. * * Since Commands are now part of the public API, internal code should use * NodeCommands and this function (instead of the one above) to dump them. */ - CVC4dumpstream& operator<<(const NodeCommand& nc); + CVC5dumpstream& operator<<(const NodeCommand& nc); private: std::ostream* d_os; -}; /* class CVC4dumpstream */ +}; /* class CVC5dumpstream */ #else @@ -52,14 +52,14 @@ class CVC4dumpstream * Dummy implementation of the dump stream when dumping is disabled or the * build is muzzled. */ -class CVC4dumpstream +class CVC5dumpstream { public: - CVC4dumpstream() {} - CVC4dumpstream(std::ostream& os) {} - CVC4dumpstream& operator<<(const Command& c); - CVC4dumpstream& operator<<(const NodeCommand& nc); -}; /* class CVC4dumpstream */ + CVC5dumpstream() {} + CVC5dumpstream(std::ostream& os) {} + CVC5dumpstream& operator<<(const Command& c); + CVC5dumpstream& operator<<(const NodeCommand& nc); +}; /* class CVC5dumpstream */ #endif /* CVC5_DUMPING && !CVC5_MUZZLE */ @@ -67,19 +67,21 @@ class CVC4dumpstream class DumpC { public: - CVC4dumpstream operator()(const char* tag) { + CVC5dumpstream operator()(const char* tag) + { if(!d_tags.empty() && d_tags.find(std::string(tag)) != d_tags.end()) { - return CVC4dumpstream(getStream()); + return CVC5dumpstream(getStream()); } else { - return CVC4dumpstream(); + return CVC5dumpstream(); } } - CVC4dumpstream operator()(std::string tag) { + CVC5dumpstream operator()(std::string tag) + { if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) { - return CVC4dumpstream(getStream()); + return CVC5dumpstream(getStream()); } else { - return CVC4dumpstream(); + return CVC5dumpstream(); } } diff --git a/src/smt/logic_exception.h b/src/smt/logic_exception.h index 96963eb31..6e2f3f606 100644 --- a/src/smt/logic_exception.h +++ b/src/smt/logic_exception.h @@ -11,7 +11,7 @@ * **************************************************************************** * * An exception that is thrown when a feature is used outside - * the logic that CVC4 is currently using (for example, a quantifier + * the logic that cvc5 is currently using (for example, a quantifier * is used while running in a quantifier-free logic). */ diff --git a/src/smt/managed_ostreams.cpp b/src/smt/managed_ostreams.cpp index b0f9aef21..31bcc5f2f 100644 --- a/src/smt/managed_ostreams.cpp +++ b/src/smt/managed_ostreams.cpp @@ -77,7 +77,7 @@ void ManagedDumpOStream::initialize(std::ostream* outStream) { dumpGetStream.apply(outStream); #else /* CVC5_DUMPING */ throw OptionException( - "The dumping feature was disabled in this build of CVC4."); + "The dumping feature was disabled in this build of cvc5."); #endif /* CVC5_DUMPING */ } @@ -123,9 +123,9 @@ ManagedDiagnosticOutputChannel::~ManagedDiagnosticOutputChannel() { if(Warning.getStreamPointer() == getManagedOstream()){ Warning.setStream(&null_os); } - if (CVC4Message.getStreamPointer() == getManagedOstream()) + if (CVC5Message.getStreamPointer() == getManagedOstream()) { - CVC4Message.setStream(&null_os); + CVC5Message.setStream(&null_os); } if(Notice.getStreamPointer() == getManagedOstream()){ Notice.setStream(&null_os); diff --git a/src/smt/model.h b/src/smt/model.h index dd5d94d23..342a9f3b0 100644 --- a/src/smt/model.h +++ b/src/smt/model.h @@ -58,7 +58,7 @@ class Model { std::string getInputName() const { return d_inputName; } /** * Returns true if this model is guaranteed to be a model of the input - * formula. Notice that when CVC4 answers "unknown", it may have a model + * formula. Notice that when cvc5 answers "unknown", it may have a model * available for which this method returns false. In this case, this model is * only a candidate solution. */ diff --git a/src/smt/options_manager.cpp b/src/smt/options_manager.cpp index 2c732fa9d..68ee629dc 100644 --- a/src/smt/options_manager.cpp +++ b/src/smt/options_manager.cpp @@ -77,7 +77,7 @@ void OptionsManager::notifySetOption(const std::string& key) Trace.getStream() << expr::ExprSetDepth(depth); Notice.getStream() << expr::ExprSetDepth(depth); Chat.getStream() << expr::ExprSetDepth(depth); - CVC4Message.getStream() << expr::ExprSetDepth(depth); + CVC5Message.getStream() << expr::ExprSetDepth(depth); Warning.getStream() << expr::ExprSetDepth(depth); // intentionally exclude Dump stream from this list } @@ -88,7 +88,7 @@ void OptionsManager::notifySetOption(const std::string& key) Trace.getStream() << expr::ExprDag(dag); Notice.getStream() << expr::ExprDag(dag); Chat.getStream() << expr::ExprDag(dag); - CVC4Message.getStream() << expr::ExprDag(dag); + CVC5Message.getStream() << expr::ExprDag(dag); Warning.getStream() << expr::ExprDag(dag); Dump.getStream() << expr::ExprDag(dag); } @@ -104,7 +104,7 @@ void OptionsManager::notifySetOption(const std::string& key) Trace.getStream() << Command::printsuccess(value); Notice.getStream() << Command::printsuccess(value); Chat.getStream() << Command::printsuccess(value); - CVC4Message.getStream() << Command::printsuccess(value); + CVC5Message.getStream() << Command::printsuccess(value); Warning.getStream() << Command::printsuccess(value); *options::out() << Command::printsuccess(value); } diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index d3347b019..c877b7ce3 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -268,7 +268,7 @@ void SmtEngine::finishInit() everything.lock(); getPrinter().toStreamCmdComment( getOutputManager().getDumpOut(), - "CVC4 always dumps the most general, all-supported logic (below), as " + "cvc5 always dumps the most general, all-supported logic (below), as " "some internals might require the use of a logic more general than " "the input."); getPrinter().toStreamCmdSetBenchmarkLogic(getOutputManager().getDumpOut(), @@ -357,8 +357,7 @@ SmtEngine::~SmtEngine() // destroy the environment d_env.reset(nullptr); } catch(Exception& e) { - Warning() << "CVC4 threw an exception during cleanup." << endl - << e << endl; + Warning() << "cvc5 threw an exception during cleanup." << endl << e << endl; } } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 5947367f2..151b6106b 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -269,7 +269,7 @@ class CVC4_EXPORT SmtEngine * block-models option is set to a mode other than "none". * * This adds an assertion to the assertion stack that blocks the current - * model based on the current options configured by CVC4. + * model based on the current options configured by cvc5. * * The return value has the same meaning as that of assertFormula. */ @@ -704,14 +704,14 @@ class CVC4_EXPORT SmtEngine /** * Get an unsatisfiable core (only if immediately preceded by an UNSAT or - * ENTAILED query). Only permitted if CVC4 was built with unsat-core support + * ENTAILED query). Only permitted if cvc5 was built with unsat-core support * and produce-unsat-cores is on. */ UnsatCore getUnsatCore(); /** * Get a refutation proof (only if immediately preceded by an UNSAT or - * ENTAILED query). Only permitted if CVC4 was built with proof support and + * ENTAILED query). Only permitted if cvc5 was built with proof support and * the proof option is on. */ std::string getProof(); @@ -750,9 +750,9 @@ class CVC4_EXPORT SmtEngine * limit, but it's deterministic so that reproducible results can be * obtained. Currently, it's based on the number of conflicts. * However, please note that the definition may change between different - * versions of CVC4 (as may the number of conflicts required, anyway), + * versions of cvc5 (as may the number of conflicts required, anyway), * and it might even be different between instances of the same version - * of CVC4 on different platforms. + * of cvc5 on different platforms. * * A cumulative and non-cumulative (per-call) resource limit can be * set at the same time. A call to setResourceLimit() with @@ -927,7 +927,7 @@ class CVC4_EXPORT SmtEngine /** * Internal method to get an unsatisfiable core (only if immediately preceded - * by an UNSAT or ENTAILED query). Only permitted if CVC4 was built with + * by an UNSAT or ENTAILED query). Only permitted if cvc5 was built with * unsat-core support and produce-unsat-cores is on. Does not dump the * command. */ @@ -983,7 +983,7 @@ class CVC4_EXPORT SmtEngine * return nullptr. * * This ensures that the underlying theory model of the SmtSolver maintained - * by this class is currently available, which means that CVC4 is producing + * by this class is currently available, which means that cvc5 is producing * models, and is in "SAT mode", otherwise a recoverable exception is thrown. * * @param c used for giving an error message to indicate the context diff --git a/src/smt/update_ostream.h b/src/smt/update_ostream.h index be2489a87..d81a507f8 100644 --- a/src/smt/update_ostream.h +++ b/src/smt/update_ostream.h @@ -95,8 +95,8 @@ class WarningOstreamUpdate : public OstreamUpdate { class MessageOstreamUpdate : public OstreamUpdate { public: - std::ostream& get() override { return CVC4Message.getStream(); } - void set(std::ostream* setTo) override { CVC4Message.setStream(setTo); } + std::ostream& get() override { return CVC5Message.getStream(); } + void set(std::ostream* setTo) override { CVC5Message.setStream(setTo); } }; /* class MessageOstreamUpdate */ class NoticeOstreamUpdate : public OstreamUpdate { |