[SAVer] First draft for saver support

README.md

 # caisar
+
+## How to add a solver
+Make sure the solver is added to your systems for tests.
+1. Create a `new_solver.drv` in `config/drivers`

config/caisar-detection-data.conf

@@ -29,3 +29,13 @@ version_ok  = "1.1"
 command = "%e --model_path %{nnet-onnx} --property_path %f"
 driver = "caisar_drivers/pyrat.drv"
 use_at_auto_level = 1
+
+[ATP saver]
+name = "SAVER"
+exec = "saver"
+version_switch = "--version"
+version_regexp = "PyRAT \\([0-9.]+\\)"
+version_ok  = "1.1"
+command = "%e --model_path %{nnet-onnx} --property_path %f"
+driver = "caisar_drivers/pyrat.drv"
+use_at_auto_level = 1

config/drivers/saver.drv

+(* Why3 drivers for SAVER *)
+
+printer "saver"
+filename "%f-%t-%g.why"
+
+valid "Result = [Tt]rue"
+invalid "Result = [Ff]alse"
+timeout "Result = [Tt]imeout"
+unknown "Result = [Uu]nknown" ""
+
+transformation "inline_trivial"
+transformation "introduce_premises"
+transformation "eliminate_builtin"
+transformation "simplify_formula"
+transformation "native_nn_prover"
+
+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 Bool
+  syntax type     bool  "bool"
+  syntax function True  "true"
+  syntax function False "false"
+end
+
+theory Tuple0
+  syntax type     tuple0 "unit"
+  syntax function Tuple0 "void"
+end
+
+theory algebra.AC
+  meta AC function op
+  remove prop Comm
+  remove prop Assoc
+end
+
+theory ieee_float.Float64
+  syntax predicate is_not_nan ""
+  remove allprops
+end