drivers/cvc4_16.gen

   1 (** Why3 driver for CVC4 >= 1.6 (with floating point support) *)
   2
   3 prelude ";; produced by cvc4_16.drv"
   4 prelude "(set-info :smt-lib-version 2.6)"
   5
   6 import "smt-libv2.gen"
   7 filename "%f-%t-%g.smt2"
   8 printer "smtv2.6"
   9 import "smt-libv2-bv.gen"
  10 import "cvc4_bv.gen"
  11 import "smt-libv2-floats.gen"
  12 import "discrimination.gen"
  13
  14 (* Performed introductions depending on whether counterexamples are
  15    requested, as said by the meta "get_counterexmp". When this meta
  16    set, this transformation introduces the model variables that are
  17    still embedded in the goal. When it is not set, it removes all
  18    these unused-ce-related variables, even in the context.  *)
  19 transformation "counterexamples_dependent_intros"
  20
  21 import "common-transformations.gen"
  22 transformation "detect_polymorphism"
  23 transformation "eliminate_definition_conditionally"
  24 transformation "eliminate_inductive"
  25 transformation "eliminate_epsilon"
  26 transformation "eliminate_algebraic_if_poly"
  27 transformation "eliminate_literal"
  28 transformation "simplify_formula"
  29
  30 transformation "discriminate_if_poly"
  31 transformation "encoding_smt_if_poly"
  32
  33 (** Error messages specific to CVC4 *)
  34
  35 outofmemory "(error \".*out of memory\")"
  36 outofmemory "CVC4 suffered a segfault"
  37 outofmemory "CVC4::BVMinisat::OutOfMemoryException"
  38 outofmemory "std::bad_alloc"
  39 outofmemory "Cannot allocate memory"
  40 timeout "interrupted by timeout"
  41 steps "smt::SmtEngine::resourceUnitsUsed, \\([0-9]+.?[0-9]*\\)" 1
  42 (*
  43 specific output message when CVC4 reaches its resource limit
  44 *)
  45 steplimitexceeded "unknown (RESOURCEOUT)"
  46
  47 theory int.Int
  48   remove prop CompatOrderMult
  49 end
  50
  51 theory real.Real
  52   remove prop add_div
  53   remove prop sub_div
  54   remove prop neg_div
  55   remove prop assoc_mul_div
  56   remove prop assoc_div_mul
  57   remove prop assoc_div_div
  58   remove prop CompatOrderMult
  59 end
  60
  61 (** Extra theories supported by CVC4 *)
  62
  63 (* CVC4 division seems to be the Euclidean one, not the Computer one *)
  64 theory int.EuclideanDivision
  65   syntax function div "(div %1 %2)"
  66   syntax function mod "(mod %1 %2)"
  67   remove prop Mod_bound
  68   remove prop Div_mod
  69   remove prop Mod_1
  70   remove prop Div_1
  71 end
  72
  73 (*
  74 theory int.ComputerDivision
  75   syntax function div "(div %1 %2)"
  76   syntax function mod "(mod %1 %2)"
  77   remove prop Mod_bound
  78   remove prop Div_mod
  79   remove prop Mod_1
  80   remove prop Div_1
  81 end
  82 *)