alt_ergo.drv 1.4 KB
Newer Older
1
(* Driver for Alt-Ergo version >= 0.95 *)
2

3
import "alt_ergo_common.drv"
4
import "no-bv.gen"
5

6
theory BuiltIn
7 8 9

  (* Alt-Ergo >= 0.95 supports enumerated datatypes and records *)

10
  meta "eliminate_algebraic" "keep_enums"
Andrei Paskevich's avatar
Andrei Paskevich committed
11
  meta "eliminate_algebraic" "keep_recs"
12

13 14
end

MARCHE Claude's avatar
MARCHE Claude committed
15

16 17
theory int.EuclideanDivision

18 19 20
  (* protection against wrong semantics for negative arguments
    last checked on 0.99.1: this is still needed
  *)
MARCHE Claude's avatar
MARCHE Claude committed
21

MARCHE Claude's avatar
MARCHE Claude committed
22 23
  prelude "logic safe_eucl_div: int, int -> int"
  prelude "axiom safe_eucl_div_def: forall x, y:int. x >= 0 and y > 0 -> safe_eucl_div(x,y) = x / y"
MARCHE Claude's avatar
MARCHE Claude committed
24

MARCHE Claude's avatar
MARCHE Claude committed
25 26
  prelude "logic safe_eucl_mod: int, int -> int"
  prelude "axiom safe_eucl_mod_def: forall x, y:int. x >= 0 and y > 0 -> safe_eucl_mod(x,y) = x % y"
MARCHE Claude's avatar
MARCHE Claude committed
27

MARCHE Claude's avatar
MARCHE Claude committed
28 29
  syntax function div "safe_eucl_div(%1,%2)"
  syntax function mod "safe_eucl_mod(%1,%2)"
MARCHE Claude's avatar
MARCHE Claude committed
30 31 32 33 34

end

theory int.ComputerDivision

35 36 37
  (* protection against wrong semantics for negative arguments
     last checked on 0.99.1: this is still needed
  *)
MARCHE Claude's avatar
MARCHE Claude committed
38

MARCHE Claude's avatar
MARCHE Claude committed
39 40
  prelude "logic safe_comp_div: int, int -> int"
  prelude "axiom safe_comp_div_def: forall x, y:int. x >= 0 and y > 0 -> safe_comp_div(x,y) = x / y"
MARCHE Claude's avatar
MARCHE Claude committed
41

MARCHE Claude's avatar
MARCHE Claude committed
42 43
  prelude "logic safe_comp_mod: int, int -> int"
  prelude "axiom safe_comp_mod_def: forall x, y:int. x >= 0 and y > 0 -> safe_comp_mod(x,y) = x % y"
MARCHE Claude's avatar
MARCHE Claude committed
44

MARCHE Claude's avatar
MARCHE Claude committed
45 46
  syntax function div "safe_comp_div(%1,%2)"
  syntax function mod "safe_comp_mod(%1,%2)"
47 48 49

end

50 51

(*
52
Local Variables:
53
mode: why
54
compile-command: "make -C .. bench"
55
End:
56
*)