drivers/z3_471.drv

   1 (** Why3 driver for Z3 >= 4.7.1 *)
   2
   3 import "z3_440.drv"
   4 import "smtlib-strings.gen"
   5
   6 theory string.RegExpr
   7
   8   syntax type re             "(RegEx String)"
   9
  10   syntax function to_re      "(str.to.re %1)"
  11   syntax predicate in_re     "(str.in.re %1 %2)"
  12
  13   syntax function concat     "(re.++ %1 %2)"
  14   syntax function union      "(re.union %1 %2)"
  15   syntax function inter      "(re.inter %1 %2)"
  16   syntax function star       "(re.* %1)"
  17   syntax function plus       "(re.+ %1)"
  18
  19   syntax function none       "re.nostr"
  20   syntax function allchar    "re.allchar"
  21
  22   syntax function opt        "(re.opt %1)"
  23   syntax function range      "(re.range %1 %2)"
  24   syntax function power      "(re.loop %2 %1 %1)"
  25   syntax function loop       "(re.loop %3 %1 %2)"
  26
  27 end