diff options
Diffstat (limited to 'src/api')
| -rw-r--r-- | src/api/cpp/cvc5.cpp | 36 | ||||
| -rw-r--r-- | src/api/cpp/cvc5.h | 20 |
2 files changed, 46 insertions, 10 deletions
diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index d03b8975e..d6c0a58ee 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -7381,6 +7381,36 @@ bool Solver::isModelCoreSymbol(const Term& v) const CVC5_API_TRY_CATCH_END; } +std::string Solver::getModel(const std::vector<Sort>& sorts, + const std::vector<Term>& vars) const +{ + CVC5_API_TRY_CATCH_BEGIN; + NodeManagerScope scope(getNodeManager()); + CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getOptions().smt.produceModels) + << "Cannot get model unless model generation is enabled " + "(try --produce-models)"; + CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat()) + << "Cannot get model unless after a SAT or unknown response."; + CVC5_API_SOLVER_CHECK_SORTS(sorts); + for (const Sort& s : sorts) + { + CVC5_API_RECOVERABLE_CHECK(s.isUninterpretedSort()) + << "Expecting an uninterpreted sort as argument to " + "getModel."; + } + CVC5_API_SOLVER_CHECK_TERMS(vars); + for (const Term& v : vars) + { + CVC5_API_RECOVERABLE_CHECK(v.getKind() == CONSTANT) + << "Expecting a free constant as argument to getModel."; + } + //////// all checks before this line + return d_smtEngine->getModel(Sort::sortVectorToTypeNodes(sorts), + Term::termVectorToNodes(vars)); + //////// + CVC5_API_TRY_CATCH_END; +} + Term Solver::getQuantifierElimination(const Term& q) const { NodeManagerScope scope(getNodeManager()); @@ -7900,12 +7930,6 @@ std::vector<Term> Solver::getSynthSolutions( CVC5_API_TRY_CATCH_END; } -/* - * !!! This is only temporarily available until the parser is fully migrated to - * the new API. !!! - */ -SmtEngine* Solver::getSmtEngine(void) const { return d_smtEngine.get(); } - Statistics Solver::getStatistics() const { return Statistics(d_smtEngine->getStatisticsRegistry()); diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 11b138a50..a221f3711 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -3951,6 +3951,22 @@ class CVC5_EXPORT Solver bool isModelCoreSymbol(const Term& v) const; /** + * Get the model + * SMT-LIB: + * \verbatim + * ( get-model ) + * \endverbatim + * Requires to enable option 'produce-models'. + * @param sorts The list of uninterpreted sorts that should be printed in the + * model. + * @param vars The list of free constants that should be printed in the + * model. A subset of these may be printed based on isModelCoreSymbol. + * @return a string representing the model. + */ + std::string getModel(const std::vector<Sort>& sorts, + const std::vector<Term>& vars) const; + + /** * Do quantifier elimination. * SMT-LIB: * \verbatim @@ -4329,10 +4345,6 @@ class CVC5_EXPORT Solver */ std::vector<Term> getSynthSolutions(const std::vector<Term>& terms) const; - // !!! This is only temporarily available until the parser is fully migrated - // to the new API. !!! - SmtEngine* getSmtEngine(void) const; - /** * Returns a snapshot of the current state of the statistic values of this * solver. The returned object is completely decoupled from the solver and |