add mk_term with ops

cvc5.ml

@@ -43,6 +43,29 @@ module Sort = struct
   let mk_uninterpreted_sort = Cvc5_external.mk_uninterpreted_sort
 end
 
+module Op = struct
+  type op = Cvc5_external.op
+
+  let mk_op tm kind args = Cvc5_external.mk_op tm (Kind.to_cpp kind) args
+
+  let equal = Cvc5_external.op_equal
+
+  let delete = Cvc5_external.op_delete
+
+  let to_string = Cvc5_external.op_to_string
+
+  let is_indexed = Cvc5_external.op_is_indexed
+
+  (* let get_index = Cvc5_external.op_get_index *)
+
+  let kind o = Kind.of_cpp @@ Cvc5_external.op_get_kind o
+
+  let hash = Cvc5_external.op_hash
+
+  let get_num_indices = Cvc5_external.op_get_num_indices
+end
+
+
 module Term = struct
   type term = Cvc5_external.term
 
@@ -64,6 +87,9 @@ module Term = struct
 
   let mk_term (tm : TermManager.tm) (k : Kind.t) (terms : term array) =
     Cvc5_external.mk_term tm (Kind.to_cpp k) terms
+
+  let mk_term_op (tm : TermManager.tm) (op : Op.op) (terms : term array) =
+    Cvc5_external.mk_term_op tm op terms
 
   let mk_true = Cvc5_external.mk_true
 
@@ -191,26 +217,4 @@ module Solver = struct
   let get_unsat_core = Cvc5_external.solver_get_unsat_core
 
   let get_model = Cvc5_external.solver_get_model
-end
-
-module Op = struct
-  type op = Cvc5_external.op
-
-  let mk_op tm kind args = Cvc5_external.mk_op tm (Kind.to_cpp kind) args
-
-  let equal = Cvc5_external.op_equal
-
-  let delete = Cvc5_external.op_delete
-
-  let to_string = Cvc5_external.op_to_string
-
-  let is_indexed = Cvc5_external.op_is_indexed
-
-  let get_index = Cvc5_external.op_get_index
-
-  let kind o = Kind.of_cpp @@ Cvc5_external.op_get_kind o
-
-  let hash = Cvc5_external.op_hash
-
-  let get_num_indices = Cvc5_external.op_get_num_indices
-end
+end

cvc5.mli

@@ -41,6 +41,29 @@ module Sort : sig
   val mk_uninterpreted_sort : TermManager.tm -> string -> sort
 end
 
+module Op : sig
+  type op
+
+  val mk_op : TermManager.tm -> Kind.t -> int array -> op
+
+  val equal : op -> op -> bool
+
+  val to_string : op -> string
+
+  val delete : op -> unit
+
+  val is_indexed : op -> bool
+
+  (* val get_index : op -> int -> Term.term *)
+
+  val kind : op -> Kind.t
+
+  val hash : op -> int
+
+  val get_num_indices : op -> int
+end
+
+
 module Term : sig
   type term
 
@@ -62,6 +85,8 @@ module Term : sig
 
   val mk_term : TermManager.tm -> Kind.t -> term array -> term
 
+  val mk_term_op : TermManager.tm -> Op.op -> term array -> term
+
   val mk_true : TermManager.tm -> term
 
   val mk_false : TermManager.tm -> term
@@ -175,26 +200,4 @@ module Solver : sig
   val get_unsat_core : solver -> Term.term array
 
   val get_model : solver -> Sort.sort array -> Term.term array -> string
-end
-
-module Op : sig
-  type op
-
-  val mk_op : TermManager.tm -> Kind.t -> int array -> op
-
-  val equal : op -> op -> bool
-
-  val to_string : op -> string
-
-  val delete : op -> unit
-
-  val is_indexed : op -> bool
-
-  val get_index : op -> int -> Term.term
-
-  val kind : op -> Kind.t
-
-  val hash : op -> int
-
-  val get_num_indices : op -> int
-end
+end

cvc5_external.ml

@@ -108,6 +108,9 @@ external mk_fp :
 external mk_term : term_manager -> int -> term array -> term
   = "ocaml_cvc5_stub_mk_term"
 
+external mk_term_op : term_manager -> op -> term array -> term
+  = "ocaml_cvc5_stub_mk_term_with_op"
+
 external term_get_int_val : term -> string = "ocaml_cvc5_stub_get_int_value"
 
 external term_is_int_val : term -> bool = "ocaml_cvc5_stub_is_int_value"
@@ -203,7 +206,7 @@ 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
+external mk_roundingmode : term_manager -> int -> rounding_mode
   = "ocaml_cvc5_stub_mk_rounding_mode"
 
 external term_to_string : term -> string = "ocaml_cvc5_stub_term_to_string"

cvc5_stubs.cpp

@@ -435,6 +435,23 @@ CAMLprim value ocaml_cvc5_stub_mk_term(value v, value kind, value t){
   CVC5_TRY_CATCH_END;
 }
 
+CAMLprim value ocaml_cvc5_stub_mk_term_with_op(value v, value op, value t){
+  cvc5::TermManager* term_manager = TermManager_val(v);
+  value custom = Val_unit;
+  CVC5_TRY_CATCH_BEGIN;
+  std::vector<cvc5::Term> args;
+  size_t arity = Wosize_val(t);
+  args.reserve(arity);
+
+  for (size_t i = 0; i < arity; i++)
+    args.emplace_back(*Term_val(Field(t, i)));
+
+  new(&term_operations, &custom) 
+    Term(term_manager->mkTerm(*OP_val(op), args));
+  return custom;
+  CVC5_TRY_CATCH_END;
+}
+
 CAMLprim value ocaml_cvc5_stub_get_int_value(value t){
   CVC5_TRY_CATCH_BEGIN;
   return caml_copy_string(Term_val(t)->getIntegerValue().c_str());