add character sort to Python API and allchar function to API for ease. #5500

src/api/api_ast.cpp

@@ -719,6 +719,9 @@ extern "C" {
         else if (fid == mk_c(c)->get_seq_fid() && k == RE_SORT) {
             return Z3_RE_SORT;
         }
+	else if (fid == mk_c(c)->get_char_fid() && k == CHAR_SORT) {
+            return Z3_SEQ_SORT;
+        }
         else {
             return Z3_UNKNOWN_SORT;
         }

src/api/api_context.cpp

@@ -98,6 +98,7 @@ namespace api {
         m_datalog_fid = m().mk_family_id("datalog_relation");
         m_fpa_fid   = m().mk_family_id("fpa");
         m_seq_fid   = m().mk_family_id("seq");
+	m_char_fid   = m().mk_family_id("char");
         m_special_relations_fid   = m().mk_family_id("specrels");
         m_dt_plugin = static_cast<datatype_decl_plugin*>(m().get_plugin(m_dt_fid));
     

src/api/api_context.h

@@ -104,6 +104,7 @@ namespace api {
         family_id                  m_pb_fid;
         family_id                  m_fpa_fid;
         family_id                  m_seq_fid;
+        family_id                  m_char_fid;
         family_id                  m_special_relations_fid;
         datatype_decl_plugin *     m_dt_plugin;
         
@@ -159,6 +160,7 @@ namespace api {
         family_id get_pb_fid() const { return m_pb_fid; }
         family_id get_fpa_fid() const { return m_fpa_fid; }
         family_id get_seq_fid() const { return m_seq_fid; }
+        family_id get_char_fid() const { return m_char_fid; }
         datatype_decl_plugin * get_dt_plugin() const { return m_dt_plugin; }
         family_id get_special_relations_fid() const { return m_special_relations_fid; }
 

src/api/api_seq.cpp

@@ -266,7 +266,8 @@ extern "C" {
     MK_NARY(Z3_mk_re_intersect, mk_c(c)->get_seq_fid(), OP_RE_INTERSECT, SKIP);
     MK_NARY(Z3_mk_re_concat, mk_c(c)->get_seq_fid(), OP_RE_CONCAT, SKIP);
     MK_BINARY(Z3_mk_re_range, mk_c(c)->get_seq_fid(), OP_RE_RANGE, SKIP);
-
+  
+    MK_SORTED(Z3_mk_re_allchar, mk_c(c)->sutil().re.mk_full_char);
     MK_SORTED(Z3_mk_re_empty, mk_c(c)->sutil().re.mk_empty);
     MK_SORTED(Z3_mk_re_full, mk_c(c)->sutil().re.mk_full_seq);
 

src/api/python/z3/z3.py

@@ -680,6 +680,8 @@ def _to_sort_ref(s, ctx):
         return ReSortRef(s, ctx)
     elif k == Z3_SEQ_SORT:
         return SeqSortRef(s, ctx)
+    elif k == Z3_CHAR_SORT:
+        return CharSortRef(s, ctx)
     return SortRef(s, ctx)
 
 
@@ -10574,6 +10576,10 @@ class SeqSortRef(SortRef):
     def basis(self):
         return _to_sort_ref(Z3_get_seq_sort_basis(self.ctx_ref(), self.ast), self.ctx)
 
+class CharSortRef(SortRef):
+    """Character sort."""
+    
+
 
 def StringSort(ctx=None):
     """Create a string sort
@@ -10584,6 +10590,15 @@ def StringSort(ctx=None):
     ctx = _get_ctx(ctx)
     return SeqSortRef(Z3_mk_string_sort(ctx.ref()), ctx)
 
+def CharSort(ctx=None):
+    """Create a character sort
+    >>> ch = CharSort()
+    >>> print(ch)
+    Char
+    """
+    ctx = _get_ctx(ctx)
+    return CharSortRef(Z3_mk_char_sort(ctx.ref()), ctx)
+
 
 def SeqSort(s):
     """Create a sequence sort over elements provided in the argument
@@ -11051,6 +11066,11 @@ def Range(lo, hi, ctx=None):
     hi = _coerce_seq(hi, ctx)
     return ReRef(Z3_mk_re_range(lo.ctx_ref(), lo.ast, hi.ast), lo.ctx)
 
+def AllChar(regex_sort, ctx=None):
+    """Create a regular expression that accepts all single character strings
+    """
+    return ReRef(Z3_mk_re_allchar(regex_sort.ctx_ref(), regex_sort.ast), regex_sort.ctx)
+
 # Special Relations
 
 

src/api/python/z3/z3printer.py

@@ -757,6 +757,8 @@ class Formatter:
             if s.is_string():
                 return to_format("String")
             return seq1("Seq", (self.pp_sort(s.basis()), ))
+        elif isinstance(s, z3.CharSortRef):
+            return to_format("Char")
         else:
             return to_format(s.name())
 

src/api/z3_api.h

@@ -161,6 +161,7 @@ typedef enum
     Z3_ROUNDING_MODE_SORT,
     Z3_SEQ_SORT,
     Z3_RE_SORT,
+    Z3_CHAR_SORT,
     Z3_UNKNOWN_SORT = 1000
 } Z3_sort_kind;
 
@@ -3724,6 +3725,14 @@ extern "C" {
      */
     Z3_ast Z3_API Z3_mk_re_range(Z3_context c, Z3_ast lo, Z3_ast hi);
 
+
+    /**
+       \brief Create a regular expression that accepts all singleton sequences of the regular expression sort
+
+      def_API('Z3_mk_re_allchar', AST, (_in(CONTEXT), _in(SORT)))
+    */
+    Z3_ast Z3_API Z3_mk_re_allchar(Z3_context c, Z3_sort regex_sort);
+  
     /**
        \brief Create a regular expression loop. The supplied regular expression \c r is repeated
        between \c lo and \c hi times. The \c lo should be below \c hi with one exception: when