Context Dependent Piecewise Linear Constraint #422
Conversation
| /* | ||
| If the constraint's phase has been fixed, get the (valid) case split. | ||
| */ | ||
| virtual PiecewiseLinearCaseSplit getImpliedCaseSplit() const = 0; |
There was a problem hiding this comment.
As a side note, we said we wanted to change this name, right? Maybe getImpliedCase, to be consistent with getAllCases()?
There was a problem hiding this comment.
So I would keep the name as is because there is a distinction in the return type - get*Case(s) all return PhaseStatus enumeration in some form, while this one returns an actual PiecewiseLinearCaseSplit. In the long run this should be the only method to return a PiecewiseLinearCaseSplit.
| /* | ||
| Returns true if there is only one feasible case remaining. | ||
| */ | ||
| bool isImplication() |
There was a problem hiding this comment.
Make function const?
Also, we usually do == 1 ad not 1 ==.
There was a problem hiding this comment.
Fixed, changed style. The idea is to avoid accidental assignment, but I understand that with our style and reviews this should be unnecessary.
|
|
||
| /* | ||
| Returns phaseStatus representing next feasible case. | ||
| Returns PHASE_NOT_FIXED if no feasible case exists. |
There was a problem hiding this comment.
Can we perhaps add a dedicated sentinel? CONSTRAINT_INFEASIBLE or something?
There was a problem hiding this comment.
I have not done that because it would make dealing with Max and Disjunction trickier, but I will see what I can do.
There was a problem hiding this comment.
I was overthinking things, I added a high-valued entry to PhaseStatus enumeration, and updated this method accordingly.
|
@guykatzz I think I've addressed all the concerns you raised, assuming the check passes, you can take another look. And if everything is fine I will rebase the branch onto master for a merge. Wasn't sure if rebase and force push would lose the review discussion or not. |
This reverts commit 5f7d23c.
AleksandarZeljic
force-pushed
the
cdPWLC
branch
from
fab76b8 to
fabc573
Compare
* Add virtual class ContextDependentPiecewiseLinearConstraint WIP * Remove virtual methods common to CDPWLC and PWLC * Add CDPWLC class description * Remove PhaseStatus enum (already present on master) * Move cdoCleanup behind initialization methods * Move simple methods to header, fix comments * Fix formatting * Update nextFeasibleCase to match assumptions * Remove redeclaration of inherited virtual methods that are still virtual * Add comments * Update header comment * Update header description * Fix comments * Remove virtual inheritance * Make debugging methods return const pointers * Remove empty line * Make testers consts * Add virtual to nextFeasibleCase() * Flip argument order in comparisons with constants * Fix initialization of _cdConstraintActive * Fix comparison order for consistency * Add sentinel value CONSTRAINT_INFEASIBLE to PhaseStatus enum * Use relative maraboupy path for code coverage * Fix initialization of _cdPhaseStatus
This PR introduces an implementation of PiecewiseLinearConstraint using
context-dependent (CD) data structures from CVC4, which lazily and automatically
backtrack in sync with the central context object. These data structures
are delicate and require that data stored is safe to memcopy around.
Members are initialized using the initializeCDOs( Context context ) method.
Subclasses need to call initializeDuplicatesCDOs() method in the
duplicateConstraint() method to avoid sharing context-dependent members.
CDOs need not be initialized for pre-processing purposes.
The class uses CDOs to record:
PhaseStatus enumeration is used to keep track of current phase of the
object, as well as to record previously explored phases. This replaces
moving PiecewiseLinearCaseSplits around.
ContextDependentPiecewiseLinearConstraint stores locally which phases have
been explored so far using _cdInfeasibleCases. To communicate with the
search it implements two methods:
These methods rely on subclass properly handling:
segments the constraint has, initialized by the constructor.
PhaseStatus enumeration. The order of returned cases will determine the
search order, so this method should implement any search heuristics.