diff options
Diffstat (limited to 'src/api/cvc4cpp.cpp')
| -rw-r--r-- | src/api/cvc4cpp.cpp | 19 |
1 files changed, 7 insertions, 12 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 7db0e41db..5ccb4c6c1 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -52,6 +52,7 @@ #include "options/smt_options.h" #include "smt/model.h" #include "smt/smt_engine.h" +#include "smt/smt_mode.h" #include "theory/logic_info.h" #include "theory/theory_model.h" #include "util/random.h" @@ -4819,8 +4820,7 @@ std::vector<Term> Solver::getUnsatAssumptions(void) const CVC4_API_CHECK(d_smtEngine->getOptions()[options::unsatAssumptions]) << "Cannot get unsat assumptions unless explicitly enabled " "(try --produce-unsat-assumptions)"; - CVC4_API_CHECK(d_smtEngine->getSmtMode() - == SmtEngine::SmtMode::SMT_MODE_UNSAT) + CVC4_API_CHECK(d_smtEngine->getSmtMode() == SmtMode::UNSAT) << "Cannot get unsat assumptions unless in unsat mode."; std::vector<Node> uassumptions = d_smtEngine->getUnsatAssumptions(); @@ -4846,8 +4846,7 @@ std::vector<Term> Solver::getUnsatCore(void) const CVC4_API_CHECK(d_smtEngine->getOptions()[options::unsatCores]) << "Cannot get unsat core unless explicitly enabled " "(try --produce-unsat-cores)"; - CVC4_API_CHECK(d_smtEngine->getSmtMode() - == SmtEngine::SmtMode::SMT_MODE_UNSAT) + CVC4_API_CHECK(d_smtEngine->getSmtMode() == SmtMode::UNSAT) << "Cannot get unsat core unless in unsat mode."; UnsatCore core = d_smtEngine->getUnsatCore(); /* Can not use @@ -4883,8 +4882,7 @@ std::vector<Term> Solver::getValue(const std::vector<Term>& terms) const CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels]) << "Cannot get value unless model generation is enabled " "(try --produce-models)"; - CVC4_API_CHECK(d_smtEngine->getSmtMode() - != SmtEngine::SmtMode::SMT_MODE_UNSAT) + CVC4_API_CHECK(d_smtEngine->getSmtMode() != SmtMode::UNSAT) << "Cannot get value when in unsat mode."; std::vector<Term> res; for (size_t i = 0, n = terms.size(); i < n; ++i) @@ -4910,8 +4908,7 @@ Term Solver::getSeparationHeap() const CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels]) << "Cannot get separation heap term unless model generation is enabled " "(try --produce-models)"; - CVC4_API_CHECK(d_smtEngine->getSmtMode() - != SmtEngine::SmtMode::SMT_MODE_UNSAT) + CVC4_API_CHECK(d_smtEngine->getSmtMode() != SmtMode::UNSAT) << "Cannot get separtion heap term when in unsat mode."; theory::TheoryModel* m = @@ -4935,8 +4932,7 @@ Term Solver::getSeparationNilTerm() const CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels]) << "Cannot get separation nil term unless model generation is enabled " "(try --produce-models)"; - CVC4_API_CHECK(d_smtEngine->getSmtMode() - != SmtEngine::SmtMode::SMT_MODE_UNSAT) + CVC4_API_CHECK(d_smtEngine->getSmtMode() != SmtMode::UNSAT) << "Cannot get separtion nil term when in unsat mode."; theory::TheoryModel* m = @@ -5034,8 +5030,7 @@ void Solver::printModel(std::ostream& out) const CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels]) << "Cannot get value unless model generation is enabled " "(try --produce-models)"; - CVC4_API_CHECK(d_smtEngine->getSmtMode() - != SmtEngine::SmtMode::SMT_MODE_UNSAT) + CVC4_API_CHECK(d_smtEngine->getSmtMode() != SmtMode::UNSAT) << "Cannot get value when in unsat mode."; out << *d_smtEngine->getModel(); CVC4_API_SOLVER_TRY_CATCH_END; |