Adding support for integer sets in the statics for patsolve_z3

contrib/SMT/Z3/CATS/z3.cats

@@ -110,6 +110,10 @@ atscntrb_Z3_dec_ref(ctx, ast) Z3_dec_ref(ctx, ast)
 
 /* ****** ****** */
 
+#include "z3_sets.cats"
+
+/* ****** ****** */
+
 #include "z3_quantifier.cats"
 
 /* ****** ****** */

contrib/SMT/Z3/CATS/z3_parsers.cats

@@ -0,0 +1,66 @@
+/***********************************************************************/
+/*                                                                     */
+/*                         Applied Type System                         */
+/*                                                                     */
+/***********************************************************************/
+
+/* (*
+** ATS/Postiats - Unleashing the Potential of Types!
+** Copyright (C) 2011-2012 Hongwei Xi, ATS Trustful Software, Inc.
+** All rights reserved
+**
+** ATS is free software;  you can  redistribute it and/or modify it under
+** the terms of the GNU LESSER GENERAL PUBLIC LICENSE as published by the
+** Free Software Foundation; either version 2.1, or (at your option)  any
+** later version.
+**
+** ATS is distributed in the hope that it will be useful, but WITHOUT ANY
+** WARRANTY; without  even  the  implied  warranty  of MERCHANTABILITY or
+** FITNESS FOR A PARTICULAR PURPOSE.  See the  GNU General Public License
+** for more details.
+**
+** You  should  have  received  a  copy of the GNU General Public License
+** along  with  ATS;  see the  file COPYING.  If not, please write to the
+** Free Software Foundation,  51 Franklin Street, Fifth Floor, Boston, MA
+** 02110-1301, USA.
+*) */
+
+/* ****** ****** */
+
+#ifndef Z3_Z3_PARSERS_CATS
+#define Z3_Z3_PARSERS_CATS
+
+/* ****** ****** */
+
+ATSinline()
+Z3_ast
+atscntrb_Z3_parse_smtlib2_string
+  (Z3_context c, Z3_string str,
+   unsigned num_sorts, Z3_symbol const sort_names[], Z3_sort const sorts[],
+   unsigned num_decls, Z3_symbol const decl_names[], Z3_func_decl const decls[] )
+{
+  return
+  atscntrb_Z3_inc_ref(c, 
+  	Z3_parse_smtlib2_string(c, str, num_sorts, sort_names, sorts, num_decls, decl_names, decls)); // end of [return]
+} // end of [atscntrb_Z3_mk_empty_set]
+
+
+ATSinline()
+Z3_ast
+atscntrb_Z3_parse_smtlib2_file
+  (Z3_context c, Z3_string file,
+   unsigned num_sorts, Z3_symbol const sort_names[], Z3_sort const sorts[],
+   unsigned num_decls, Z3_symbol const decl_names[], Z3_func_decl const decls[] )
+{
+  return
+  atscntrb_Z3_inc_ref(c, 
+  	Z3_parse_smtlib2_string(c, file, num_sorts, sort_names, sorts, num_decls, decl_names, decls)); // end of [return]
+} // end of [atscntrb_Z3_mk_empty_set]
+
+
+
+#endif // end of [Z3_Z3_PARSERS_CATS]
+
+/* ****** ****** */
+
+/* end of [z3_sets.cats] */

contrib/SMT/Z3/CATS/z3_sets.cats

