mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
48 lines
1.1 KiB
Plaintext
48 lines
1.1 KiB
Plaintext
(** Why3 driver for CVC5 1.0.0 with string support *)
|
|
|
|
prelude ";; produced by cvc5_strings.drv ;;"
|
|
|
|
import "cvc5.drv"
|
|
|
|
import "smtlib-strings.gen"
|
|
|
|
theory string.String
|
|
|
|
remove prop lt_empty
|
|
remove prop lt_not_com
|
|
remove prop lt_ref
|
|
remove prop lt_ref
|
|
remove prop lt_trans
|
|
remove prop le_empty
|
|
remove prop le_ref
|
|
remove prop lt_le
|
|
remove prop lt_le_eq
|
|
remove prop le_trans
|
|
remove prop replaceall_empty1
|
|
remove prop not_contains_replaceall
|
|
|
|
end
|
|
|
|
theory string.RegExpr
|
|
|
|
syntax type re "RegLan"
|
|
|
|
syntax function to_re "(str.to_re %1)"
|
|
syntax predicate in_re "(str.in_re %1 %2)"
|
|
|
|
syntax function concat "(re.++ %1 %2)"
|
|
syntax function union "(re.union %1 %2)"
|
|
syntax function inter "(re.inter %1 %2)"
|
|
syntax function star "(re.* %1)"
|
|
syntax function plus "(re.+ %1)"
|
|
|
|
syntax function none "re.none"
|
|
syntax function allchar "re.allchar"
|
|
|
|
syntax function opt "(re.opt %1)"
|
|
syntax function range "(re.range %1 %2)"
|
|
syntax function power "((_ re.^ %1) %2)"
|
|
syntax function loop "((_ re.loop %1 %2) %3)"
|
|
|
|
end
|