drivers/cvc4_15.drv

   1 (** Why3 driver for CVC4 1.5 *)
   2
   3 prelude ";; produced by cvc4_15.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_conditionally"
  31 transformation "eliminate_inductive"
  32 transformation "eliminate_epsilon"
  33 transformation "eliminate_algebraic_if_poly"
  34 transformation "eliminate_literal"
  35 transformation "simplify_formula"
  36
  37 transformation "discriminate_if_poly"
  38 transformation "encoding_smt_if_poly"
  39
  40 (** Error messages specific to CVC4 *)
  41
  42 outofmemory "(error \".*out of memory\")"
  43 outofmemory "CVC4 suffered a segfault"
  44 outofmemory "CVC4::BVMinisat::OutOfMemoryException"
  45 outofmemory "std::bad_alloc"
  46 outofmemory "Cannot allocate memory"
  47 timeout "interrupted by timeout"
  48 steps "smt::SmtEngine::resourceUnitsUsed, \\([0-9]+.?[0-9]*\\)" 1
  49 (**
  50 Unfortunately, there is no specific output message when CVC4 reaches its resource limit
  51 steplimitexceeded "??"
  52 *)
  53
  54 (** Extra theories supported by CVC4 *)
  55
  56 (* CVC4 division seems to be the Euclidean one, not the Computer one *)
  57 theory int.EuclideanDivision
  58   syntax function div "(div %1 %2)"
  59   syntax function mod "(mod %1 %2)"
  60   remove prop Mod_bound
  61   remove prop Div_mod
  62   remove prop Mod_1
  63   remove prop Div_1
  64 end
  65
  66 (*
  67 theory int.ComputerDivision
  68   syntax function div "(div %1 %2)"
  69   syntax function mod "(mod %1 %2)"
  70   remove prop Mod_bound
  71   remove prop Div_mod
  72   remove prop Mod_1
  73   remove prop Div_1
  74 end
  75 *)