drivers/cvc5_strings.drv

   1 (** Why3 driver for CVC5 1.0.0 with string support *)
   2
   3 prelude ";; produced by cvc5_strings.drv ;;"
   4
   5 import "cvc5.drv"
   6
   7 import "smtlib-strings.gen"
   8
   9 theory string.String
  10
  11   remove prop lt_empty
  12   remove prop lt_not_com
  13   remove prop lt_ref
  14   remove prop lt_ref
  15   remove prop lt_trans
  16   remove prop le_empty
  17   remove prop le_ref
  18   remove prop lt_le
  19   remove prop lt_le_eq
  20   remove prop le_trans
  21   remove prop replaceall_empty1
  22   remove prop not_contains_replaceall
  23
  24 end
  25
  26 theory string.RegExpr
  27
  28   syntax type re             "RegLan"
  29
  30   syntax function to_re      "(str.to_re %1)"
  31   syntax predicate in_re     "(str.in_re %1 %2)"
  32
  33   syntax function concat     "(re.++ %1 %2)"
  34   syntax function union      "(re.union %1 %2)"
  35   syntax function inter      "(re.inter %1 %2)"
  36   syntax function star       "(re.* %1)"
  37   syntax function plus       "(re.+ %1)"
  38
  39   syntax function none       "re.none"
  40   syntax function allchar    "re.allchar"
  41
  42   syntax function opt        "(re.opt %1)"
  43   syntax function range      "(re.range %1 %2)"
  44   syntax function power      "((_ re.^ %1) %2)"
  45   syntax function loop       "((_ re.loop %1 %2) %3)"
  46
  47 end