@@ -0,0 +1,150 @@
+/***********************************************************************/
+/*                                                                     */
+/*                         Applied Type System                         */
+/*                                                                     */
+/***********************************************************************/
+
+/* (*
+** ATS/Postiats - Unleashing the Potential of Types!
+** Copyright (C) 2011-2012 Hongwei Xi, ATS Trustful Software, Inc.
+** All rights reserved
+**
+** ATS is free software;  you can  redistribute it and/or modify it under
+** the terms of the GNU LESSER GENERAL PUBLIC LICENSE as published by the
+** Free Software Foundation; either version 2.1, or (at your option)  any
+** later version.
+**
+** ATS is distributed in the hope that it will be useful, but WITHOUT ANY
+** WARRANTY; without  even  the  implied  warranty  of MERCHANTABILITY or
+** FITNESS FOR A PARTICULAR PURPOSE.  See the  GNU General Public License
+** for more details.
+**
+** You  should  have  received  a  copy of the GNU General Public License
+** along  with  ATS;  see the  file COPYING.  If not, please write to the
+** Free Software Foundation,  51 Franklin Street, Fifth Floor, Boston, MA
+** 02110-1301, USA.
+*) */
+
+/* ****** ****** */
+
+#ifndef Z3_Z3_SETS_CATS
+#define Z3_Z3_SETS_CATS
+
+/* ****** ****** */
+
+ATSinline()
+Z3_ast
+atscntrb_Z3_mk_empty_set
+  (Z3_context ctx, Z3_sort domain)
+{
+  return
+  atscntrb_Z3_inc_ref(
+    ctx, Z3_mk_empty_set(ctx, domain)
+  ) ; // end of [return]
+} // end of [atscntrb_Z3_mk_empty_set]
+
+
+ATSinline()
+Z3_ast
+atscntrb_Z3_mk_full_set 
+  (Z3_context ctx, Z3_sort domain)
+{
+	return atscntrb_Z3_inc_ref (
+		ctx, Z3_mk_full_set(ctx, domain)
+	);
+}
+
+ATSinline()
+Z3_ast
+atscntrb_Z3_mk_set_add 
+  (Z3_context ctx, Z3_ast set, Z3_ast elem)
+{
+	return atscntrb_Z3_inc_ref (
+		ctx, Z3_mk_set_add(ctx, set, elem)
+	);
+}
+
+ATSinline()
+Z3_ast
+atscntrb_Z3_mk_set_del 
+  (Z3_context ctx, Z3_ast set, Z3_ast elem)
+{
+	return atscntrb_Z3_inc_ref (
+		ctx, Z3_mk_set_del(ctx, set, elem)
+	);
+}
+
+ATSinline()
+Z3_ast
+atscntrb_Z3_mk_set_union 
+  (Z3_context ctx, Z3_ast a, Z3_ast b)
+{
+	Z3_ast all[2] = {a, b};
+	return
+	atscntrb_Z3_inc_ref (
+		ctx, Z3_mk_set_union(ctx, 2, all)
+	);
+}
+
+ATSinline()
+Z3_ast
+atscntrb_Z3_mk_set_intersect 
+  (Z3_context ctx, Z3_ast a, Z3_ast b)
+{
+	Z3_ast all[2] = {a, b};
+	return
+	atscntrb_Z3_inc_ref (
+		ctx, Z3_mk_set_intersect(ctx, 2, all)
+	);
+}
+
+ATSinline()
+Z3_ast
+atscntrb_Z3_mk_set_difference 
+  (Z3_context ctx, Z3_ast arg1, Z3_ast arg2)
+{
+	return
+	atscntrb_Z3_inc_ref (
+		ctx, Z3_mk_set_difference(ctx, arg1, arg2)
+	);
+}
+
+ATSinline()
+Z3_ast
+atscntrb_Z3_mk_set_complement 
+  (Z3_context ctx, Z3_ast arg)
+{
+	return
+	atscntrb_Z3_inc_ref (
+		ctx, Z3_mk_set_complement(ctx, arg)
+	);
+}
+
+ATSinline()
+Z3_ast
+atscntrb_Z3_mk_set_member 
+  (Z3_context ctx, Z3_ast elem, Z3_ast set)
+{
+	return
+	atscntrb_Z3_inc_ref (
+		ctx, Z3_mk_set_member(ctx, elem, set)
+	);
+}
+
+ATSinline()
+Z3_ast
+atscntrb_Z3_mk_set_subset 
+  (Z3_context ctx, Z3_ast arg1, Z3_ast arg2)
+{
+	return
+	atscntrb_Z3_inc_ref (
+		ctx, Z3_mk_set_subset(ctx, arg1, arg2)
+	);
+}
+/* ****** ****** */
+
+#endif // end of [Z3_Z3_SETS_CATS]
+
+/* ****** ****** */
+
+/* end of [z3_sets.cats] */

