diff options
author | Gereon Kremer <nafur42@gmail.com> | 2021-06-02 15:21:22 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-06-02 15:21:22 +0200 |
commit | 66cdf5254bc58ecff335321478e73c8c0d6df296 (patch) | |
tree | 6b38ac130e7e05479c599e32b40c8c9b6c4acdb6 /src/api/cpp | |
parent | 6d359817283f196034d8e36d0b9c1f10fb16d644 (diff) |
Remove `Options::operator[]` (#6649)
This PR removes the next heavily specialized template function Options::operator[] in favor of direct access to the option data.
Diffstat (limited to 'src/api/cpp')
-rw-r--r-- | src/api/cpp/cvc5.cpp | 32 |
1 files changed, 16 insertions, 16 deletions
diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 0f2d5ad1b..668fc9382 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -4743,7 +4743,7 @@ Solver::Solver(Options* opts) } d_smtEngine.reset(new SmtEngine(d_nodeMgr.get(), d_originalOptions.get())); d_smtEngine->setSolver(this); - d_rng.reset(new Random(d_smtEngine->getOptions()[options::seed])); + d_rng.reset(new Random(d_smtEngine->getOptions().driver.seed)); resetStatistics(); } @@ -6452,7 +6452,7 @@ Result Solver::checkEntailed(const Term& term) const NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK(!d_smtEngine->isQueryMade() - || d_smtEngine->getOptions()[options::incrementalSolving]) + || d_smtEngine->getOptions().smt.incrementalSolving) << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; CVC5_API_SOLVER_CHECK_TERM(term); @@ -6468,7 +6468,7 @@ Result Solver::checkEntailed(const std::vector<Term>& terms) const CVC5_API_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); CVC5_API_CHECK(!d_smtEngine->isQueryMade() - || d_smtEngine->getOptions()[options::incrementalSolving]) + || d_smtEngine->getOptions().smt.incrementalSolving) << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; CVC5_API_SOLVER_CHECK_TERMS(terms); @@ -6497,7 +6497,7 @@ Result Solver::checkSat(void) const CVC5_API_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); CVC5_API_CHECK(!d_smtEngine->isQueryMade() - || d_smtEngine->getOptions()[options::incrementalSolving]) + || d_smtEngine->getOptions().smt.incrementalSolving) << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; //////// all checks before this line @@ -6512,7 +6512,7 @@ Result Solver::checkSatAssuming(const Term& assumption) const CVC5_API_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); CVC5_API_CHECK(!d_smtEngine->isQueryMade() - || d_smtEngine->getOptions()[options::incrementalSolving]) + || d_smtEngine->getOptions().smt.incrementalSolving) << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; CVC5_API_SOLVER_CHECK_TERM_WITH_SORT(assumption, getBooleanSort()); @@ -6528,7 +6528,7 @@ Result Solver::checkSatAssuming(const std::vector<Term>& assumptions) const CVC5_API_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); CVC5_API_CHECK(!d_smtEngine->isQueryMade() || assumptions.size() == 0 - || d_smtEngine->getOptions()[options::incrementalSolving]) + || d_smtEngine->getOptions().smt.incrementalSolving) << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; CVC5_API_SOLVER_CHECK_TERMS_WITH_SORT(assumptions, getBooleanSort()); @@ -6863,10 +6863,10 @@ std::vector<Term> Solver::getUnsatAssumptions(void) const { CVC5_API_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); - CVC5_API_CHECK(d_smtEngine->getOptions()[options::incrementalSolving]) + CVC5_API_CHECK(d_smtEngine->getOptions().smt.incrementalSolving) << "Cannot get unsat assumptions unless incremental solving is enabled " "(try --incremental)"; - CVC5_API_CHECK(d_smtEngine->getOptions()[options::unsatAssumptions]) + CVC5_API_CHECK(d_smtEngine->getOptions().smt.unsatAssumptions) << "Cannot get unsat assumptions unless explicitly enabled " "(try --produce-unsat-assumptions)"; CVC5_API_CHECK(d_smtEngine->getSmtMode() == SmtMode::UNSAT) @@ -6891,7 +6891,7 @@ std::vector<Term> Solver::getUnsatCore(void) const { CVC5_API_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); - CVC5_API_CHECK(d_smtEngine->getOptions()[options::unsatCores]) + CVC5_API_CHECK(d_smtEngine->getOptions().smt.unsatCores) << "Cannot get unsat core unless explicitly enabled " "(try --produce-unsat-cores)"; CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getSmtMode() == SmtMode::UNSAT) @@ -6925,7 +6925,7 @@ std::vector<Term> Solver::getValue(const std::vector<Term>& terms) const { CVC5_API_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); - CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getOptions()[options::produceModels]) + CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getOptions().smt.produceModels) << "Cannot get value unless model generation is enabled " "(try --produce-models)"; CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat()) @@ -6992,7 +6992,7 @@ Term Solver::getSeparationHeap() const d_smtEngine->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP)) << "Cannot obtain separation logic expressions if not using the " "separation logic theory."; - CVC5_API_CHECK(d_smtEngine->getOptions()[options::produceModels]) + CVC5_API_CHECK(d_smtEngine->getOptions().smt.produceModels) << "Cannot get separation heap term unless model generation is enabled " "(try --produce-models)"; CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat()) @@ -7011,7 +7011,7 @@ Term Solver::getSeparationNilTerm() const d_smtEngine->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP)) << "Cannot obtain separation logic expressions if not using the " "separation logic theory."; - CVC5_API_CHECK(d_smtEngine->getOptions()[options::produceModels]) + CVC5_API_CHECK(d_smtEngine->getOptions().smt.produceModels) << "Cannot get separation nil term unless model generation is enabled " "(try --produce-models)"; CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat()) @@ -7044,7 +7044,7 @@ void Solver::pop(uint32_t nscopes) const { NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(d_smtEngine->getOptions()[options::incrementalSolving]) + CVC5_API_CHECK(d_smtEngine->getOptions().smt.incrementalSolving) << "Cannot pop when not solving incrementally (use --incremental)"; CVC5_API_CHECK(nscopes <= d_smtEngine->getNumUserLevels()) << "Cannot pop beyond first pushed context"; @@ -7133,7 +7133,7 @@ void Solver::blockModel() const { NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(d_smtEngine->getOptions()[options::produceModels]) + CVC5_API_CHECK(d_smtEngine->getOptions().smt.produceModels) << "Cannot get value unless model generation is enabled " "(try --produce-models)"; CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat()) @@ -7148,7 +7148,7 @@ void Solver::blockModelValues(const std::vector<Term>& terms) const { NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(d_smtEngine->getOptions()[options::produceModels]) + CVC5_API_CHECK(d_smtEngine->getOptions().smt.produceModels) << "Cannot get value unless model generation is enabled " "(try --produce-models)"; CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat()) @@ -7176,7 +7176,7 @@ void Solver::push(uint32_t nscopes) const { NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(d_smtEngine->getOptions()[options::incrementalSolving]) + CVC5_API_CHECK(d_smtEngine->getOptions().smt.incrementalSolving) << "Cannot push when not solving incrementally (use --incremental)"; //////// all checks before this line for (uint32_t n = 0; n < nscopes; ++n) |