z3.drv 1.56 KB
Newer Older
1 2 3

(* Why driver for SMT syntax *)

4
prelude ";;; this is a prelude for Z3"
5 6

printer "smtv1"
7
filename "%f-%t-%g.smt"
8

9 10
valid "^unsat"
unknown "^\\(unknown\\|sat\\|Fail\\)" "Unknown"
11 12

(* À discuter *)
13
transformation "simplify_recursive_definition"      
14
(*transformation "inline_trivial"*)
15

16
transformation "eliminate_builtin"
17 18 19 20
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"

21
transformation "encoding_decorate"
22
(* transformation "encoding_decorate_every_simple" *)
23 24 25 26 27 28 29 30 31 32 33 34


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


theory int.Int

35
  prelude ";;; this is a prelude for Z3, Arithmetic"
36 37 38 39 40 41

  syntax logic zero "0"

  syntax logic (_+_) "(+ %1 %2)"
  syntax logic (_-_) "(- %1 %2)"
  syntax logic (_*_) "(* %1 %2)"
42
  syntax logic (-_)  "(- %1)"
43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65

  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

end

theory algebra.AC
  tag cloned logic op "AC"
  remove cloned prop Comm.Comm
  remove cloned prop Assoc.Assoc
end

66 67 68 69
theory transform.encoding_decorate.Kept
  tag cloned type t "encoding_decorate : kept"
end

70 71 72
(*
Local Variables: 
mode: why
73
compile-command: "unset LANG; make -C .. bench"
74 75
End: 
*)