extend stubs

api/build_enums.cpp

@@ -29,7 +29,6 @@ extern "C" void build_enums(){
     to_cpp_stream <<
       "  | " << name << " -> " << i << std::endl;
     of_cpp_stream << "  | " << i << " -> " << name << std::endl;
-    ss.clear();
   }
   of_cpp_stream << "  | _ -> assert false" << std::endl;
   std::cout << "module Kind = struct" << std::endl
@@ -97,32 +96,4 @@ extern "C" void build_enums(){
 	    << to_string_stream.str() << std::endl
 	    << to_cpp_stream.str() << std::endl
 	    << of_cpp_stream.str() << "end" << std::endl;
-
-  // type_stream.str("");
-  // to_string_stream.str("");
-  // to_cpp_stream.str("");
-  // of_cpp_stream.str("");
-
-  // type_stream << "type t =" << std::endl;
-  // to_string_stream << "let to_string = function" << std::endl;
-  // to_cpp_stream << "let to_cpp = function" << std::endl;
-  // of_cpp_stream << "let of_cpp = function" << std::endl;
-  // for (int i = 0; i < (int)ProofRule::UNKNOWN; i += 1){
-  //   std::string ln(std::string(toString((ProofRule)i)));
-  //   std::string name(ln);
-  //   for (int j = 1; j < name.length(); j += 1)
-  //     name[j] = std::tolower(name[j]);
-  //   type_stream << "  | " << name << std::endl;
-  //   to_string_stream <<
-  //     "  | " << name << " -> " << '"' << ln << '"' << std::endl;
-  //   to_cpp_stream <<
-  //     "  | " << name << " -> " << i << std::endl;
-  //   of_cpp_stream << "  | " << i << " -> " << name << std::endl;
-  // }
-  // of_cpp_stream << "  | _ -> assert false" << std::endl;
-  // std::cout << "module ProofRule = struct" << std::endl
-  //     << type_stream.str() << std::endl
-	//     << to_string_stream.str() << std::endl
-	//     << to_cpp_stream.str() << std::endl
-	//     << of_cpp_stream.str() << "end" << std::endl;
 }

cvc5.ml

@@ -1,10 +1,9 @@
-open Cvc5_enums
-
 exception Error of string
 
 let _ = Callback.register_exception "cvc5Exception" (Error "")
 
-module Kind = Kind
+module Kind = Cvc5_enums.Kind
+module RoundingMode = Cvc5_enums.RoundingMode
 
 module TermManager =
 struct
@@ -29,6 +28,10 @@ module Term =
 struct
   type term = Cvc5_external.term
 
+  let id = Cvc5_external.term_id
+  let equal = Cvc5_external.term_equal
+  let kind t = Kind.of_cpp @@ Cvc5_external.term_kind t
+  let sort = Cvc5_external.term_sort
   let to_string = Cvc5_external.term_to_string
   let mk_const = Cvc5_external.mk_const
   let mk_const_s = Cvc5_external.mk_const_s
@@ -38,6 +41,8 @@ struct
   let mk_false = Cvc5_external.mk_false
   let mk_bool = Cvc5_external.mk_bool
   let mk_int = Cvc5_external.mk_int
+  let mk_rm (tm : TermManager.tm) (rm : RoundingMode.t) = 
+    Cvc5_external.mk_roundingmode tm (RoundingMode.to_cpp rm)
 end
 
 module Result =

cvc5.mli

@@ -1,6 +1,7 @@
 exception Error of string
 
 module Kind = Cvc5_enums.Kind
+module RoundingMode = Cvc5_enums.RoundingMode
 
 module TermManager :
 sig 
@@ -25,6 +26,10 @@ module Term :
 sig 
   type term
 
+  val id : term -> int
+  val equal : term -> term -> bool
+  val kind : term -> Kind.t
+  val sort : term -> Sort.sort
   val to_string : term -> string
   val mk_const : TermManager.tm -> Sort.sort -> term
   val mk_const_s : TermManager.tm -> Sort.sort -> string -> term
@@ -33,6 +38,7 @@ sig
   val mk_false : TermManager.tm -> term
   val mk_bool : TermManager.tm -> bool -> term
   val mk_int : TermManager.tm -> int -> term
+  val mk_rm : TermManager.tm -> RoundingMode.t -> term
 end
 
 module Result : 

cvc5_external.ml

@@ -31,9 +31,9 @@ and learned_lit_type = ptr
 and block_model_mode = ptr
 and find_synth_target = ptr
 
-external result_is_sat : result -> bool = "ocaml_cvc5_stub_result_is_sat"
-external result_is_unsat : result -> bool = "ocaml_cvc5_stub_result_is_unsat"
-external result_is_unknown : result -> bool = "ocaml_cvc5_stub_result_is_unknown"
+external result_is_sat : result -> bool = "ocaml_cvc5_stub_result_is_sat" [@@noalloc]
+external result_is_unsat : result -> bool = "ocaml_cvc5_stub_result_is_unsat" [@@noalloc]
+external result_is_unknown : result -> bool = "ocaml_cvc5_stub_result_is_unknown" [@@noalloc]
 external mk_true : term_manager -> term = "ocaml_cvc5_stub_mk_true"
 external mk_false : term_manager -> term = "ocaml_cvc5_stub_mk_false"
 external mk_bool : term_manager -> bool -> term = "ocaml_cvc5_stub_mk_bool"
