UNSAT Certificate core modules (only) #530

OmriIsacHUJI · 2022-02-17T14:39:48Z

Added files for constructing UNSAT certificate, without changing Marabou's functionality (modules are not used):

BoundsExplainer - manages all bounds' explanations.
UNSATcertificate - contains classes of the certificate tree and other data structures.
SmtLibWriter - enables writing a query (or a node in its search tree) as an smtlib format query.
Tests for BoundsExplainer and CertificateNode

guykatzz

I reviewed only the first 3 files for now. Most comments are about the coding convention - please apply them throughout the PR, not just for the lines I commented on, and I'll re-review afterwards.

src/common/SmtLibWriter.h

src/engine/BoundsExplainer.cpp

Added removeIf wrapper function

Fixed Identation

Fixed indentation

Correct version of file

Fixed formatting

guykatzz

Another batch of comments, mostly about style.

src/common/List.h

src/common/Vector.h

src/common/SmtLibWriter.cpp

src/engine/UNSATCertificate.h

src/engine/UNSATCertificate.cpp

Added appendHead function that enables adding another list.

Row coefficients vector is added with coefficient 1. Minor modifications.

Test match changes in BoundExplainer

Match changes in UnsatCertificateNode

Added a couple of consts

Class is responsible for memory allocation. Added getters.

Moved certification methods to Checker class

When checking an explanation, it is received as an array (rather than a vector). Changed the row produced from an explanation, to match the changes in BoundExplainer.

g/setPhaseStatus() methods are public

OmriIsacHUJI added 3 commits February 17, 2022 16:01

Add files via upload

aa4b0a4

Add files via upload

626acc3

Add files via upload

99665c8

OmriIsacHUJI marked this pull request as ready for review February 17, 2022 16:51

guykatzz reviewed Feb 17, 2022

View reviewed changes

OmriIsacHUJI added 22 commits February 20, 2022 17:04

Merge branch 'master' into master

b7ef45a

Update SmtLibWriter.h

4588718

Add files via upload

5ab0def

Update SmtLibWriter.cpp

f7565a3

Update Vector.h

6ce624a

Update List.h

bb48611

Added removeIf wrapper function

Update List.h

18d654a

Add files via upload

4159229

Delete Test_BoundsExplainer.h

1677664

Update Test_CertificateNode.h

acf469f

Delete BoundsExplainer.cpp

67babac

Delete BoundsExplainer.h

4ccfab4

Add files via upload

bfce896

Update UNSATCertificate.h

99f1d16

Update BoundExplainer.h

703442f

Fixed Identation

Update UNSATCertificate.cpp

361cb9d

Fixed indentation

Update UNSATCertificate.h

4cbc967

Fixed indentation

Update UNSATCertificate.cpp

8801552

Correct version of file

Update BoundExplainer.h

309038e

Fixed formatting

Update UNSATCertificate.cpp

9f15cbb

Fixed formatting

Update UNSATCertificate.cpp

caedb50

Update UNSATCertificate.cpp

180fd9c

guykatzz reviewed Feb 21, 2022

View reviewed changes

OmriIsacHUJI added 2 commits March 3, 2022 11:10

Merge branch 'NeuralNetworkVerification:master' into master

d04763a

Merge branch 'NeuralNetworkVerification:master' into master

f046fa4

OmriIsacHUJI and others added 27 commits March 10, 2022 10:43

Merge branch 'master' into master

ac2c68f

Update List.h

2ed2afa

Added appendHead function that enables adding another list.

Added const access to data

c6b7156

Added tests to data() functions

c52eb43

Delete UnsatCertificateProblemConstraint.h

f7a3e2e

Update Test_List.h

33c9b6a

Changed folder name

df5a4c3

Update BoundExplainer.cpp

42ecf37

Row coefficients vector is added with coefficient 1. Minor modifications.

Update BoundExplainer.h

f3df970

Update CMakeLists.txt

e6ac2bc

Update Test_BoundExplainer.h

98a3dd8

Test match changes in BoundExplainer

Update Test_UnsatCertificateNode.h

c7abff0

Match changes in UnsatCertificateNode

Update Test_UnsatCertificateUtils.h

ccf1077

Add files via upload

6f9c511

Add files via upload

512f34d

Update Checker.cpp

1c511a7

Added a couple of consts

Update Contradiction.cpp

9178576

Class is responsible for memory allocation. Added getters.

Update Contradiction.h

7397b55

Class is responsible for memory allocation. Added getters.

Update PlcExplanation.cpp

8408740

Class is responsible for memory allocation. Added getters.

Update PlcExplanation.h

0528603

Class is responsible for memory allocation. Added getters.

Update Checker.cpp

452427c

Update UnsatCertificateNode.cpp

3447bb4

Moved certification methods to Checker class

Update UnsatCertificateNode.h

46ffbe7

Moved certification methods to Checker class

Update UnsatCertificateUtils.cpp

d9568ab

When checking an explanation, it is received as an array (rather than a vector). Changed the row produced from an explanation, to match the changes in BoundExplainer.

Update UnsatCertificateUtils.h

51506e5

When checking an explanation, it is received as an array (rather than a vector). Changed the row produced from an explanation, to match the changes in BoundExplainer.

Merge branch 'master' into master

674067f

Update PiecewiseLinearConstraint.h

42b4fb9

g/setPhaseStatus() methods are public

guykatzz approved these changes Mar 22, 2022

View reviewed changes

Merge branch 'master' into master

6923f5b

omriisack merged commit 69dc5eb into NeuralNetworkVerification:master Mar 23, 2022

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

UNSAT Certificate core modules (only) #530

UNSAT Certificate core modules (only) #530

OmriIsacHUJI commented Feb 17, 2022 •

edited

Loading

guykatzz left a comment

guykatzz left a comment

UNSAT Certificate core modules (only) #530

UNSAT Certificate core modules (only) #530

Conversation

OmriIsacHUJI commented Feb 17, 2022 • edited Loading

guykatzz left a comment

Choose a reason for hiding this comment

guykatzz left a comment

Choose a reason for hiding this comment

OmriIsacHUJI commented Feb 17, 2022 •

edited

Loading