From b741263f47382c0218f17a3981deb6d8eae04d12 Mon Sep 17 00:00:00 2001 From: Andrew Brown <92134285+andrewj-brown@users.noreply.github.com> Date: Thu, 21 Aug 2025 13:44:46 +1000 Subject: [PATCH 1/4] working sygus interface! greatly increase CPU abuse dummy implementation (all returning TermManager) --- api/build_enums.cpp | 8 +- cvc5.ml | 36 ++++++ cvc5.mli | 36 ++++++ cvc5_external.ml | 42 +++++++ cvc5_stubs.cpp | 263 ++++++++++++++++++++++++++++++++++++++++++++ 5 files changed, 381 insertions(+), 4 deletions(-) diff --git a/api/build_enums.cpp b/api/build_enums.cpp index 7178349..0b9bacb 100644 --- a/api/build_enums.cpp +++ b/api/build_enums.cpp @@ -25,7 +25,7 @@ extern "C" void build_enums(){ ss << (Kind)i; std::string ln(ss.str()); std::string name(ln); - for (long unsigned int j = 1; j < name.length(); j += 1) + for (size_t j = 1; j < name.length(); j += 1) name[j] = std::tolower(name[j]); type_stream << " | " << name << std::endl; to_string_stream << @@ -55,7 +55,7 @@ extern "C" void build_enums(){ ss << (RoundingMode)i; std::string ln(ss.str()); std::string name(ln); - for (long unsigned int j = 1; j < name.length(); j += 1) + for (size_t j = 1; j < name.length(); j += 1) name[j] = std::tolower(name[j]); type_stream << " | " << name << std::endl; to_string_stream << @@ -85,7 +85,7 @@ extern "C" void build_enums(){ ss << (UnknownExplanation)i; std::string ln(ss.str()); std::string name(ln); - for (long unsigned int j = 1; j < name.length(); j += 1) + for (size_t j = 1; j < name.length(); j += 1) name[j] = std::tolower(name[j]); type_stream << " | " << name << std::endl; to_string_stream << @@ -100,4 +100,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; -} \ No newline at end of file +} diff --git a/cvc5.ml b/cvc5.ml index 5a4fb09..c8e2008 100644 --- a/cvc5.ml +++ b/cvc5.ml @@ -220,6 +220,26 @@ module Result = struct let is_unknown = Cvc5_external.result_is_unknown end +module Grammar = struct + type grammar = Cvc5_external.grammar + + let add_rules = Cvc5_external.grammar_add_rules +end + +module SynthResult = struct + type synthresult = Cvc5_external.synthresult + + let is_null = Cvc5_external.synth_is_null + + let has_solution = Cvc5_external.synth_has_solution + + let has_no_solution = Cvc5_external.synth_has_no_solution + + let is_unknown = Cvc5_external.synth_is_unknown + + let to_string = Cvc5_external.synth_to_string +end + module Solver = struct type solver = Cvc5_external.solver @@ -264,4 +284,20 @@ module Solver = struct let declare_fun = Cvc5_external.solver_declare_fun let define_fun = Cvc5_external.solver_define_fun + + let mk_grammar = Cvc5_external.solver_mk_grammar + + let synth_fun (a: solver) (b : TermManager.tm) (c : string) (d : Term.term array) (e : Sort.sort) (grammar : Grammar.grammar option) = match grammar with + | Some f -> Cvc5_external.solver_synth_fun_with_grammar a b c d e f + | None -> Cvc5_external.solver_synth_fun_no_grammar a b c d e + + let declare_sygus_var = Cvc5_external.solver_declare_sygus_var + + let add_sygus_constraint = Cvc5_external.solver_add_sygus_constraint + + let check_synth = Cvc5_external.solver_check_synth + + let get_synth_solution = Cvc5_external.solver_get_synth_solution + + let get_synth_solutions solver = Array.map (get_synth_solution solver) end diff --git a/cvc5.mli b/cvc5.mli index 679642f..a88f845 100644 --- a/cvc5.mli +++ b/cvc5.mli @@ -395,6 +395,26 @@ module Result : sig val is_unknown : result -> bool end +module Grammar : sig + type grammar + + val add_rules : grammar -> Term.term -> Term.term array -> unit +end + +module SynthResult : sig + type synthresult + + val is_null : synthresult -> bool + + val has_solution : synthresult -> bool + + val has_no_solution : synthresult -> bool + + val is_unknown : synthresult -> bool + + val to_string : synthresult -> string +end + module Solver : sig type solver @@ -485,4 +505,20 @@ module Solver : sig - The function body *) val define_fun : solver -> string -> Term.term array -> Sort.sort -> Term.term -> Term.term + + val mk_grammar : + solver -> Term.term array -> Term.term array -> Grammar.grammar + + val synth_fun : + solver -> TermManager.tm -> string -> Term.term array -> Sort.sort -> Grammar.grammar option -> Term.term + + val declare_sygus_var : solver -> string -> Sort.sort -> Term.term + + val add_sygus_constraint : solver -> Term.term -> unit + + val check_synth : solver -> SynthResult.synthresult + + val get_synth_solution : solver -> Term.term -> Term.term + + val get_synth_solutions : solver -> Term.term array -> Term.term array end diff --git a/cvc5_external.ml b/cvc5_external.ml index 0ee0f08..a15b94b 100644 --- a/cvc5_external.ml +++ b/cvc5_external.ml @@ -60,6 +60,8 @@ type block_model_mode = ptr type find_synth_target = ptr +type synthresult = 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" @@ -327,4 +329,44 @@ external mk_term_2 : term_manager -> int -> term -> term -> term external mk_term_3 : term_manager -> int -> term -> term -> term -> term = "ocaml_cvc5_stub_mk_term_3" +external solver_mk_grammar : solver -> term array -> term array -> grammar + = "ocaml_cvc5_stub_solver_mk_grammar" + +external solver_synth_fun_with_grammar : + solver -> term_manager -> string -> term array -> sort -> grammar -> term + = "ocaml_cvc5_stub_synth_fun_unpack" "ocaml_cvc5_stub_solver_synth_fun_grammar" + +external solver_synth_fun_no_grammar : solver -> term_manager -> string -> term array -> sort -> term + = "ocaml_cvc5_stub_solver_synth_fun" + +external solver_declare_sygus_var : solver -> string -> sort -> term + = "ocaml_cvc5_stub_solver_declare_sygus_var" + +external solver_add_sygus_constraint : solver -> term -> unit + = "ocaml_cvc5_stub_solver_add_sygus_constraint" + +external solver_check_synth : solver -> synthresult + = "ocaml_cvc5_stub_solver_check_synth" + +external solver_get_synth_solution : solver -> term -> term + = "ocaml_cvc5_stub_solver_get_synth_solution" + +external grammar_add_rules : grammar -> term -> term array -> unit + = "ocaml_cvc5_stub_grammar_add_rules" + +external synth_is_null : synthresult -> bool + = "ocaml_cvc5_stub_synthresult_is_null" + +external synth_has_solution : synthresult -> bool + = "ocaml_cvc5_stub_synthresult_has_solution" + +external synth_has_no_solution : synthresult -> bool + = "ocaml_cvc5_stub_synthresult_no_solution" + +external synth_is_unknown : synthresult -> bool + = "ocaml_cvc5_stub_synthresult_is_unknown" + +external synth_to_string : synthresult -> string + = "ocaml_cvc5_stub_synthresult_to_string" + (**/**) diff --git a/cvc5_stubs.cpp b/cvc5_stubs.cpp index 2db36b3..61a7a30 100644 --- a/cvc5_stubs.cpp +++ b/cvc5_stubs.cpp @@ -69,6 +69,31 @@ struct TermManagerHandle { cvc5::TermManager* tm; std::atomic rc; std::unordered_map const_map; + TermManager() : cvc5::TermManager() { + rc = 2; + termMap = new std::unordered_map(); + } + ~TermManager() {} + void * operator new(size_t size, + struct custom_operations *ops, + value *custom){ + *custom = caml_alloc_custom(ops, size, 0, 1); + return Data_custom_val(*custom); + } + void operator delete(void *ptr) {} + void addRef() { rc.fetch_add(1, std::memory_order_release); } + void addTerm(const std::string &key, cvc5::Term* term) { + termMap->emplace(key, term); + } + + cvc5::Term* getTerm(const std::string &key) const { + auto it = termMap->find(key); + if (it != termMap->end()) { + return it->second; + } + return nullptr; + } +>>>>>>> 573b291 (working sygus interface!) }; #define TermManager_val(v) ((*(TermManagerHandle **)Data_custom_val(v))->tm) @@ -149,6 +174,81 @@ static struct custom_operations term_operations = custom_fixed_length_default }; +/*============================================================================ + * Grammar + ============================================================================*/ + +class Grammar : public cvc5::Grammar { +public: + Grammar(cvc5::Grammar t) : cvc5::Grammar(t) {} + + ~Grammar() {} + + void * operator new(size_t size, + struct custom_operations *ops, + value *custom){ + *custom = caml_alloc_custom(ops, size, 0, 1); + return Data_custom_val(*custom); + } + void operator delete(void *ptr) {} +}; + +#define Grammar_val(v) ((Grammar*)Data_custom_val(v)) + +static void grammar_delete(value v){ + delete Grammar_val(v); +} + +static struct custom_operations grammar_operations = +{ + "https://cvc5.github.io/", + &grammar_delete, + custom_compare_default, + custom_hash_default, + custom_serialize_default, + custom_deserialize_default, + custom_compare_ext_default, + custom_fixed_length_default +}; + + +/*============================================================================ + * SynthResult + ============================================================================*/ + +class SynthResult : public cvc5::SynthResult { +public: + SynthResult(cvc5::SynthResult t) : cvc5::SynthResult(t) {} + ~SynthResult() {} + + void * operator new(size_t size, + struct custom_operations *ops, + value *custom){ + *custom = caml_alloc_custom(ops, size, 0, 1); + return Data_custom_val(*custom); + } + void operator delete(void *ptr) {} +}; + +#define Synthresult_val(v) ((SynthResult*)Data_custom_val(v)) + +static void synth_delete(value v) { + delete Synthresult_val(v); +} + +static struct custom_operations synthresult_operations = +{ + "https://cvc5.github.io/", + &synth_delete, + custom_compare_default, + custom_hash_default, + custom_serialize_default, + custom_deserialize_default, + custom_compare_ext_default, + custom_fixed_length_default +}; + + /*============================================================================ * Sort ============================================================================*/ @@ -1267,4 +1367,167 @@ CAMLprim value ocaml_cvc5_stub_op_delete(value v){ CVC5_TRY_CATCH_END; } +CAMLprim value ocaml_cvc5_stub_solver_mk_grammar(value s, value t1, value t2){ + CAMLparam3(s, t1, t2); + CAMLlocal1(custom); + cvc5::Solver* solver = Solver_val(s); + CVC5_TRY_CATCH_BEGIN; + + std::vector nonterminal_vec; + size_t arity1 = Wosize_val(t1); + nonterminal_vec.reserve(arity1); + for (size_t i = 0; i < arity1; i++) { + nonterminal_vec.emplace_back(*Term_val(Field(t1, i))); + } + + std::vector rules_vec; + size_t arity2 = Wosize_val(t2); + rules_vec.reserve(arity2); + for (size_t i = 0; i < arity2; i++) { + rules_vec.emplace_back(*Term_val(Field(t2, i))); + } + + new(&grammar_operations, &custom) + Grammar(solver->mkGrammar(nonterminal_vec, rules_vec)); + CAMLreturn(custom); + CVC5_TRY_CATCH_END; +} + +CAMLprim value ocaml_cvc5_stub_solver_synth_fun_grammar(value s, value tm, value name, value terms, value sort, value gram) { + CAMLparam5(s, name, terms, sort, gram); + CAMLlocal1(custom); + CVC5_TRY_CATCH_BEGIN; + + std::vector inputs; + size_t arity = Wosize_val(terms); + inputs.reserve(arity); + + for (size_t i = 0; i < arity; i++) { + inputs.emplace_back(*Term_val(Field(terms, i))); + } + + cvc5::Term fun = Solver_val(s)->synthFun(String_val(name), inputs, *(Sort_val(sort)), *(Grammar_val(gram))); + + new(&term_operations, &custom) Term(fun, TermManager_val(tm)); + + CAMLreturn(custom); + CVC5_TRY_CATCH_END; +} + +CAMLprim value ocaml_cvc5_stub_synth_fun_unpack(value* argv, int argc) { + return ocaml_cvc5_stub_solver_synth_fun_grammar(argv[0], argv[1], argv[2], argv[3], argv[4], argv[5]); +} + +CAMLprim value ocaml_cvc5_stub_solver_synth_fun(value s, value tm, value name, value terms, value sort) { + CAMLparam4(s, name, terms, sort); + CAMLlocal1(custom); + CVC5_TRY_CATCH_BEGIN; + + std::vector inputs; + size_t arity = Wosize_val(terms); + inputs.reserve(arity); + + for (size_t i = 0; i < arity; i++) { + inputs.emplace_back(*Term_val(Field(terms, i))); + } + + cvc5::Term fun = Solver_val(s)->synthFun(String_val(name), inputs, *(Sort_val(sort))); + + new(&term_operations, &custom) Term(fun, TermManager_val(tm)); + CAMLreturn(custom); + CVC5_TRY_CATCH_END; +} + +CAMLprim value ocaml_cvc5_stub_solver_declare_sygus_var(value s, value name, value sort) { + CAMLparam3(s, name, sort); + CAMLlocal1(custom); + CVC5_TRY_CATCH_BEGIN; + + cvc5::Term var = Solver_val(s)->declareSygusVar(String_val(name), *(Sort_val(sort))); + + new(&term_operations, &custom) Term(var, NULL); + CAMLreturn(custom); + CVC5_TRY_CATCH_END; +} + +CAMLprim value ocaml_cvc5_stub_solver_add_sygus_constraint(value s, value term) { + CAMLparam2(s, term); + CVC5_TRY_CATCH_BEGIN; + Solver_val(s)->addSygusConstraint(*(Term_val(term))); + CAMLreturn(Val_unit); + CVC5_TRY_CATCH_END; +} + +CAMLprim value ocaml_cvc5_stub_solver_check_synth(value s) { + CAMLparam1(s); + CAMLlocal1(custom); + CVC5_TRY_CATCH_BEGIN; + new(&synthresult_operations, &custom) SynthResult(Solver_val(s)->checkSynth()); + CAMLreturn(custom); + CVC5_TRY_CATCH_END; +} + +CAMLprim value ocaml_cvc5_stub_grammar_add_rules(value gram, value term, value terms) { + CAMLparam3(gram, term, terms); + Grammar* grammar = Grammar_val(gram); + CVC5_TRY_CATCH_BEGIN; + + std::vector rules; + size_t arity = Wosize_val(terms); + rules.reserve(arity); + + for (size_t i = 0; i < arity; i++) { + rules.emplace_back(*Term_val(Field(terms, i))); + } + + grammar->addRules(*Term_val(term), rules); + CAMLreturn(Val_unit); + CVC5_TRY_CATCH_END; +} + +CAMLprim value ocaml_cvc5_stub_solver_get_synth_solution(value s, value term) { + CAMLparam2(s, term); + CAMLlocal1(custom); + CVC5_TRY_CATCH_BEGIN; + cvc5::Term sol = Solver_val(s)->getSynthSolution(*(Term_val(term))); + new(&term_operations, &custom) Term(sol, NULL); + CAMLreturn(custom); + CVC5_TRY_CATCH_END; +} + +CAMLprim value ocaml_cvc5_stub_synthresult_is_null(value res) { + CAMLparam1(res); + CVC5_TRY_CATCH_BEGIN; + CAMLreturn(Val_bool(Synthresult_val(res)->isNull())); + CVC5_TRY_CATCH_END; +} + +CAMLprim value ocaml_cvc5_stub_synthresult_has_solution(value res) { + CAMLparam1(res); + CVC5_TRY_CATCH_BEGIN; + CAMLreturn(Val_bool(Synthresult_val(res)->hasSolution())); + CVC5_TRY_CATCH_END; +} + +CAMLprim value ocaml_cvc5_stub_synthresult_no_solution(value res) { + CAMLparam1(res); + CVC5_TRY_CATCH_BEGIN; + CAMLreturn(Val_bool(Synthresult_val(res)->hasNoSolution())); + CVC5_TRY_CATCH_END; +} + +CAMLprim value ocaml_cvc5_stub_synthresult_is_unknown(value res) { + CAMLparam1(res); + CVC5_TRY_CATCH_BEGIN; + CAMLreturn(Val_bool(Synthresult_val(res)->isUnknown())); + CVC5_TRY_CATCH_END; +} + +CAMLprim value ocaml_cvc5_stub_synthresult_to_string(value res) { + CAMLparam1(res); + CVC5_TRY_CATCH_BEGIN; + CAMLreturn(caml_copy_string(Synthresult_val(res)->toString().data())); + CVC5_TRY_CATCH_END; +} + } // extern "C" From 24a0830ee841567538a44012e0eaa85ecf1859e1 Mon Sep 17 00:00:00 2001 From: Andrew Brown <92134285+andrewj-brown@users.noreply.github.com> Date: Wed, 27 Aug 2025 16:12:34 +1000 Subject: [PATCH 2/4] formatting --- cvc5.ml | 8 +++++--- cvc5.mli | 8 +++++++- cvc5_external.ml | 8 +++++--- 3 files changed, 17 insertions(+), 7 deletions(-) diff --git a/cvc5.ml b/cvc5.ml index c8e2008..5bca5f5 100644 --- a/cvc5.ml +++ b/cvc5.ml @@ -287,9 +287,11 @@ module Solver = struct let mk_grammar = Cvc5_external.solver_mk_grammar - let synth_fun (a: solver) (b : TermManager.tm) (c : string) (d : Term.term array) (e : Sort.sort) (grammar : Grammar.grammar option) = match grammar with - | Some f -> Cvc5_external.solver_synth_fun_with_grammar a b c d e f - | None -> Cvc5_external.solver_synth_fun_no_grammar a b c d e + let synth_fun (a : solver) (b : TermManager.tm) (c : string) + (d : Term.term array) (e : Sort.sort) (grammar : Grammar.grammar option) = + match grammar with + | Some f -> Cvc5_external.solver_synth_fun_with_grammar a b c d e f + | None -> Cvc5_external.solver_synth_fun_no_grammar a b c d e let declare_sygus_var = Cvc5_external.solver_declare_sygus_var diff --git a/cvc5.mli b/cvc5.mli index a88f845..214686f 100644 --- a/cvc5.mli +++ b/cvc5.mli @@ -510,7 +510,13 @@ module Solver : sig solver -> Term.term array -> Term.term array -> Grammar.grammar val synth_fun : - solver -> TermManager.tm -> string -> Term.term array -> Sort.sort -> Grammar.grammar option -> Term.term + solver + -> TermManager.tm + -> string + -> Term.term array + -> Sort.sort + -> Grammar.grammar option + -> Term.term val declare_sygus_var : solver -> string -> Sort.sort -> Term.term diff --git a/cvc5_external.ml b/cvc5_external.ml index a15b94b..0113552 100644 --- a/cvc5_external.ml +++ b/cvc5_external.ml @@ -333,10 +333,12 @@ external solver_mk_grammar : solver -> term array -> term array -> grammar = "ocaml_cvc5_stub_solver_mk_grammar" external solver_synth_fun_with_grammar : - solver -> term_manager -> string -> term array -> sort -> grammar -> term - = "ocaml_cvc5_stub_synth_fun_unpack" "ocaml_cvc5_stub_solver_synth_fun_grammar" + solver -> term_manager -> string -> term array -> sort -> grammar -> term + = "ocaml_cvc5_stub_synth_fun_unpack" + "ocaml_cvc5_stub_solver_synth_fun_grammar" -external solver_synth_fun_no_grammar : solver -> term_manager -> string -> term array -> sort -> term +external solver_synth_fun_no_grammar : + solver -> term_manager -> string -> term array -> sort -> term = "ocaml_cvc5_stub_solver_synth_fun" external solver_declare_sygus_var : solver -> string -> sort -> term From 252a6cad4f35c6780f06c420671f594a42a262b4 Mon Sep 17 00:00:00 2001 From: Andrew Brown <92134285+andrewj-brown@users.noreply.github.com> Date: Thu, 4 Sep 2025 12:38:22 +1000 Subject: [PATCH 3/4] add binding for sygus assumptions --- cvc5.ml | 2 ++ cvc5.mli | 2 ++ cvc5_external.ml | 3 +++ cvc5_stubs.cpp | 8 ++++++++ 4 files changed, 15 insertions(+) diff --git a/cvc5.ml b/cvc5.ml index 5bca5f5..f153f5b 100644 --- a/cvc5.ml +++ b/cvc5.ml @@ -297,6 +297,8 @@ module Solver = struct let add_sygus_constraint = Cvc5_external.solver_add_sygus_constraint + let add_sygus_assume = Cvc5_external.solver_add_sygus_assume + let check_synth = Cvc5_external.solver_check_synth let get_synth_solution = Cvc5_external.solver_get_synth_solution diff --git a/cvc5.mli b/cvc5.mli index 214686f..90db2a8 100644 --- a/cvc5.mli +++ b/cvc5.mli @@ -522,6 +522,8 @@ module Solver : sig val add_sygus_constraint : solver -> Term.term -> unit + val add_sygus_assume : solver -> Term.term -> unit + val check_synth : solver -> SynthResult.synthresult val get_synth_solution : solver -> Term.term -> Term.term diff --git a/cvc5_external.ml b/cvc5_external.ml index 0113552..5126abe 100644 --- a/cvc5_external.ml +++ b/cvc5_external.ml @@ -347,6 +347,9 @@ external solver_declare_sygus_var : solver -> string -> sort -> term external solver_add_sygus_constraint : solver -> term -> unit = "ocaml_cvc5_stub_solver_add_sygus_constraint" +external solver_add_sygus_assume : solver -> term -> unit + = "ocaml_cvc5_stub_solver_add_sygus_assume" + external solver_check_synth : solver -> synthresult = "ocaml_cvc5_stub_solver_check_synth" diff --git a/cvc5_stubs.cpp b/cvc5_stubs.cpp index 61a7a30..209f5fa 100644 --- a/cvc5_stubs.cpp +++ b/cvc5_stubs.cpp @@ -1458,6 +1458,14 @@ CAMLprim value ocaml_cvc5_stub_solver_add_sygus_constraint(value s, value term) CVC5_TRY_CATCH_END; } +CAMLprim value ocaml_cvc5_stub_solver_add_sygus_assume(value s, value term) { + CAMLparam2(s, term); + CVC5_TRY_CATCH_BEGIN; + Solver_val(s)->addSygusAssume(*(Term_val(term))); + CAMLreturn(Val_unit); + CVC5_TRY_CATCH_END; +} + CAMLprim value ocaml_cvc5_stub_solver_check_synth(value s) { CAMLparam1(s); CAMLlocal1(custom); From 8c07f2fc3e1f78b508558d6014affdd7aa2f8a3b Mon Sep 17 00:00:00 2001 From: Andrew Brown <92134285+andrewj-brown@users.noreply.github.com> Date: Tue, 10 Feb 2026 10:37:41 +1000 Subject: [PATCH 4/4] fix rebase --- cvc5_stubs.cpp | 29 ++--------------------------- 1 file changed, 2 insertions(+), 27 deletions(-) diff --git a/cvc5_stubs.cpp b/cvc5_stubs.cpp index 209f5fa..ae5a66f 100644 --- a/cvc5_stubs.cpp +++ b/cvc5_stubs.cpp @@ -69,31 +69,6 @@ struct TermManagerHandle { cvc5::TermManager* tm; std::atomic rc; std::unordered_map const_map; - TermManager() : cvc5::TermManager() { - rc = 2; - termMap = new std::unordered_map(); - } - ~TermManager() {} - void * operator new(size_t size, - struct custom_operations *ops, - value *custom){ - *custom = caml_alloc_custom(ops, size, 0, 1); - return Data_custom_val(*custom); - } - void operator delete(void *ptr) {} - void addRef() { rc.fetch_add(1, std::memory_order_release); } - void addTerm(const std::string &key, cvc5::Term* term) { - termMap->emplace(key, term); - } - - cvc5::Term* getTerm(const std::string &key) const { - auto it = termMap->find(key); - if (it != termMap->end()) { - return it->second; - } - return nullptr; - } ->>>>>>> 573b291 (working sygus interface!) }; #define TermManager_val(v) ((*(TermManagerHandle **)Data_custom_val(v))->tm) @@ -1408,7 +1383,7 @@ CAMLprim value ocaml_cvc5_stub_solver_synth_fun_grammar(value s, value tm, value cvc5::Term fun = Solver_val(s)->synthFun(String_val(name), inputs, *(Sort_val(sort)), *(Grammar_val(gram))); - new(&term_operations, &custom) Term(fun, TermManager_val(tm)); + new(&term_operations, &custom) Term(fun, TermManager_handle_val(tm)); CAMLreturn(custom); CVC5_TRY_CATCH_END; @@ -1433,7 +1408,7 @@ CAMLprim value ocaml_cvc5_stub_solver_synth_fun(value s, value tm, value name, v cvc5::Term fun = Solver_val(s)->synthFun(String_val(name), inputs, *(Sort_val(sort))); - new(&term_operations, &custom) Term(fun, TermManager_val(tm)); + new(&term_operations, &custom) Term(fun, TermManager_handle_val(tm)); CAMLreturn(custom); CVC5_TRY_CATCH_END; }