(** Why3 driver for CVC4 >= 1.4 *) 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" import "smt-libv2-bv.gen" import "discrimination.gen" transformation "inline_trivial" transformation "eliminate_builtin" transformation "detect_polymorphism" 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) *) 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" steps "smt::SmtEngine::resourceUnitsUsed, \\([0-9]+.?[0-9]*\\)" 1 (** Unfortunately, there is no specific output message when CVC4 reaches its resource limit steplimitexceeded "??" *) (** Extra theories supported by CVC4 *) (* Disabled: CVC4 seems less efficient with its built-in implementation than with the axiomatic version *) (* 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 *) import "cvc4_bv.gen"