drivers/why3_smt.drv

   1 (* Why driver for Why3 syntax *)
   2
   3 printer "why3"
   4 filename "%f-%t-%g.why"
   5
   6 (* Performed introductions depending on whether counterexamples are
   7    requested, as said by the meta "get_counterexmp". When this meta
   8    set, this transformation introduces the model variables that are
   9    still embedded in the goal. When it is not set, it removes all
  10    these unused-ce-related variables, even in the context.  *)
  11 transformation "counterexamples_dependent_intros"
  12
  13 transformation "inline_trivial"
  14 transformation "eliminate_builtin"
  15 transformation "detect_polymorphism"
  16
  17 transformation "eliminate_definition"
  18 (* We could keep more definitions by using
  19    transformation "eliminate_definition_conditionally"
  20    instead, but some proofs are lost
  21    (examples/logic/triangle_inequality.why)
  22 *)
  23 transformation "eliminate_inductive"
  24 transformation "eliminate_epsilon"
  25
  26 transformation "simplify_formula"
  27 (*transformation "simplify_trivial_quantification"*)
  28
  29 transformation "eliminate_projections_sums"
  30 transformation "discriminate_if_poly"
  31 transformation "eliminate_algebraic_if_poly"
  32 transformation "encoding_smt_if_poly"
  33
  34 theory BuiltIn
  35   syntax type  int  "int"
  36   syntax type  real "real"
  37   syntax predicate (=)  "(%1 = %2)"
  38
  39   meta "encoding:kept" type int
  40   meta "encoding:kept" type real
  41   meta "encoding:ignore_polymorphism_ls" predicate (=)
  42 end
  43
  44 theory bool.Ite
  45   meta "encoding:lskept" function ite
  46   meta "encoding:ignore_polymorphism_ls" function ite
  47 end
  48
  49 theory HighOrd
  50   meta "encoding:lskept" function (@)
  51   meta "encoding:ignore_polymorphism_ts" type (->)
  52   meta "encoding:ignore_polymorphism_ls" function (@)
  53 end
  54
  55 theory map.Map
  56   meta "encoding:lskept" function get
  57   meta "encoding:lskept" function set
  58   meta "encoding:ignore_polymorphism_ls" function get
  59   meta "encoding:ignore_polymorphism_ls" function ([])
  60   meta "encoding:ignore_polymorphism_ls" function set
  61   meta "encoding:ignore_polymorphism_ls" function ([<-])
  62 end
  63
  64 import "discrimination.gen"
  65 theory BuiltIn
  66   meta "select_alginst_default" "local"
  67   meta "eliminate_algebraic" "keep_mono"
  68 end