Merge branch 'master' of https://github.com/z3prover/z3

src/api/ml/z3.ml

@@ -916,6 +916,12 @@ struct
 
   let mk_sort_s (ctx:context) (name:string) (constructors:Constructor.constructor list) =
     mk_sort ctx (Symbol.mk_string ctx name) constructors
+
+  let mk_sort_ref (ctx: context) (name:Symbol.symbol) =
+    Z3native.mk_datatype_sort ctx name
+
+  let mk_sort_ref_s (ctx: context) (name: string) =
+    mk_sort_ref ctx (Symbol.mk_string ctx name)
 
   let mk_sorts (ctx:context) (names:Symbol.symbol list) (c:Constructor.constructor list list) =
     let n = List.length names in
@@ -1260,7 +1266,9 @@ struct
   let mk_seq_replace = Z3native.mk_seq_replace
   let mk_seq_at = Z3native.mk_seq_at
   let mk_seq_length = Z3native.mk_seq_length
+  let mk_seq_nth = Z3native.mk_seq_nth
   let mk_seq_index = Z3native.mk_seq_index
+  let mk_seq_last_index = Z3native.mk_seq_last_index
   let mk_str_to_int = Z3native.mk_str_to_int
   let mk_str_le = Z3native.mk_str_le
   let mk_str_lt = Z3native.mk_str_lt

src/api/ml/z3.mli

@@ -1061,6 +1061,15 @@ sig
       if the corresponding sort reference is 0, then the value in sort_refs should be an index
       referring to one of the recursive datatypes that is declared. *)
   val mk_constructor_s : context -> string -> Symbol.symbol -> Symbol.symbol list -> Sort.sort option list -> int list -> Constructor.constructor
+
+  (* Create a forward reference to a recursive datatype being declared.
+     The forward reference can be used in a nested occurrence: the range of an array
+     or as element sort of a sequence. The forward reference should only be used when
+     used in an accessor for a recursive datatype that gets declared. *)
+  val mk_sort_ref : context -> Symbol.symbol -> Sort.sort
+
+  (* [mk_sort_ref_s ctx s] is [mk_sort_ref ctx (Symbol.mk_string ctx s)] *)
+  val mk_sort_ref_s : context -> string -> Sort.sort
 
   (** Create a new datatype sort. *)
   val mk_sort : context -> Symbol.symbol -> Constructor.constructor list -> Sort.sort
@@ -1858,7 +1867,7 @@ sig
 
   (** create regular expression sorts over sequences of the argument sort *)   
   val mk_re_sort : context -> Sort.sort -> Sort.sort
-
+  
   (** test if sort is a regular expression sort *)
   val is_re_sort : context -> Sort.sort -> bool
 
@@ -1906,10 +1915,17 @@ sig
 
   (** length of a sequence *)
   val mk_seq_length : context -> Expr.expr -> Expr.expr  
+
+  (** [mk_seq_nth ctx s index] retrieves from [s] the element at position [index]. 
+      The function is under-specified if the index is out of bounds. *)
+  val mk_seq_nth : context -> Expr.expr -> Expr.expr -> Expr.expr
 
   (** index of the first occurrence of the second argument in the first *)
   val mk_seq_index : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr 
 
+  (** [mk_seq_last_index ctx s substr] occurence of [substr] in the sequence [s] *)
+  val mk_seq_last_index : context -> Expr.expr -> Expr.expr -> Expr.expr
+
   (** retrieve integer expression encoded in string *)
   val mk_str_to_int : context -> Expr.expr -> Expr.expr
 

src/api/z3_api.h

@@ -3710,7 +3710,7 @@ extern "C" {
 
 
     /**
-       \brief Return index of first occurrence of \c substr in \c s starting from offset \c offset.
+       \brief Return index of the first occurrence of \c substr in \c s starting from offset \c offset.
        If \c s does not contain \c substr, then the value is -1, if \c offset is the length of \c s, then the value is -1 as well.
        The value is -1 if \c offset is negative or larger than the length of \c s.
 
@@ -3719,7 +3719,7 @@ extern "C" {
     Z3_ast Z3_API Z3_mk_seq_index(Z3_context c, Z3_ast s, Z3_ast substr, Z3_ast offset);
 
     /**
-       \brief Return the last occurrence of \c substr in \c s.
+       \brief Return index of the last occurrence of \c substr in \c s.
        If \c s does not contain \c substr, then the value is -1, 
        def_API('Z3_mk_seq_last_index', AST, (_in(CONTEXT), _in(AST), _in(AST)))
     */