Commit dd26dc45 authored by Sylvain Dailler's avatar Sylvain Dailler

minor update of smtlib reserved words

Updated for smtlib 2.6. Remove a few duplicates.

Change-Id: Ib05b0f5274d10838ed2aba8049b33596d127d597

Conflicts:
	src/printer/smtv2.ml
parent 649b4118
......@@ -2,11 +2,11 @@
prelude "(set-logic AUFBVDTNIRA)"
(*
A : Array
UF : Uninterpreted Function
BV : BitVectors
DT : Datatypes
NIRA : NonLinear Integer Reals Arithmetic
A : Array
UF : Uninterpreted Function
BV : BitVectors
DT : Datatypes
NIRA : NonLinear Integer Real Arithmetic
*)
(* prelude "(set-logic ALL_SUPPORTED)"
does not seem to include DT
......
(**********************************************************************
*** gnat2why theories ***
**********************************************************************)
theory _gnatprove_standard_th.Floating_Func
syntax predicate neq "(not (fp.eq %1 %2))"
syntax function bool_lt "(fp.lt %1 %2)"
syntax function bool_le "(fp.leq %1 %2)"
syntax function bool_gt "(fp.gt %1 %2)"
syntax function bool_ge "(fp.geq %1 %2)"
syntax function bool_eq "(fp.eq %1 %2)"
syntax function bool_neq "(not (fp.eq %1 %2))"
remove allprops
end
(*************************************************************************)
theory "_gnatprove_standard".Floating
syntax function rem "(fp.rem %1 %2)"
syntax function div_rne "(fp.div RNE %1 %2)"
remove allprops
end
theory "_gnatprove_standard".Float32_next_prev
syntax function max_value "(fp #b0 #b11111110 #b11111111111111111111111)"
end
theory "_gnatprove_standard".Float64_next_prev
syntax function max_value "(fp #b0 #b11111111110 #b1111111111111111111111111111111111111111111111111111)"
end
theory "_gnatprove_standard".Float32
syntax function one "(fb #b0 #b01111111 #b00000000000000000000000)"
remove allprops
end
theory "_gnatprove_standard".Float64
syntax function one "(fb #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)"
remove allprops
end
(*************************************************************************)
theory ada__model.Floating_Point_Base
syntax function bool_eq "(fp.eq %1 %2)"
remove allprops
end
(*************************************************************************)
theory ieee_float.Float64
(* function to_int *)
end
theory ieee_float.Float32
(* function to_int *)
end
theory real.Square
remove allprops
end
(**********************************************************************
*** gnat2why theories ***
**********************************************************************)
theory _gnatprove_standard_th.Integer
syntax function bool_eq "(= %1 %2)"
syntax function bool_ne "(not (= %1 %2))"
syntax function bool_lt "(< %1 %2)"
syntax function bool_le "(<= %1 %2)"
syntax function bool_gt "(> %1 %2)"
syntax function bool_ge "(>= %1 %2)"
remove allprops
end
theory _gnatprove_standard_th.Boolean_Func
syntax function bool_eq "(= %1 %2)"
remove allprops
end
(*************************************************************************)
theory _gnatprove_standard.BVAda
syntax function bool_eq "(= %1 %2)"
syntax function bool_ne "(not (= %1 %2))"
syntax function bool_lt "(bvult %1 %2)"
syntax function bool_le "(bvule %1 %2)"
syntax function bool_gt "(bvugt %1 %2)"
syntax function bool_ge "(bvuge %1 %2)"
remove allprops
end
(*************************************************************************)
theory ada__model.Discrete_Base
syntax function bool_eq "(= %1 %2)"
remove allprops
end
(*************************************************************************)
theory ada__model_th.Discrete_Base_Theory
syntax function bool_eq "(= %1 %2)"
remove allprops
end
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