Commits

Arlen Cox  committed c35f237

Fixing missing routines. Some parsing routines appear to have been removed from Z3 and they were still in the OCaml bindings.

  • Participants
  • Parent commits a60ab1c

Comments (0)

Files changed (4)

File src/api/ml/Makefile

 	@echo "linkopts=\"-cclib -lz3caml -cclib -lz3 -cclib -L$(OCAML_LOC) -cclib -lcamlidl -cclib -fopenmp\"" >> META
 
 clean :
-	-rm -rf META $(LIBS) z3_theory_stubs.o z3_stubs.o
+	-rm -rf META $(LIBS) z3_theory_stubs.o z3_stubs.o z3caml.a z3caml.cmxa z3caml.cma
 
 remove uninstall :
 	$(OCAMLFIND) remove z3

File src/api/ml/z3.ml

 external get_smtlib_error : context -> string
 	= "camlidl_z3_Z3_get_smtlib_error"
 
-external parse_z3_string : context -> string -> ast
-	= "camlidl_z3_Z3_parse_z3_string"
-
-external parse_z3_file : context -> string -> ast
-	= "camlidl_z3_Z3_parse_z3_file"
-
 external set_error : context -> error_code -> unit
 	= "camlidl_z3_Z3_set_error"
 
 external get_smtlib_error : context -> string
 	= "camlidl_z3V3_Z3_get_smtlib_error"
 
-external parse_z3_string : context -> string -> ast
-	= "camlidl_z3_Z3_parse_z3V3_string"
-
-external parse_z3_file : context -> string -> ast
-	= "camlidl_z3_Z3_parse_z3V3_file"
-
 external get_version : unit -> int * int * int * int
 	= "camlidl_z3V3_Z3_get_version"
 

File src/api/ml/z3.mli

 	= "camlidl_z3_Z3_get_smtlib_error"
 
 *)
-(**
-       Summary: \[ [ parse_z3_string c str ] \]
-       Parse the given string using the Z3 native parser.
-       
-       Return the conjunction of asserts made in the input.
-
-       def_API('parse_z3_string', AST, (_in(CONTEXT), _in(STRING)))
-*)
-external parse_z3_string : context -> string -> ast
-	= "camlidl_z3_Z3_parse_z3_string"
-
-(**
-       Summary: Similar to {!parse_z3_string}, but reads the benchmark from a file.
-
-       def_API('parse_z3_file', AST, (_in(CONTEXT), _in(STRING)))
-*)
-external parse_z3_file : context -> string -> ast
-	= "camlidl_z3_Z3_parse_z3_file"
 
 (**
        {2 {L Error Handling}}
 	= "camlidl_z3V3_Z3_get_smtlib_error"
 
 (**
-       Summary: \[ [ parse_z3_string c str ] \]
-       Parse the given string using the Z3 native parser.
-       
-       Return the conjunction of asserts made in the input.
-
-       def_API('parse_z3_string', AST, (_in(CONTEXT), _in(STRING)))
-*)
-external parse_z3_string : context -> string -> ast
-	= "camlidl_z3_Z3_parse_z3V3_string"
-
-(**
-       Summary: Similar to {!parse_z3_string}, but reads the benchmark from a file.
-
-       def_API('parse_z3_file', AST, (_in(CONTEXT), _in(STRING)))
-*)
-external parse_z3_file : context -> string -> ast
-	= "camlidl_z3_Z3_parse_z3V3_file"
-
-(**
        {2 {L Miscellaneous}}
 *)
 (**

File src/api/ml/z3_stubs.c

   return _vres;
 }
 
-value camlidl_z3_Z3_parse_z3_string(
-	value _v_c,
-	value _v_str)
-{
-  Z3_context c; /*in*/
-  Z3_string str; /*in*/
-  Z3_ast _res;
-  value _vres;
-
-  struct camlidl_ctx_struct _ctxs = { CAMLIDL_TRANSIENT, NULL };
-  camlidl_ctx _ctx = &_ctxs;
-  camlidl_ml2c_z3_Z3_context(_v_c, &c, _ctx);
-  camlidl_ml2c_z3_Z3_string(_v_str, &str, _ctx);
-  _res = Z3_parse_z3_string(c, str);
-  _vres = camlidl_c2ml_z3_Z3_ast(&_res, _ctx);
-  camlidl_free(_ctx);
-  /* begin user-supplied deallocation sequence */
-check_error_code(c);
-  /* end user-supplied deallocation sequence */
-  return _vres;
-}
-
-value camlidl_z3_Z3_parse_z3_file(
-	value _v_c,
-	value _v_file_name)
-{
-  Z3_context c; /*in*/
-  Z3_string file_name; /*in*/
-  Z3_ast _res;
-  value _vres;
-
-  struct camlidl_ctx_struct _ctxs = { CAMLIDL_TRANSIENT, NULL };
-  camlidl_ctx _ctx = &_ctxs;
-  camlidl_ml2c_z3_Z3_context(_v_c, &c, _ctx);
-  camlidl_ml2c_z3_Z3_string(_v_file_name, &file_name, _ctx);
-  _res = Z3_parse_z3_file(c, file_name);
-  _vres = camlidl_c2ml_z3_Z3_ast(&_res, _ctx);
-  camlidl_free(_ctx);
-  /* begin user-supplied deallocation sequence */
-check_error_code(c);
-  /* end user-supplied deallocation sequence */
-  return _vres;
-}
-
 value camlidl_z3_Z3_set_error(
 	value _v_c,
 	value _v_e)
   return _vres;
 }
 
-value camlidl_z3_Z3_parse_z3V3_string(
-	value _v_c,
-	value _v_str)
-{
-  Z3_context c; /*in*/
-  Z3_string str; /*in*/
-  Z3_ast _res;
-  value _vres;
-
-  struct camlidl_ctx_struct _ctxs = { CAMLIDL_TRANSIENT, NULL };
-  camlidl_ctx _ctx = &_ctxs;
-  camlidl_ml2c_z3V3_Z3_context(_v_c, &c, _ctx);
-  camlidl_ml2c_z3V3_Z3_string(_v_str, &str, _ctx);
-  _res = Z3_parse_z3_string(c, str);
-  _vres = camlidl_c2ml_z3V3_Z3_ast(&_res, _ctx);
-  camlidl_free(_ctx);
-  return _vres;
-}
-
-value camlidl_z3_Z3_parse_z3V3_file(
-	value _v_c,
-	value _v_file_name)
-{
-  Z3_context c; /*in*/
-  Z3_string file_name; /*in*/
-  Z3_ast _res;
-  value _vres;
-
-  struct camlidl_ctx_struct _ctxs = { CAMLIDL_TRANSIENT, NULL };
-  camlidl_ctx _ctx = &_ctxs;
-  camlidl_ml2c_z3V3_Z3_context(_v_c, &c, _ctx);
-  camlidl_ml2c_z3V3_Z3_string(_v_file_name, &file_name, _ctx);
-  _res = Z3_parse_z3_file(c, file_name);
-  _vres = camlidl_c2ml_z3V3_Z3_ast(&_res, _ctx);
-  camlidl_free(_ctx);
-  return _vres;
-}
-
 value camlidl_z3V3_Z3_get_version(value _unit)
 {
   unsigned int *major; /*out*/