diff options
Diffstat (limited to 'src/api/cpp/cvc5.h')
| -rw-r--r-- | src/api/cpp/cvc5.h | 26 |
1 files changed, 24 insertions, 2 deletions
diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 3c0241311..9f805fa65 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -3782,7 +3782,7 @@ class CVC5_EXPORT Solver std::string getProof() const; /** - * Get the value of the given term. + * Get the value of the given term in the current model. * SMT-LIB: * \verbatim * ( get-value ( <term> ) ) @@ -3791,8 +3791,9 @@ class CVC5_EXPORT Solver * @return the value of the given term */ Term getValue(const Term& term) const; + /** - * Get the values of the given terms. + * Get the values of the given terms in the current model. * SMT-LIB: * \verbatim * ( get-value ( <term>+ ) ) @@ -3803,6 +3804,27 @@ class CVC5_EXPORT Solver std::vector<Term> getValue(const std::vector<Term>& terms) const; /** + * Get the domain elements of uninterpreted sort s in the current model. The + * current model interprets s as the finite sort whose domain elements are + * given in the return value of this method. + * + * @param s The uninterpreted sort in question + * @return the domain elements of s in the current model + */ + std::vector<Term> getModelDomainElements(const Sort& s) const; + + /** + * This returns false if the model value of free constant v was not essential + * for showing the satisfiability of the last call to checkSat using the + * current model. This method will only return false (for any v) if + * the model-cores option has been set. + * + * @param v The term in question + * @return true if v is a model core symbol + */ + bool isModelCoreSymbol(const Term& v) const; + + /** * Do quantifier elimination. * SMT-LIB: * \verbatim |