Add function to get finite-field value.

Author: abdoo8080

cvc5.lean

@@ -1402,6 +1402,14 @@ Requires `term` to have a bit-vector sort.
 -/
 extern_def!? getBitVectorValue : Term → UInt32 → Except Error String
 
+/-- Get the string representation of a finite field value.
+
+Requires `term` to have a finite-field sort.
+
+-/
+extern_def!? getFiniteFieldValue : Term → Except Error String
+
+
 /-- Get the native integral value of an integral value. -/
 extern_def!? getIntegerValue : Term → Except Error Int
 

ffi/ffi.cpp

@@ -982,6 +982,14 @@ LEAN_EXPORT lean_obj_res term_getBitVectorValue(lean_obj_arg t, uint32_t base)
   CVC5_LEAN_API_TRY_CATCH_EXCEPT_END;
 }
 
+LEAN_EXPORT lean_obj_res term_getFiniteFieldValue(lean_obj_arg t)
+{
+  CVC5_LEAN_API_TRY_CATCH_EXCEPT_BEGIN;
+  return except_ok(
+      lean_mk_string(term_unbox(t)->getFiniteFieldValue().c_str()));
+  CVC5_LEAN_API_TRY_CATCH_EXCEPT_END;
+}
+
 LEAN_EXPORT lean_obj_res term_getIntegerValue(lean_obj_arg t)
 {
   CVC5_LEAN_API_TRY_CATCH_EXCEPT_BEGIN;