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

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

10
import "smt-libv2.gen"
11
printer "smtv2"
12
import "no-bv.gen"
François Bobot's avatar
François Bobot committed
13
import "discrimination.gen"
14 15 16 17 18 19

transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
Clément Fumex's avatar
Clément Fumex committed
20
transformation "eliminate_literal"
21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37
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:
38 39
   CVC4 seems less efficient with its built-in implementation than
   with the axiomatic version
40
theory int.EuclideanDivision
41 42 43 44 45 46
  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
47 48
end
*)