Bound Manager Class #429
Merged
Bound Manager Class #429
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
guykatzz
reviewed
Feb 8, 2021
guykatzz
approved these changes
Feb 20, 2021
Co-authored-by: anwu1219 <haozewu@stanford.edu>
Co-authored-by: anwu1219 <haozewu@stanford.edu>
Co-authored-by: anwu1219 <haozewu@stanford.edu>
Add tightened flag to BoundManager The flag is set whenever a bound is updated. The flag is cleared when getBoundTightnings is called. Serves as a pooling mechanism for constraint bound propagation. Allows for elimination of ConstraintBoundTightener class.
AleksandarZeljic
force-pushed
the
boundManagerPR
branch
from
a6b4895 to
2e471e2
Compare
matanost
pushed a commit
that referenced
this pull request
Nov 2, 2021
* Add Bound Manager class first version Co-authored-by: anwu1219 <haozewu@stanford.edu> * Fix BoundManager ctr and dtr * Add BoundManger tests (fix initialize method) Co-authored-by: anwu1219 <haozewu@stanford.edu> * Add Test BoundManager correctly advances/backtracks with Context Co-authored-by: anwu1219 <haozewu@stanford.edu> * Add growing functionality to BoundManager class * Rename BoundManager getter/setter methods * Add test for BoundManager::registerVariable() * Add CVC4 dependencies to MarabouTestLib in CMakeLists * Store bounds in BoundManager to Vector<CDO<double> *> * Refactor Tableau tighten*Bound methods * Add ptr to Tableau to BoundManager * Protect registerTableauReference( ptrTableau ) * Separate setter and tighten methods in BoundManager * Add tighten flag for each variable in BoundManager Add tightened flag to BoundManager The flag is set whenever a bound is updated. The flag is cleared when getBoundTightnings is called. Serves as a pooling mechanism for constraint bound propagation. Allows for elimination of ConstraintBoundTightener class. * Add boundsValid check in BoundManager * Rename boundsValid to consistentBounds * Add comments, rename getSize, match method order * Add one central context object for all tests. * Add BoundManager::getTightenings test * Fix formatting, typos and comments * Add BoundManager class description and comments * Fix formatting in BoundManager.cpp * Fix wording * Order includes by own header, name complexity, then alphabetically * Fix indentation * Fix spacing * Remove compilation suffix * Make getNumberOfVariables const * Fix indentation, empty lines * Fix orientation of Boolean comparisons * Fix blank spaces in Tableau * Make get*Bound const * Make consistentBounds() const * Rename updateNonBasicVariable* to updateVariableToComplyWith* * Fix indentation in updateVarableToComplyWith*BoundUpdate * Fix renaming typo Co-authored-by: anwu1219 <haozewu@stanford.edu> Co-authored-by: ahmed-irfan <irfan@cs.stanford.edu>
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.
BoundManager class is a context-dependent implementation of a centralized
variable registry and their bounds. The intent it so use a single BoundManager
object between multiple bound tightener classes, which enables
those classes to care only about bounds and forget about book-keeping.
Furthermore, the context-dependent implementation eliminates the need for
eager memory book-keeping.
BoundManager provides a method to obtain a new variable with:
The bound values and tighten flags are stored using context-dependent objects,
which backtrack automatically with the central _context object.
There are two sets of methods to set bounds:
propagates the new bounds to the _tableau (if registered) to keep the
assignment and basic/non-basic variables updated accordingly.
As soon as bounds become inconsistent, i.e. lowerBound > upperBound, an
InfeasableQueryException is thrown. In the long run, we want the exception
replaced by a flag, and switch to the conflict analysis mode instead.
It is assumed that variables are not introduced on the fly, and as such
interaction with context-dependent features is not implemented.
Another thing we may want to consider in the long run, is to make the
BoundManager a VariableWatcher, and move those features from Tableau.
Integration into the master can be gradual, first allowing each class storing
bounds a private copy of the object, before switching to a centralized object,
instant bound visibility and elimination of tightening propagation.