drivers/cvc4_14.drv

   1 (** Why3 driver for CVC4 1.4 *)
   2
   3 prelude ";; produced by cvc4_14.drv ;;"
   4 prelude "(set-logic AUFBVDTNIRA)"
   5 (*
   6     A    : Array
   7     UF   : Uninterpreted Function
   8     BV   : BitVectors
   9     DT   : Datatypes
  10     NIRA : NonLinear Integer+Real Arithmetic
  11 *)
  12
  13 import "smt-libv2.gen"
  14 filename "%f-%t-%g.smt2"
  15 printer "smtv2"
  16 import "smt-libv2-bv.gen"
  17 import "cvc4_bv.gen"
  18 import "discrimination.gen"
  19
  20 (* Performed introductions depending on whether counterexamples are
  21    requested, as said by the meta "get_counterexmp". When this meta
  22    set, this transformation introduces the model variables that are
  23    still embedded in the goal. When it is not set, it removes all
  24    these unused-ce-related variables, even in the context.  *)
  25 transformation "counterexamples_dependent_intros"
  26
  27 transformation "inline_trivial"
  28 transformation "eliminate_builtin"
  29 transformation "detect_polymorphism"
  30 transformation "eliminate_definition"
  31 (* We could keep more definitions by using
  32    transformation "eliminate_definition_conditionally"
  33    instead, but some proofs are lost
  34    (examples/logic/triangle_inequality.why)
  35 *)
  36 transformation "eliminate_inductive"
  37 transformation "eliminate_epsilon"
  38 transformation "eliminate_algebraic_if_poly"
  39 transformation "eliminate_literal"
  40
  41 transformation "simplify_formula"
  42 (*transformation "simplify_trivial_quantification"*)
  43
  44 transformation "discriminate_if_poly"
  45 transformation "encoding_smt_if_poly"
  46
  47 (** Error messages specific to CVC4 *)
  48
  49 outofmemory "(error \".*out of memory\")"
  50 outofmemory "CVC4 suffered a segfault"
  51 outofmemory "CVC4::BVMinisat::OutOfMemoryException"
  52 outofmemory "std::bad_alloc"
  53 outofmemory "Cannot allocate memory"
  54 timeout "interrupted by timeout"
  55 steps "smt::SmtEngine::resourceUnitsUsed, \\([0-9]+.?[0-9]*\\)" 1
  56 (**
  57 Unfortunately, there is no specific output message when CVC4 (<1.6) reaches its resource limit
  58 steplimitexceeded "??"
  59 *)
  60
  61 (** Extra theories supported by CVC4 *)
  62
  63 (* Disabled:
  64    CVC4 seems less efficient with its built-in implementation than
  65    with the axiomatic version
  66 *)
  67 (*
  68 theory int.EuclideanDivision
  69   syntax function div "(div %1 %2)"
  70   syntax function mod "(mod %1 %2)"
  71   remove prop Mod_bound
  72   remove prop Div_mod
  73   remove prop Mod_1
  74   remove prop Div_1
  75 end
  76 *)