c api: Add support for model value related functions. (cvc5#10881)

include/cvc5/c/cvc5.h

@@ -3875,42 +3875,46 @@ Cvc5Term cvc5_get_value(Cvc5* cvc5, Cvc5Term term);
  *     (get-value ( <term>* ))
  * \endverbatim
  *
- * @param cvc5 The solver instance.
- * @param size The number of terms for which the value is queried.
+ * @param cvc5  The solver instance.
+ * @param size  The number of terms for which the value is queried.
  * @param terms The terms.
+ * @param rsize The resulting size of the timeout core.
  * @return The values of the given terms.
  */
 const Cvc5Term* cvc5_get_values(Cvc5* cvc5,
                                 size_t size,
-                                const Cvc5Term terms[]);
+                                const Cvc5Term terms[],
+                                size_t* rsize);
 
 /**
  * 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 function.
  *
  * @param cvc5 The solver instance.
- * @param s The uninterpreted sort in question.
+ * @param sort The uninterpreted sort in question.
  * @param size The size of the resulting domain elements array.
  * @return The domain elements of s in the current model.
  */
 const Cvc5Term* cvc5_get_model_domain_elements(Cvc5* cvc5,
-                                               Cvc5Sort s,
+                                               Cvc5Sort sort,
                                                size_t* size);
 
 /**
- * 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 function will only return false (for any `v`) if
- * option
+ * Determine if the model value of the given free constant was essential for
+ * showing satisfiability of the last `cvc5_check_sat()` query based on the
+ * current model.
+ *
+ * For any free constant `v`, this will only return false if
  * \verbatim embed:rst:inline :ref:`model-cores
- * <lbl-option-model-cores>`\endverbatim has been set.
+ * <lbl-option-model-cores>`\endverbatim
+ * has been set to true.
  *
  * @warning This function is experimental and may change in future versions.
  *
  * @param cvc5 The solver instance.
  * @param v The term in question.
- * @return True if `v` is a model core symbol.
+ * @return True if `v` was essential and is thus a model core symbol.
  */
 bool cvc5_is_model_core_symbol(Cvc5* cvc5, Cvc5Term v);
 

include/cvc5/cvc5.h

@@ -6113,13 +6113,14 @@ class CVC5_EXPORT Solver
   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 function will only return false (for any `v`) if
-   * option
-   * \verbatim embed:rst:inline :ref:`model-cores
-   * <lbl-option-model-cores>`\endverbatim has been set.
+   * Determine if the model value of the given free constant was essential for
+   * showing satisfiability of the last `checkSat()` query based on the current
+   * model.
    *
+   * For any free constant `v`, this will only return false if
+   * \verbatim embed:rst:inline :ref:`model-cores
+   * <lbl-option-model-cores>`\endverbatim
+   * has been set to true.
    * @warning This function is experimental and may change in future versions.
    *
    * @param v The term in question.

src/api/c/cvc5.cpp

@@ -5109,6 +5109,102 @@ const Cvc5Term* cvc5_get_learned_literals(Cvc5* cvc5,
   return res.data();
 }
 
+Cvc5Term cvc5_get_value(Cvc5* cvc5, Cvc5Term term)
+{
+  Cvc5Term res = nullptr;
+  CVC5_CAPI_TRY_CATCH_BEGIN;
+  CVC5_CAPI_CHECK_NOT_NULL(cvc5);
+  CVC5_CAPI_CHECK_TERM(term);
+  res = cvc5->d_tm->export_term(cvc5->d_solver.getValue(term->d_term));
+  CVC5_CAPI_TRY_CATCH_END;
+  return res;
+}
+
+const Cvc5Term* cvc5_get_values(Cvc5* cvc5,
+                                size_t size,
+                                const Cvc5Term terms[],
+                                size_t* rsize)
+{
+  static thread_local std::vector<Cvc5Term> res;
+  CVC5_CAPI_TRY_CATCH_BEGIN;
+  CVC5_CAPI_CHECK_NOT_NULL(cvc5);
+  CVC5_CAPI_CHECK_NOT_NULL(terms);
+  CVC5_CAPI_CHECK_NOT_NULL(rsize);
+  res.clear();
+  std::vector<cvc5::Term> cterms;
+  for (size_t i = 0; i < size; ++i)
+  {
+    cterms.push_back(terms[i]->d_term);
+  }
+  auto values = cvc5->d_solver.getValue(cterms);
+  for (const auto& t : values)
+  {
+    res.push_back(cvc5->d_tm->export_term(t));
+  }
+  *rsize = res.size();
+  CVC5_CAPI_TRY_CATCH_END;
+  return res.data();
+}
+
+const Cvc5Term* cvc5_get_model_domain_elements(Cvc5* cvc5,
+                                               Cvc5Sort sort,
+                                               size_t* size)
+{
+  static thread_local std::vector<Cvc5Term> res;
+  CVC5_CAPI_TRY_CATCH_BEGIN;
+  CVC5_CAPI_CHECK_NOT_NULL(cvc5);
+  CVC5_CAPI_CHECK_SORT(sort);
+  CVC5_CAPI_CHECK_NOT_NULL(size);
+  res.clear();
+  auto elems = cvc5->d_solver.getModelDomainElements(sort->d_sort);
+  for (const auto& t : elems)
+  {
+    res.push_back(cvc5->d_tm->export_term(t));
+  }
+  *size = res.size();
+  CVC5_CAPI_TRY_CATCH_END;
+  return res.data();
+}
+
+bool cvc5_is_model_core_symbol(Cvc5* cvc5, Cvc5Term v)
+{
+  bool res = false;
+  CVC5_CAPI_TRY_CATCH_BEGIN;
+  CVC5_CAPI_CHECK_NOT_NULL(cvc5);
+  if (v)
+  {
+    res = cvc5->d_solver.isModelCoreSymbol(v->d_term);
+  }
+  CVC5_CAPI_TRY_CATCH_END;
+  return res;
+}
+
+const char* cvc5_get_model(Cvc5* cvc5,
+                           size_t nsorts,
+                           const Cvc5Sort sorts[],
+                           size_t nconsts,
+                           const Cvc5Term consts[])
+{
+  static thread_local std::string str;
+  CVC5_CAPI_TRY_CATCH_BEGIN;
+  CVC5_CAPI_CHECK_NOT_NULL(cvc5);
+  CVC5_CAPI_CHECK_NOT_NULL(sorts);
+  CVC5_CAPI_CHECK_NOT_NULL(consts);
+  std::vector<cvc5::Sort> csorts;
+  for (size_t i = 0; i < nsorts; ++i)
+  {
+    csorts.push_back(sorts[i]->d_sort);
+  }
+  std::vector<cvc5::Term> cconsts;
+  for (size_t i = 0; i < nconsts; ++i)
+  {
+    cconsts.push_back(consts[i]->d_term);
+  }
+  str = cvc5->d_solver.getModel(csorts, cconsts);
+  CVC5_CAPI_TRY_CATCH_END;
+  return str.c_str();
+}
+
 void cvc5_push(Cvc5* cvc5, uint32_t nscopes)
 {
   CVC5_CAPI_TRY_CATCH_BEGIN;