Skip to content

Commit

Permalink
add stubs for value interpretation
Browse files Browse the repository at this point in the history
joaomhmpereira committed Apr 8, 2024
1 parent b856a8f commit 939ad2e
Showing 4 changed files with 239 additions and 2 deletions.
40 changes: 40 additions & 0 deletions cvc5.ml
Original file line number Diff line number Diff line change
@@ -30,6 +30,8 @@ module Sort = struct

let mk_bv_sort = Cvc5_external.mk_bitvector_sort

let bv_size = Cvc5_external.sort_get_bv_size

let mk_rm_sort = Cvc5_external.get_rm_sort

let mk_fp_sort = Cvc5_external.mk_fp_sort
@@ -79,6 +81,44 @@ module Term = struct

let mk_rm (tm : TermManager.tm) (rm : RoundingMode.t) =
Cvc5_external.mk_roundingmode tm (RoundingMode.to_cpp rm)

let is_int = Cvc5_external.term_is_int_val

let is_real = Cvc5_external.term_is_real_val

let is_string = Cvc5_external.term_is_string_val

let is_bv = Cvc5_external.term_is_bv_val

let is_int32 = Cvc5_external.term_is_int32_val

let is_int64 = Cvc5_external.term_is_int64_val

let is_uint32 = Cvc5_external.term_is_uint32_val

let is_uint64 = Cvc5_external.term_is_uint64_val

let is_rm = Cvc5_external.term_is_rm_val

let is_bool = Cvc5_external.term_is_bool_val

let get_int t = int_of_string (Cvc5_external.term_get_int_val t)

let get_real t = float_of_string (Cvc5_external.term_get_real_val t)

let get_int32 = Cvc5_external.term_get_int32_val

let get_int64 = Cvc5_external.term_get_int64_val

let get_bv = Cvc5_external.term_get_bv_val

let get_uint32 = Cvc5_external.term_get_uint32_val

let get_uint64 = Cvc5_external.term_get_uint64_val

let get_rm t = RoundingMode.of_cpp @@ Cvc5_external.term_get_rm_val t

let get_bool = Cvc5_external.term_get_bool_val
end

module Result = struct
40 changes: 40 additions & 0 deletions cvc5.mli
Original file line number Diff line number Diff line change
@@ -28,6 +28,8 @@ module Sort : sig

val mk_bv_sort : TermManager.tm -> int -> sort

val bv_size : sort -> int32

val mk_rm_sort : TermManager.tm -> sort

val mk_fp_sort : TermManager.tm -> int -> int -> sort
@@ -75,6 +77,44 @@ module Term : sig
val mk_bv_s : TermManager.tm -> int -> string -> int -> term

val mk_rm : TermManager.tm -> RoundingMode.t -> term

val is_int : term -> bool

val is_real : term -> bool

val is_string : term -> bool

val is_bool : term -> bool

val is_int32 : term -> bool

val is_bv : term -> bool

val is_int64 : term -> bool

val is_uint32 : term -> bool

val is_uint64 : term -> bool

val is_rm : term -> bool

val get_int : term -> int

val get_real : term -> float

val get_bool : term -> bool

val get_int32 : term -> int32

val get_int64 : term -> int64

val get_uint32 : term -> int32

val get_uint64 : term -> int64

val get_bv : term -> int32 -> string

val get_rm : term -> RoundingMode.t
end

module Result : sig
61 changes: 59 additions & 2 deletions cvc5_external.ml
Original file line number Diff line number Diff line change
@@ -1,5 +1,3 @@
(* This file is automatically generated *)

