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

Merge branch 'fix/michele/vnnlib-driver' into 'master' 

Only use non-strict inequality symbols in VNNLIB driver/printer

Closes #49

See merge request laiser/caisar!110
parents 160a4912 b9fd3743
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
config/drivers/marabou.drv
+ 18
− 6
View file @ 0c0df078
......@@ -117,9 +117,13 @@ theory real.Real
meta "invalid trigger" predicate (>)
syntax predicate (<=) "%1 <= %2"
syntax predicate (<) "%1 < %2"
syntax predicate (>=) "%1 >= %2"
syntax predicate (>) "%1 > %2"
(* Marabou supports only non-strict inequalities, hence we force strict
inequalities to be printed as non-strict ones.
This is not correct in general, and should be taken into account. *)
syntax predicate (<) "%1 <= %2"
syntax predicate (>) "%1 >= %2"
remove prop MulComm.Comm
remove prop MulAssoc.Assoc
......@@ -167,9 +171,13 @@ theory ieee_float.Float64
syntax function (.-_) "(-%1)"
syntax predicate le "%1 <= %2"
syntax predicate lt "%1 < %2"
syntax predicate ge "%1 >= %2"
syntax predicate gt "%1 > %2"
(* Marabou supports only non-strict inequalities, hence we force strict
inequalities to be printed as non-strict ones.
This is not correct in general, and should be taken into account. *)
syntax predicate lt "%1 <= %2"
syntax predicate gt "%1 >= %2"
end
theory real.RealInfix
......@@ -185,9 +193,13 @@ theory real.RealInfix
meta "invalid trigger" predicate (>.)
syntax predicate (<=.) "(%1 <= %2)"
syntax predicate (<.) "(%1 < %2)"
syntax predicate (>=.) "(%1 >= %2)"
syntax predicate (>.) "(%1 > %2)"
(* Marabou supports only non-strict inequalities, hence we force strict
inequalities to be printed as non-strict ones.
This is not correct in general, and should be taken into account. *)
syntax predicate (<.) "(%1 <= %2)"
syntax predicate (>.) "(%1 >= %2)"
end
theory Bool
......
config/drivers/vnnlib.gen
+ 12
− 4
View file @ 0c0df078
......@@ -77,9 +77,13 @@ theory real.Real
syntax function inv "(/ 1.0 %1)"
syntax predicate (<=) "(<= %1 %2)"
syntax predicate (<) "(< %1 %2)"
syntax predicate (>=) "(>= %1 %2)"
syntax predicate (>) "(> %1 %2)"
(* VNN-LIB supports only non-strict inequalities, hence we force strict
inequalities to be printed as non-strict ones.
This is not correct in general, and should be taken into account. *)
syntax predicate (<) "(<= %1 %2)"
syntax predicate (>) "(>= %1 %2)"
remove allprops
meta "encoding:kept" type real
......@@ -123,9 +127,13 @@ theory ieee_float.Float64
syntax function (.-_) "(-%1)"
syntax predicate le "(<= %1 %2)"
syntax predicate lt "(< %1 %2)"
syntax predicate ge "(>= %1 %2)"
syntax predicate gt "(> %1 %2)"
(* VNN-LIB supports only non-strict inequalities, hence we force strict
inequalities to be printed as non-strict ones.
This is not correct in general, and should be taken into account. *)
syntax predicate lt "(<= %1 %2)"
syntax predicate gt "(>= %1 %2)"
syntax predicate is_not_nan ""
remove allprops
......
src/printers/marabou.ml
+ 8
− 4
View file @ 0c0df078
......@@ -128,20 +128,24 @@ let rec negate_term info t =
(* Negate float relational symbols. *)
let ls_neg =
if Term.ls_equal ls info.ls_rel_float.le
|| Term.ls_equal ls info.ls_rel_float.lt
then info.ls_rel_float.gt
else if Term.ls_equal ls info.ls_rel_float.lt
then info.ls_rel_float.ge
else if Term.ls_equal ls info.ls_rel_float.ge
|| Term.ls_equal ls info.ls_rel_float.gt
then info.ls_rel_float.lt
else if Term.ls_equal ls info.ls_rel_float.gt
then info.ls_rel_float.le
else ls
in
(* Negate real relational symbols. *)
let ls_neg =
if Term.ls_equal ls info.ls_rel_real.le
|| Term.ls_equal ls info.ls_rel_real.lt
then info.ls_rel_real.gt
else if Term.ls_equal ls info.ls_rel_real.lt
then info.ls_rel_real.ge
else if Term.ls_equal ls info.ls_rel_real.ge
|| Term.ls_equal ls info.ls_rel_real.gt
then info.ls_rel_real.lt
else if Term.ls_equal ls info.ls_rel_real.gt
then info.ls_rel_real.le
else ls_neg
in
......
src/printers/pyrat.ml
+ 8
− 4
View file @ 0c0df078
......@@ -96,20 +96,24 @@ let rec negate_term info t =
(* Negate float relational symbols. *)
let ls_neg =
if Term.ls_equal ls info.ls_rel_float.le
|| Term.ls_equal ls info.ls_rel_float.lt
then info.ls_rel_float.gt
else if Term.ls_equal ls info.ls_rel_float.lt
then info.ls_rel_float.ge
else if Term.ls_equal ls info.ls_rel_float.ge
|| Term.ls_equal ls info.ls_rel_float.gt
then info.ls_rel_float.lt
else if Term.ls_equal ls info.ls_rel_float.gt
then info.ls_rel_float.le
else ls
in
(* Negate real relational symbols. *)
let ls_neg =
if Term.ls_equal ls info.ls_rel_real.le
|| Term.ls_equal ls info.ls_rel_real.lt
then info.ls_rel_real.gt
else if Term.ls_equal ls info.ls_rel_real.lt
then info.ls_rel_real.ge
else if Term.ls_equal ls info.ls_rel_real.ge
|| Term.ls_equal ls info.ls_rel_real.gt
then info.ls_rel_real.lt
else if Term.ls_equal ls info.ls_rel_real.gt
then info.ls_rel_real.le
else ls_neg
in
......
src/printers/vnnlib.ml
+ 8
− 4
View file @ 0c0df078
......@@ -445,20 +445,24 @@ let rec negate_term info t =
(* Negate float relational symbols. *)
let ls_neg =
if Term.ls_equal ls info.ls_rel_float.le
|| Term.ls_equal ls info.ls_rel_float.lt
then info.ls_rel_float.gt
else if Term.ls_equal ls info.ls_rel_float.lt
then info.ls_rel_float.ge
else if Term.ls_equal ls info.ls_rel_float.ge
|| Term.ls_equal ls info.ls_rel_float.gt
then info.ls_rel_float.lt
else if Term.ls_equal ls info.ls_rel_float.gt
then info.ls_rel_float.le
else ls
in
(* Negate real relational symbols. *)
let ls_neg =
if Term.ls_equal ls info.ls_rel_real.le
|| Term.ls_equal ls info.ls_rel_real.lt
then info.ls_rel_real.gt
else if Term.ls_equal ls info.ls_rel_real.lt
then info.ls_rel_real.ge
else if Term.ls_equal ls info.ls_rel_real.ge
|| Term.ls_equal ls info.ls_rel_real.gt
then info.ls_rel_real.lt
else if Term.ls_equal ls info.ls_rel_real.gt
then info.ls_rel_real.le
else ls_neg
in
......
tests/interpretation_acasxu.t
+ 215
− 1
View file @ 0c0df078
......@@ -4,7 +4,7 @@ Test interpret on acasxu
$ bin/pyrat.py --version
PyRAT 1.1
$ caisar verify --format whyml --prover PyRAT --ltag=ProverSpec - 2>&1 <<EOF | ./filter_tmpdir.sh
$ cat > file.mlw <<EOF
> theory T
> use ieee_float.Float64
> use bool.Bool
......@@ -92,6 +92,8 @@ Test interpret on acasxu
> not (advises nn i clear_of_conflict)
> end
> EOF
$ caisar verify --prover PyRAT --ltag=ProverSpec file.mlw 2>&1 | ./filter_tmpdir.sh
[DEBUG]{ProverSpec} Prover-tailored specification:
-0.328421367053318091766556108268559910356998443603515625 <= x0
x0 <= 0.67985927880386987087746319957659579813480377197265625
......@@ -130,3 +132,215 @@ Test interpret on acasxu
Goal P1: Unknown ()
Goal P3: Unknown ()
$ caisar verify --prover PyRAT --prover-altern VNNLIB --ltag=ProverSpec file.mlw 2>&1 | ./filter_tmpdir.sh
[DEBUG]{ProverSpec} Prover-tailored specification:
;;; produced by PyRAT/VNN-LIB driver
;;; produced by VNN-LIB driver
;; X_0
(declare-const X_0 Real)
;; X_1
(declare-const X_1 Real)
;; X_2
(declare-const X_2 Real)
;; X_3
(declare-const X_3 Real)
;; X_4
(declare-const X_4 Real)
;; H
(assert (>= X_0 -0.328421367053318091766556108268559910356998443603515625))
;; H
(assert (<= X_0 0.67985927880386987087746319957659579813480377197265625))
;; H
(assert (>= X_1 -0.499999999999967081887319864108576439321041107177734375))
;; H
(assert (<= X_1 0.499999999999967081887319864108576439321041107177734375))
;; H
(assert (>= X_2 -0.499999999999967081887319864108576439321041107177734375))
;; H
(assert (<= X_2 0.499999999999967081887319864108576439321041107177734375))
;; H
(assert (>= X_3 -0.5))
;; H
(assert (<= X_3 0.5))
;; H
(assert (>= X_4 -0.5))
;; H
(assert (<= X_4 0.5))
;; H
(assert (>= X_0 0.60000151009774149724051994780893437564373016357421875))
;; H
(assert (>= X_3 0.450000000000000011102230246251565404236316680908203125))
;; H
(assert (<= X_4 -0.450000000000000011102230246251565404236316680908203125))
;; Y_0
(declare-const Y_0 Real)
;; Y_1
(declare-const Y_1 Real)
;; Y_2
(declare-const Y_2 Real)
;; Y_3
(declare-const Y_3 Real)
;; Y_4
(declare-const Y_4 Real)
;; Goal P1
(assert (>= Y_0 3.991125645861615112153231166303157806396484375))
[DEBUG]{ProverSpec} Prover-tailored specification:
;;; produced by PyRAT/VNN-LIB driver
;;; produced by VNN-LIB driver
;; X_0
(declare-const X_0 Real)
;; X_1
(declare-const X_1 Real)
;; X_2
(declare-const X_2 Real)
;; X_3
(declare-const X_3 Real)
;; X_4
(declare-const X_4 Real)
;; H
(assert (>= X_0 -0.328421367053318091766556108268559910356998443603515625))
;; H
(assert (<= X_0 0.67985927880386987087746319957659579813480377197265625))
;; H
(assert (>= X_1 -0.499999999999967081887319864108576439321041107177734375))
;; H
(assert (<= X_1 0.499999999999967081887319864108576439321041107177734375))
;; H
(assert (>= X_2 -0.499999999999967081887319864108576439321041107177734375))
;; H
(assert (<= X_2 0.499999999999967081887319864108576439321041107177734375))
;; H
(assert (>= X_3 -0.5))
;; H
(assert (<= X_3 0.5))
;; H
(assert (>= X_4 -0.5))
;; H
(assert (<= X_4 0.5))
;; H
(assert (>= X_0 -0.303529646039727207806890874053351581096649169921875))
;; H
(assert (<= X_0 -0.298551301837009008810497334707179106771945953369140625))
;; H
(assert (>= X_1 -0.0095492965855130916563719978285007528029382228851318359375))
;; H
(assert (<= X_1 0.0095492965855130916563719978285007528029382228851318359375))
;; H
(assert (>= X_2 0.493380323584843072382000173092819750308990478515625))
;; H
(assert (>= X_3 0.299999999999999988897769753748434595763683319091796875))
;; H
(assert (>= X_4 0.299999999999999988897769753748434595763683319091796875))
;; Y_0
(declare-const Y_0 Real)
;; Y_1
(declare-const Y_1 Real)
;; Y_2
(declare-const Y_2 Real)
;; Y_3
(declare-const Y_3 Real)
;; Y_4
(declare-const Y_4 Real)
;; Goal P3
(assert (<= Y_0 Y_1))
(assert (<= Y_0 Y_2))
(assert (<= Y_0 Y_3))
(assert (<= Y_0 Y_4))
Goal P1: Unknown ()
Goal P3: Unknown ()
$ caisar verify --prover Marabou --ltag=ProverSpec file.mlw 2>&1 | ./filter_tmpdir.sh
[DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= -0.328421367053318091766556108268559910356998443603515625
x0 <= 0.67985927880386987087746319957659579813480377197265625
x1 >= -0.499999999999967081887319864108576439321041107177734375
x1 <= 0.499999999999967081887319864108576439321041107177734375
x2 >= -0.499999999999967081887319864108576439321041107177734375
x2 <= 0.499999999999967081887319864108576439321041107177734375
x3 >= -0.5
x3 <= 0.5
x4 >= -0.5
x4 <= 0.5
x0 >= 0.60000151009774149724051994780893437564373016357421875
x3 >= 0.450000000000000011102230246251565404236316680908203125
x4 <= -0.450000000000000011102230246251565404236316680908203125
y0 >= 3.991125645861615112153231166303157806396484375
[DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= -0.328421367053318091766556108268559910356998443603515625
x0 <= 0.67985927880386987087746319957659579813480377197265625
x1 >= -0.499999999999967081887319864108576439321041107177734375
x1 <= 0.499999999999967081887319864108576439321041107177734375
x2 >= -0.499999999999967081887319864108576439321041107177734375
x2 <= 0.499999999999967081887319864108576439321041107177734375
x3 >= -0.5
x3 <= 0.5
x4 >= -0.5
x4 <= 0.5
x0 >= -0.303529646039727207806890874053351581096649169921875
x0 <= -0.298551301837009008810497334707179106771945953369140625
x1 >= -0.0095492965855130916563719978285007528029382228851318359375
x1 <= 0.0095492965855130916563719978285007528029382228851318359375
x2 >= 0.493380323584843072382000173092819750308990478515625
x3 >= 0.299999999999999988897769753748434595763683319091796875
x4 >= 0.299999999999999988897769753748434595763683319091796875
+y0 -y1 <= 0
+y0 -y2 <= 0
+y0 -y3 <= 0
+y0 -y4 <= 0
Goal P1: Unknown ()
Goal P3: Unknown ()
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