cvc4_14.drv 1.63 KB
Newer Older
1
(** Why3 driver for CVC4 >= 1.4 *)
2 3 4 5 6 7 8 9 10 11 12 13 14 15

prelude "(set-logic AUFBVDTNIRA)"
(*
    A  : Array
    UF : Uninterpreted Function
    BV : BitVectors
    DT : Datatypes
    NIRA : NonLinear Integer Reals Arithmetic
*)
(* prelude "(set-logic ALL_SUPPORTED)"
   does not seem to include DT
*)

import "smt-libv2.drv"
16
import "smt-libv2-bv.gen"
17 18 19 20 21
import "discrimination.gen"

transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "detect_polymorphism"
22 23 24 25 26
transformation "eliminate_definition"
(* We could keep more definitions by using
   transformation "eliminate_definition_if_poly"
   instead, but some proofs are lost
   (examples/logic/triangle_inequality.why)
27
*)
28 29 30 31 32 33 34 35 36 37 38 39 40 41
transformation "eliminate_inductive"
transformation "eliminate_algebraic_if_poly"
transformation "eliminate_epsilon"

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

transformation "discriminate_if_poly"
transformation "encoding_smt_if_poly"

(** Error messages specific to CVC4 *)

outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
timeout "interrupted by timeout"
42
steps "smt::SmtEngine::resourceUnitsUsed, \\([0-9]+.?[0-9]*\\)" 1
43 44
(**
Unfortunately, there is no specific output message when CVC4 reaches its resource limit
45
steplimitexceeded "??"
46
*)
47 48 49 50

(** Extra theories supported by CVC4 *)

(* Disabled:
51 52
   CVC4 seems less efficient with its built-in implementation than
   with the axiomatic version
53 54
*)
(*
55
theory int.EuclideanDivision
56 57 58 59 60 61 62 63
   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
*)
64

65
import "cvc4_bv.gen"