Add interface to cvc5 sygus bindings

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;
-}
+}

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

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

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"
+
 (**/**)