Transition to context dependent search state

src/common/Statistics.cpp

@@ -148,6 +148,12 @@ void Statistics::print()
             , printPercents( timeSimplexStepsMicro, timeMainLoopMicro )
             , timeSimplexStepsMicro / 1000
             );
+    unsigned long long totalTimePerformingLocalSearch =
+        getLongAttribute( Statistics::TOTAL_TIME_LOCAL_SEARCH_MICRO );
+    printf( "\t\t\t[%.2lf%%] SoI-based local search: %llu milli\n"
+            , printPercents( totalTimePerformingLocalSearch, timeMainLoopMicro )
+            , totalTimePerformingLocalSearch / 1000
+            );
     unsigned long long totalTimeExplicitBasisBoundTighteningMicro =
         getLongAttribute(TOTAL_TIME_EXPLICIT_BASIS_BOUND_TIGHTENING_MICRO );
     printf( "\t\t[%.2lf%%] Explicit-basis bound tightening: %llu milli\n"
@@ -212,12 +218,6 @@ void Statistics::print()
             , printPercents( totalTimePerformingSymbolicBoundTightening, timeMainLoopMicro )
             , totalTimePerformingSymbolicBoundTightening / 1000
             );
-    unsigned long long totalTimePerformingLocalSearch =
-        getLongAttribute( Statistics::TOTAL_TIME_LOCAL_SEARCH_MICRO );
-    printf( "\t\t[%.2lf%%] SoI-based local search: %llu milli\n"
-            , printPercents( totalTimePerformingLocalSearch, timeMainLoopMicro )
-            , totalTimePerformingLocalSearch / 1000
-            );
     unsigned long long totalTimeAddingConstraintsToMILPSolver =
         getLongAttribute( Statistics::TIME_ADDING_CONSTRAINTS_TO_MILP_SOLVER_MICRO );
     printf( "\t\t[%.2lf%%] SoI-based local search: %llu milli\n"
@@ -326,7 +326,7 @@ void Statistics::print()
             , getUnsignedAttribute( Statistics::CURRENT_DECISION_LEVEL )
             , getUnsignedAttribute( Statistics::NUM_VISITED_TREE_STATES )
             , getUnsignedAttribute( Statistics::NUM_SPLITS )
-            , getUnsignedAttribute( Statistics::NUM_POPS ) );
+            , getUnsignedAttribute( Statistics::NUM_CONTEXT_POPS ) );
     printf( "\tMax stack depth: %u\n"
             , getUnsignedAttribute( Statistics::MAX_DECISION_LEVEL ) );
 

src/engine/AbsoluteValueConstraint.cpp

@@ -33,7 +33,8 @@ AbsoluteValueConstraint::AbsoluteValueConstraint( unsigned b, unsigned f )
 }
 
 AbsoluteValueConstraint::AbsoluteValueConstraint( const String &serializedAbs )
-    : _auxVarsInUse( false )
+    : PiecewiseLinearConstraint( TWO_PHASE_PIECEWISE_LINEAR_CONSTRAINT )
+    , _auxVarsInUse( false )
     , _haveEliminatedVariables( false )
 {
     String constraintType = serializedAbs.substring( 0, 13 );
@@ -125,7 +126,7 @@ void AbsoluteValueConstraint::notifyLowerBound( unsigned variable, double bound
 
     if ( _boundManager == nullptr && existsLowerBound( variable ) &&
          !FloatUtils::gt( bound, getLowerBound( variable ) ) )
-      return;
+        return;
 
     setLowerBound( variable, bound );
 
@@ -179,7 +180,7 @@ void AbsoluteValueConstraint::notifyUpperBound( unsigned variable, double bound
          !FloatUtils::lt( bound, getUpperBound( variable ) ) )
         return;
 
-     setUpperBound( variable, bound );
+    setUpperBound( variable, bound );
     // Check whether the phase has become fixed
     fixPhaseIfNeeded();
 
@@ -320,7 +321,7 @@ List<PiecewiseLinearConstraint::Fix> AbsoluteValueConstraint::getPossibleFixes()
     return fixes;
 }
 
-List<PiecewiseLinearConstraint::Fix> AbsoluteValueConstraint::getSmartFixes( ITableau */* tableau */ ) const
+List<PiecewiseLinearConstraint::Fix> AbsoluteValueConstraint::getSmartFixes( ITableau * /* tableau */ ) const
 {
     return getPossibleFixes();
 }
@@ -395,10 +396,6 @@ PiecewiseLinearCaseSplit AbsoluteValueConstraint::getPositiveSplit() const
     return positivePhase;
 }
 
