(* Why3 drivers for PyRAT *)

prelude "(* This is the prelude for PyRAT *)"

(* additional regexp for detection of answers, needed for alt-ergo <= 0.99 *)
valid "^Inconsistent assumption$"


printer "pyrat"
filename "%f-%t-%g.why"

valid "^File \".*\", line [0-9]+, characters [0-9]+-[0-9]+:Valid"
invalid "^File \".*\", line [0-9]+, characters [0-9]+-[0-9]+:Invalid"
unknown "^File \".*\", line [0-9]+, characters [0-9]+-[0-9]+:I don't know" ""
timeout "^File \".*\", line [0-9]+, characters [0-9]+-[0-9]+:Timeout"
timeout "^Timeout$"
steplimitexceeded "^File \".*\", line [0-9]+, characters [0-9]+-[0-9]+:Steps limit reached"
outofmemory "Fatal error: out of memory"
outofmemory "Fatal error: exception Stack_overflow"
fail "typing error:\\(.*\\)$" "Failure : File generation error : \\1"
time "Valid (%s)"
time "Valid (%s)"
steps "Valid (\\([0-9]+.?[0-9]*\\)) (\\([0-9]+.?[0-9]*\\))" 2
steps "Valid (\\([0-9]+.?[0-9]*\\)) (\\([0-9]+.?[0-9]*\\) steps)" 2
time "why3cpulimit time : %s s"

transformation "inline_trivial"
transformation "introduce_premises"
transformation "eliminate_builtin"
transformation "simplify_formula"
transformation "caisar_native_prover"

theory BuiltIn
  syntax type int   "int"
  syntax type real  "real"

  syntax predicate (=)  "(%1 = %2)"

  meta "eliminate_algebraic" "keep_enums"
  meta "eliminate_algebraic" "keep_recs"

end

theory int.Int

  prelude "(* this is a prelude for Alt-Ergo integer arithmetic *)"

  syntax function zero "0"
  syntax function one  "1"

  syntax function (+)  "(%1 + %2)"
  syntax function (-)  "(%1 - %2)"
  syntax function (*)  "(%1 * %2)"
  syntax function (-_) "(-%1)"

  meta "invalid trigger" predicate (<=)
  meta "invalid trigger" predicate (<)
  meta "invalid trigger" predicate (>=)
  meta "invalid trigger" predicate (>)

  syntax predicate (<=) "(%1 <= %2)"
  syntax predicate (<)  "(%1 <  %2)"
  syntax predicate (>=) "(%1 >= %2)"
  syntax predicate (>)  "(%1 >  %2)"

  remove prop MulComm.Comm
  remove prop MulAssoc.Assoc
  remove prop Unit_def_l
  remove prop Unit_def_r
  remove prop Inv_def_l
  remove prop Inv_def_r
  remove prop Assoc
  remove prop Mul_distr_l
  remove prop Mul_distr_r
  remove prop Comm
  remove prop Unitary
  remove prop Refl
  remove prop Trans
  remove prop Total
  remove prop Antisymm
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
  remove prop ZeroLessOne

end

theory int.EuclideanDivision

  syntax function div "(%1 / %2)"
  syntax function mod "(%1 % %2)"

end

theory int.ComputerDivision

  use for_drivers.ComputerOfEuclideanDivision

end


theory real.Real

  prelude "(* this is a prelude for Alt-Ergo real arithmetic *)"

  syntax function zero "0.0"
  syntax function one  "1.0"

  syntax function (+)  "(%1 + %2)"
  syntax function (-)  "(%1 - %2)"
  syntax function (*)  "(%1 * %2)"
  syntax function (/)  "(%1 / %2)"
  syntax function (-_) "(-%1)"
  syntax function inv  "(1.0 / %1)"

  meta "invalid trigger" predicate (<=)
  meta "invalid trigger" predicate (<)
  meta "invalid trigger" predicate (>=)
  meta "invalid trigger" predicate (>)

  syntax predicate (<=) "(%1 <= %2)"
  syntax predicate (<)  "(%1 <  %2)"
  syntax predicate (>=) "(%1 >= %2)"
  syntax predicate (>)  "(%1 >  %2)"

  remove prop MulComm.Comm
  remove prop MulAssoc.Assoc
  remove prop Unit_def_l
  remove prop Unit_def_r
  remove prop Inv_def_l
  remove prop Inv_def_r
  remove prop Assoc
  remove prop Mul_distr_l
  remove prop Mul_distr_r
  remove prop Comm
  remove prop Unitary
  remove prop Refl
  remove prop Trans
  remove prop Total
  remove prop Antisymm
  remove prop Inverse
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
  remove prop ZeroLessOne

end

theory ieee_float.Float64

  syntax function (.+)  "(%1 + %2)"
  syntax function (.-)  "(%1 - %2)"
  syntax function (.*)  "(%1 * %2)"
  syntax function (./)  "(%1 / %2)"
  syntax function (.-_) "(-%1)"

  syntax predicate le "%1 <= %2"
  syntax predicate lt  "%1 <  %2"
  syntax predicate ge "%1 >= %2"
  syntax predicate gt  "%1 >  %2"


end

theory real.RealInfix

  syntax function (+.)  "(%1 + %2)"
  syntax function (-.)  "(%1 - %2)"
  syntax function ( *.) "(%1 * %2)"
  syntax function (/.)  "(%1 / %2)"
  syntax function (-._) "(-%1)"

  meta "invalid trigger" predicate (<=.)
  meta "invalid trigger" predicate (<.)
  meta "invalid trigger" predicate (>=.)
  meta "invalid trigger" predicate (>.)

  syntax predicate (<=.) "(%1 <= %2)"
  syntax predicate (<.)  "(%1 <  %2)"
  syntax predicate (>=.) "(%1 >= %2)"
  syntax predicate (>.)  "(%1 >  %2)"

end

theory Bool
  syntax type     bool  "bool"
  syntax function True  "true"
  syntax function False "false"
end

theory Tuple0
  syntax type     tuple0 "unit"
  syntax function Tuple0 "void"
end

theory algebra.AC
  meta AC function op
  remove prop Comm
  remove prop Assoc
end

theory HighOrd
  syntax type     (->) "(%1,%2) farray"
  syntax function (@)  "(%1[%2])"
end

theory map.Map
  syntax function get  "(%1[%2])"
  syntax function set  "(%1[%2 <- %3])"
end

theory ieee_float.Float64
  syntax predicate is_not_nan ""
  remove allprops
end