contrib/SMT/Z3/CATS/z3_sort.cats

@@ -71,6 +71,19 @@ atscntrb_Z3_mk_real_sort
 
 /* ****** ****** */
 
+ATSinline()
+Z3_sort
+atscntrb_Z3_mk_set_sort
+  (Z3_context ctx, Z3_sort domain)
+{
+  Z3_sort
+  ty = Z3_mk_set_sort(ctx, domain);
+  Z3_inc_ref(ctx, Z3_sort_to_ast(ctx, ty));
+  return ty;
+} // end of [atscntrb_Z3_mk_set_sort]
+
+/* ****** ****** */
+
 ATSinline()
 Z3_sort
 atscntrb_Z3_mk_uninterpreted_sort

contrib/SMT/Z3/SATS/z3.sats

@@ -217,6 +217,10 @@ fun Z3_interrupt (ctx: !Z3_context): void = "mac#%"
 
 (* ****** ****** *)
 
+#include "./z3_sets.sats"
+
+(* ****** ****** *)
+
 #include "./z3_bitvector.sats"
 
 (* ****** ****** *)

contrib/SMT/Z3/SATS/z3_parsers.sats

@@ -0,0 +1,72 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                         Applied Type System                         *)
+(*                                                                     *)
+(***********************************************************************)
+
+(*
+** ATS/Postiats - Unleashing the Potential of Types!
+** Copyright (C) 2011-2012 Hongwei Xi, ATS Trustful Software, Inc.
+** All rights reserved
+**
+** ATS is free software;  you can  redistribute it and/or modify it under
+** the terms of the GNU LESSER GENERAL PUBLIC LICENSE as published by the
+** Free Software Foundation; either version 2.1, or (at your option)  any
+** later version.
+**
+** ATS is distributed in the hope that it will be useful, but WITHOUT ANY
+** WARRANTY; without  even  the  implied  warranty  of MERCHANTABILITY or
+** FITNESS FOR A PARTICULAR PURPOSE.  See the  GNU General Public License
+** for more details.
+**
+** You  should  have  received  a  copy of the GNU General Public License
+** along  with  ATS;  see the  file COPYING.  If not, please write to the
+** Free Software Foundation,  51 Franklin Street, Fifth Floor, Boston, MA
+** 02110-1301, USA.
+*)
+
+(* ****** ****** *)
+
+(*
+** Start Time: February, 2016
+**
+** Author: Hanwen Wu
+** Authoremail: steinwaywhw AT gmail DOT com
+**
+** Author: William Blair 
+** Authoremail: wdblair AT bu DOT edu
+**
+** Author: Hongwei Xi
+** Authoremail: gmhwxi AT gmail DOT com
+*)
+
+(* ****** ****** *)
+//
+#ifndef
+ATSCNTRB_SMT_Z3_Z3_HEADER
+#include "./z3_header.sats"
+#endif // end of [ifndef]
+//
+(* ****** ****** *)
+
+fun
+Z3_parse_smtlib2_string {m,n:nat}
+(
+  ctx: !Z3_context, str: Z3_string, 
+  num_sort: uint m, sort_names: &(@[Z3_symbol][m]), sorts: &(@[Z3_sort][m]),
+  num_decl: uint n, decl_names: &(@[Z3_symbol][n]), decls: &(@[Z3_func_decl][n])
+): Z3_ast = "mac#%" // end-of-fun
+
+
+fun
+Z3_parse_smtlib2_file {m,n:nat}
+(
+  ctx: !Z3_context, file: Z3_string, 
+  num_sort: uint m, sort_names: &(@[Z3_symbol][m]), sorts: &(@[Z3_sort][m]),
+  num_decl: uint n, decl_names: &(@[Z3_symbol][n]), decls: &(@[Z3_func_decl][n])
+): Z3_ast = "mac#%" // end-of-fun
+
+
+(* ****** ****** *)
+
+(* end of [z3_parsers.sats] *)