@@ -49,17 +49,22 @@ external get_string_sort : term_manager -> sort = "ocaml_cvc5_stub_get_string_so
 external mk_bitvector_sort : term_manager -> int -> sort = "ocaml_cvc5_stub_mk_bitvector_sort"
 external mk_const_s : term_manager -> sort -> string -> term = "ocaml_cvc5_stub_mk_const_s"
 external mk_const : term_manager -> sort -> term = "ocaml_cvc5_stub_mk_const"
+external mk_roundingmode : term_manager -> int -> term = "ocaml_cvc5_stub_mk_rounding_mode"
 external term_to_string : term -> string = "ocaml_cvc5_stub_term_to_string"
+external term_equal : term -> term -> bool = "ocaml_cvc5_stub_term_equal" [@@noalloc]
+external term_id : term -> int = "ocaml_cvc5_stub_term_id" [@@noalloc]
+external term_kind : term -> int = "ocaml_cvc5_stub_term_kind" [@@noalloc]
+external term_sort : term -> sort = "ocaml_cvc5_stub_term_sort"
 external new_solver : term_manager -> solver = "ocaml_cvc5_stub_new_solver"
 external new_term_manager : unit -> term_manager = "ocaml_cvc5_stub_new_term_manager"
 external delete_term_manager : term_manager -> unit = "ocaml_cvc5_stub_delete_term_manager"
 external delete : solver -> unit = "ocaml_cvc5_stub_delete"
-external assert_formula : solver -> term -> unit = "ocaml_cvc5_stub_assert_formula"
+external assert_formula : solver -> term -> unit = "ocaml_cvc5_stub_assert_formula" [@@noalloc]
 external check_sat : solver -> result = "ocaml_cvc5_stub_check_sat"
-external set_logic : solver -> string -> unit = "ocaml_cvc5_stub_set_logic"
+external set_logic : solver -> string -> unit = "ocaml_cvc5_stub_set_logic" [@@noalloc]
 external simplify : solver -> term -> term = "ocaml_cvc5_stub_simplify"
-external push : solver -> int -> unit = "ocaml_cvc5_stub_push"
-external pop : solver -> int -> unit = "ocaml_cvc5_stub_pop"
-external reset_assertions : solver -> unit = "ocaml_cvc5_stub_reset_assertions"
+external push : solver -> int -> unit = "ocaml_cvc5_stub_push" [@@noalloc]
+external pop : solver -> int -> unit = "ocaml_cvc5_stub_pop" [@@noalloc]
+external reset_assertions : solver -> unit = "ocaml_cvc5_stub_reset_assertions" [@@noalloc]
 
 (**/**)

cvc5_stubs.cpp

@@ -221,6 +221,27 @@ CAMLprim value ocaml_cvc5_stub_delete_term_manager(value v){
   CVC5_TRY_CATCH_END;
 }
 
+CAMLprim value ocaml_cvc5_stub_term_equal(value t1, value t2){
+  return Val_bool(*Term_val(t1) == *Term_val(t2));
+}
+
+CAMLprim value ocaml_cvc5_stub_term_id(value v){
+  return Val_int(Term_val(v)->getId());
+}
+
+CAMLprim value ocaml_cvc5_stub_term_kind(value v){
+  return Val_int(Term_val(v)->getKind());
+}
+
+CAMLprim value ocaml_cvc5_stub_term_sort(value v){
+  value custom = Val_unit;
+  CVC5_TRY_CATCH_BEGIN;
+  new(&sort_operations, &custom) 
+    Sort(Term_val(v)->getSort());
+  return custom;
+  CVC5_TRY_CATCH_END;
+}
+
 CAMLprim value ocaml_cvc5_stub_mk_true(value v){
   cvc5::TermManager* term_manager = TermManager_val(v);
   value custom = Val_unit;
@@ -306,6 +327,16 @@ CAMLprim value ocaml_cvc5_stub_mk_term(value v, value kind, value t){
   CVC5_TRY_CATCH_END;
 }
 
+CAMLprim value ocaml_cvc5_stub_mk_rounding_mode(value v, value rm){
+  cvc5::TermManager* term_manager = TermManager_val(v);
+  value custom = Val_unit;
+  CVC5_TRY_CATCH_BEGIN;
+  new(&term_operations, &custom) 
+    Term(term_manager->mkRoundingMode((cvc5::RoundingMode)Int_val(rm)));
+  return custom;
+  CVC5_TRY_CATCH_END;
+}
+
 CAMLprim value ocaml_cvc5_stub_get_boolean_sort(value v){
   cvc5::TermManager* term_manager = TermManager_val(v);
   value custom = Val_unit;