drivers/cvc5.drv

   1 (** Why3 driver for CVC5 1.0.0 *)
   2
   3 prelude ";; produced by cvc5.drv ;;"
   4 prelude "(set-logic ALL)"
   5 prelude "(set-info :smt-lib-version 2.6)"
   6
   7 unknown "^(error \"Can't get-info :reason-unknown when the last result wasn't unknown!\")$" "(not unknown!)"
   8
   9 outofmemory "cvc5 suffered a segfault"
  10 outofmemory "cvc5::internal::Minisat::OutOfMemoryException"
  11
  12 steps "resource::resourceUnitsUsed = \\([0-9]+\\)" 1
  13
  14 theory BuiltIn
  15   meta "supports_smt_get_info_unknown_reason" ""
  16 end
  17
  18 import "smt-libv2.gen"
  19 filename "%f-%t-%g.smt2"
  20 printer "smtv2.6"
  21 import "smt-libv2-bv.gen"
  22 import "cvc4_bv.gen"
  23 import "smt-libv2-floats.gen"
  24
  25 import "discrimination.gen"
  26 theory BuiltIn
  27   meta "select_alginst_default" "local"
  28   meta "eliminate_algebraic" "keep_mono"
  29 end
  30
  31 (* Performed introductions depending on whether counterexamples are
  32    requested, as said by the meta "get_counterexmp". When this meta
  33    set, this transformation introduces the model variables that are
  34    still embedded in the goal. When it is not set, it removes all
  35    these unused-ce-related variables, even in the context.  *)
  36 transformation "counterexamples_dependent_intros"
  37
  38 transformation "inline_trivial"
  39 transformation "eliminate_builtin"
  40 transformation "remove_unused_keep_constants"
  41 transformation "detect_polymorphism"
  42 transformation "eliminate_definition_conditionally"
  43 transformation "eliminate_inductive"
  44 transformation "eliminate_epsilon"
  45 transformation "eliminate_literal"
  46 transformation "simplify_formula"
  47
  48 (* Prepare for counter-example query: get rid of some quantifiers
  49    (makes it possible to query model values of the variables in
  50    premises) and introduce counter-example projections.  Note: does
  51    nothing if meta get_counterexmp is not set *)
  52 transformation "prepare_for_counterexmp"
  53
  54 transformation "eliminate_projections_sums"
  55 transformation "discriminate_if_poly"
  56 transformation "eliminate_algebraic_if_poly"
  57 transformation "encoding_smt_if_poly"
  58
  59 (** Error messages specific to CVC4 *)
  60
  61 outofmemory "(error \".*out of memory\")"
  62 outofmemory "CVC4 suffered a segfault"
  63 outofmemory "CVC4::BVMinisat::OutOfMemoryException"
  64 outofmemory "std::bad_alloc"
  65 outofmemory "Cannot allocate memory"
  66 timeout "interrupted by timeout"
  67 steps "smt::SmtEngine::resourceUnitsUsed, \\([0-9]+.?[0-9]*\\)" 1
  68 (*
  69 specific output message when CVC4 reaches its resource limit
  70 *)
  71 steplimitexceeded "unknown (RESOURCEOUT)"
  72
  73 theory real.Real
  74   remove prop add_div
  75   remove prop sub_div
  76   remove prop neg_div
  77   remove prop assoc_mul_div
  78   remove prop assoc_div_mul
  79   remove prop assoc_div_div
  80   remove prop CompatOrderMult
  81 end
  82
  83 (** Extra theories supported by CVC4 *)
  84
  85 (* CVC4 division seems to be the Euclidean one, not the Computer one *)
  86 theory int.EuclideanDivision
  87   syntax function div "(div %1 %2)"
  88   syntax function mod "(mod %1 %2)"
  89   remove prop Mod_bound
  90   remove prop Div_mod
  91   remove prop Mod_1
  92   remove prop Div_1
  93 end
  94
  95 (*
  96 theory int.ComputerDivision
  97   syntax function div "(div %1 %2)"
  98   syntax function mod "(mod %1 %2)"
  99   remove prop Mod_bound
 100   remove prop Div_mod
 101   remove prop Mod_1
 102   remove prop Div_1
 103 end
 104 *)