Produce proofs for Sign, Max, Absolute Value and Disjunction constraints #689
Conversation
Added removeIf wrapper function
Fixed Identation
Fixed indentation
Fixed indentation
Correct version of file
Fixed formatting
Fixed formatting
Added a test of removeIf() method
Added a test of const operator[]
| if ( variable == _b ) | ||
| { | ||
| if ( bound > 0 ) | ||
| if ( FloatUtils::gt( bound, 0 ) && ( !proofs || !phaseFixed() ) ) |
There was a problem hiding this comment.
I don't understand the logic of the second conjunct. If proofs are off, this is the normal case - sure. But if they are on, what does the phase matter? Please make it clearer
There was a problem hiding this comment.
If proofs are on and the phase is fixed, then we have a row in the tableau that corresponds exactly to this phase. Thus we don't need to update a lemma and we can skip this part. An alternative solution would be to add a conditional, that will deduce bound without a lemma in the case the phase is fixed. What do you think?
regress/regress1/CMakeLists.txt
Outdated
| @@ -164,5 +164,4 @@ marabou_add_input_query_test(1 ACASXU_maxtest2.ipq unsat "--prove-unsat" "ipq") | |||
| # Sign | |||
| marabou_add_input_query_test(1 deep_6_index_5566.ipq unsat "--prove-unsat" "ipq") | |||
| marabou_add_input_query_test(1 deep_6_index_5567.ipq unsat "--prove-unsat" "ipq") | |||
| marabou_add_input_query_test(1 deep_6_index_5525.ipq unsat "--prove-unsat" "ipq") | |||
There was a problem hiding this comment.
What was problematic about this test?
This reverts commit f3c7a73.
|
Just a quick reminder that if you're adding functionality, it would be great to get an entry in the CHANGELOG file. |
CHANGELOG.md
Outdated
| @@ -1,5 +1,9 @@ | |||
| # Changelog | |||
|
|
|||
| ## Version 1.2.0 | |||
|
|
|||
| * Added proof producing versions for Sign, Max, Absolute Value and Disjunction constraints | |||
There was a problem hiding this comment.
I think we're still on v1.1.0 actually as it hasn't been released. Maybe the v1.1.0 title should Next release to avoid confusion?
No description provided.