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/command.cpp | |
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/command.cpp')
-rw-r--r-- | src/smt/command.cpp | 22 |
1 files changed, 11 insertions, 11 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(); } |