Merge branch 'main' into portable-installation

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
   type tm = Cvc5_external.term_manager
@@ -31,6 +30,14 @@ end
 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
@@ -47,6 +54,9 @@ module Term = struct
   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 = struct

cvc5.mli

@@ -1,6 +1,7 @@
 exception Error of string
 
 module Kind = Cvc5_enums.Kind
+module RoundingMode = Cvc5_enums.RoundingMode
 
 module TermManager : sig
   type tm
@@ -27,6 +28,14 @@ end
 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
@@ -42,6 +51,8 @@ module Term : sig
   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 : sig

cvc5_external.ml

@@ -59,11 +59,14 @@ and block_model_mode = ptr
 and find_synth_target = ptr
 
 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"
 
@@ -102,8 +105,20 @@ external mk_const_s : term_manager -> sort -> string -> term
 
 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
@@ -116,17 +131,20 @@ external delete : solver -> unit = "ocaml_cvc5_stub_delete"
 
 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"
+[@@noalloc]
 
 external simplify : solver -> term -> term = "ocaml_cvc5_stub_simplify"
 
-external push : solver -> int -> unit = "ocaml_cvc5_stub_push"
+external push : solver -> int -> unit = "ocaml_cvc5_stub_push" [@@noalloc]
 
-external pop : solver -> int -> unit = "ocaml_cvc5_stub_pop"
+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;