Commit 866daead authored by MARCHE Claude's avatar MARCHE Claude

make cos, sin, tan, atan and pi built-in symbols for SMTv2

Z3 apparently supports them, but any attempt to use thme makes Z3 segfault
parent 81e4e058
......@@ -20,4 +20,16 @@ theory real.FromInt
remove prop Neg
end
(* does not work: Z3 segfaults
theory real.Trigonometry
syntax function cos "(cos %1)"
syntax function sin "(sin %1)"
syntax function pi "pi"
syntax function tan "(tan %1)"
syntax function atan "(atan %1)"
end
*)
import "discrimination.gen"
\ No newline at end of file
......@@ -55,6 +55,8 @@ let ident_printer =
"bvcomp"; "bvsub"; "bvsdiv"; "bvsrem"; "bvsmod"; "bvashr"; "bvule";
"bvugt"; "bvuge"; "bvslt"; "bvsle"; "bvsgt"; "bvsge"; "rotate_left"; "rotate_right";
"cos"; "sin"; "tan"; "atan"; "pi";
(** Other stuff that Why3 seems to need *)
"DECIMAL"; "NUMERAL"; "par"; "STRING";
"unsat";"sat";
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment