cvc4.drv 1.05 KB
Newer Older
1
(** Why3 driver for CVC4 <= 1.3 *)
2

3
prelude "(set-logic AUFNIRA)"
4 5 6 7 8 9 10
(*
    A  : Array
    UF : Uninterpreted Function
    NIRA : NonLinear Integer Reals Arithmetic
*)

import "smt-libv2.drv"
François Bobot's avatar
François Bobot committed
11
import "discrimination.gen"
12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34

transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_epsilon"

transformation "simplify_formula"
(*transformation "simplify_trivial_quantification"*)

transformation "discriminate"
transformation "encoding_smt"

(** Error messages specific to CVC4 *)

outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
timeout "interrupted by timeout"


(** Extra theories supported by CVC4 *)

(* Disabled:
35 36
   CVC4 seems less efficient with its built-in implementation than
   with the axiomatic version
37 38 39 40 41 42 43 44 45
theory int.EuclideanDivision
   syntax function div "(div %1 %2)"
   syntax function mod "(mod %1 %2)"
   remove prop Mod_bound
   remove prop Div_mod
   remove prop Mod_1
   remove prop Div_1
end
*)