Skip to content
Snippets Groups Projects
Commit a62054f6 authored by Michele Alberti's avatar Michele Alberti
Browse files

[drivers] Rework drivers for handling floats with rounding information.

parent cc4df3cc
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
config/drivers/marabou.drv
+ 15
− 12
View file @ a62054f6
......@@ -44,11 +44,9 @@ theory BuiltIn
meta "eliminate_algebraic" "keep_enums"
meta "eliminate_algebraic" "keep_recs"
end
theory int.Int
prelude "(* this is a prelude for Alt-Ergo integer arithmetic *)"
syntax function zero "0"
......@@ -87,25 +85,19 @@ theory int.Int
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop ZeroLessOne
end
theory int.EuclideanDivision
syntax function div "(%1 / %2)"
syntax function mod "(%1 % %2)"
end
theory int.ComputerDivision
use for_drivers.ComputerOfEuclideanDivision
end
theory real.Real
prelude "(* this is a prelude for Alt-Ergo real arithmetic *)"
syntax function zero "0.0"
......@@ -147,10 +139,25 @@ theory real.Real
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop ZeroLessOne
end
theory ieee_float.RoundingMode
syntax type mode "RoundingMode"
syntax function RNE "RNE"
syntax function RNA "RNA"
syntax function RTP "RTP"
syntax function RTN "RTN"
syntax function RTZ "RTZ"
syntax predicate to_nearest "(or (= %1 RNE) (= %1 RNA))"
end
theory ieee_float.Float64
syntax function add "(%2 + %3)"
syntax function sub "(%2 - %3)"
syntax function mul "(%2 * %3)"
syntax function div "(%2 / %3)"
syntax function neg "(-%1)"
syntax function (.+) "(%1 + %2)"
syntax function (.-) "(%1 - %2)"
......@@ -162,12 +169,9 @@ theory ieee_float.Float64
syntax predicate lt "%1 < %2"
syntax predicate ge "%1 >= %2"
syntax predicate gt "%1 > %2"
end
theory real.RealInfix
syntax function (+.) "(%1 + %2)"
syntax function (-.) "(%1 - %2)"
syntax function ( *.) "(%1 * %2)"
......@@ -183,7 +187,6 @@ theory real.RealInfix
syntax predicate (<.) "(%1 < %2)"
syntax predicate (>=.) "(%1 >= %2)"
syntax predicate (>.) "(%1 > %2)"
end
theory Bool
......
config/drivers/pyrat.drv
+ 17
− 13
View file @ a62054f6
......@@ -46,7 +46,6 @@ theory BuiltIn
end
theory int.Int
prelude "(* this is a prelude for Alt-Ergo integer arithmetic *)"
syntax function zero "0"
......@@ -85,25 +84,18 @@ theory int.Int
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop ZeroLessOne
end
theory int.EuclideanDivision
syntax function div "(%1 / %2)"
syntax function mod "(%1 % %2)"
end
theory int.ComputerDivision
use for_drivers.ComputerOfEuclideanDivision
end
theory real.Real
prelude "(* this is a prelude for Alt-Ergo real arithmetic *)"
syntax function zero "0.0"
......@@ -145,10 +137,25 @@ theory real.Real
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop ZeroLessOne
end
theory ieee_float.RoundingMode
syntax type mode "RoundingMode"
syntax function RNE "RNE"
syntax function RNA "RNA"
syntax function RTP "RTP"
syntax function RTN "RTN"
syntax function RTZ "RTZ"
syntax predicate to_nearest "(or (= %1 RNE) (= %1 RNA))"
end
theory ieee_float.Float64
syntax function add "(%2 + %3)"
syntax function sub "(%2 - %3)"
syntax function mul "(%2 * %3)"
syntax function div "(%2 / %3)"
syntax function neg "(-%1)"
syntax function (.+) "(%1 + %2)"
syntax function (.-) "(%1 - %2)"
......@@ -157,14 +164,12 @@ theory ieee_float.Float64
syntax function (.-_) "(-%1)"
syntax predicate le "%1 <= %2"
syntax predicate lt "%1 < %2"
syntax predicate lt "%1 < %2"
syntax predicate ge "%1 >= %2"
syntax predicate gt "%1 > %2"
syntax predicate gt "%1 > %2"
end
theory real.RealInfix
syntax function (+.) "(%1 + %2)"
syntax function (-.) "(%1 - %2)"
syntax function ( *.) "(%1 * %2)"
......@@ -180,7 +185,6 @@ theory real.RealInfix
syntax predicate (<.) "(%1 < %2)"
syntax predicate (>=.) "(%1 >= %2)"
syntax predicate (>.) "(%1 > %2)"
end
theory Bool
......
config/drivers/saver.drv
+ 0
− 155
View file @ a62054f6
......@@ -21,158 +21,3 @@
(**************************************************************************)
(* Why3 drivers for SAVER *)
theory BuiltIn
syntax type int "int"
syntax type real "real"
syntax predicate (=) "(%1 = %2)"
meta "eliminate_algebraic" "keep_enums"
meta "eliminate_algebraic" "keep_recs"
end
theory int.Int
prelude "(* this is a prelude for Alt-Ergo integer arithmetic *)"
syntax function zero "0"
syntax function one "1"
syntax function (+) "(%1 + %2)"
syntax function (-) "(%1 - %2)"
syntax function (*) "(%1 * %2)"
syntax function (-_) "(-%1)"
meta "invalid trigger" predicate (<=)
meta "invalid trigger" predicate (<)
meta "invalid trigger" predicate (>=)
meta "invalid trigger" predicate (>)
syntax predicate (<=) "(%1 <= %2)"
syntax predicate (<) "(%1 < %2)"
syntax predicate (>=) "(%1 >= %2)"
syntax predicate (>) "(%1 > %2)"
remove prop MulComm.Comm
remove prop MulAssoc.Assoc
remove prop Unit_def_l
remove prop Unit_def_r
remove prop Inv_def_l
remove prop Inv_def_r
remove prop Assoc
remove prop Mul_distr_l
remove prop Mul_distr_r
remove prop Comm
remove prop Unitary
remove prop Refl
remove prop Trans
remove prop Total
remove prop Antisymm
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop ZeroLessOne
end
theory int.EuclideanDivision
syntax function div "(%1 / %2)"
syntax function mod "(%1 % %2)"
end
theory int.ComputerDivision
use for_drivers.ComputerOfEuclideanDivision
end
theory real.Real
prelude "(* this is a prelude for Alt-Ergo real arithmetic *)"
syntax function zero "0.0"
syntax function one "1.0"
syntax function (+) "(%1 + %2)"
syntax function (-) "(%1 - %2)"
syntax function (*) "(%1 * %2)"
syntax function (/) "(%1 / %2)"
syntax function (-_) "(-%1)"
syntax function inv "(1.0 / %1)"
meta "invalid trigger" predicate (<=)
meta "invalid trigger" predicate (<)
meta "invalid trigger" predicate (>=)
meta "invalid trigger" predicate (>)
syntax predicate (<=) "(%1 <= %2)"
syntax predicate (<) "(%1 < %2)"
syntax predicate (>=) "(%1 >= %2)"
syntax predicate (>) "(%1 > %2)"
remove prop MulComm.Comm
remove prop MulAssoc.Assoc
remove prop Unit_def_l
remove prop Unit_def_r
remove prop Inv_def_l
remove prop Inv_def_r
remove prop Assoc
remove prop Mul_distr_l
remove prop Mul_distr_r
remove prop Comm
remove prop Unitary
remove prop Refl
remove prop Trans
remove prop Total
remove prop Antisymm
remove prop Inverse
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop ZeroLessOne
end
theory ieee_float.Float64
syntax function (.+) "(%1 + %2)"
syntax function (.-) "(%1 - %2)"
syntax function (.*) "(%1 * %2)"
syntax function (./) "(%1 / %2)"
syntax function (.-_) "(-%1)"
syntax predicate le "%1 <= %2"
syntax predicate lt "%1 < %2"
syntax predicate ge "%1 >= %2"
syntax predicate gt "%1 > %2"
end
theory real.RealInfix
syntax function (+.) "(%1 + %2)"
syntax function (-.) "(%1 - %2)"
syntax function ( *.) "(%1 * %2)"
syntax function (/.) "(%1 / %2)"
syntax function (-._) "(-%1)"
meta "invalid trigger" predicate (<=.)
meta "invalid trigger" predicate (<.)
meta "invalid trigger" predicate (>=.)
meta "invalid trigger" predicate (>.)
syntax predicate (<=.) "(%1 <= %2)"
syntax predicate (<.) "(%1 < %2)"
syntax predicate (>=.) "(%1 >= %2)"
syntax predicate (>.) "(%1 > %2)"
end
theory ieee_float.Float64
syntax predicate is_not_nan ""
remove allprops
end
config/drivers/vnnlib.gen
+ 17
− 0
View file @ a62054f6
......@@ -97,7 +97,24 @@ theory Bool
meta "encoding:kept" type bool
end
theory ieee_float.RoundingMode
syntax type mode "RoundingMode"
syntax function RNE "RNE"
syntax function RNA "RNA"
syntax function RTP "RTP"
syntax function RTN "RTN"
syntax function RTZ "RTZ"
syntax predicate to_nearest "(or (= %1 RNE) (= %1 RNA))"
end
theory ieee_float.Float64
syntax function add "(%2 + %3)"
syntax function sub "(%2 - %3)"
syntax function mul "(%2 * %3)"
syntax function div "(%2 / %3)"
syntax function neg "(-%1)"
syntax function (.+) "(%1 + %2)"
syntax function (.-) "(%1 - %2)"
syntax function (.*) "(%1 * %2)"
......
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