simplify.drv 1.79 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23

(* Why driver for Simplify *)

prelude ";;; this is a prelude for Simplify"

printer "simplify"
filename "%f-%t-%g.sx"

valid "\\bValid\\b"
unknown "\\bInvalid\\b" "Unknown"

transformation "simplify_recursive_definition"      
transformation "inline_trivial"

transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_if"
transformation "eliminate_let"
transformation "simplify_formula"
transformation "simplify_trivial_quantification"

24 25 26 27 28 29
transformation "filter_trigger_no_predicate"
(* predicate are *currently* translated to P(\x) = true, thus in a
trigger they can't appear since = can't appear *)
(*transformation "filter_trigger_builtin"*)

transformation "encoding_decorate_mono"
30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46

theory BuiltIn
  syntax type int "Int"
  syntax type real "Real"
  syntax logic (_=_) "(EQ %1 %2)"
  syntax logic (_<>_) "(NEQ %1 %2)"
end

theory int.Int

  prelude ";;; this is a prelude for Simplify, Arithmetic"

  syntax logic zero "0"

  syntax logic (_+_) "(+ %1 %2)"
  syntax logic (_-_) "(- %1 %2)"
  syntax logic (_*_) "(* %1 %2)"
47
  syntax logic (-_)  "(- 0 %1)"
48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77

  syntax logic (_<=_) "(<= %1 %2)"
  syntax logic (_< _) "(< %1 %2)"
  syntax logic (_>=_) "(>= %1 %2)"
  syntax logic (_> _) "(> %1 %2)"

  remove prop CommutativeGroup.Comm.Comm
  remove prop CommutativeGroup.Assoc.Assoc
  remove prop CommutativeGroup.Unit_def
  remove prop CommutativeGroup.Inv_def
  remove prop Assoc.Assoc
  remove prop Mul_distr
  remove prop Comm.Comm
  remove prop Unitary
  remove prop Refl
  remove prop Trans
  remove prop Antisymm
  remove prop Total
end

theory transform.encoding_decorate.Kept
  tag cloned type t "encoding_decorate : kept"
end

(*
Local Variables: 
mode: why
compile-command: "make -C .. bench"
End: 
*)