drivers/z3_440.drv

   1 (** Why3 driver for Z3 >= 4.3.2 *)
   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"
  13 import "smt-libv2-bv.gen"
  14 import "z3_bv.gen"
  15 import "smt-libv2-floats.gen"
  16 import "discrimination.gen"
  17
  18 (* Performed introductions depending on whether counterexamples are
  19    requested, as said by the meta "get_counterexmp". When this meta
  20    set, this transformation introduces the model variables that are
  21    still embedded in the goal. When it is not set, it removes all
  22    these unused-ce-related variables, even in the context.  *)
  23 transformation "counterexamples_dependent_intros"
  24
  25 transformation "inline_trivial"
  26 transformation "eliminate_builtin"
  27 transformation "remove_unused_keep_constants"
  28 transformation "detect_polymorphism"
  29 transformation "eliminate_definition_conditionally"
  30 transformation "eliminate_inductive"
  31 transformation "eliminate_epsilon"
  32 transformation "eliminate_algebraic_if_poly"
  33 transformation "eliminate_literal"
  34
  35 transformation "simplify_formula"
  36 (*transformation "simplify_trivial_quantification"*)
  37
  38 (* Prepare for counter-example query: get rid of some quantifiers (makes it
  39 possible to query model values of the variables in premises) and introduce
  40 counter-example projections  *)
  41 transformation "prepare_for_counterexmp"
  42
  43 transformation "discriminate_if_poly"
  44 transformation "encoding_smt_if_poly"
  45
  46
  47 (** Error messages specific to Z3 *)
  48
  49 outofmemory "(error \".*out of memory\")"
  50 outofmemory "Failed to verify: pthread_create"
  51 outofmemory "std::bad_alloc"
  52 outofmemory "Resource temporarily unavailable"
  53 outofmemory "Cannot allocate memory"
  54 (* not convenient: is more a problem of fork
  55 outofmemory "error while loading shared libraries:.*failed to map segment from shared object"
  56 *)
  57 timeout "^timeout$"
  58 timeout "interrupted by timeout"
  59 steps ":rlimit-count +\\([0-9]+\\)" 1
  60 steplimitexceeded "Maximal allocation counts [0-9]+ have been exceeded"
  61
  62 (** Z3 needs "(push)" to provide models *)
  63 theory BuiltIn
  64   meta "counterexample_need_smtlib_push" ""
  65 end
  66
  67 (** Extra theories supported by Z3 *)
  68
  69 (* div/mod of Z3 seems to be Euclidean Division *)
  70 theory int.EuclideanDivision
  71   syntax function div "(div %1 %2)"
  72   syntax function mod "(mod %1 %2)"
  73   remove prop Mod_bound
  74   remove prop Div_mod
  75   remove prop Mod_1
  76   remove prop Div_1
  77 end
  78
  79 theory int.MinMax
  80   remove allprops
  81 end
  82
  83 theory real.FromInt
  84   syntax function from_int "(to_real %1)"
  85   remove prop Zero
  86   remove prop One
  87   remove prop Add
  88   remove prop Sub
  89   remove prop Mul
  90   remove prop Neg
  91 end
  92
  93 (* does not work: Z3 segfaults
  94 theory real.Trigonometry
  95
  96   syntax function cos "(cos %1)"
  97   syntax function sin "(sin %1)"
  98   syntax function pi "pi"
  99   syntax function tan "(tan %1)"
 100   syntax function atan "(atan %1)"
 101
 102 end
 103 *)
 104
 105 theory ieee_float.Float64
 106 (* check the sign bit; if pos |%1| else |%1| - 2^1025 *)
 107    syntax function to_int
 108      "(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)))))"
 109  (* we do not define of_int since z3 will not prove anything if it
 110     appears (05/01/2017) *)
 111 end
 112
 113 theory ieee_float.Float32
 114   (* check the sign bit; if pos |%1| else |%1| - 2^129 *)
 115    syntax function to_int
 116      "(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)))))"
 117 end
 118
 119 theory real.Square
 120   remove allprops
 121 end