Transition to context dependent search state#580
Transition to context dependent search state#580AleksandarZeljic wants to merge 39 commits intoNeuralNetworkVerification:masterfrom
Conversation
AleksandarZeljic
force-pushed
the
cdSmtCore
branch
from
1c03f5a to
c603ece
Compare
AleksandarZeljic
force-pushed
the
cdSmtCore
branch
from
8931930 to
cc8dce6
Compare
AleksandarZeljic
force-pushed
the
cdSmtCore
branch
from
5cd09ed to
5a10f4e
Compare
| bool fullSolveNeeded = true; // denotes whether we need to solve the subquery | ||
| if ( restoreTreeStates && smtState ) | ||
| fullSolveNeeded = _engine->restoreSmtState( *smtState ); | ||
| fullSolveNeeded = true; //_engine->restoreSmtState( *smtState ); |
There was a problem hiding this comment.
Do we want to fully remove this functionality for now? Maybe we want to also purge this option here:
Marabou/src/configuration/OptionParser.cpp
Line 148 in bdcd044
There was a problem hiding this comment.
Good point, I will remove it altogether as it is obsolete now.
| */ | ||
| bool isCaseInfeasible( PhaseStatus phase ) const; | ||
|
|
||
|
|
src/engine/oldSmtCore
Outdated
| @@ -0,0 +1,257 @@ | |||
| /********************* */ | |||
There was a problem hiding this comment.
Remove this and oldSmtCorecpp?
| _statistics = statistics; | ||
| } | ||
|
|
||
| bool PiecewiseLinearConstraint::phaseFixed() const |
There was a problem hiding this comment.
When _cdPhaseStatus is not null, does this method always have the same output as isImplication()? If so do we want to merge the two methods?
There was a problem hiding this comment.
Longterm we want to merge the two methods. This PR already does a lot and I didn't want to complicate things further, since I am not convinced that this would be a trivial change (e.g. Max/Disjunction semantics). PhaseFixed currently is derived from bound propagation while isImplication is derived from search/backtracking.
| dc.notifyUpperBound( 2, 10 ); | ||
|
|
||
| TS_ASSERT( !dc.phaseFixed() ); | ||
| TS_ASSERT( !dc.isImplication() ); |
There was a problem hiding this comment.
Do we want to also check phaseFixed() iff isImplication()?
There was a problem hiding this comment.
No the semantics actually differ. Disjunction does not ever explicitly fix the phase, it actually used a test that is exactly the implementation of isImplication. Therefore I removed the special implementation of DisjunctionConstraint::phaseFixed() and replaced the calls with isImplication().
AleksandarZeljic
force-pushed
the
cdSmtCore
branch
from
90d7105 to
ae98cd4
Compare
This reverts commit 59db095.
…arts. This change is to avoid violating preconditions of the PiecewiseLinearConstraints::registerBoundManager method.
Previous semantics matched an empty/infeasible disjunction.
The method encapsulates both phaseFixed and isImplication semantics, prioritizing isImplication.
AleksandarZeljic
force-pushed
the
cdSmtCore
branch
from
ae98cd4 to
6dba340
Compare
2 participants
This PR transitions to using Context dependent architecture to store the search state.
This is achieved by using the CD features of PiecewiseLinearConstraints to store their current state in the search.
The SmtCore now uses the PiecewiseLinearConstraint::nextFeasibleCase/markUnfeasible to record the advancement of the search with the PiecewiseLinearConstraints.
This PR: