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 transformation "inline_trivial"
  22 transformation "eliminate_builtin"
  23 transformation "remove_unused_keep_constants"
  24 transformation "detect_polymorphism"
  25 transformation "eliminate_definition_conditionally"
  26 transformation "eliminate_inductive"
  27 transformation "eliminate_epsilon"
  28 transformation "eliminate_algebraic_if_poly"
  29 transformation "eliminate_literal"
  30 transformation "simplify_formula"
  31
  32 (* Prepare for counter-example query: get rid of some quantifiers
  33    (makes it possible to query model values of the variables in
  34    premises) and introduce counter-example projections.  Note: does
  35    nothing if meta get_counterexmp is not set *)
  36 transformation "prepare_for_counterexmp"
  37
  38 transformation "discriminate_if_poly"
  39 transformation "encoding_smt_if_poly"
  40
  41 (** Error messages specific to CVC4 *)
  42
  43 outofmemory "(error \".*out of memory\")"
  44 outofmemory "CVC4 suffered a segfault"
  45 outofmemory "CVC4::BVMinisat::OutOfMemoryException"
  46 outofmemory "std::bad_alloc"
  47 outofmemory "Cannot allocate memory"
  48 timeout "interrupted by timeout"
  49 steps "smt::SmtEngine::resourceUnitsUsed, \\([0-9]+.?[0-9]*\\)" 1
  50 (*
  51 specific output message when CVC4 reaches its resource limit
  52 *)
  53 steplimitexceeded "unknown (RESOURCEOUT)"
  54
  55 theory int.Int
  56   remove prop CompatOrderMult
  57 end
  58
  59 theory real.Real
  60   remove prop add_div
  61   remove prop sub_div
  62   remove prop neg_div
  63   remove prop assoc_mul_div
  64   remove prop assoc_div_mul
  65   remove prop assoc_div_div
  66   remove prop CompatOrderMult
  67 end
  68
  69 (** Extra theories supported by CVC4 *)
  70
  71 (* CVC4 division seems to be the Euclidean one, not the Computer one *)
  72 theory int.EuclideanDivision
  73   syntax function div "(div %1 %2)"
  74   syntax function mod "(mod %1 %2)"
  75   remove prop Mod_bound
  76   remove prop Div_mod
  77   remove prop Mod_1
  78   remove prop Div_1
  79 end
  80
  81 (*
  82 theory int.ComputerDivision
  83   syntax function div "(div %1 %2)"
  84   syntax function mod "(mod %1 %2)"
  85   remove prop Mod_bound
  86   remove prop Div_mod
  87   remove prop Mod_1
  88   remove prop Div_1
  89 end
  90 *)