drivers/cvc4.drv

   1 (** Why3 driver for CVC4 <= 1.3 *)
   2
   3 prelude "(set-logic AUFNIRA)"
   4 (*
   5     A  : Array
   6     UF : Uninterpreted Function
   7     NIRA : NonLinear Integer Reals Arithmetic
   8 *)
   9
  10 import "smt-libv2.gen"
  11 filename "%f-%t-%g.smt2"
  12 printer "smtv2"
  13 import "no-bv.gen"
  14 import "discrimination.gen"
  15
  16 (* Performed introductions depending on whether counterexamples are
  17    requested, as said by the meta "get_counterexmp". When this meta
  18    set, this transformation introduces the model variables that are
  19    still embedded in the goal. When it is not set, it removes all
  20    these unused-ce-related variables, even in the context.  *)
  21 transformation "counterexamples_dependent_intros"
  22
  23 transformation "inline_trivial"
  24 transformation "eliminate_builtin"
  25 transformation "eliminate_definition"
  26 transformation "eliminate_inductive"
  27 transformation "eliminate_epsilon"
  28 transformation "eliminate_algebraic"
  29 transformation "eliminate_literal"
  30
  31 transformation "simplify_formula"
  32 (*transformation "simplify_trivial_quantification"*)
  33
  34 transformation "discriminate"
  35 transformation "encoding_smt"
  36
  37 (** Error messages specific to CVC4 *)
  38
  39 outofmemory "(error \".*out of memory\")"
  40 outofmemory "CVC4 suffered a segfault"
  41 outofmemory "CVC4::BVMinisat::OutOfMemoryException"
  42 outofmemory "std::bad_alloc"
  43 outofmemory "Cannot allocate memory"
  44 timeout "interrupted by timeout"
  45
  46
  47 (** Extra theories supported by CVC4 *)
  48
  49 (* Disabled:
  50    CVC4 seems less efficient with its built-in implementation than
  51    with the axiomatic version
  52 theory int.EuclideanDivision
  53   syntax function div "(div %1 %2)"
  54   syntax function mod "(mod %1 %2)"
  55   remove prop Mod_bound
  56   remove prop Div_mod
  57   remove prop Mod_1
  58   remove prop Div_1
  59 end
  60 *)