(** External declarations for cvc5's OCaml bindings. *)

(**/**)
@@ -106,6 +104,62 @@ external mk_string : term_manager -> string -> term
external mk_term : term_manager -> int -> term array -> term
= "ocaml_cvc5_stub_mk_term"

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"
[@@noalloc]

external term_get_real_val : term -> string = "ocaml_cvc5_stub_get_real_value"

external term_is_real_val : term -> bool = "ocaml_cvc5_stub_is_real_value"
[@@noalloc]

external term_is_string_val : term -> bool = "ocaml_cvc5_stub_is_string_value"
[@@noalloc]

external term_is_int32_val : term -> bool = "ocaml_cvc5_stub_is_int32_value"
[@@noalloc]

external term_get_int32_val : term -> int32 = "ocaml_cvc5_stub_get_int32_value"
[@@noalloc]

external term_is_uint32_val : term -> bool = "ocaml_cvc5_stub_is_uint32_value"
[@@noalloc]

external term_get_uint32_val : term -> int32
= "ocaml_cvc5_stub_get_uint32_value"
[@@noalloc]

external term_is_int64_val : term -> bool = "ocaml_cvc5_stub_is_int64_value"
[@@noalloc]

external term_get_int64_val : term -> int64 = "ocaml_cvc5_stub_get_int64_value"
[@@noalloc]

external term_is_uint64_val : term -> bool = "ocaml_cvc5_stub_is_uint64_value"
[@@noalloc]

external term_get_uint64_val : term -> int64
= "ocaml_cvc5_stub_get_uint64_value"
[@@noalloc]

external term_is_bv_val : term -> bool = "ocaml_cvc5_stub_is_bv_value"
[@@noalloc]

external term_get_bv_val : term -> int32 -> string = "ocaml_cvc5_stub_get_bv_value"

external term_is_rm_val : term -> bool = "ocaml_cvc5_stub_is_rm_value"
[@@noalloc]

external term_get_rm_val : term -> int = "ocaml_cvc5_stub_get_rm_value"
[@@noalloc]

external term_is_bool_val : term -> bool = "ocaml_cvc5_stub_is_bool_value"
[@@noalloc]

external term_get_bool_val : term -> bool = "ocaml_cvc5_stub_get_bool_value"
[@@noalloc]

external get_boolean_sort : term_manager -> sort
= "ocaml_cvc5_stub_get_boolean_sort"

@@ -132,6 +186,9 @@ external mk_seq_sort : term_manager -> sort -> sort
external mk_uninterpreted_sort : term_manager -> string -> sort
= "ocaml_cvc5_stub_mk_uninterpreted_sort"

external sort_get_bv_size : sort -> int32 = "ocaml_cvc5_stub_sort_get_bv_size"
[@@noalloc]

external sort_to_string : sort -> string = "ocaml_cvc5_stub_sort_to_string"
[@@noalloc]

100 changes: 100 additions & 0 deletions cvc5_stubs.cpp
Original file line number Diff line number Diff line change
@@ -379,6 +379,100 @@ CAMLprim value ocaml_cvc5_stub_mk_term(value v, value kind, value t){
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());
CVC5_TRY_CATCH_END;
}

CAMLprim value ocaml_cvc5_stub_is_int_value(value t){
return Val_bool(Term_val(t)->isIntegerValue());
}

CAMLprim value ocaml_cvc5_stub_get_real_value(value t){
CVC5_TRY_CATCH_BEGIN;
return caml_copy_string(Term_val(t)->getRealValue().c_str());
CVC5_TRY_CATCH_END;
}

CAMLprim value ocaml_cvc5_stub_is_real_value(value t){
return Val_bool(Term_val(t)->isRealValue());
}

CAMLprim value ocaml_cvc5_stub_is_string_value(value t){
return Val_bool(Term_val(t)->isStringValue());
}

CAMLprim value ocaml_cvc5_stub_get_int32_value(value t){
CVC5_TRY_CATCH_BEGIN;
return caml_copy_int32(Term_val(t)->getInt32Value());
CVC5_TRY_CATCH_END;
}

CAMLprim value ocaml_cvc5_stub_is_int32_value(value t){
return Val_bool(Term_val(t)->isInt32Value());
}

CAMLprim value ocaml_cvc5_stub_get_int64_value(value t){
CVC5_TRY_CATCH_BEGIN;
return caml_copy_int64(Term_val(t)->getInt64Value());
CVC5_TRY_CATCH_END;
}

CAMLprim value ocaml_cvc5_stub_is_int64_value(value t){
return Val_bool(Term_val(t)->isInt64Value());
}

CAMLprim value ocaml_cvc5_stub_get_uint32_value(value t){
CVC5_TRY_CATCH_BEGIN;
return caml_copy_int32(Term_val(t)->getUInt32Value());
CVC5_TRY_CATCH_END;
}

CAMLprim value ocaml_cvc5_stub_is_uint32_value(value t){
return Val_bool(Term_val(t)->isUInt32Value());
}

CAMLprim value ocaml_cvc5_stub_get_uint64_value(value t){
CVC5_TRY_CATCH_BEGIN;
return caml_copy_int64(Term_val(t)->getUInt64Value());
CVC5_TRY_CATCH_END;
}

CAMLprim value ocaml_cvc5_stub_is_uint64_value(value t){
return Val_bool(Term_val(t)->isUInt64Value());
}

CAMLprim value ocaml_cvc5_stub_get_bv_value(value t, value base){
CVC5_TRY_CATCH_BEGIN;
return caml_copy_string(Term_val(t)->getBitVectorValue(Int32_val(base)).c_str());
CVC5_TRY_CATCH_END;
}

CAMLprim value ocaml_cvc5_stub_is_bv_value(value t){
return Val_bool(Term_val(t)->isBitVectorValue());
}

CAMLprim value ocaml_cvc5_stub_get_rm_value(value t){
CVC5_TRY_CATCH_BEGIN;
return Val_int((int)(Term_val(t)->getRoundingModeValue()));
CVC5_TRY_CATCH_END;
}

CAMLprim value ocaml_cvc5_stub_is_rm_value(value t){
return Val_bool(Term_val(t)->isRoundingModeValue());
}

CAMLprim value ocaml_cvc5_stub_is_bool_value(value t){
return Val_bool(Term_val(t)->isBooleanValue());
}

CAMLprim value ocaml_cvc5_stub_get_bool_value(value t){
CVC5_TRY_CATCH_BEGIN;
return Val_bool(Term_val(t)->getBooleanValue());
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;
@@ -449,6 +543,12 @@ CAMLprim value ocaml_cvc5_stub_get_rm_sort(value v){
CVC5_TRY_CATCH_END;
}

CAMLprim value ocaml_cvc5_stub_sort_get_bv_size(value v){
CVC5_TRY_CATCH_BEGIN;
return caml_copy_int32(Sort_val(v)->getBitVectorSize());
CVC5_TRY_CATCH_END;
}

CAMLprim value native_cvc5_stub_mk_fp_sort(value v, uint32_t exp, uint32_t sig){
cvc5::TermManager* term_manager = TermManager_val(v);
value custom = Val_unit;

0 comments on commit 939ad2e

Please sign in to comment.