diff --git a/tests/interpretation_acasxu.t b/tests/interpretation_acasxu.t index 8591192094f156eba26c4a530922313d44a4557f..480f92600b0d11c12ceb67cefdf192d8b0425444 100644 --- a/tests/interpretation_acasxu.t +++ b/tests/interpretation_acasxu.t @@ -7,7 +7,7 @@ Test interpret on acasxu $ PATH=$(pwd)/bin:$PATH - $ caisar verify -L . --format whyml --prover PyRAT - 2>&1 <<EOF | ./filter_tmpdir.sh + $ caisar verify -L . --format whyml --prover PyRAT --verbosity=info - 2>&1 <<EOF | ./filter_tmpdir.sh > theory T > use ieee_float.Float64 > use bool.Bool @@ -95,5 +95,42 @@ Test interpret on acasxu > not (advises nn i clear_of_conflict) > end > EOF + [caisar][INFO] Specification to verify: + -0.328421367053318091766556108268559910356998443603515625 <= x0 + x0 <= 0.67985927880386987087746319957659579813480377197265625 + -0.499999999999967081887319864108576439321041107177734375 <= x1 + x1 <= 0.499999999999967081887319864108576439321041107177734375 + -0.499999999999967081887319864108576439321041107177734375 <= x2 + x2 <= 0.499999999999967081887319864108576439321041107177734375 + -0.5 <= x3 + x3 <= 0.5 + -0.5 <= x4 + x4 <= 0.5 + 0.60000151009774149724051994780893437564373016357421875 <= x0 + 0.450000000000000011102230246251565404236316680908203125 <= x3 + x4 <= -0.450000000000000011102230246251565404236316680908203125 + y0 <= 3.991125645861615112153231166303157806396484375 + + [caisar][INFO] Specification to verify: + -0.328421367053318091766556108268559910356998443603515625 <= x0 + x0 <= 0.67985927880386987087746319957659579813480377197265625 + -0.499999999999967081887319864108576439321041107177734375 <= x1 + x1 <= 0.499999999999967081887319864108576439321041107177734375 + -0.499999999999967081887319864108576439321041107177734375 <= x2 + x2 <= 0.499999999999967081887319864108576439321041107177734375 + -0.5 <= x3 + x3 <= 0.5 + -0.5 <= x4 + x4 <= 0.5 + -0.303529646039727207806890874053351581096649169921875 <= x0 + x0 <= -0.298551301837009008810497334707179106771945953369140625 + -0.0095492965855130916563719978285007528029382228851318359375 <= x1 + x1 <= 0.0095492965855130916563719978285007528029382228851318359375 + 0.493380323584843072382000173092819750308990478515625 <= x2 + 0.299999999999999988897769753748434595763683319091796875 <= x3 + 0.299999999999999988897769753748434595763683319091796875 <= x4 + (((y0 >= y1 or y0 >= y2) or y0 >= y3) or y0 >= y4) + + [caisar][INFO] Verification results for theory 'T' [caisar] Goal P1: Unknown () [caisar] Goal P3: Unknown () diff --git a/tests/interpretation_dataset.t b/tests/interpretation_dataset.t index 9996b4544ebb90ec070a0730f800f908427f9a1e..ec06cb0840e9a72b9602e31df0fae7b9154c773b 100644 --- a/tests/interpretation_dataset.t +++ b/tests/interpretation_dataset.t @@ -11,7 +11,7 @@ Test interpret on dataset $ PATH=$(pwd)/bin:$PATH - $ caisar verify -L . --format whyml --prover Marabou - 2>&1 <<EOF | ./filter_tmpdir.sh + $ caisar verify -L . --format whyml --prover Marabou --verbosity=info - 2>&1 <<EOF | ./filter_tmpdir.sh > theory T > use ieee_float.Float64 > use bool.Bool @@ -53,4 +53,97 @@ Test interpret on dataset > robust nn dataset eps > end > EOF + [caisar][INFO] Specification to verify: + x0 >= 0.0 + x0 <= 1.0 + x1 >= 0.0 + x1 <= 1.0 + x2 >= 0.0 + x2 <= 1.0 + x3 >= 0.0 + x3 <= 1.0 + x4 >= 0.0 + x4 <= 1.0 + x0 >= -0.375 + x0 <= 0.375 + x1 >= 0.625 + x1 <= 1.375 + x2 >= 0.40931372499999996161790249971090815961360931396484375 + x2 <= 1.159313725000000072640204962226562201976776123046875 + x3 >= -0.355392156999999986322080758327501825988292694091796875 + x3 <= 0.394607843000000013677919241672498174011707305908203125 + x4 >= 0.401470588000000017103729987866245210170745849609375 + x4 <= 1.151470588000000017103729987866245210170745849609375 + +y0 -y1 >= 0 + + [caisar][INFO] Specification to verify: + x0 >= 0.0 + x0 <= 1.0 + x1 >= 0.0 + x1 <= 1.0 + x2 >= 0.0 + x2 <= 1.0 + x3 >= 0.0 + x3 <= 1.0 + x4 >= 0.0 + x4 <= 1.0 + x0 >= -0.375 + x0 <= 0.375 + x1 >= 0.625 + x1 <= 1.375 + x2 >= 0.40931372499999996161790249971090815961360931396484375 + x2 <= 1.159313725000000072640204962226562201976776123046875 + x3 >= -0.355392156999999986322080758327501825988292694091796875 + x3 <= 0.394607843000000013677919241672498174011707305908203125 + x4 >= 0.401470588000000017103729987866245210170745849609375 + x4 <= 1.151470588000000017103729987866245210170745849609375 + +y2 -y1 >= 0 + + [caisar][INFO] Specification to verify: + x0 >= 0.0 + x0 <= 1.0 + x1 >= 0.0 + x1 <= 1.0 + x2 >= 0.0 + x2 <= 1.0 + x3 >= 0.0 + x3 <= 1.0 + x4 >= 0.0 + x4 <= 1.0 + x0 >= 0.625 + x0 <= 1.375 + x1 >= -0.375 + x1 <= 0.375 + x2 >= -0.355392156999999986322080758327501825988292694091796875 + x2 <= 0.394607843000000013677919241672498174011707305908203125 + x3 >= 0.401470588000000017103729987866245210170745849609375 + x3 <= 1.151470588000000017103729987866245210170745849609375 + x4 >= 0.40931372499999996161790249971090815961360931396484375 + x4 <= 1.159313725000000072640204962226562201976776123046875 + +y1 -y0 >= 0 + + [caisar][INFO] Specification to verify: + x0 >= 0.0 + x0 <= 1.0 + x1 >= 0.0 + x1 <= 1.0 + x2 >= 0.0 + x2 <= 1.0 + x3 >= 0.0 + x3 <= 1.0 + x4 >= 0.0 + x4 <= 1.0 + x0 >= 0.625 + x0 <= 1.375 + x1 >= -0.375 + x1 <= 0.375 + x2 >= -0.355392156999999986322080758327501825988292694091796875 + x2 <= 0.394607843000000013677919241672498174011707305908203125 + x3 >= 0.401470588000000017103729987866245210170745849609375 + x3 <= 1.151470588000000017103729987866245210170745849609375 + x4 >= 0.40931372499999996161790249971090815961360931396484375 + x4 <= 1.159313725000000072640204962226562201976776123046875 + +y2 -y0 >= 0 + + [caisar][INFO] Verification results for theory 'T' [caisar] Goal G: Unknown ()