summaryrefslogtreecommitdiff
path: root/src/smt
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt')
-rw-r--r--src/smt/command.cpp22
-rw-r--r--src/smt/dump.cpp12
-rw-r--r--src/smt/dump.h38
-rw-r--r--src/smt/logic_exception.h2
-rw-r--r--src/smt/managed_ostreams.cpp6
-rw-r--r--src/smt/model.h2
-rw-r--r--src/smt/options_manager.cpp6
-rw-r--r--src/smt/smt_engine.cpp5
-rw-r--r--src/smt/smt_engine.h14
-rw-r--r--src/smt/update_ostream.h4
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 {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback