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..f153f5b 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,24 @@ 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 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 + + let get_synth_solutions solver = Array.map (get_synth_solution solver) end diff --git a/cvc5.mli b/cvc5.mli index 679642f..90db2a8 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,28 @@ 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 add_sygus_assume : 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..5126abe 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,49 @@ 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_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" + +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..ae5a66f 100644 --- a/cvc5_stubs.cpp +++ b/cvc5_stubs.cpp @@ -149,6 +149,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 +1342,175 @@ 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_handle_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_handle_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_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); + 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"