NeVerTools / pyNeVer

A Python library for learning and verification of neural networks and other machine learning models
Other
9 stars 3 forks source link

Incorrect property parsing #21

Closed KarimPedemonte closed 8 months ago

KarimPedemonte commented 8 months ago

When parsing a property, if a condition is written as such

(assert (or
    (and (<= Y_1 Y_0)(<= Y_2 Y_0)(<= Y_3 Y_0)(<= Y_4 Y_6)(<= Y_5 Y_6)(<= Y_7 Y_6))
))

rather than

(assert (<= Y_1 Y_0))
(assert (<= Y_2 Y_0))
(assert (<= Y_3 Y_0))
(assert (<= Y_4 Y_6))
(assert (<= Y_5 Y_6))
(assert (<= Y_7 Y_6))

it is parsed incorrectly. The coefficient matrix returned by SmtPropertyParser in this case is

[[0. 1. 1. 1. 1. 1. 0. 1.]]

rather than being

[[-1.  1.  0.  0.  0.  0.  0.  0.]
 [-1.  0.  1.  0.  0.  0.  0.  0.]
 [-1.  0.  0.  1.  0.  0.  0.  0.]
 [ 0.  0.  0.  0.  1.  0. -1.  0.]
 [ 0.  0.  0.  0.  0.  1. -1.  0.]
 [ 0.  0.  0.  0.  0.  0. -1.  1.]]

Here is the property