Support for more regular expression operations (#275)

* Add new regexp operations

* Z3_mk_re_option typo?

* Attempt at testing Regexp

* Use from_str instead of new_const

z3-sys/src/lib.rs

@@ -3124,7 +3124,7 @@ extern "C" {
     /// Create the regular language `re*`.
     pub fn Z3_mk_re_star(c: Z3_context, re: Z3_ast) -> Z3_ast;
 
-    /// Create the regular language `[re]`.
+    /// Create the regular language `re?`.
     pub fn Z3_mk_re_option(c: Z3_context, re: Z3_ast) -> Z3_ast;
 
     /// Create the union of the regular languages.

z3/src/ast.rs

@@ -1825,6 +1825,17 @@ impl<'ctx> Regexp<'ctx> {
         }
     }
 
+    /// Creates a regular expression that recognizes this regular expression
+    /// n number of times
+    /// Requires Z3 4.8.15 or later.
+    pub fn power(&self, n: u32) -> Self {
+        unsafe {
+            Self::wrap(self.ctx, {
+                Z3_mk_re_power(self.ctx.z3_ctx, self.z3_ast, n)
+            })
+        }
+    }
+
     /// Creates a regular expression that recognizes all sequences
     pub fn full(ctx: &'ctx Context) -> Self {
         unsafe {
@@ -1837,6 +1848,19 @@ impl<'ctx> Regexp<'ctx> {
         }
     }
 
+    /// Creates a regular expression that accepts all singleton sequences of the characters
+    /// Requires Z3 4.8.13 or later.
+    pub fn allchar(ctx: &'ctx Context) -> Self {
+        unsafe {
+            Self::wrap(ctx, {
+                Z3_mk_re_allchar(
+                    ctx.z3_ctx,
+                    Z3_mk_re_sort(ctx.z3_ctx, Z3_mk_string_sort(ctx.z3_ctx)),
+                )
+            })
+        }
+    }
+
     /// Creates a regular expression that doesn't recognize any sequences
     pub fn empty(ctx: &'ctx Context) -> Self {
         unsafe {
@@ -1858,6 +1882,13 @@ impl<'ctx> Regexp<'ctx> {
        /// Creates a regular expression that recognizes any sequence that this regular expression
        /// doesn't
        complement(Z3_mk_re_complement, Self);
+       /// Creates a regular expression that optionally accepts this regular expression (e.g. `a?`)
+       option(Z3_mk_re_option, Self);
+    }
+    binop! {
+        /// Creates a difference regular expression
+        /// Requires Z3 4.8.14 or later.
+        diff(Z3_mk_re_diff, Self);
     }
     varop! {
        /// Concatenates regular expressions

z3/tests/lib.rs

@@ -1648,6 +1648,44 @@ fn test_regex_capital_foobar_intersect_az_plus_is_unsat() {
     assert!(solver.check() == SatResult::Unsat);
 }
 
+#[test]
+fn test_regex_union() {
+    let cfg = Config::new();
+    let ctx = &Context::new(&cfg);
+    let solver = Solver::new(ctx);
+    let a = ast::String::from_str(ctx, "a").unwrap();
+    let b = ast::String::from_str(ctx, "b").unwrap();
+    let c = ast::String::from_str(ctx, "c").unwrap();
+    let re = ast::Regexp::union(
+        ctx,
+        &[
+            ast::Regexp::literal(ctx, "a"),
+            ast::Regexp::literal(ctx, "b"),
+        ],
+    );
+    solver.assert(&a.regex_matches(&re));
+    solver.assert(&b.regex_matches(&re));
+    solver.assert(&c.regex_matches(&re).not());
+    assert!(solver.check() == SatResult::Sat);
+}
+
+#[test]
+fn test_regex_union2() {
+    let cfg = Config::new();
+    let ctx = &Context::new(&cfg);
+    let solver = Solver::new(ctx);
+    let c = ast::String::from_str(ctx, "c").unwrap();
+    let re = ast::Regexp::union(
+        ctx,
+        &[
+            ast::Regexp::literal(ctx, "a"),
+            ast::Regexp::literal(ctx, "b"),
+        ],
+    );
+    solver.assert(&c.regex_matches(&re));
+    assert!(solver.check() == SatResult::Unsat);
+}
+
 #[test]
 /// <https://github.com/Z3Prover/z3/blob/21e59f7c6e5033006265fc6bc16e2c9f023db0e8/examples/dotnet/Program.cs#L329-L370>
 fn test_array_example1() {