-bool AbsoluteValueConstraint::phaseFixed() const
-{
-    return _phaseStatus != PhaseStatus::PHASE_NOT_FIXED;
-}
 
 PiecewiseLinearCaseSplit AbsoluteValueConstraint::getImpliedCaseSplit() const
 {
@@ -454,6 +451,8 @@ void AbsoluteValueConstraint::dump( String &output ) const
                            existsLowerBound( _negAux ) ? Stringf( "%lf", getLowerBound( _negAux ) ).ascii() : "-inf",
                            existsUpperBound( _negAux ) ? Stringf( "%lf", getUpperBound( _negAux ) ).ascii() : "inf" );
     }
+
+    serializeInfeasibleCases( output );
 }
 
 void AbsoluteValueConstraint::updateVariableIndex( unsigned oldIndex, unsigned newIndex )
@@ -602,8 +601,7 @@ void AbsoluteValueConstraint::getEntailedTightenings( List<Tightening> &tighteni
     }
 }
 
-void AbsoluteValueConstraint::transformToUseAuxVariables( InputQuery
-                                                                  &inputQuery )
+void AbsoluteValueConstraint::transformToUseAuxVariables( InputQuery &inputQuery )
 {
     /*
       We want to add the two equations
@@ -662,7 +660,7 @@ void AbsoluteValueConstraint::getCostFunctionComponent( LinearExpression &cost,
                                                         PhaseStatus phase ) const
 {
     // If the constraint is not active or is fixed, it contributes nothing
-    if( !isActive() || phaseFixed() )
+    if ( !isActive() || phaseFixed() )
         return;
 
     ASSERT( phase == ABS_PHASE_NEGATIVE || phase == ABS_PHASE_POSITIVE );

src/engine/AbsoluteValueConstraint.h

@@ -23,8 +23,8 @@
  **   * context dependent mode, used during the search.
  **
  ** Invoking initializeCDOs method activates the context dependent mode, and the
- ** AbsoluteValueConstraint object synchronizes its state automatically with the central
- ** Context object.
+ ** AbsoluteValueConstraint object synchronizes its state automatically with the
+ ** central Context object.
  **/
 
 #ifndef __AbsoluteValueConstraint_h__
@@ -34,7 +34,6 @@
 
 class AbsoluteValueConstraint : public PiecewiseLinearConstraint
 {
-
 public:
     /*
       The f variable is the absolute value of the b variable:
@@ -61,8 +60,8 @@ class AbsoluteValueConstraint : public PiecewiseLinearConstraint
     /*
       Register/unregister the constraint with a talbeau.
      */
-    void registerAsWatcher( ITableau *tableau) override;
-    void unregisterAsWatcher( ITableau *tableau) override;
+    void registerAsWatcher( ITableau *tableau ) override;
+    void unregisterAsWatcher( ITableau *tableau ) override;
 
     /*
       These callbacks are invoked when a watched variable's value
@@ -114,8 +113,8 @@ class AbsoluteValueConstraint : public PiecewiseLinearConstraint
 
     /*
        Returns a list of all cases - { ABS_POSITIVE, ABS_NEGATIVE }
-       The order of returned cases affects the search, and this method is where related
-       heuristics should be implemented.
+       The order of returned cases affects the search, and this method is where
+       related heuristics should be implemented.
      */
     List<PhaseStatus> getAllCases() const override;
 
@@ -133,7 +132,6 @@ class AbsoluteValueConstraint : public PiecewiseLinearConstraint
       Check whether the constraint's phase has been fixed.
      */
     void fixPhaseIfNeeded();
-    bool phaseFixed() const override;
 
     /*
       Preprocessing related functions, to inform that a variable has
@@ -233,4 +231,3 @@ class AbsoluteValueConstraint : public PiecewiseLinearConstraint
 };
 
 #endif // __AbsoluteValueConstraint_h__
-