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 import "common-transformations.gen"
  26 transformation "detect_polymorphism"
  27 transformation "eliminate_definition_conditionally"
  28 transformation "eliminate_inductive"
  29 transformation "eliminate_epsilon"
  30 transformation "eliminate_algebraic_if_poly"
  31 transformation "eliminate_literal"
  32
  33 transformation "simplify_formula"
  34 (*transformation "simplify_trivial_quantification"*)
  35
  36 transformation "discriminate_if_poly"
  37 transformation "encoding_smt_if_poly"
  38
  39
  40 (** Error messages specific to Z3 *)
  41
  42 outofmemory "(error \".*out of memory\")"
  43 outofmemory "Failed to verify: pthread_create"
  44 outofmemory "std::bad_alloc"
  45 outofmemory "Resource temporarily unavailable"
  46 outofmemory "Cannot allocate memory"
  47 (* not convenient: is more a problem of fork
  48 outofmemory "error while loading shared libraries:.*failed to map segment from shared object"
  49 *)
  50 timeout "^timeout$"
  51 timeout "interrupted by timeout"
  52 steps ":rlimit-count +\\([0-9]+\\)" 1
  53 steplimitexceeded "Maximal allocation counts [0-9]+ have been exceeded"
  54
  55 (** Z3 needs "(push)" to provide models *)
  56 theory BuiltIn
  57   meta "counterexample_need_smtlib_push" ""
  58 end
  59
  60 (** Extra theories supported by Z3 *)
  61
  62 (* div/mod of Z3 seems to be Euclidean Division *)
  63 theory int.EuclideanDivision
  64   syntax function div "(div %1 %2)"
  65   syntax function mod "(mod %1 %2)"
  66   remove prop Mod_bound
  67   remove prop Div_mod
  68   remove prop Mod_1
  69   remove prop Div_1
  70 end
  71
  72 theory int.MinMax
  73   remove allprops
  74 end
  75
  76 theory real.FromInt
  77   syntax function from_int "(to_real %1)"
  78   remove prop Zero
  79   remove prop One
  80   remove prop Add
  81   remove prop Sub
  82   remove prop Mul
  83   remove prop Neg
  84 end
  85
  86 (* does not work: Z3 segfaults
  87 theory real.Trigonometry
  88
  89   syntax function cos "(cos %1)"
  90   syntax function sin "(sin %1)"
  91   syntax function pi "pi"
  92   syntax function tan "(tan %1)"
  93   syntax function atan "(atan %1)"
  94
  95 end
  96 *)
  97
  98 theory ieee_float.Float64
  99 (* check the sign bit; if pos |%1| else |%1| - 2^1025 *)
 100    syntax function to_int
 101      "(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)))))"
 102  (* we do not define of_int since z3 will not prove anything if it
 103     appears (05/01/2017) *)
 104 end
 105
 106 theory ieee_float.Float32
 107   (* check the sign bit; if pos |%1| else |%1| - 2^129 *)
 108    syntax function to_int
 109      "(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)))))"
 110 end
 111
 112 theory real.Square
 113   remove allprops
 114 end