Absolute value PL constraint #228
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
…natures, fix satisfied(), implement getPossibleFixes()
…d bound. add some documentation
* Use ndebug (#229) Used NDEBUG flag to indicate of not debug mode (CMake adds this flag be default in release mode) Default compilation is release mode * Cmake: Minor (#230) * fix a couple of warnings * minor Co-authored-by: yuvaljacoby <yuvaljacoby@users.noreply.github.com> Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
| // Also, if for some reason we only know a negative lower bound for f, | ||
| // we attempt to tighten it to 0 | ||
| if ( bound < 0 && variable == _f ) | ||
| _constraintBoundTightener->registerTighterLowerBound( _f, 0 ); |
There was a problem hiding this comment.
This should be done only once, ideally at the start of solving. What is the reason to keep attempting it?
There was a problem hiding this comment.
Indeed, this should only apply in the beginning, but we don't know whether it's been done before or not. I refactored it a bit, for efficiency (moved it into the previous if condition).
| */ | ||
| void eliminateVariable( unsigned variable, double fixedValue ); | ||
| void updateVariableIndex( unsigned oldIndex, unsigned newIndex ); | ||
| bool constraintObsolete() const; |
There was a problem hiding this comment.
Maybe name the bool returning test functions with is prefix, i.e. isConstraintObsolete()? It would distinguish from imperative function names and make the code easier to read.
There was a problem hiding this comment.
Currently this convention is not really followed, not even in this particular class. Is it in our coding guidelines?
AleksandarZeljic
pushed a commit
to AleksandarZeljic/Marabou
that referenced
this pull request
Oct 9, 2020
* initial abs cinstraint, three files - h, cpp and error * variable name * removing run3 files * wip * Sources.mk - add AbsConstraint.cpp; AbsConstraint.cpp - Add some signatures, fix satisfied(), implement getPossibleFixes() * add constant ABS_CONSTRAINT_COMPARISON_TOLERANCE * add ifndef to AbsConstraint.h * add some signatures to AbsConstraint.h and fix some signatures at AbsConstraint.cpp * fixing errors * fix errors * split and more * add some signatures * notify functions * finsh write functions. next step - testing * test file * notifyLowerBound and notifyUpperBound * test with sumathi * add check at notify lower/upper bound if new bound is better then old bound. add some documentation * getEntailedTightenings * fix at notifyUpperBound * Test to entailed_tighteningst * duplicate and restore * register_and_unregister * test for notifyVariableValue, satisfied and updateVariableIndex * more tests * edit comments * more tests * some fixes * some fixes * fix * add getter to _lowerBounds * test_abs_entailed_tighteningst * fix * upper\lower bpound f <0 , get_upper_bound * more testing and print func * fix x_f<0 * fix x_f<0 * some changes * some changes * without test_abs_entailed_tighteningst2 * some changes if upper/ lower bound <0 * fix tighteningst2 * some fixes * more tests for getEntailedTightenings * add cases to getEntailedTightnings * finish testing getEntailedTighteningsgit add Test_AbsConstraint.h! * change non overlap at getEntailedTightenings * change ovelap tests * CMakeLists * test fixes and case split * fix * finish tests * abs_feasible_2 like relu_feasible_2 * add regress for abs constraint * add some print at getEntailedTightening befor ASSERT * notifynotifyLowerBound if var == _f && bound <0. i delete & bound ==0 * same as befor change not is posetive * change the part when the bounds of _f need to be zero * notifyLowerBound and upper, when update the prtner, if var is f, i add && bound>0 * test_abs_entailed_tighteningst0 if lower bound of f is <0 * check that _constraintBoundTightener exists before using it * add test for _f bound<0 * more test lower bounf f<0 * 1 is UNSAT- not working, 2 is SAT * getE fix overlap * get lower bound, change to double * more tests * add feasible2 * non * better printing of bounds * without no overlap * fix * unsat * more regress * getEntailedTightenings without max positive * fix a bug regarding bound extraction of fixed variables * Entailed_Tightenings without max and min * more regress * match to tha changes at absconstraint * without max/min at getEntailedTightenings * match to changes at ans * more regress * add new files acas regress fixed input and with constraint. inputQuery fix typo * check correctness * fix the new network, but there is steal problem * fix the new network, but there is yet problem * change fix point * configuration * fix acas abs constraint * add for at the main, add documentaion * coding style * changes * minor * the old regression test moved to be a system test * moving some files around * typo * compilation issues * cleanup * cleanup * refactoring * finished pass on main class * remove AbsError class * compilation * thorough phass over the unit tests * more polishing of bound tighting and phase-fixing-detection * system test cleanup * dont override variable elimination * additional tests * some more cleanup * remove a few comments * Merge from master (NeuralNetworkVerification#231) * Use ndebug (NeuralNetworkVerification#229) Used NDEBUG flag to indicate of not debug mode (CMake adds this flag be default in release mode) Default compilation is release mode * Cmake: Minor (NeuralNetworkVerification#230) * fix a couple of warnings * minor Co-authored-by: yuvaljacoby <yuvaljacoby@users.noreply.github.com> Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com> * bug fix * remove "unused"s * minor * Aleks' comments * space * test no longer needed Co-authored-by: shirana <shiran.aziz@gmail.com> Co-authored-by: Christopher Lazarus <clazarusg@gmail.com> Co-authored-by: Guy Katz <guykatz@cs.huji.ac.il> Co-authored-by: yuvaljacoby <yuvaljacoby@users.noreply.github.com> Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
matanost
pushed a commit
that referenced
this pull request
Nov 2, 2021
* initial abs cinstraint, three files - h, cpp and error * variable name * removing run3 files * wip * Sources.mk - add AbsConstraint.cpp; AbsConstraint.cpp - Add some signatures, fix satisfied(), implement getPossibleFixes() * add constant ABS_CONSTRAINT_COMPARISON_TOLERANCE * add ifndef to AbsConstraint.h * add some signatures to AbsConstraint.h and fix some signatures at AbsConstraint.cpp * fixing errors * fix errors * split and more * add some signatures * notify functions * finsh write functions. next step - testing * test file * notifyLowerBound and notifyUpperBound * test with sumathi * add check at notify lower/upper bound if new bound is better then old bound. add some documentation * getEntailedTightenings * fix at notifyUpperBound * Test to entailed_tighteningst * duplicate and restore * register_and_unregister * test for notifyVariableValue, satisfied and updateVariableIndex * more tests * edit comments * more tests * some fixes * some fixes * fix * add getter to _lowerBounds * test_abs_entailed_tighteningst * fix * upper\lower bpound f <0 , get_upper_bound * more testing and print func * fix x_f<0 * fix x_f<0 * some changes * some changes * without test_abs_entailed_tighteningst2 * some changes if upper/ lower bound <0 * fix tighteningst2 * some fixes * more tests for getEntailedTightenings * add cases to getEntailedTightnings * finish testing getEntailedTighteningsgit add Test_AbsConstraint.h! * change non overlap at getEntailedTightenings * change ovelap tests * CMakeLists * test fixes and case split * fix * finish tests * abs_feasible_2 like relu_feasible_2 * add regress for abs constraint * add some print at getEntailedTightening befor ASSERT * notifynotifyLowerBound if var == _f && bound <0. i delete & bound ==0 * same as befor change not is posetive * change the part when the bounds of _f need to be zero * notifyLowerBound and upper, when update the prtner, if var is f, i add && bound>0 * test_abs_entailed_tighteningst0 if lower bound of f is <0 * check that _constraintBoundTightener exists before using it * add test for _f bound<0 * more test lower bounf f<0 * 1 is UNSAT- not working, 2 is SAT * getE fix overlap * get lower bound, change to double * more tests * add feasible2 * non * better printing of bounds * without no overlap * fix * unsat * more regress * getEntailedTightenings without max positive * fix a bug regarding bound extraction of fixed variables * Entailed_Tightenings without max and min * more regress * match to tha changes at absconstraint * without max/min at getEntailedTightenings * match to changes at ans * more regress * add new files acas regress fixed input and with constraint. inputQuery fix typo * check correctness * fix the new network, but there is steal problem * fix the new network, but there is yet problem * change fix point * configuration * fix acas abs constraint * add for at the main, add documentaion * coding style * changes * minor * the old regression test moved to be a system test * moving some files around * typo * compilation issues * cleanup * cleanup * refactoring * finished pass on main class * remove AbsError class * compilation * thorough phass over the unit tests * more polishing of bound tighting and phase-fixing-detection * system test cleanup * dont override variable elimination * additional tests * some more cleanup * remove a few comments * Merge from master (#231) * Use ndebug (#229) Used NDEBUG flag to indicate of not debug mode (CMake adds this flag be default in release mode) Default compilation is release mode * Cmake: Minor (#230) * fix a couple of warnings * minor Co-authored-by: yuvaljacoby <yuvaljacoby@users.noreply.github.com> Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com> * bug fix * remove "unused"s * minor * Aleks' comments * space * test no longer needed Co-authored-by: shirana <shiran.aziz@gmail.com> Co-authored-by: Christopher Lazarus <clazarusg@gmail.com> Co-authored-by: Guy Katz <guykatz@cs.huji.ac.il> Co-authored-by: yuvaljacoby <yuvaljacoby@users.noreply.github.com> Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
No description provided.