drivers/z3_smtv1.drv

   1 (* Why driver for SMT syntax *)
   2
   3 prelude ";;; this is a prelude for Z3"
   4
   5 printer "smtv1"
   6 filename "%f-%t-%g.smt"
   7
   8 valid "^unsat"
   9 unknown "^\\(unknown\\|sat\\|Fail\\)" ""
  10 time "why3cpulimit time : %s s"
  11
  12
  13 (* Performed introductions depending on whether counterexamples are
  14    requested, as said by the meta "get_counterexmp". When this meta
  15    set, this transformation introduces the model variables that are
  16    still embedded in the goal. When it is not set, it removes all
  17    these unused-ce-related variables, even in the context.  *)
  18 transformation "counterexamples_dependent_intros"
  19
  20 transformation "inline_trivial"
  21 transformation "eliminate_builtin"
  22 transformation "eliminate_definition"
  23 transformation "eliminate_inductive"
  24 transformation "eliminate_epsilon"
  25 transformation "eliminate_algebraic"
  26 transformation "eliminate_literal"
  27
  28 transformation "simplify_formula"
  29 (*transformation "simplify_trivial_quantification"*)
  30
  31 transformation "encoding_smt"
  32
  33 theory BuiltIn
  34   syntax type int   "Int"
  35   syntax type real  "Real"
  36   syntax predicate (=)  "(= %1 %2)"
  37
  38   meta "encoding:kept" type int
  39 end
  40
  41 theory int.Int
  42
  43   prelude ";;; this is a prelude for Z3 integer arithmetic"
  44
  45   syntax function zero "0"
  46   syntax function one  "1"
  47
  48   syntax function (+)  "(+ %1 %2)"
  49   syntax function (-)  "(- %1 %2)"
  50   syntax function (*)  "(* %1 %2)"
  51   syntax function (-_) "(- %1)"
  52
  53   syntax predicate (<=) "(<= %1 %2)"
  54   syntax predicate (<)  "(< %1 %2)"
  55   syntax predicate (>=) "(>= %1 %2)"
  56   syntax predicate (>)  "(> %1 %2)"
  57
  58   remove prop MulComm.Comm
  59   remove prop MulAssoc.Assoc
  60   remove prop Unit_def_l
  61   remove prop Unit_def_r
  62   remove prop Inv_def_l
  63   remove prop Inv_def_r
  64   remove prop Assoc
  65   remove prop Mul_distr_l
  66   remove prop Mul_distr_r
  67   remove prop Comm
  68   remove prop Unitary
  69   remove prop Refl
  70   remove prop Trans
  71   remove prop Antisymm
  72   remove prop Total
  73   remove prop NonTrivialRing
  74   remove prop CompatOrderAdd
  75   remove prop ZeroLessOne
  76
  77 end
  78
  79
  80 theory real.Real
  81
  82   prelude ";;; this is a prelude for Z3 real arithmetic"
  83
  84   syntax function zero "0.0"
  85   syntax function one  "1.0"
  86
  87   syntax function (+)  "(+ %1 %2)"
  88   syntax function (-)  "(- %1 %2)"
  89   syntax function (*)  "(* %1 %2)"
  90   syntax function (/)  "(/ %1 %2)"
  91   syntax function (-_) "(- %1)"
  92   syntax function inv  "(/ 1.0 %1)"
  93
  94   syntax predicate (<=) "(<= %1 %2)"
  95   syntax predicate (<)  "(< %1 %2)"
  96   syntax predicate (>=) "(>= %1 %2)"
  97   syntax predicate (>)  "(> %1 %2)"
  98
  99   remove prop MulComm.Comm
 100   remove prop MulAssoc.Assoc
 101   remove prop Unit_def_l
 102   remove prop Unit_def_r
 103   remove prop Inv_def_l
 104   remove prop Inv_def_r
 105   remove prop Assoc
 106   remove prop Mul_distr_l
 107   remove prop Mul_distr_r
 108   remove prop Comm
 109   remove prop Unitary
 110   remove prop Inverse
 111   remove prop Refl
 112   remove prop Trans
 113   remove prop Antisymm
 114   remove prop Total
 115   remove prop NonTrivialRing
 116   remove prop CompatOrderAdd
 117   remove prop ZeroLessOne
 118
 119   meta "encoding:kept" type real
 120
 121 end
 122
 123 (*
 124 (* L'encodage des types sommes bloquent cette théorie builtin *)
 125
 126 theory Bool
 127   syntax type bool   "bool"
 128   syntax function True  "true"
 129   syntax function False "false"
 130
 131   meta "encoding_decorate:kept" type bool
 132 end
 133
 134 theory bool.Bool
 135   syntax function andb  "(and %1 %2)"
 136   syntax function orb   "(or %1 %2)"
 137   syntax function xorb  "(xor %1 %2)"
 138   syntax function notb  "(not %1)"
 139 end
 140 *)