drivers/z3_487.drv

   1 (** Why3 driver for Z3 >= 4.8.7 *)
   2
   3 (* Do not set any logic, let z3 choose by itself
   4    prelude "(set-logic AUFNIRA)"
   5 *)
   6
   7 (* Counterexamples: set model parser *)
   8 model_parser "smtv2"
   9
  10 import "smt-libv2.gen"
  11 filename "%f-%t-%g.smt2"
  12 printer "smtv2.6"
  13 import "smt-libv2-bv.gen"
  14 import "z3_bv.gen"
  15 import "smt-libv2-floats.gen"
  16 import "discrimination.gen"
  17 theory BuiltIn
  18   meta "select_alginst_default" "local"
  19   meta "eliminate_algebraic" "keep_mono"
  20 end
  21
  22 (* Performed introductions depending on whether counterexamples are
  23    requested, as said by the meta "get_counterexmp". When this meta
  24    set, this transformation introduces the model variables that are
  25    still embedded in the goal. When it is not set, it removes all
  26    these unused-ce-related variables, even in the context.  *)
  27 transformation "counterexamples_dependent_intros"
  28
  29 transformation "inline_trivial"
  30 transformation "eliminate_builtin"
  31 transformation "remove_unused_keep_constants"
  32 transformation "detect_polymorphism"
  33 transformation "eliminate_definition_conditionally"
  34 transformation "eliminate_inductive"
  35 transformation "eliminate_epsilon"
  36 transformation "eliminate_literal"
  37
  38 transformation "simplify_formula"
  39 (*transformation "simplify_trivial_quantification"*)
  40
  41 (* Prepare for counter-example query: get rid of some quantifiers (makes it
  42 possible to query model values of the variables in premises) and introduce
  43 counter-example projections  *)
  44 transformation "prepare_for_counterexmp"
  45
  46 transformation "eliminate_projections_sums"
  47 transformation "discriminate_if_poly"
  48 transformation "eliminate_algebraic_if_poly"
  49 transformation "encoding_smt_if_poly"
  50
  51
  52 (** Error messages specific to Z3 *)
  53
  54 outofmemory "(error \".*out of memory\")"
  55 outofmemory "Failed to verify: pthread_create"
  56 outofmemory "std::bad_alloc"
  57 outofmemory "Resource temporarily unavailable"
  58 outofmemory "Cannot allocate memory"
  59 (* not convenient: is more a problem of fork
  60 outofmemory "error while loading shared libraries:.*failed to map segment from shared object"
  61 *)
  62 timeout "^timeout$"
  63 timeout "interrupted by timeout"
  64 steps ":rlimit-count +\\([0-9]+\\)" 1
  65 steplimitexceeded "Maximal allocation counts [0-9]+ have been exceeded"
  66
  67 (** Z3 needs "(push)" to provide models *)
  68 theory BuiltIn
  69   meta "counterexample_need_smtlib_push" ""
  70 end
  71
  72 theory int.Int
  73   remove prop CompatOrderMult
  74 end
  75
  76 (** Extra theories supported by Z3 *)
  77
  78 (* div/mod of Z3 seems to be Euclidean Division *)
  79 theory int.EuclideanDivision
  80   syntax function div "(div %1 %2)"
  81   syntax function mod "(mod %1 %2)"
  82   remove prop Mod_bound
  83   remove prop Div_mod
  84   remove prop Mod_1
  85   remove prop Div_1
  86 end
  87
  88 theory int.MinMax
  89   remove allprops
  90 end
  91
  92 theory real.FromInt
  93   syntax function from_int "(to_real %1)"
  94   remove prop Zero
  95   remove prop One
  96   remove prop Add
  97   remove prop Sub
  98   remove prop Mul
  99   remove prop Neg
 100 end
 101
 102 (* does not work: Z3 segfaults
 103 theory real.Trigonometry
 104
 105   syntax function cos "(cos %1)"
 106   syntax function sin "(sin %1)"
 107   syntax function pi "pi"
 108   syntax function tan "(tan %1)"
 109   syntax function atan "(atan %1)"
 110
 111 end
 112 *)
 113
 114 theory ieee_float.Float64
 115 (* check the sign bit; if pos |%1| else |%1| - 2^1025 *)
 116    syntax function to_int
 117      "(ite (= ((_ extract 1024 1024) ((_ fp.to_sbv 1025) %1 %2)) #b0) (bv2int ((_ fp.to_sbv 1025) %1 %2)) (- (bv2int ((_ fp.to_sbv 1025) %1 %2)) (bv2int (bvshl (_ bv1 1026) (_ bv1025 1026)))))"
 118  (* we do not define of_int since z3 will not prove anything if it
 119     appears (05/01/2017) *)
 120 end
 121
 122 theory ieee_float.Float32
 123   (* check the sign bit; if pos |%1| else |%1| - 2^129 *)
 124    syntax function to_int
 125      "(ite (= ((_ extract 128 128) ((_ fp.to_sbv 129) %1 %2)) #b0) (bv2int ((_ fp.to_sbv 129) %1 %2)) (- (bv2int ((_ fp.to_sbv 129) %1 %2)) (bv2int (bvshl (_ bv1 130) (_ bv129 130)))))"
 126 end
 127
 128 theory real.Real
 129   remove prop add_div
 130   remove prop sub_div
 131   remove prop neg_div
 132   remove prop assoc_mul_div
 133   remove prop assoc_div_mul
 134   remove prop assoc_div_div
 135   remove prop CompatOrderMult
 136 end
 137
 138 theory real.Square
 139   remove allprops
 140 end
 141
 142 import "smtlib-strings.gen"
 143
 144 theory string.RegExpr
 145
 146   syntax type re             "(RegEx String)"
 147
 148   syntax function to_re      "(str.to.re %1)"
 149   syntax predicate in_re     "(str.in.re %1 %2)"
 150
 151   syntax function concat     "(re.++ %1 %2)"
 152   syntax function union      "(re.union %1 %2)"
 153   syntax function inter      "(re.inter %1 %2)"
 154   syntax function star       "(re.* %1)"
 155   syntax function plus       "(re.+ %1)"
 156
 157   syntax function none       "re.nostr"
 158   syntax function allchar    "re.allchar"
 159
 160   syntax function opt        "(re.opt %1)"
 161   syntax function range      "(re.range %1 %2)"
 162   syntax function power      "(re.loop %2 %1 %1)"
 163   syntax function loop       "(re.loop %3 %1 %2)"
 164
 165 end