diff --git a/src/common/Statistics.cpp b/src/common/Statistics.cpp index 2ebb9d54d3..2a69b0e85b 100644 --- a/src/common/Statistics.cpp +++ b/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 ) ); diff --git a/src/engine/AbsoluteValueConstraint.cpp b/src/engine/AbsoluteValueConstraint.cpp index 41944d27e9..158cb3330c 100644 --- a/src/engine/AbsoluteValueConstraint.cpp +++ b/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 AbsoluteValueConstraint::getPossibleFixes() return fixes; } -List AbsoluteValueConstraint::getSmartFixes( ITableau */* tableau */ ) const +List 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 &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 ); diff --git a/src/engine/AbsoluteValueConstraint.h b/src/engine/AbsoluteValueConstraint.h index 5d01c00d77..bdd25b6216 100644 --- a/src/engine/AbsoluteValueConstraint.h +++ b/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 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__ - diff --git a/src/engine/CDSmtCore.cpp b/src/engine/CDSmtCore.cpp deleted file mode 100644 index 46888c1b57..0000000000 --- a/src/engine/CDSmtCore.cpp +++ /dev/null @@ -1,479 +0,0 @@ -/********************* */ -/*! \file CDSmtCore.cpp - ** \verbatim - ** Top contributors (to current version): - ** Guy Katz, Aleksandar Zeljic, Haoze Wu, Parth Shah - ** This file is part of the Marabou project. - ** Copyright (c) 2017-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** See the description of the class in CDSmtCore.h. - **/ - -#include "CDSmtCore.h" - -#include "Debug.h" -#include "DivideStrategy.h" -#include "EngineState.h" -#include "FloatUtils.h" -#include "GlobalConfiguration.h" -#include "IEngine.h" -#include "MStringf.h" -#include "MarabouError.h" -#include "PseudoImpactTracker.h" -#include "ReluConstraint.h" - -using namespace CVC4::context; - -CDSmtCore::CDSmtCore( IEngine *engine, Context &ctx ) - : _statistics( NULL ) - , _context( ctx ) - , _trail( &_context ) - , _decisions( &_context ) - , _engine( engine ) - , _needToSplit( false ) - , _constraintForSplitting( NULL ) - , _constraintViolationThreshold - ( Options::CONSTRAINT_VIOLATION_THRESHOLD ) - , _deepSoIRejectionThreshold( Options::get()->getInt - ( Options::DEEP_SOI_REJECTION_THRESHOLD ) ) - , _branchingHeuristic( Options::get()->getDivideStrategy() ) - , _scoreTracker( nullptr ) - , _numRejectedPhasePatternProposal( 0 ) -{ -} - -CDSmtCore::~CDSmtCore() -{ -} - -void CDSmtCore::reportViolatedConstraint( PiecewiseLinearConstraint *constraint ) -{ - ASSERT( !constraint->phaseFixed() ); - - if ( !_constraintToViolationCount.exists( constraint ) ) - _constraintToViolationCount[constraint] = 0; - - ++_constraintToViolationCount[constraint]; - - if ( _constraintToViolationCount[constraint] >= - _constraintViolationThreshold ) - { - _needToSplit = true; - if ( GlobalConfiguration::SPLITTING_HEURISTICS == - DivideStrategy::ReLUViolation || !pickSplitPLConstraint() ) - // If pickSplitConstraint failed to pick one, use the native - // relu-violation based splitting heuristic. - _constraintForSplitting = constraint; - ASSERT( !_constraintForSplitting->phaseFixed() ); - } -} - -unsigned CDSmtCore::getViolationCounts( PiecewiseLinearConstraint *constraint ) const -{ - if ( !_constraintToViolationCount.exists( constraint ) ) - return 0; - - return _constraintToViolationCount[constraint]; -} - -void CDSmtCore::initializeScoreTrackerIfNeeded( const - List - &plConstraints ) -{ - if ( GlobalConfiguration::USE_DEEPSOI_LOCAL_SEARCH ) - { - _scoreTracker = std::unique_ptr - ( new PseudoImpactTracker() ); - _scoreTracker->initialize( plConstraints ); - - SMT_LOG( "\tTracking Pseudo Impact..." ); - } -} - -void CDSmtCore::reportRejectedPhasePatternProposal() -{ - ++_numRejectedPhasePatternProposal; - - if ( _numRejectedPhasePatternProposal >= - _deepSoIRejectionThreshold ) - { - _needToSplit = true; - if ( !pickSplitPLConstraint() ) - // If pickSplitConstraint failed to pick one, use the native - // relu-violation based splitting heuristic. - _constraintForSplitting = _scoreTracker->topUnfixed(); - } -} - -bool CDSmtCore::needToSplit() const -{ - return _needToSplit; -} - -void CDSmtCore::pushDecision( PiecewiseLinearConstraint *constraint, PhaseStatus decision ) -{ - SMT_LOG( Stringf( "Decision @ %d )", _context.getLevel() + 1 ).ascii() ); - TrailEntry te( constraint, decision ); - applyTrailEntry( te, true ); - SMT_LOG( Stringf( "Decision push @ %d DONE", _context.getLevel() ).ascii() ); -} - -void CDSmtCore::pushImplication( PiecewiseLinearConstraint *constraint ) -{ - ASSERT( constraint->isImplication() ); - SMT_LOG( Stringf( "Implication @ %d ... ", _context.getLevel() ).ascii() ); - TrailEntry te( constraint, constraint->nextFeasibleCase() ); - applyTrailEntry( te, false ); - SMT_LOG( Stringf( "Implication @ %d DONE", _context.getLevel() ).ascii() ); -} - -void CDSmtCore::applyTrailEntry( TrailEntry &te, bool isDecision ) -{ - if ( isDecision ) - { - _context.push(); - _decisions.push_back( te ); - } - - _trail.push_back( te ); - _engine->applySplit( te.getPiecewiseLinearCaseSplit() ); -} - -void CDSmtCore::decide() -{ - ASSERT( _needToSplit ); - SMT_LOG( "Performing a ReLU split" ); - - _numRejectedPhasePatternProposal = 0; - // Maybe the constraint has already become inactive - if so, ignore - // TODO: Ideally we will not ever reach this point - // TODO: Maintain a vector of constraints above the threshold - // Iterate until we find an active one - if ( !_constraintForSplitting->isActive() ) - { - _needToSplit = false; - _constraintToViolationCount[_constraintForSplitting] = 0; - _constraintForSplitting = nullptr; - return; - } - - ASSERT( _constraintForSplitting->isActive() ); - _needToSplit = false; - _constraintForSplitting->setActiveConstraint( false ); - - decideSplit( _constraintForSplitting ); -} - -void CDSmtCore::decideSplit( PiecewiseLinearConstraint *constraint ) -{ - struct timespec start = TimeUtils::sampleMicro(); - - if ( _statistics ) - { - _statistics->incUnsignedAttribute( Statistics::NUM_SPLITS ); - _statistics->incUnsignedAttribute( Statistics::NUM_VISITED_TREE_STATES ); - } - - if ( !constraint->isFeasible() ) - throw MarabouError( MarabouError::DEBUGGING_ERROR ); - ASSERT( constraint->isFeasible() ); - ASSERT( !constraint->isImplication() ); - - PhaseStatus decision = constraint->nextFeasibleCase(); - pushDecision( constraint, decision ); - - if ( _statistics ) - { - unsigned level = _context.getLevel(); - _statistics->setUnsignedAttribute( Statistics::CURRENT_DECISION_LEVEL, - level ); - if ( level > _statistics->getUnsignedAttribute - ( Statistics::MAX_DECISION_LEVEL ) ) - _statistics->setUnsignedAttribute( Statistics::MAX_DECISION_LEVEL, - level ); - - struct timespec end = TimeUtils::sampleMicro(); - _statistics->incLongAttribute( Statistics::TOTAL_TIME_SMT_CORE_MICRO, TimeUtils::timePassed( start, end ) ); - } - SMT_LOG( "Performing a ReLU split - DONE" ); -} - - -unsigned CDSmtCore::getDecisionLevel() const -{ - return _decisions.size(); -} - -bool CDSmtCore::popDecisionLevel( TrailEntry &lastDecision ) -{ - //ASSERT( static_cast( _context.getLevel() ) == _decisions.size() ); - if ( _decisions.empty() ) - return false; - - SMT_LOG( "Popping trail ..." ); - lastDecision = _decisions.back(); - _context.pop(); - _engine->postContextPopHook(); - SMT_LOG( Stringf( "to %d DONE", _context.getLevel() ).ascii() ); - return true; -} - -void CDSmtCore::interruptIfCompliantWithDebugSolution() -{ - if ( checkSkewFromDebuggingSolution() ) - { - SMT_LOG( "Error! Popping from a compliant stack\n" ); - throw MarabouError( MarabouError::DEBUGGING_ERROR ); - } -} - -PiecewiseLinearCaseSplit CDSmtCore::getDecision( unsigned decisionLevel ) const -{ - ASSERT( decisionLevel <= getDecisionLevel() ); - ASSERT( decisionLevel > 0 ); - return _decisions[decisionLevel - 1].getPiecewiseLinearCaseSplit(); -} - -bool CDSmtCore::backtrackToFeasibleDecision( TrailEntry &lastDecision ) -{ - SMT_LOG( "Backtracking to a feasible decision..." ); - - if ( getDecisionLevel() == 0 ) - return false; - - popDecisionLevel( lastDecision ); - lastDecision.markInfeasible(); - - while ( !lastDecision.isFeasible() ) - { - interruptIfCompliantWithDebugSolution(); - - if ( !popDecisionLevel( lastDecision ) ) - return false; - - lastDecision.markInfeasible(); - } - - interruptIfCompliantWithDebugSolution(); - - return true; -} - -bool CDSmtCore::backtrackAndContinueSearch() -{ - TrailEntry feasibleDecision( nullptr, CONSTRAINT_INFEASIBLE ); - struct timespec start = TimeUtils::sampleMicro(); - - if ( !backtrackToFeasibleDecision( feasibleDecision ) ) - return false; - - ASSERT( feasibleDecision.isFeasible() ); - - if ( _statistics ) - _statistics->incUnsignedAttribute( Statistics::NUM_VISITED_TREE_STATES ); - - PiecewiseLinearConstraint *pwlc = feasibleDecision._pwlConstraint; - if ( pwlc->isImplication() ) - pushImplication( pwlc ); - else - decideSplit( pwlc ); - - if ( _statistics ) - { - unsigned level = _context.getLevel(); - _statistics->setUnsignedAttribute( Statistics::CURRENT_DECISION_LEVEL, - level ); - if ( level > _statistics->getUnsignedAttribute - ( Statistics::MAX_DECISION_LEVEL ) ) - _statistics->setUnsignedAttribute( Statistics::MAX_DECISION_LEVEL, - level ); - struct timespec end = TimeUtils::sampleMicro(); - _statistics->incLongAttribute( Statistics::TOTAL_TIME_SMT_CORE_MICRO, TimeUtils::timePassed( start, end ) ); - } - - checkSkewFromDebuggingSolution(); - return true; -} - -void CDSmtCore::resetReportedViolations() -{ - _constraintToViolationCount.clear(); - _numRejectedPhasePatternProposal = 0; - _needToSplit = false; -} - -void CDSmtCore::allSplitsSoFar( List &result ) const -{ - result.clear(); - - for ( auto trailEntry : _trail ) - result.append( trailEntry.getPiecewiseLinearCaseSplit() ); -} - -void CDSmtCore::setStatistics( Statistics *statistics ) -{ - _statistics = statistics; -} - -void CDSmtCore::storeDebuggingSolution( const Map &debuggingSolution ) -{ - _debuggingSolution = debuggingSolution; -} - -// Return true if stack is currently compliant, false otherwise -// If there is no stored solution, return false --- incompliant. -bool CDSmtCore::checkSkewFromDebuggingSolution() -{ - if ( _debuggingSolution.empty() ) - return false; - - String error; - - int decisionLevel = 0; - bool isDecision = false; - // First check that the valid splits implied at the root level are okay - for ( const auto &trailEntry : _trail ) - { - if ( trailEntry._pwlConstraint != _decisions[decisionLevel]._pwlConstraint ) - isDecision = false; - else - { - ASSERT( trailEntry._phase == _decisions[decisionLevel]._phase ); - isDecision = true; - ++decisionLevel; - } - - PiecewiseLinearCaseSplit caseSplit = trailEntry.getPiecewiseLinearCaseSplit(); - if ( decisionLevel == 0 ) - { - if ( !splitAllowsStoredSolution( caseSplit, error ) ) - { - printf( "Error with one of the splits implied at root level:\n\t%s\n", error.ascii() ); - throw MarabouError( MarabouError::DEBUGGING_ERROR ); - } - } - else - { - // If the active split is non-compliant but there are alternatives, - // i.e. it was a decision, that's fine - if ( isDecision && !splitAllowsStoredSolution( caseSplit, error ) ) - { - // Active split is non-compliant but this is fine, because there - // are alternatives. We're done. - return false; - } - else // Implied split - { - if ( !splitAllowsStoredSolution( caseSplit, error ) ) - { - printf( "Error with one of the splits implied at this stack level:\n\t%s\n", - error.ascii() ); - throw MarabouError( MarabouError::DEBUGGING_ERROR ); - } - } - } - } - - // No problems were detected, the stack is compliant with the stored solution - return true; -} - -bool CDSmtCore::splitAllowsStoredSolution( const PiecewiseLinearCaseSplit &split, String &error ) const -{ - // False if the split prevents one of the values in the stored solution, true otherwise. - error = ""; - if ( _debuggingSolution.empty() ) - return true; - - for ( const auto bound : split.getBoundTightenings() ) - { - unsigned variable = bound._variable; - - // If the possible solution doesn't care about this variable, - // ignore it - if ( !_debuggingSolution.exists( variable ) ) - continue; - - // Otherwise, check that the bound is consistent with the solution - double solutionValue = _debuggingSolution[variable]; - double boundValue = bound._value; - - if ( ( bound._type == Tightening::LB ) && FloatUtils::gt( boundValue, solutionValue ) ) - { - error = Stringf( "Variable %u: new LB is %.5lf, which contradicts possible solution %.5lf", - variable, - boundValue, - solutionValue ); - return false; - } - else if ( ( bound._type == Tightening::UB ) && FloatUtils::lt( boundValue, solutionValue ) ) - { - error = Stringf( "Variable %u: new UB is %.5lf, which contradicts possible solution %.5lf", - variable, - boundValue, - solutionValue ); - return false; - } - } - - return true; -} - -void CDSmtCore::setConstraintViolationThreshold( unsigned threshold ) -{ - _constraintViolationThreshold = threshold; -} - -PiecewiseLinearConstraint *CDSmtCore::chooseViolatedConstraintForFixing( List &_violatedPlConstraints ) const -{ - ASSERT( !_violatedPlConstraints.empty() ); - - if ( !GlobalConfiguration::USE_LEAST_FIX ) - return *_violatedPlConstraints.begin(); - - PiecewiseLinearConstraint *candidate; - - // Apply the least fix heuristic - auto it = _violatedPlConstraints.begin(); - - candidate = *it; - unsigned minFixes = getViolationCounts( candidate ); - - PiecewiseLinearConstraint *contender; - unsigned contenderFixes; - while ( it != _violatedPlConstraints.end() ) - { - contender = *it; - contenderFixes = getViolationCounts( contender ); - if ( contenderFixes < minFixes ) - { - minFixes = contenderFixes; - candidate = contender; - } - - ++it; - } - - return candidate; -} - -bool CDSmtCore::pickSplitPLConstraint() -{ - if ( _needToSplit ) - _constraintForSplitting = _engine->pickSplitPLConstraint - ( _branchingHeuristic ); - return _constraintForSplitting != NULL; -} - -void CDSmtCore::reset() -{ - _context.popto( 0 ); - _engine->postContextPopHook(); - _needToSplit = false; - _constraintForSplitting = NULL; - _constraintToViolationCount.clear(); - _numRejectedPhasePatternProposal = 0; -} diff --git a/src/engine/CDSmtCore.h b/src/engine/CDSmtCore.h deleted file mode 100644 index 31dedf9813..0000000000 --- a/src/engine/CDSmtCore.h +++ /dev/null @@ -1,333 +0,0 @@ -/********************* */ -/*! \file CDSmtCore.h - ** \verbatim - ** Top contributors (to current version): - ** Guy Katz, AleksandarZeljic, Haoze Wu, Parth Shah - ** This file is part of the Marabou project. - ** Copyright (c) 2017-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** The CDSmtCore class implements a context-dependent SmtCore class. - ** The CDSmtCore distinguishes between: **decisions** and **implications**. - ** - ** Decision is a case of PiecewiseLinearConstraint asserted on the trail. - ** A decision is a choice between multiple feasible cases of a - ** PiecewiseLinearConstraint and represents nodes in the search tree. - ** - ** Implication is the last feasible case of a PiecewiseLinearConstraint and as - ** soon as it is detected it is asserted on the trail. - ** - ** Case splitting on a PiecewiseLinearConstraint performs a decision. - ** Fixing a case of a PiecewiseLinearConstraint (e.g., via bound propagation or - ** by exhausting all other cases) performs an implication. - ** - ** The overall search state is stored in a distributed way: - ** - CDSmtCore::_trail is the current search state in a chronological order - ** - PiecewiseLinearConstraints' infeasible cases enumerate all the explored - ** states w.r.t to the chronological order on the _trail. - ** - ** _trail is a chronological list of cases of PiecewiseLinearConstraints - ** asserted to hold (as TrailEntries) - both decisions and implications. - ** _decisions is a chronological list of decisions stored on the trail. - ** _trail and _decisions are both context dependent and will synchronize in - ** unison with the _context object. - ** - ** When a search state is found to be infeasible, CDSmtCore backtracks to the - ** last decision and continues the search. - ** - ** PushDecision advances the decision level and context level. - ** popDecisionLevel backtracks the last decision and context level. - ** - ** Advancing a context level creates a synchronization point to which all - ** context dependent members can backtrack in unison. - ** Backtracking a context level restores all context dependent members to the - ** state of the last synchronization point. This operation is O(1) complexity. - ** - ** Since the entire search state is context dependent, backtracking the context - ** (via popDecisionLevel) backtracks the entire Marabou search state. - ** The only exception is the labeling of basic/non-basic variables in the - ** tableau, which may need to be recalculated using Tableau's - ** postContextPopHook exposed via Engine. - ** - ** Implementation relies on: - ** - ** - _context is a unique Context object from which all the context-dependent - ** structures are obtained. - ** - ** - PiecewiseLinearConstraint class stores its search state in a - ** context-dependent manner and exposes it using nextFeasibleCase() and - ** markInfeasible() methods. - ** - ** - Using BoundManager class to store bounds in a context-dependent manner - **/ - -#ifndef __CDSmtCore_h__ -#define __CDSmtCore_h__ - -#include "Options.h" -#include "PiecewiseLinearCaseSplit.h" -#include "PiecewiseLinearConstraint.h" -#include "PLConstraintScoreTracker.h" -#include "Stack.h" -#include "Statistics.h" -#include "TrailEntry.h" -#include "context/cdlist.h" -#include "context/context.h" - -#define SMT_LOG( x, ... ) LOG( GlobalConfiguration::SMT_CORE_LOGGING, "CDSmtCore: %s\n", x ) - -class EngineState; -class Engine; -class String; - -class CDSmtCore -{ -public: - CDSmtCore( IEngine *engine, CVC4::context::Context &context ); - ~CDSmtCore(); - - /* - Clear the stack. - */ - void freeMemory(); - - /* - Initialize the score tracker with the given list of pl constraints. - */ - void initializeScoreTrackerIfNeeded( const List - &plConstraints ); - - /* - Inform the SMT core that a SoI phase pattern proposal is rejected. - */ - void reportRejectedPhasePatternProposal(); - - /* - Update the score of the constraint with the given score in the costTracker. - */ - inline void updatePLConstraintScore( PiecewiseLinearConstraint *constraint, - double score ) - { - ASSERT( _scoreTracker != nullptr ); - _scoreTracker->updateScore( constraint, score ); - } - - /* - Get the constraint in the score tracker with the highest score - */ - inline PiecewiseLinearConstraint *getConstraintsWithHighestScore() const - { - return _scoreTracker->topUnfixed(); - } - - /* - Inform the SMT core that a PL constraint is violated. - */ - void reportViolatedConstraint( PiecewiseLinearConstraint *constraint ); - - /* - Get the number of times a specific PL constraint has been reported as - violated. - */ - unsigned getViolationCounts( PiecewiseLinearConstraint *constraint ) const; - - /* - Reset all reported violation counts. - */ - void resetReportedViolations(); - - /* - Returns true iff the SMT core wants to perform a case split. - */ - bool needToSplit() const; - - /* - Push TrailEntry representing the decision onto the trail. - */ - void pushDecision( PiecewiseLinearConstraint *constraint, PhaseStatus decision ); - - /* - Inform SmtCore of an implied (formerly valid) case split that was discovered. - */ - void pushImplication( PiecewiseLinearConstraint *constraint ); - - /* - Pushes trail entry onto trail, handles decision book-keeping and - update bounds and add equations to the engine. - */ - void applyTrailEntry( TrailEntry &te, bool isDecision = false ); - - /* - Decide and apply a case split using the constraint marked for splitting. - */ - void decide(); - - /* - Decide a constraint's feasible case. Update bounds, add equations - and trail. - */ - void decideSplit( PiecewiseLinearConstraint *constraint ); - - /* - Backtracks fully explored decisions and stores the last feasible decision - */ - bool backtrackToFeasibleDecision( TrailEntry &feasibleDecision ); - - /* - Return to a feasible state and resume search by asserting the next case - (as either a decision or implication) - */ - bool backtrackAndContinueSearch(); - - /* - Pop a stack frame. Return true if successful, false if the stack is empty. - */ - bool popSplit(); - - /* - Pop a context level - lazily backtracking trail, bounds, etc. - Return true if successful, false if the stack is empty. - */ - bool popDecisionLevel( TrailEntry &lastDecision ); - - /* - The current stack depth. - */ - unsigned getDecisionLevel() const; - - /* - Return a list of all splits performed so far, both SMT-originating and - valid ones, in the correct order. - */ - void allSplitsSoFar( List &result ) const; - - /* - Get trail begin iterator. - */ - CVC4::context::CDList::const_iterator trailBegin() const - { - return _trail.begin(); - }; - - /* - Get trail end iterator. - */ - CVC4::context::CDList::const_iterator trailEnd() const - { - return _trail.end(); - }; - - /* - Have the SMT core start reporting statistics. - */ - void setStatistics( Statistics *statistics ); - - /* - Have the SMT core choose, among a set of violated PL constraints, which - constraint should be repaired (without splitting) - */ - PiecewiseLinearConstraint *chooseViolatedConstraintForFixing( List &_violatedPlConstraints ) const; - - void setConstraintViolationThreshold( unsigned threshold ); - - inline void setBranchingHeuristics( DivideStrategy strategy ) - { - _branchingHeuristic = strategy; - } - - /* - Pick the piecewise linear constraint for splitting, returns true - if a constraint for splitting is successfully picked - */ - bool pickSplitPLConstraint(); - - /* - * For testing purposes - */ - PiecewiseLinearCaseSplit getDecision( unsigned decisionLevel ) const; - - void reset(); - - /* - For debugging purposes only - store a correct possible solution - TODO: Create a user interface for this - */ - void storeDebuggingSolution( const Map &debuggingSolution ); - bool checkSkewFromDebuggingSolution(); - bool splitAllowsStoredSolution( const PiecewiseLinearCaseSplit &split, String &error ) const; - void interruptIfCompliantWithDebugSolution(); -private: - /* - Collect and print various statistics. - */ - Statistics *_statistics; - - /* - CVC4 Context, constructed in Engine - */ - CVC4::context::Context &_context; - - /* - Trail is context dependent and contains all the asserted PWLCaseSplits - */ - CVC4::context::CDList _trail; - - /* - * _decisions stores the decision TrailEntries - */ - CVC4::context::CDList _decisions; - - /* - The engine. - */ - IEngine *_engine; - - /* - Do we need to perform a split and on which constraint. - */ - bool _needToSplit; - PiecewiseLinearConstraint *_constraintForSplitting; - - /* - Count how many times each constraint has been violated. - */ - Map _constraintToViolationCount; - - /* - For debugging purposes only - */ - Map _debuggingSolution; - - /* - Split when some relu has been violated for this many times during the - Reluplex procedure - */ - unsigned _constraintViolationThreshold; - - /* - Split when there have been this many rejected phase pattern proposal - during the SoI-based local search. - */ - unsigned _deepSoIRejectionThreshold; - - /* - The strategy to pick the piecewise linear constraint to branch on. - */ - DivideStrategy _branchingHeuristic; - - /* - Heap to store the scores of each PLConstraint. - */ - std::unique_ptr _scoreTracker; - - /* - Number of times the phase pattern proposal has been rejected at the - current search state. - */ - unsigned _numRejectedPhasePatternProposal; - -}; - -#endif // __CDSmtCore_h__ diff --git a/src/engine/DisjunctionConstraint.cpp b/src/engine/DisjunctionConstraint.cpp index 0519af3b52..fb419fcfa2 100644 --- a/src/engine/DisjunctionConstraint.cpp +++ b/src/engine/DisjunctionConstraint.cpp @@ -49,24 +49,24 @@ DisjunctionConstraint::DisjunctionConstraint( const String &serializedDisjunctio ( 5, serializedDisjunction.length() - 5 ); List values = serializedValues.tokenize( "," ); auto val = values.begin(); - unsigned numDisjuncts = atoi(val->ascii()); + unsigned numDisjuncts = atoi( val->ascii() ); ++val; for ( unsigned i = 0; i < numDisjuncts; ++i ) { PiecewiseLinearCaseSplit split; - unsigned numBounds = atoi(val->ascii()); + unsigned numBounds = atoi( val->ascii() ); ++val; for ( unsigned bi = 0; bi < numBounds; ++bi ) { - Tightening::BoundType type = ( *val == "l") ? Tightening::LB : Tightening::UB; + Tightening::BoundType type = ( *val == "l" ) ? Tightening::LB : Tightening::UB; ++val; - unsigned var = atoi(val->ascii()); + unsigned var = atoi( val->ascii() ); ++val; - double bd = atof(val->ascii()); + double bd = atof( val->ascii() ); ++val; - split.storeBoundTightening( Tightening(var, bd, type) ); + split.storeBoundTightening( Tightening( var, bd, type ) ); } - unsigned numEquations = atoi(val->ascii()); + unsigned numEquations = atoi( val->ascii() ); ++val; for ( unsigned ei = 0; ei < numEquations; ++ei ) @@ -78,29 +78,29 @@ DisjunctionConstraint::DisjunctionConstraint( const String &serializedDisjunctio type = Equation::GE; else { - ASSERT( *val == "e"); + ASSERT( *val == "e" ); } - Equation eq(type); + Equation eq( type ); ++val; - unsigned numAddends = atoi(val->ascii()); + unsigned numAddends = atoi( val->ascii() ); ++val; for ( unsigned ai = 0; ai < numAddends; ++ai ) { - double coef = atof(val->ascii()); + double coef = atof( val->ascii() ); ++val; - unsigned var = atoi(val->ascii()); + unsigned var = atoi( val->ascii() ); ++val; eq.addAddend( coef, var ); } - eq.setScalar(atof(val->ascii())); + eq.setScalar( atof( val->ascii() ) ); ++val; - split.addEquation(eq); + split.addEquation( eq ); } - disjuncts.append(split); + disjuncts.append( split ); } _disjuncts = disjuncts; - for ( unsigned ind = 0; ind < disjuncts.size(); ++ind ) + for ( unsigned ind = 0; ind < disjuncts.size(); ++ind ) _feasibleDisjuncts.append( ind ); extractParticipatingVariables(); @@ -151,10 +151,12 @@ void DisjunctionConstraint::notifyLowerBound( unsigned variable, double bound ) if ( _boundManager == nullptr && existsLowerBound( variable ) && !FloatUtils::gt( bound, getLowerBound( variable ) ) ) - return; + return; setLowerBound( variable, bound ); + // TODO: Maintain a mapping from variables to disjuncts and only check relevant + // disjuncts for feasibility updateFeasibleDisjuncts(); } @@ -165,10 +167,12 @@ void DisjunctionConstraint::notifyUpperBound( unsigned variable, double bound ) if ( _boundManager == nullptr && existsUpperBound( variable ) && !FloatUtils::lt( bound, getUpperBound( variable ) ) ) - return; + return; setUpperBound( variable, bound ); + // TODO: Maintain a mapping from variables to disjuncts and only check relevant + // disjuncts for feasibility updateFeasibleDisjuncts(); } @@ -203,7 +207,7 @@ List DisjunctionConstraint::getPossibleFixes() c return List(); } -List DisjunctionConstraint::getSmartFixes( ITableau */* tableau */ ) const +List DisjunctionConstraint::getSmartFixes( ITableau * /* tableau */ ) const { // Reluplex does not currently work with Gurobi. ASSERT( _gurobi == NULL ); @@ -226,17 +230,20 @@ List DisjunctionConstraint::getAllCases() const PiecewiseLinearCaseSplit DisjunctionConstraint::getCaseSplit( PhaseStatus phase ) const { + ASSERT( phase != PHASE_NOT_FIXED ); return _disjuncts.get( phaseStatusToInd( phase ) ); } -bool DisjunctionConstraint::phaseFixed() const +PhaseStatus DisjunctionConstraint::getPhaseStatus() const { - return _feasibleDisjuncts.size() == 1; + ASSERT( phaseFixed() ); + return indToPhaseStatus( *_feasibleDisjuncts.begin() ); } PiecewiseLinearCaseSplit DisjunctionConstraint::getImpliedCaseSplit() const { - return _disjuncts.get( *_feasibleDisjuncts.begin() ); + ASSERT( isImplication() ); + return _disjuncts.get( phaseStatusToInd( getImpliedCase() ) ); } PiecewiseLinearCaseSplit DisjunctionConstraint::getValidCaseSplit() const @@ -244,8 +251,7 @@ PiecewiseLinearCaseSplit DisjunctionConstraint::getValidCaseSplit() const return getImpliedCaseSplit(); } -void DisjunctionConstraint::transformToUseAuxVariables( InputQuery - &inputQuery ) +void DisjunctionConstraint::transformToUseAuxVariables( InputQuery &inputQuery ) { Vector newDisjuncts; for ( const auto &disjunct : _disjuncts ) @@ -336,6 +342,8 @@ void DisjunctionConstraint::dump( String &output ) const } output += Stringf( "Active? %s.", _constraintActive ? "Yes" : "No" ); + + serializeInfeasibleCases( output ); } void DisjunctionConstraint::updateVariableIndex( unsigned oldIndex, unsigned newIndex ) @@ -378,42 +386,42 @@ void DisjunctionConstraint::eliminateVariable( unsigned /* variable */, double / bool DisjunctionConstraint::constraintObsolete() const { - return _feasibleDisjuncts.empty(); + return false; // A Disjunction is obsolete only when a literal is always true. } -void DisjunctionConstraint::getEntailedTightenings( List &/* tightenings */ ) const +void DisjunctionConstraint::getEntailedTightenings( List & /* tightenings */ ) const { } String DisjunctionConstraint::serializeToString() const { String s = "disj,"; - s += Stringf("%u,", _disjuncts.size()); + s += Stringf( "%u,", _disjuncts.size() ); for ( const auto &disjunct : _disjuncts ) { - s += Stringf("%u,", disjunct.getBoundTightenings().size()); + s += Stringf( "%u,", disjunct.getBoundTightenings().size() ); for ( const auto &bound : disjunct.getBoundTightenings() ) { if ( bound._type == Tightening::LB ) - s += Stringf("l,%u,%f,", bound._variable, bound._value); + s += Stringf( "l,%u,%f,", bound._variable, bound._value ); else if ( bound._type == Tightening::UB ) - s += Stringf("u,%u,%f,", bound._variable, bound._value); + s += Stringf( "u,%u,%f,", bound._variable, bound._value ); } - s += Stringf("%u,", disjunct.getEquations().size()); + s += Stringf( "%u,", disjunct.getEquations().size() ); for ( const auto &equation : disjunct.getEquations() ) { if ( equation._type == Equation::LE ) - s += Stringf("l,"); + s += Stringf( "l," ); else if ( equation._type == Equation::GE ) - s += Stringf("g,"); + s += Stringf( "g," ); else - s += Stringf("e,"); - s += Stringf("%u,", equation._addends.size()); + s += Stringf( "e," ); + s += Stringf( "%u,", equation._addends.size() ); for ( const auto &addend : equation._addends ) { - s += Stringf("%f,%u,", addend._coefficient, addend._variable); + s += Stringf( "%f,%u,", addend._coefficient, addend._variable ); } - s += Stringf("%f,", equation._scalar ); + s += Stringf( "%f,", equation._scalar ); } } return s; @@ -471,23 +479,25 @@ bool DisjunctionConstraint::disjunctSatisfied( const PiecewiseLinearCaseSplit &d void DisjunctionConstraint::updateFeasibleDisjuncts() { - _feasibleDisjuncts.clear(); - - for ( unsigned ind = 0; ind < _disjuncts.size(); ++ind ) + if ( _cdInfeasibleCases ) { - if ( disjunctIsFeasible( ind ) ) - _feasibleDisjuncts.append( ind ); - else if ( _cdInfeasibleCases && !isCaseInfeasible( indToPhaseStatus( ind ) ) ) - markInfeasible( indToPhaseStatus( ind ) ); + for ( unsigned ind = 0; ind < _disjuncts.size(); ++ind ) + { + if ( !isCaseInfeasible( indToPhaseStatus( ind ) ) && + !caseSplitIsFeasible( _disjuncts.get( ind ) ) ) + markInfeasible( indToPhaseStatus( ind ) ); + } } -} - -bool DisjunctionConstraint::disjunctIsFeasible( unsigned ind ) const -{ - if ( _cdInfeasibleCases && isCaseInfeasible( indToPhaseStatus( ind ) ) ) - return false; + else + { + _feasibleDisjuncts.clear(); - return caseSplitIsFeasible( _disjuncts.get( ind ) ); + for ( unsigned ind = 0; ind < _disjuncts.size(); ++ind ) + { + if ( caseSplitIsFeasible( _disjuncts.get( ind ) ) ) + _feasibleDisjuncts.append( ind ); + } + } } bool DisjunctionConstraint::caseSplitIsFeasible( const PiecewiseLinearCaseSplit &disjunct ) const diff --git a/src/engine/DisjunctionConstraint.h b/src/engine/DisjunctionConstraint.h index e39448ffa1..e6026e901f 100644 --- a/src/engine/DisjunctionConstraint.h +++ b/src/engine/DisjunctionConstraint.h @@ -2,7 +2,7 @@ /*! \file DisjunctionConstraint.h ** \verbatim ** Top contributors (to current version): - ** Guy Katz, Duligur Ibeling, Christopher Lazarus, Haoze Wu + ** Guy Katz, Duligur Ibeling, Christopher Lazarus, Haoze Wu, Aleksandar Zeljic ** This file is part of the Marabou project. ** Copyright (c) 2017-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. @@ -13,28 +13,34 @@ ** e1 \/ e2 \/ ... \/ eM, where _elements = { e1, e2, ..., eM } ** ** The constraint introduces identifiers for its PiecewiseLinearCaseSplit - ** elements. + ** elements. The mapping between the cases (PhaseStatus) and local indices is + ** available via indToPhaseStatus and phaseStatusToInd methods. ** ** The constraint is implemented as PiecewiseLinearConstraint ** and operates in two modes: - ** * pre-processing mode, which stores bounds locally, and - ** * context dependent mode, used during the search. + ** * pre-processing mode, which stores _feasibleDisjuncts locally, and + ** * context dependent mode, used during the SMT search. ** ** Invoking initializeCDOs method activates the context dependent mode, and the ** DisjunctionConstraint object synchronizes its state automatically with the central ** Context object. + ** + ** TODOs: + ** - Eliminate updateFeasibleDisjuncts (and its quadratic complexity) by + ** introducing a map between variables and the disjuncts they participate in + ** which enables direct access to disjunct to check feasibility. **/ #ifndef __DisjunctionConstraint_h__ #define __DisjunctionConstraint_h__ -#include "Vector.h" #include "PiecewiseLinearConstraint.h" +#include "Vector.h" class DisjunctionConstraint : public PiecewiseLinearConstraint { public: - ~DisjunctionConstraint() {}; + ~DisjunctionConstraint(){}; DisjunctionConstraint( const List &disjuncts ); DisjunctionConstraint( const Vector &disjuncts ); DisjunctionConstraint( const String &serializedDisjunction ); @@ -118,11 +124,6 @@ class DisjunctionConstraint : public PiecewiseLinearConstraint */ PiecewiseLinearCaseSplit getCaseSplit( PhaseStatus phase ) const override; - /* - Check if the constraint's phase has been fixed. - */ - bool phaseFixed() const override; - /* If the constraint's phase has been fixed, get the implied case split. */ @@ -153,7 +154,7 @@ class DisjunctionConstraint : public PiecewiseLinearConstraint virtual bool supportVariableElimination() const override { - return false; + return false; } /* @@ -172,6 +173,8 @@ class DisjunctionConstraint : public PiecewiseLinearConstraint */ String serializeToString() const override; + PhaseStatus getPhaseStatus() const override; + private: /* The disjuncts that form this PL constraint @@ -206,8 +209,7 @@ class DisjunctionConstraint : public PiecewiseLinearConstraint still feasible, given the current variable bounds */ void updateFeasibleDisjuncts(); - bool disjunctIsFeasible( unsigned ind ) const; - bool caseSplitIsFeasible( const PiecewiseLinearCaseSplit & caseSplit ) const; + bool caseSplitIsFeasible( const PiecewiseLinearCaseSplit &caseSplit ) const; inline PhaseStatus indToPhaseStatus( unsigned ind ) const { @@ -216,7 +218,7 @@ class DisjunctionConstraint : public PiecewiseLinearConstraint inline unsigned phaseStatusToInd( PhaseStatus phase ) const { - //ASSERT( phase != PHASE_NOT_FIXED ); + // ASSERT( phase != PHASE_NOT_FIXED ); return static_cast( phase ) - 1; } }; diff --git a/src/engine/DnCWorker.cpp b/src/engine/DnCWorker.cpp index 455a8ef192..8420a8d483 100644 --- a/src/engine/DnCWorker.cpp +++ b/src/engine/DnCWorker.cpp @@ -101,7 +101,7 @@ void DnCWorker::popOneSubQueryAndSolve( bool restoreTreeStates ) bool fullSolveNeeded = true; // denotes whether we need to solve the subquery if ( restoreTreeStates && smtState ) - fullSolveNeeded = _engine->restoreSmtState( *smtState ); + fullSolveNeeded = true; //_engine->restoreSmtState( *smtState ); IEngine::ExitCode result = IEngine::NOT_DONE; if ( fullSolveNeeded ) { @@ -141,7 +141,7 @@ void DnCWorker::popOneSubQueryAndSolve( bool restoreTreeStates ) { newSmtStates.push_back( std::unique_ptr ( new SmtState() ) ); - _engine->storeSmtState( *( newSmtStates[i] ) ); + //_engine->storeSmtState( *( newSmtStates[i] ) ); } } diff --git a/src/engine/Engine.cpp b/src/engine/Engine.cpp index 7776587e52..f344e5b5a7 100644 --- a/src/engine/Engine.cpp +++ b/src/engine/Engine.cpp @@ -40,7 +40,7 @@ Engine::Engine() , _tableau( _boundManager ) , _preprocessedQuery( nullptr ) , _rowBoundTightener( *_tableau ) - , _smtCore( this ) + , _smtCore( this, _context ) , _numPlConstraintsDisabledByValidSplits( 0 ) , _preprocessingEnabled( false ) , _initialStateStored( false ) @@ -91,6 +91,9 @@ Engine::~Engine() delete[] _work; _work = NULL; } + + for ( auto d : _disjunctionForSplitting ) + delete d; } void Engine::setVerbosity( unsigned verbosity ) @@ -163,7 +166,10 @@ bool Engine::solve( unsigned timeoutInSeconds ) // Register the boundManager with all the PL constraints for ( auto &plConstraint : _plConstraints ) + { plConstraint->registerBoundManager( &_boundManager ); + plConstraint->initializeCDOs( &_context ); + } if ( _solveWithMILP ) return solveWithMILPEncoding( timeoutInSeconds ); @@ -263,7 +269,7 @@ bool Engine::solve( unsigned timeoutInSeconds ) // Perform any SmtCore-initiated case splits if ( _smtCore.needToSplit() ) { - _smtCore.performSplit(); + _smtCore.decide(); splitJustPerformed = true; continue; } @@ -334,7 +340,7 @@ bool Engine::solve( unsigned timeoutInSeconds ) _tableau->toggleOptimization( false ); // The current query is unsat, and we need to pop. // If we're at level 0, the whole query is unsat. - if ( !_smtCore.popSplit() ) + if ( !_smtCore.backtrackAndContinueSearch() ) { struct timespec mainLoopEnd = TimeUtils::sampleMicro(); _statistics.incLongAttribute @@ -1258,6 +1264,8 @@ void Engine::initializeTableau( const double *constraintMatrix, const ListsetDimensions(); + _plConstraints = _preprocessedQuery->getPiecewiseLinearConstraints(); for ( const auto &constraint : _plConstraints ) { @@ -1644,27 +1652,18 @@ void Engine::restoreState( const EngineState &state ) _tableau->restoreState( state._tableauState, state._tableauStateStorageLevel ); - ENGINE_LOG( "\tRestoring constraint states" ); - for ( auto &constraint : _plConstraints ) - { - if ( !state._plConstraintToState.exists( constraint ) ) - throw MarabouError( MarabouError::MISSING_PL_CONSTRAINT_STATE ); - - constraint->restoreState( state._plConstraintToState[constraint] ); - } - _numPlConstraintsDisabledByValidSplits = state._numPlConstraintsDisabledByValidSplits; if ( _lpSolverType == LPSolverType::NATIVE ) { - // Make sure the data structures are initialized to the correct size - _rowBoundTightener->setDimensions(); - adjustWorkMemorySize(); - _activeEntryStrategy->resizeHook( _tableau ); - _costFunctionManager->initialize(); + // Make sure the data structures are initialized to the correct size + _rowBoundTightener->setDimensions(); + adjustWorkMemorySize(); + _activeEntryStrategy->resizeHook( _tableau ); + _costFunctionManager->initialize(); } - // Reset the violation counts in the SMT core + //Reset the violation counts in the SMT core _smtCore.resetSplitConditions(); } @@ -1951,17 +1950,16 @@ bool Engine::applyAllValidConstraintCaseSplits() bool Engine::applyValidConstraintCaseSplit( PiecewiseLinearConstraint *constraint ) { - if ( constraint->isActive() && constraint->phaseFixed() ) + if ( constraint->isActive() && ( constraint->phaseFixed() || constraint->isImplication() ) ) { String constraintString; + // This is a performance issue constraint->dump( constraintString ); ENGINE_LOG( Stringf( "A constraint has become valid. Dumping constraint: %s", constraintString.ascii() ).ascii() ); constraint->setActiveConstraint( false ); - PiecewiseLinearCaseSplit validSplit = constraint->getValidCaseSplit(); - _smtCore.recordImpliedValidSplit( validSplit ); - applySplit( validSplit ); + _smtCore.pushImplication( constraint ); if ( _soiManager ) _soiManager->removeCostComponentFromHeuristicCost( constraint ); ++_numPlConstraintsDisabledByValidSplits; @@ -2140,7 +2138,7 @@ void Engine::checkBoundCompliancyWithDebugSolution() var.second, _tableau->getLowerBound( var.first ) ); - throw MarabouError( MarabouError::DEBUGGING_ERROR ); + throw MarabouError( MarabouError::DEBUGGING_ERROR, "Check bound compliance with debug solution" ); } if ( FloatUtils::lt( _tableau->getUpperBound( var.first ), var.second, 1e-5 ) ) @@ -2151,7 +2149,7 @@ void Engine::checkBoundCompliancyWithDebugSolution() var.second, _tableau->getUpperBound( var.first ) ); - throw MarabouError( MarabouError::DEBUGGING_ERROR ); + throw MarabouError( MarabouError::DEBUGGING_ERROR, "Check bound compliance with debug solution" ); } } } @@ -2576,9 +2574,11 @@ PiecewiseLinearConstraint *Engine::pickSplitPLConstraintBasedOnIntervalWidth() List splits; splits.append( s1 ); splits.append( s2 ); - _disjunctionForSplitting = std::unique_ptr - ( new DisjunctionConstraint( splits ) ); - return _disjunctionForSplitting.get(); + _disjunctionForSplitting.append( new DisjunctionConstraint( splits ) ); + _disjunctionForSplitting.last()->registerBoundManager( &_boundManager ); + _disjunctionForSplitting.last()->initializeCDOs( &_context ); + + return _disjunctionForSplitting.last(); } } @@ -2590,7 +2590,7 @@ PiecewiseLinearConstraint *Engine::pickSplitPLConstraint( DivideStrategy PiecewiseLinearConstraint *candidatePLConstraint = NULL; if ( strategy == DivideStrategy::PseudoImpact ) { - if ( _smtCore.getStackDepth() > 3 ) + if ( _smtCore.getDecisionLevel() > 3 ) candidatePLConstraint = _smtCore.getConstraintsWithHighestScore(); else if ( _preprocessedQuery->getInputVariables().size() < GlobalConfiguration::INTERVAL_SPLITTING_THRESHOLD ) @@ -2603,7 +2603,7 @@ PiecewiseLinearConstraint *Engine::pickSplitPLConstraint( DivideStrategy else if ( strategy == DivideStrategy::EarliestReLU ) candidatePLConstraint = pickSplitPLConstraintBasedOnTopology(); else if ( strategy == DivideStrategy::LargestInterval && - ( _smtCore.getStackDepth() % + ( _smtCore.getDecisionLevel() % GlobalConfiguration::INTERVAL_SPLITTING_FREQUENCY == 0 ) ) { @@ -2631,68 +2631,6 @@ PiecewiseLinearConstraint *Engine::pickSplitPLConstraintSnC( SnCDivideStrategy s return candidatePLConstraint; } -bool Engine::restoreSmtState( SmtState & smtState ) -{ - try - { - ASSERT( _smtCore.getStackDepth() == 0 ); - - // Step 1: all implied valid splits at root - for ( auto &validSplit : smtState._impliedValidSplitsAtRoot ) - { - applySplit( validSplit ); - _smtCore.recordImpliedValidSplit( validSplit ); - } - - tightenBoundsOnConstraintMatrix(); - applyAllBoundTightenings(); - // For debugging purposes - checkBoundCompliancyWithDebugSolution(); - do - performSymbolicBoundTightening(); - while ( applyAllValidConstraintCaseSplits() ); - - // Step 2: replay the stack - for ( auto &stackEntry : smtState._stack ) - { - _smtCore.replaySmtStackEntry( stackEntry ); - // Do all the bound propagation, and set ReLU constraints to inactive (at - // least the one corresponding to the _activeSplit applied above. - tightenBoundsOnConstraintMatrix(); - applyAllBoundTightenings(); - // For debugging purposes - checkBoundCompliancyWithDebugSolution(); - do - performSymbolicBoundTightening(); - while ( applyAllValidConstraintCaseSplits() ); - - } - } - catch ( const InfeasibleQueryException & ) - { - // The current query is unsat, and we need to pop. - // If we're at level 0, the whole query is unsat. - if ( !_smtCore.popSplit() ) - { - if ( _verbosity > 0 ) - { - printf( "\nEngine::solve: UNSAT query\n" ); - _statistics.print(); - } - _exitCode = Engine::UNSAT; - for ( PiecewiseLinearConstraint *p : _plConstraints ) - p->setActiveConstraint( true ); - return false; - } - } - return true; -} - -void Engine::storeSmtState( SmtState & smtState ) -{ - _smtCore.storeSmtState( smtState ); -} - bool Engine::solveWithMILPEncoding( unsigned timeoutInSeconds ) { try diff --git a/src/engine/Engine.h b/src/engine/Engine.h index a18297596d..93988c9139 100644 --- a/src/engine/Engine.h +++ b/src/engine/Engine.h @@ -173,17 +173,6 @@ class Engine : public IEngine, public SignalHandler::Signalable */ void setVerbosity( unsigned verbosity ); - /* - Apply the stack to the newly created SmtCore, returns false if UNSAT is - found in this process. - */ - bool restoreSmtState( SmtState &smtState ); - - /* - Store the current stack of the smtCore into smtState - */ - void storeSmtState( SmtState &smtState ); - /* Pick the piecewise linear constraint for splitting */ @@ -410,7 +399,7 @@ class Engine : public IEngine, public SignalHandler::Signalable /* Disjunction that is used for splitting but doesn't exist in the beginning */ - std::unique_ptr _disjunctionForSplitting; + Vector _disjunctionForSplitting; /* Solve the query with MILP encoding diff --git a/src/engine/IEngine.h b/src/engine/IEngine.h index 8a5c4c4c1c..4536b2156f 100644 --- a/src/engine/IEngine.h +++ b/src/engine/IEngine.h @@ -72,17 +72,6 @@ class IEngine virtual void restoreState( const EngineState &state ) = 0; virtual void setNumPlConstraintsDisabledByValidSplits( unsigned numConstraints ) = 0; - /* - Store the current stack of the smtCore into smtState - */ - virtual void storeSmtState( SmtState &smtState ) = 0; - - /* - Apply the stack to the newly created SmtCore, returns false if UNSAT is - found in this process. - */ - virtual bool restoreSmtState( SmtState &smtState ) = 0; - /* Solve the encoded query. */ diff --git a/src/engine/MaxConstraint.cpp b/src/engine/MaxConstraint.cpp index 3ec796e2e4..296d6fbc52 100644 --- a/src/engine/MaxConstraint.cpp +++ b/src/engine/MaxConstraint.cpp @@ -503,7 +503,7 @@ void MaxConstraint::updateVariableIndex( unsigned oldIndex, unsigned newIndex ) _auxToElement[auxVar] = newIndex; if ( _phaseStatus == variableToPhase( oldIndex ) ) - _phaseStatus = variableToPhase( newIndex ) ; + _phaseStatus = variableToPhase( newIndex ); } else { @@ -615,7 +615,7 @@ void MaxConstraint::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; if ( phase == MAX_PHASE_ELIMINATED ) diff --git a/src/engine/MaxConstraint.h b/src/engine/MaxConstraint.h index fa36337eb0..a80097a03e 100644 --- a/src/engine/MaxConstraint.h +++ b/src/engine/MaxConstraint.h @@ -46,9 +46,9 @@ #ifndef __MaxConstraint_h__ #define __MaxConstraint_h__ -#include "PiecewiseLinearConstraint.h" #include "LinearExpression.h" #include "Map.h" +#include "PiecewiseLinearConstraint.h" #define MAX_VARIABLE_TO_PHASE_OFFSET 1 diff --git a/src/engine/PiecewiseLinearConstraint.cpp b/src/engine/PiecewiseLinearConstraint.cpp index 69523612f0..67efe67e17 100644 --- a/src/engine/PiecewiseLinearConstraint.cpp +++ b/src/engine/PiecewiseLinearConstraint.cpp @@ -14,6 +14,7 @@ **/ #include "PiecewiseLinearConstraint.h" + #include "Statistics.h" PiecewiseLinearConstraint::PiecewiseLinearConstraint() @@ -153,7 +154,7 @@ void PiecewiseLinearConstraint::initializeDuplicateCDOs( ASSERT( clone->_cdPhaseStatus != nullptr ); clone->_cdPhaseStatus = nullptr; clone->initializeCDPhaseStatus(); - clone->setPhaseStatus( this->getPhaseStatus() ); + clone->setPhaseStatus( *_cdPhaseStatus ); ASSERT( clone->_cdInfeasibleCases != nullptr ); clone->_cdInfeasibleCases = nullptr; @@ -168,13 +169,14 @@ void PiecewiseLinearConstraint::markInfeasible( _cdInfeasibleCases->push_back( infeasibleCase ); } -PhaseStatus PiecewiseLinearConstraint::nextFeasibleCase() +PhaseStatus PiecewiseLinearConstraint::nextFeasibleCase() const { - ASSERT( getPhaseStatus() == PHASE_NOT_FIXED ); - if ( !isFeasible() ) return CONSTRAINT_INFEASIBLE; + if ( phaseFixed() ) + return getPhaseStatus(); + List allCases = getAllCases(); for ( PhaseStatus thisCase : allCases ) { @@ -201,6 +203,35 @@ void PiecewiseLinearConstraint::setStatistics( Statistics *statistics ) _statistics = statistics; } +bool PiecewiseLinearConstraint::phaseFixed() const +{ + if ( _cdPhaseStatus != nullptr ) + return *_cdPhaseStatus != PHASE_NOT_FIXED; + else + return _phaseStatus != PHASE_NOT_FIXED; +}; + +PhaseStatus PiecewiseLinearConstraint::getImpliedCase() const +{ + ASSERT( isImplication() || phaseFixed() ); + PhaseStatus impliedCase = PHASE_NOT_FIXED; + if ( isImplication() ) + impliedCase = nextFeasibleCase(); + else + impliedCase = getPhaseStatus(); + + ASSERT( impliedCase != PHASE_NOT_FIXED ); + return impliedCase; +} +void PiecewiseLinearConstraint::serializeInfeasibleCases( String &output ) const +{ + if ( _cdInfeasibleCases ) + { + output += Stringf( "Infeasible cases ( %d/%d):", _cdInfeasibleCases->size(), _numCases ); + for ( auto infeasible : *_cdInfeasibleCases ) + output += Stringf( "%d", infeasible ); + } +} // // Local Variables: // compile-command: "make -C ../.. " diff --git a/src/engine/PiecewiseLinearConstraint.h b/src/engine/PiecewiseLinearConstraint.h index b7e68fc589..aa35be7330 100644 --- a/src/engine/PiecewiseLinearConstraint.h +++ b/src/engine/PiecewiseLinearConstraint.h @@ -197,7 +197,7 @@ class PiecewiseLinearConstraint : public ITableau::VariableWatcher /* Check if the constraint's phase has been fixed. */ - virtual bool phaseFixed() const = 0; + virtual bool phaseFixed() const; /* If the constraint's phase has been fixed, get the (valid) case split. @@ -207,6 +207,11 @@ class PiecewiseLinearConstraint : public ITableau::VariableWatcher virtual PiecewiseLinearCaseSplit getValidCaseSplit() const = 0; virtual PiecewiseLinearCaseSplit getImpliedCaseSplit() const = 0; + /* + Get implied case split - either based on search (_cdInfeasibleCases) or assignment (_cdPhaseFixed) + */ + PhaseStatus getImpliedCase() const; + /* Returns a list of all cases of this constraint. Used by the nextFeasibleCase to track the state during search. The order of returned @@ -244,7 +249,7 @@ class PiecewiseLinearConstraint : public ITableau::VariableWatcher Transform the piecewise linear constraint so that each disjunct contains only bound constraints. */ - virtual void transformToUseAuxVariables( InputQuery & ) {}; + virtual void transformToUseAuxVariables( InputQuery & ){}; void setStatistics( Statistics *statistics ); @@ -349,7 +354,7 @@ class PiecewiseLinearConstraint : public ITableau::VariableWatcher Method to get PhaseStatus of the constraint. Encapsulates both context dependent and context-less behavior. */ - PhaseStatus getPhaseStatus() const; + virtual PhaseStatus getPhaseStatus() const; /**********************************************************************/ /* Context-dependent Members Initialization and Cleanup */ @@ -390,13 +395,14 @@ class PiecewiseLinearConstraint : public ITableau::VariableWatcher Worst case complexity O(n^2) This method is overloaded in MAX and DISJUNCTION constraints. */ - virtual PhaseStatus nextFeasibleCase(); + virtual PhaseStatus nextFeasibleCase() const; /* Returns number of cases not yet marked as infeasible. */ unsigned numFeasibleCases() const { + ASSERT( _cdInfeasibleCases != nullptr ); return _numCases - _cdInfeasibleCases->size(); } @@ -405,6 +411,7 @@ class PiecewiseLinearConstraint : public ITableau::VariableWatcher */ bool isFeasible() const { + ASSERT( _cdInfeasibleCases != nullptr ); return numFeasibleCases() > 0u; } @@ -453,6 +460,8 @@ class PiecewiseLinearConstraint : public ITableau::VariableWatcher return _cdInfeasibleCases; } + void serializeInfeasibleCases( String &output ) const; + protected: unsigned _numCases; // Number of possible cases/phases for this constraint // (e.g. 2 for ReLU, ABS, SIGN; >=2 for Max and Disjunction ) @@ -514,6 +523,7 @@ class PiecewiseLinearConstraint : public ITableau::VariableWatcher */ bool isCaseInfeasible( PhaseStatus phase ) const; + /**********************************************************************/ /* BOUND WRAPPER METHODS */ /**********************************************************************/ diff --git a/src/engine/ReluConstraint.cpp b/src/engine/ReluConstraint.cpp index ccdd340177..d0fcadf4d3 100644 --- a/src/engine/ReluConstraint.cpp +++ b/src/engine/ReluConstraint.cpp @@ -14,7 +14,6 @@ #include "ReluConstraint.h" -#include "PiecewiseLinearConstraint.h" #include "Debug.h" #include "DivideStrategy.h" #include "FloatUtils.h" @@ -24,6 +23,7 @@ #include "MStringf.h" #include "MarabouError.h" #include "PiecewiseLinearCaseSplit.h" +#include "PiecewiseLinearConstraint.h" #include "Statistics.h" #include "TableauRow.h" @@ -42,7 +42,8 @@ ReluConstraint::ReluConstraint( unsigned b, unsigned f ) } ReluConstraint::ReluConstraint( const String &serializedRelu ) - : _haveEliminatedVariables( false ) + : PiecewiseLinearConstraint( TWO_PHASE_PIECEWISE_LINEAR_CONSTRAINT ) + , _haveEliminatedVariables( false ) { String constraintType = serializedRelu.substring( 0, 4 ); ASSERT( constraintType == String( "relu" ) ); @@ -121,12 +122,12 @@ void ReluConstraint::unregisterAsWatcher( ITableau *tableau ) void ReluConstraint::checkIfLowerBoundUpdateFixesPhase( unsigned variable, double bound ) { - if ( variable == _f && FloatUtils::isPositive( bound ) ) - setPhaseStatus( RELU_PHASE_ACTIVE ); - else if ( variable == _b && !FloatUtils::isNegative( bound ) ) - setPhaseStatus( RELU_PHASE_ACTIVE ); - else if ( _auxVarInUse && variable == _aux && FloatUtils::isPositive( bound ) ) - setPhaseStatus( RELU_PHASE_INACTIVE ); + if ( variable == _f && FloatUtils::isPositive( bound ) ) + setPhaseStatus( RELU_PHASE_ACTIVE ); + else if ( variable == _b && !FloatUtils::isNegative( bound ) ) + setPhaseStatus( RELU_PHASE_ACTIVE ); + else if ( _auxVarInUse && variable == _aux && FloatUtils::isPositive( bound ) ) + setPhaseStatus( RELU_PHASE_INACTIVE ); } void ReluConstraint::checkIfUpperBoundUpdateFixesPhase( unsigned variable, double bound ) @@ -574,11 +575,6 @@ PiecewiseLinearCaseSplit ReluConstraint::getActiveSplit() const return activePhase; } -bool ReluConstraint::phaseFixed() const -{ - return _phaseStatus != PHASE_NOT_FIXED; -} - PiecewiseLinearCaseSplit ReluConstraint::getImpliedCaseSplit() const { ASSERT( _phaseStatus != PHASE_NOT_FIXED ); @@ -617,6 +613,8 @@ void ReluConstraint::dump( String &output ) const existsLowerBound( _aux ) ? Stringf( "%lf", getLowerBound( _aux ) ).ascii() : "-inf", existsUpperBound( _aux ) ? Stringf( "%lf", getUpperBound( _aux ) ).ascii() : "inf" ); } + + serializeInfeasibleCases( output ); } void ReluConstraint::updateVariableIndex( unsigned oldIndex, unsigned newIndex ) @@ -851,7 +849,7 @@ void ReluConstraint::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; // This should not be called when the linear constraints have diff --git a/src/engine/ReluConstraint.h b/src/engine/ReluConstraint.h index f1dece1ada..3e4679c098 100644 --- a/src/engine/ReluConstraint.h +++ b/src/engine/ReluConstraint.h @@ -137,11 +137,6 @@ class ReluConstraint : public PiecewiseLinearConstraint */ PiecewiseLinearCaseSplit getImpliedCaseSplit() const override; - /* - Check if the constraint's phase has been fixed. - */ - bool phaseFixed() const override; - /* Preprocessing related functions, to inform that a variable has been eliminated completely because it was fixed to some value, diff --git a/src/engine/SignConstraint.cpp b/src/engine/SignConstraint.cpp index bf3d3492f1..f5ed9d1661 100644 --- a/src/engine/SignConstraint.cpp +++ b/src/engine/SignConstraint.cpp @@ -17,8 +17,8 @@ #include "Debug.h" #include "FloatUtils.h" #include "GlobalConfiguration.h" -#include "InputQuery.h" #include "ITableau.h" +#include "InputQuery.h" #include "MStringf.h" #include "MarabouError.h" #include "PiecewiseLinearCaseSplit.h" @@ -39,7 +39,8 @@ SignConstraint::SignConstraint( unsigned b, unsigned f ) } SignConstraint::SignConstraint( const String &serializedSign ) - : _haveEliminatedVariables( false ) + : PiecewiseLinearConstraint( TWO_PHASE_PIECEWISE_LINEAR_CONSTRAINT ) + , _haveEliminatedVariables( false ) { String constraintType = serializedSign.substring( 0, 4 ); ASSERT( constraintType == String( "sign" ) ); @@ -217,10 +218,6 @@ PiecewiseLinearCaseSplit SignConstraint::getPositiveSplit() const return positivePhase; } -bool SignConstraint::phaseFixed() const -{ - return _phaseStatus != PHASE_NOT_FIXED; -} void SignConstraint::addAuxiliaryEquationsAfterPreprocessing( InputQuery &inputQuery ) @@ -301,11 +298,10 @@ String SignConstraint::serializeToString() const return Stringf( "sign,%u,%u", _f, _b ); } -void SignConstraint::getCostFunctionComponent( LinearExpression &cost, - PhaseStatus phase ) const +void SignConstraint::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 == SIGN_PHASE_NEGATIVE || phase == SIGN_PHASE_POSITIVE ); @@ -585,6 +581,8 @@ void SignConstraint::dump( String &output ) const output += Stringf( "f in [%s, %s]\n", existsLowerBound( _f ) ? Stringf( "%lf", getLowerBound( _f ) ).ascii() : "-inf", existsUpperBound( _f ) ? Stringf( "%lf", getUpperBound( _f ) ).ascii() : "inf" ); + + serializeInfeasibleCases( output ); } double SignConstraint::computePolarity() const diff --git a/src/engine/SignConstraint.h b/src/engine/SignConstraint.h index d2d19121bb..4b655a5ad4 100644 --- a/src/engine/SignConstraint.h +++ b/src/engine/SignConstraint.h @@ -126,10 +126,6 @@ class SignConstraint : public PiecewiseLinearConstraint heuristics should be implemented. */ List getAllCases() const override; - /* - Check if the constraint's phase has been fixed. - */ - bool phaseFixed() const override; /* If the phase is not fixed, add _f <= -2/lb_b * _b + 1 diff --git a/src/engine/SmtCore.cpp b/src/engine/SmtCore.cpp index 0da2f5be06..9528c29638 100644 --- a/src/engine/SmtCore.cpp +++ b/src/engine/SmtCore.cpp @@ -2,17 +2,18 @@ /*! \file SmtCore.cpp ** \verbatim ** Top contributors (to current version): - ** Guy Katz, Parth Shah, Duligur Ibeling + ** Guy Katz, Aleksandar Zeljic, Haoze Wu, Parth Shah ** This file is part of the Marabou project. ** Copyright (c) 2017-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** [[ Add lengthier description here ]] - + ** See the description of the class in SmtCore.h. **/ +#include "SmtCore.h" + #include "Debug.h" #include "DivideStrategy.h" #include "EngineState.h" @@ -21,20 +22,23 @@ #include "IEngine.h" #include "MStringf.h" #include "MarabouError.h" -#include "Options.h" #include "PseudoImpactTracker.h" #include "ReluConstraint.h" -#include "SmtCore.h" -SmtCore::SmtCore( IEngine *engine ) +using namespace CVC4::context; + +SmtCore::SmtCore( IEngine *engine, Context &ctx ) : _statistics( NULL ) + , _context( ctx ) + , _trail( &_context ) + , _decisions( &_context ) , _engine( engine ) - , _context( _engine->getContext() ) , _needToSplit( false ) , _constraintForSplitting( NULL ) - , _stateId( 0 ) - , _constraintViolationThreshold( Options::get()->getInt( Options::CONSTRAINT_VIOLATION_THRESHOLD ) ) - , _deepSoIRejectionThreshold( Options::get()->getInt( Options::DEEP_SOI_REJECTION_THRESHOLD ) ) + , _constraintViolationThreshold + ( (unsigned)Options::get()->getInt( Options::CONSTRAINT_VIOLATION_THRESHOLD ) ) + , _deepSoIRejectionThreshold( Options::get()->getInt + ( Options::DEEP_SOI_REJECTION_THRESHOLD ) ) , _branchingHeuristic( Options::get()->getDivideStrategy() ) , _scoreTracker( nullptr ) , _numRejectedPhasePatternProposal( 0 ) @@ -43,33 +47,25 @@ SmtCore::SmtCore( IEngine *engine ) SmtCore::~SmtCore() { - freeMemory(); } -void SmtCore::freeMemory() +void SmtCore::reset() { - for ( const auto &stackEntry : _stack ) + if ( _context.getLevel() > 0 ) { - delete stackEntry->_engineState; - delete stackEntry; + _context.popto( 0 ); + _engine->postContextPopHook(); } - - _stack.clear(); -} - -void SmtCore::reset() -{ - freeMemory(); - _impliedValidSplitsAtRoot.clear(); _needToSplit = false; _constraintForSplitting = NULL; - _stateId = 0; _constraintToViolationCount.clear(); _numRejectedPhasePatternProposal = 0; } void SmtCore::reportViolatedConstraint( PiecewiseLinearConstraint *constraint ) { + ASSERT( !constraint->phaseFixed() ); + if ( !_constraintToViolationCount.exists( constraint ) ) _constraintToViolationCount[constraint] = 0; @@ -79,10 +75,12 @@ void SmtCore::reportViolatedConstraint( PiecewiseLinearConstraint *constraint ) _constraintViolationThreshold ) { _needToSplit = true; - if ( !pickSplitPLConstraint() ) + if ( GlobalConfiguration::SPLITTING_HEURISTICS == + DivideStrategy::ReLUViolation || !pickSplitPLConstraint() ) // If pickSplitConstraint failed to pick one, use the native // relu-violation based splitting heuristic. _constraintForSplitting = constraint; + ASSERT( !_constraintForSplitting->phaseFixed() ); } } @@ -95,17 +93,17 @@ unsigned SmtCore::getViolationCounts( PiecewiseLinearConstraint *constraint ) co } void SmtCore::initializeScoreTrackerIfNeeded( const - List - &plConstraints ) + List + &plConstraints ) { if ( GlobalConfiguration::USE_DEEPSOI_LOCAL_SEARCH ) - { - _scoreTracker = std::unique_ptr - ( new PseudoImpactTracker() ); - _scoreTracker->initialize( plConstraints ); + { + _scoreTracker = std::unique_ptr + ( new PseudoImpactTracker() ); + _scoreTracker->initialize( plConstraints ); - SMT_LOG( "\tTracking Pseudo Impact..." ); - } + SMT_LOG( "\tTracking Pseudo Impact..." ); + } } void SmtCore::reportRejectedPhasePatternProposal() @@ -114,15 +112,13 @@ void SmtCore::reportRejectedPhasePatternProposal() if ( _numRejectedPhasePatternProposal >= _deepSoIRejectionThreshold ) - { - _needToSplit = true; - _engine->applyAllBoundTightenings(); - _engine->applyAllValidConstraintCaseSplits(); - if ( !pickSplitPLConstraint() ) - // If pickSplitConstraint failed to pick one, use the native - // relu-violation based splitting heuristic. - _constraintForSplitting = _scoreTracker->topUnfixed(); - } + { + _needToSplit = true; + if ( !pickSplitPLConstraint() ) + // If pickSplitConstraint failed to pick one, use the native + // relu-violation based splitting heuristic. + _constraintForSplitting = _scoreTracker->topUnfixed(); + } } bool SmtCore::needToSplit() const @@ -130,24 +126,63 @@ bool SmtCore::needToSplit() const return _needToSplit; } -void SmtCore::performSplit() +void SmtCore::pushDecision( PiecewiseLinearConstraint *constraint, PhaseStatus decision ) +{ + SMT_LOG( Stringf( "Decision @ %d )", _context.getLevel() + 1 ).ascii() ); + TrailEntry te( constraint, decision ); + applyTrailEntry( te, true ); + SMT_LOG( Stringf( "Decision push @ %d DONE", _context.getLevel() ).ascii() ); +} + +void SmtCore::pushImplication( PiecewiseLinearConstraint *constraint ) +{ + ASSERT( constraint->isImplication() || constraint->phaseFixed() ); + SMT_LOG( Stringf( "Implication @ %d ... ", _context.getLevel() ).ascii() ); + TrailEntry te( constraint, constraint->getImpliedCase() ); + applyTrailEntry( te, false ); + SMT_LOG( Stringf( "Implication @ %d DONE", _context.getLevel() ).ascii() ); +} + +void SmtCore::applyTrailEntry( TrailEntry &te, bool isDecision ) +{ + if ( isDecision ) + { + _engine->preContextPushHook(); + pushContext(); + _decisions.push_back( te ); + } + + _trail.push_back( te ); + _engine->applySplit( te.getPiecewiseLinearCaseSplit() ); +} + +void SmtCore::decide() { ASSERT( _needToSplit ); + SMT_LOG( "Performing a ReLU split" ); _numRejectedPhasePatternProposal = 0; // Maybe the constraint has already become inactive - if so, ignore - if ( !_constraintForSplitting->isActive() ) + if ( !_constraintForSplitting->isActive() ) { _needToSplit = false; _constraintToViolationCount[_constraintForSplitting] = 0; - _constraintForSplitting = NULL; + _constraintForSplitting = nullptr; return; } - struct timespec start = TimeUtils::sampleMicro(); - ASSERT( _constraintForSplitting->isActive() ); _needToSplit = false; + _constraintForSplitting->setActiveConstraint( false ); + + decideSplit( _constraintForSplitting ); + _constraintForSplitting = nullptr; +} + +void SmtCore::decideSplit( PiecewiseLinearConstraint *constraint ) +{ + ASSERT( constraint != nullptr ); + struct timespec start = TimeUtils::sampleMicro(); if ( _statistics ) { @@ -155,60 +190,34 @@ void SmtCore::performSplit() _statistics->incUnsignedAttribute( Statistics::NUM_VISITED_TREE_STATES ); } - // Before storing the state of the engine, we: - // 1. Obtain the splits. - // 2. Disable the constraint, so that it is marked as disbaled in the EngineState. - List splits = _constraintForSplitting->getCaseSplits(); - ASSERT( !splits.empty() ); - ASSERT( splits.size() >= 2 ); // Not really necessary, can add code to handle this case. - _constraintForSplitting->setActiveConstraint( false ); + if ( !constraint->isFeasible() ) + throw MarabouError( MarabouError::DEBUGGING_ERROR ); + ASSERT( constraint->isFeasible() ); + ASSERT( !constraint->isImplication() ); - // Obtain the current state of the engine - EngineState *stateBeforeSplits = new EngineState; - stateBeforeSplits->_stateId = _stateId; - ++_stateId; - _engine->storeState( *stateBeforeSplits, - TableauStateStorageLevel::STORE_BOUNDS_ONLY ); - _engine->preContextPushHook(); - pushContext(); - SmtStackEntry *stackEntry = new SmtStackEntry; - // Perform the first split: add bounds and equations - List::iterator split = splits.begin(); - ASSERT( split->getEquations().size() == 0 ); - _engine->applySplit( *split ); - stackEntry->_activeSplit = *split; - - // Store the remaining splits on the stack, for later - stackEntry->_engineState = stateBeforeSplits; - ++split; - while ( split != splits.end() ) - { - stackEntry->_alternativeSplits.append( *split ); - ++split; - } - - _stack.append( stackEntry ); + PhaseStatus decision = constraint->nextFeasibleCase(); + pushDecision( constraint, decision ); if ( _statistics ) { - unsigned level = getStackDepth(); + unsigned level = _context.getLevel(); _statistics->setUnsignedAttribute( Statistics::CURRENT_DECISION_LEVEL, level ); if ( level > _statistics->getUnsignedAttribute ( Statistics::MAX_DECISION_LEVEL ) ) _statistics->setUnsignedAttribute( Statistics::MAX_DECISION_LEVEL, level ); + struct timespec end = TimeUtils::sampleMicro(); _statistics->incLongAttribute( Statistics::TOTAL_TIME_SMT_CORE_MICRO, TimeUtils::timePassed( start, end ) ); } - - _constraintForSplitting = NULL; + SMT_LOG( "Performing a ReLU split - DONE" ); } -unsigned SmtCore::getStackDepth() const + +unsigned SmtCore::getDecisionLevel() const { - ASSERT( _stack.size() == static_cast( _context.getLevel() ) ); - return _stack.size(); + return _decisions.size(); } void SmtCore::popContext() @@ -237,86 +246,75 @@ void SmtCore::pushContext() } } -bool SmtCore::popSplit() +bool SmtCore::popDecisionLevel( TrailEntry &lastDecision ) { - SMT_LOG( "Performing a pop" ); - - if ( _stack.empty() ) + ASSERT( static_cast( _context.getLevel() ) == _decisions.size() ); + if ( _decisions.empty() ) return false; - struct timespec start = TimeUtils::sampleMicro(); + SMT_LOG( "Popping trail ..." ); + lastDecision = _decisions.back(); + popContext(); + _engine->postContextPopHook(); + SMT_LOG( Stringf( "to %d DONE", _context.getLevel() ).ascii() ); + return true; +} - if ( _statistics ) +void SmtCore::interruptIfCompliantWithDebugSolution() +{ + if ( checkSkewFromDebuggingSolution() ) { - _statistics->incUnsignedAttribute( Statistics::NUM_POPS ); - // A pop always sends us to a state that we haven't seen before - whether - // from a sibling split, or from a lower level of the tree. - _statistics->incUnsignedAttribute( Statistics::NUM_VISITED_TREE_STATES ); + SMT_LOG( "Error! Popping from a compliant stack\n" ); + throw MarabouError( MarabouError::DEBUGGING_ERROR ); } +} - bool inconsistent = true; - while ( inconsistent ) - { - // Remove any entries that have no alternatives - String error; - while ( _stack.back()->_alternativeSplits.empty() ) - { - if ( checkSkewFromDebuggingSolution() ) - { - // Pops should not occur from a compliant stack! - printf( "Error! Popping from a compliant stack\n" ); - throw MarabouError( MarabouError::DEBUGGING_ERROR ); - } - - delete _stack.back()->_engineState; - delete _stack.back(); - _stack.popBack(); - popContext(); - +PiecewiseLinearCaseSplit SmtCore::getDecision( unsigned decisionLevel ) const +{ + ASSERT( decisionLevel <= getDecisionLevel() ); + ASSERT( decisionLevel > 0 ); + return _decisions[decisionLevel - 1].getPiecewiseLinearCaseSplit(); +} - if ( _stack.empty() ) - return false; - } +bool SmtCore::backtrackToFeasibleDecision( TrailEntry &lastDecision ) +{ + SMT_LOG( "Backtracking to a feasible decision..." ); - if ( checkSkewFromDebuggingSolution() ) - { - // Pops should not occur from a compliant stack! - printf( "Error! Popping from a compliant stack\n" ); - throw MarabouError( MarabouError::DEBUGGING_ERROR ); - } + do + { + if ( !popDecisionLevel( lastDecision ) ) + return false; - SmtStackEntry *stackEntry = _stack.back(); + lastDecision.markInfeasible(); + interruptIfCompliantWithDebugSolution(); + } + while ( !lastDecision.isFeasible() ); - popContext(); - _engine->postContextPopHook(); - // Restore the state of the engine - SMT_LOG( "\tRestoring engine state..." ); - _engine->restoreState( *( stackEntry->_engineState ) ); - SMT_LOG( "\tRestoring engine state - DONE" ); + return true; +} - // Apply the new split and erase it from the list - auto split = stackEntry->_alternativeSplits.begin(); +bool SmtCore::backtrackAndContinueSearch() +{ + TrailEntry feasibleDecision( nullptr, CONSTRAINT_INFEASIBLE ); + struct timespec start = TimeUtils::sampleMicro(); - // Erase any valid splits that were learned using the split we just - // popped - stackEntry->_impliedValidSplits.clear(); + if ( !backtrackToFeasibleDecision( feasibleDecision ) ) + return false; - SMT_LOG( "\tApplying new split..." ); - ASSERT( split->getEquations().size() == 0 ); - _engine->preContextPushHook(); - pushContext(); - _engine->applySplit( *split ); - SMT_LOG( "\tApplying new split - DONE" ); + ASSERT( feasibleDecision.isFeasible() ); - stackEntry->_activeSplit = *split; - stackEntry->_alternativeSplits.erase( split ); + if ( _statistics ) + _statistics->incUnsignedAttribute( Statistics::NUM_VISITED_TREE_STATES ); - inconsistent = !_engine->consistentBounds(); - } + PiecewiseLinearConstraint *pwlc = feasibleDecision._pwlConstraint; + if ( pwlc->isImplication() ) + pushImplication( pwlc ); + else + decideSplit( pwlc ); if ( _statistics ) { - unsigned level = getStackDepth(); + unsigned level = _context.getLevel(); _statistics->setUnsignedAttribute( Statistics::CURRENT_DECISION_LEVEL, level ); if ( level > _statistics->getUnsignedAttribute @@ -328,40 +326,22 @@ bool SmtCore::popSplit() } checkSkewFromDebuggingSolution(); - return true; } -void SmtCore::resetSplitConditions() +void SmtCore::resetReportedViolations() { _constraintToViolationCount.clear(); _numRejectedPhasePatternProposal = 0; _needToSplit = false; } -void SmtCore::recordImpliedValidSplit( PiecewiseLinearCaseSplit &validSplit ) -{ - if ( _stack.empty() ) - _impliedValidSplitsAtRoot.append( validSplit ); - else - _stack.back()->_impliedValidSplits.append( validSplit ); - - checkSkewFromDebuggingSolution(); -} - void SmtCore::allSplitsSoFar( List &result ) const { result.clear(); - for ( const auto &it : _impliedValidSplitsAtRoot ) - result.append( it ); - - for ( const auto &it : _stack ) - { - result.append( it->_activeSplit ); - for ( const auto &impliedSplit : it->_impliedValidSplits ) - result.append( impliedSplit ); - } + for ( auto trailEntry : _trail ) + result.append( trailEntry.getPiecewiseLinearCaseSplit() ); } void SmtCore::setStatistics( Statistics *statistics ) @@ -383,41 +363,47 @@ bool SmtCore::checkSkewFromDebuggingSolution() String error; + int decisionLevel = 0; + bool isDecision = false; // First check that the valid splits implied at the root level are okay - for ( const auto &split : _impliedValidSplitsAtRoot ) + for ( const auto &trailEntry : _trail ) { - if ( !splitAllowsStoredSolution( split, error ) ) + if ( trailEntry._pwlConstraint != _decisions[decisionLevel]._pwlConstraint ) + isDecision = false; + else { - printf( "Error with one of the splits implied at root level:\n\t%s\n", error.ascii() ); - throw MarabouError( MarabouError::DEBUGGING_ERROR ); + ASSERT( trailEntry._phase == _decisions[decisionLevel]._phase ); + isDecision = true; + ++decisionLevel; } - } - // Now go over the stack from oldest to newest and check that each level is compliant - for ( const auto &stackEntry : _stack ) - { - // If the active split is non-compliant but there are alternatives, that's fine - if ( !splitAllowsStoredSolution( stackEntry->_activeSplit, error ) ) + PiecewiseLinearCaseSplit caseSplit = trailEntry.getPiecewiseLinearCaseSplit(); + if ( decisionLevel == 0 ) { - if ( stackEntry->_alternativeSplits.empty() ) + if ( !splitAllowsStoredSolution( caseSplit, error ) ) { - printf( "Error! Have a split that is non-compliant with the stored solution, " - "without alternatives:\n\t%s\n", error.ascii() ); + printf( "Error with one of the splits implied at root level:\n\t%s\n", error.ascii() ); throw MarabouError( MarabouError::DEBUGGING_ERROR ); } - - // Active split is non-compliant but this is fine, because there are alternatives. We're done. - return false; } - - // Did we learn any valid splits that are non-compliant? - for ( auto const &split : stackEntry->_impliedValidSplits ) + else { - if ( !splitAllowsStoredSolution( split, error ) ) + // If the active split is non-compliant but there are alternatives, + // i.e. it was a decision, that's fine + if ( isDecision && !splitAllowsStoredSolution( caseSplit, error ) ) { - printf( "Error with one of the splits implied at this stack level:\n\t%s\n", - error.ascii() ); - throw MarabouError( MarabouError::DEBUGGING_ERROR ); + // Active split is non-compliant but this is fine, because there + // are alternatives. We're done. + return false; + } + else // Implied split + { + if ( !splitAllowsStoredSolution( caseSplit, error ) ) + { + printf( "Error with one of the splits implied at this stack level:\n\t%s\n", + error.ascii() ); + throw MarabouError( MarabouError::DEBUGGING_ERROR ); + } } } } @@ -433,7 +419,7 @@ bool SmtCore::splitAllowsStoredSolution( const PiecewiseLinearCaseSplit &split, if ( _debuggingSolution.empty() ) return true; - for ( const auto &bound : split.getBoundTightenings() ) + for ( const auto bound : split.getBoundTightenings() ) { unsigned variable = bound._variable; @@ -467,6 +453,11 @@ bool SmtCore::splitAllowsStoredSolution( const PiecewiseLinearCaseSplit &split, return true; } +void SmtCore::setConstraintViolationThreshold( unsigned threshold ) +{ + _constraintViolationThreshold = threshold; +} + PiecewiseLinearConstraint *SmtCore::chooseViolatedConstraintForFixing( List &_violatedPlConstraints ) const { ASSERT( !_violatedPlConstraints.empty() ); @@ -500,61 +491,17 @@ PiecewiseLinearConstraint *SmtCore::chooseViolatedConstraintForFixing( ListincUnsignedAttribute( Statistics::NUM_SPLITS ); - _statistics->incUnsignedAttribute( Statistics::NUM_VISITED_TREE_STATES ); - } - - // Obtain the current state of the engine - EngineState *stateBeforeSplits = new EngineState; - stateBeforeSplits->_stateId = _stateId; - ++_stateId; - _engine->storeState( *stateBeforeSplits, - TableauStateStorageLevel::STORE_ENTIRE_TABLEAU_STATE ); - stackEntry->_engineState = stateBeforeSplits; - - // Apply all the splits - _engine->applySplit( stackEntry->_activeSplit ); - for ( const auto &impliedSplit : stackEntry->_impliedValidSplits ) - _engine->applySplit( impliedSplit ); - - _stack.append( stackEntry ); - - if ( _statistics ) - { - unsigned level = getStackDepth(); - _statistics->setUnsignedAttribute( Statistics::CURRENT_DECISION_LEVEL, - level ); - if ( level > _statistics->getUnsignedAttribute - ( Statistics::MAX_DECISION_LEVEL ) ) - _statistics->setUnsignedAttribute( Statistics::MAX_DECISION_LEVEL, - level ); - struct timespec end = TimeUtils::sampleMicro(); - _statistics->incLongAttribute( Statistics::TOTAL_TIME_SMT_CORE_MICRO, TimeUtils::timePassed( start, end ) ); - } -} - -void SmtCore::storeSmtState( SmtState &smtState ) -{ - smtState._impliedValidSplitsAtRoot = _impliedValidSplitsAtRoot; - - for ( auto &stackEntry : _stack ) - smtState._stack.append( stackEntry->duplicateSmtStackEntry() ); - - smtState._stateId = _stateId; -} - bool SmtCore::pickSplitPLConstraint() { if ( _needToSplit ) - { _constraintForSplitting = _engine->pickSplitPLConstraint ( _branchingHeuristic ); - } return _constraintForSplitting != NULL; } + +void SmtCore::resetSplitConditions() +{ + _constraintToViolationCount.clear(); + _numRejectedPhasePatternProposal = 0; + _needToSplit = false; +} diff --git a/src/engine/SmtCore.h b/src/engine/SmtCore.h index db39ffa498..ffbb3c364e 100644 --- a/src/engine/SmtCore.h +++ b/src/engine/SmtCore.h @@ -2,44 +2,90 @@ /*! \file SmtCore.h ** \verbatim ** Top contributors (to current version): - ** Guy Katz, Parth Shah + ** Guy Katz, AleksandarZeljic, Haoze Wu, Parth Shah ** This file is part of the Marabou project. ** Copyright (c) 2017-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** [[ Add lengthier description here ]] - -**/ + ** The SmtCore class implements a context-dependent SmtCore class. + ** The SmtCore distinguishes between: **decisions** and **implications**. + ** + ** Decision is a case of PiecewiseLinearConstraint asserted on the trail. + ** A decision is a choice between multiple feasible cases of a + ** PiecewiseLinearConstraint and represents nodes in the search tree. + ** + ** Implication is the last feasible case of a PiecewiseLinearConstraint and as + ** soon as it is detected it is asserted on the trail. + ** + ** Case splitting on a PiecewiseLinearConstraint performs a decision. + ** Fixing a case of a PiecewiseLinearConstraint (e.g., via bound propagation or + ** by exhausting all other cases) performs an implication. + ** + ** The overall search state is stored in a distributed way: + ** - SmtCore::_trail is the current search state in a chronological order + ** - PiecewiseLinearConstraints' infeasible cases enumerate all the explored + ** states w.r.t to the chronological order on the _trail. + ** + ** _trail is a chronological list of cases of PiecewiseLinearConstraints + ** asserted to hold (as TrailEntries) - both decisions and implications. + ** _decisions is a chronological list of decisions stored on the trail. + ** _trail and _decisions are both context dependent and will synchronize in + ** unison with the _context object. + ** + ** When a search state is found to be infeasible, SmtCore backtracks to the + ** last decision and continues the search. + ** + ** PushDecision advances the decision level and context level. + ** popDecisionLevel backtracks the last decision and context level. + ** + ** Advancing a context level creates a synchronization point to which all + ** context dependent members can backtrack in unison. + ** Backtracking a context level restores all context dependent members to the + ** state of the last synchronization point. This operation is O(1) complexity. + ** + ** Since the entire search state is context dependent, backtracking the context + ** (via popDecisionLevel) backtracks the entire Marabou search state. + ** The only exception is the labeling of basic/non-basic variables in the + ** tableau, which may need to be recalculated using Tableau's + ** postContextPopHook exposed via Engine. + ** + ** Implementation relies on: + ** + ** - _context is a unique Context object from which all the context-dependent + ** structures are obtained. + ** + ** - PiecewiseLinearConstraint class stores its search state in a + ** context-dependent manner and exposes it using nextFeasibleCase() and + ** markInfeasible() methods. + ** + ** - Using BoundManager class to store bounds in a context-dependent manner + **/ #ifndef __SmtCore_h__ #define __SmtCore_h__ -#include "DivideStrategy.h" +#include "Options.h" #include "PiecewiseLinearCaseSplit.h" #include "PiecewiseLinearConstraint.h" #include "PLConstraintScoreTracker.h" -#include "SmtState.h" #include "Stack.h" -#include "SmtStackEntry.h" #include "Statistics.h" +#include "TrailEntry.h" +#include "context/cdlist.h" #include "context/context.h" -#include - #define SMT_LOG( x, ... ) LOG( GlobalConfiguration::SMT_CORE_LOGGING, "SmtCore: %s\n", x ) class EngineState; -class IEngine; +class Engine; class String; -using CVC4::context::Context; - class SmtCore { public: - SmtCore( IEngine *engine ); + SmtCore( IEngine *engine, CVC4::context::Context &context ); ~SmtCore(); /* @@ -47,11 +93,6 @@ class SmtCore */ void freeMemory(); - /* - Reset the SmtCore - */ - void reset(); - /* Initialize the score tracker with the given list of pl constraints. */ @@ -90,13 +131,12 @@ class SmtCore Get the number of times a specific PL constraint has been reported as violated. */ - unsigned getViolationCounts( PiecewiseLinearConstraint* constraint ) const; + unsigned getViolationCounts( PiecewiseLinearConstraint *constraint ) const; /* - Reset all reported violation counts and the number of rejected SoI - phase pattern proposal. + Reset all reported violation counts. */ - void resetSplitConditions(); + void resetReportedViolations(); /* Returns true iff the SMT core wants to perform a case split. @@ -104,43 +144,86 @@ class SmtCore bool needToSplit() const; /* - Perform the split according to the constraint marked for - splitting. Update bounds, add equations and update the stack. + Push TrailEntry representing the decision onto the trail. + */ + void pushDecision( PiecewiseLinearConstraint *constraint, PhaseStatus decision ); + + /* + Inform SmtCore of an implied (formerly valid) case split that was discovered. */ - void performSplit(); + void pushImplication( PiecewiseLinearConstraint *constraint ); + + /* + Pushes trail entry onto trail, handles decision book-keeping and + update bounds and add equations to the engine. + */ + void applyTrailEntry( TrailEntry &te, bool isDecision = false ); /* - Pop an old split from the stack, and perform a new split as - needed. Return true if successful, false if the stack is empty. + Decide and apply a case split using the constraint marked for splitting. */ - bool popSplit(); + void decide(); /* - Pop _context, record statistics + Decide a constraint's feasible case. Update bounds, add equations + and trail. */ - void popContext(); + void decideSplit( PiecewiseLinearConstraint *constraint ); + + /* + Backtracks fully explored decisions and stores the last feasible decision + */ + bool backtrackToFeasibleDecision( TrailEntry &feasibleDecision ); + + /* + Return to a feasible state and resume search by asserting the next case + (as either a decision or implication) + */ + bool backtrackAndContinueSearch(); + + /* + Pop a stack frame. Return true if successful, false if the stack is empty. + */ + bool popSplit(); /* - Push _context, record statistics + Encapsulations of _context.push/pop calls for statistics purposes. */ void pushContext(); + void popContext(); + /* + Pop a context level - lazily backtracking trail, bounds, etc. + Return true if successful, false if the stack is empty. + */ + bool popDecisionLevel( TrailEntry &lastDecision ); /* The current stack depth. */ - unsigned getStackDepth() const; + unsigned getDecisionLevel() const; /* - Let the smt core know of an implied valid case split that was discovered. + Return a list of all splits performed so far, both SMT-originating and + valid ones, in the correct order. */ - void recordImpliedValidSplit( PiecewiseLinearCaseSplit &validSplit ); + void allSplitsSoFar( List &result ) const; /* - Return a list of all splits performed so far, both SMT-originating and valid ones, - in the correct order. + Get trail begin iterator. */ - void allSplitsSoFar( List &result ) const; + CVC4::context::CDList::const_iterator trailBegin() const + { + return _trail.begin(); + }; + + /* + Get trail end iterator. + */ + CVC4::context::CDList::const_iterator trailEnd() const + { + return _trail.end(); + }; /* Have the SMT core start reporting statistics. @@ -153,59 +236,65 @@ class SmtCore */ PiecewiseLinearConstraint *chooseViolatedConstraintForFixing( List &_violatedPlConstraints ) const; + void setConstraintViolationThreshold( unsigned threshold ); + inline void setBranchingHeuristics( DivideStrategy strategy ) { _branchingHeuristic = strategy; } /* - Replay a stackEntry + Pick the piecewise linear constraint for splitting, returns true + if a constraint for splitting is successfully picked */ - void replaySmtStackEntry( SmtStackEntry *stackEntry ); + bool pickSplitPLConstraint(); /* - Store the current state of the SmtCore into smtState - */ - void storeSmtState( SmtState &smtState ); + Reset violation counts and number of rejected proposal patterns. + */ + void resetSplitConditions(); /* - Pick the piecewise linear constraint for splitting, returns true - if a constraint for splitting is successfully picked - */ - bool pickSplitPLConstraint(); + * For testing purposes + */ + PiecewiseLinearCaseSplit getDecision( unsigned decisionLevel ) const; + + void reset(); /* For debugging purposes only - store a correct possible solution + TODO: Create a user interface for this */ void storeDebuggingSolution( const Map &debuggingSolution ); bool checkSkewFromDebuggingSolution(); bool splitAllowsStoredSolution( const PiecewiseLinearCaseSplit &split, String &error ) const; - + void interruptIfCompliantWithDebugSolution(); private: /* - Valid splits that were implied by level 0 of the stack. + Collect and print various statistics. */ - List _impliedValidSplitsAtRoot; + Statistics *_statistics; /* - Collect and print various statistics. + CVC4 Context, constructed in Engine */ - Statistics *_statistics; + CVC4::context::Context &_context; /* - The case-split stack. + Trail is context dependent and contains all the asserted PWLCaseSplits */ - List _stack; + CVC4::context::CDList _trail; + + /* + * _decisions stores the decision TrailEntries + */ + CVC4::context::CDList _decisions; /* The engine. */ IEngine *_engine; - /* - Context for synchronizing the search. - */ - Context &_context; /* Do we need to perform a split and on which constraint. */ @@ -222,12 +311,6 @@ class SmtCore */ Map _debuggingSolution; - /* - A unique ID allocated to every state that is stored, for - debugging purposes. - */ - unsigned _stateId; - /* Split when some relu has been violated for this many times during the Reluplex procedure @@ -255,14 +338,7 @@ class SmtCore current search state. */ unsigned _numRejectedPhasePatternProposal; + }; #endif // __SmtCore_h__ - -// -// Local Variables: -// compile-command: "make -C ../.. " -// tags-file-name: "../../TAGS" -// c-basic-offset: 4 -// End: -// diff --git a/src/engine/tests/Test_DisjunctionConstraint.h b/src/engine/tests/Test_DisjunctionConstraint.h index 6164a0b91e..1ca8ff8bb6 100644 --- a/src/engine/tests/Test_DisjunctionConstraint.h +++ b/src/engine/tests/Test_DisjunctionConstraint.h @@ -13,16 +13,15 @@ **/ -#include - #include "DisjunctionConstraint.h" +#include "InputQuery.h" #include "MarabouError.h" #include "MockErrno.h" #include "MockTableau.h" -#include "InputQuery.h" -class MockForDisjunctionConstraint - : public MockErrno +#include + +class MockForDisjunctionConstraint : public MockErrno { public: }; @@ -49,6 +48,7 @@ class DisjunctionConstraintTestSuite : public CxxTest::TestSuite PiecewiseLinearCaseSplit *cs1; PiecewiseLinearCaseSplit *cs2; PiecewiseLinearCaseSplit *cs3; + Context ctx; void setUp() { @@ -195,8 +195,10 @@ class DisjunctionConstraintTestSuite : public CxxTest::TestSuite 5 <= x0 --> x1 = 2x2 + 5 */ + { DisjunctionConstraint dc( caseSplits ); + dc.initializeCDOs( &ctx ); dc.notifyLowerBound( 0, -10 ); dc.notifyUpperBound( 0, 10 ); @@ -205,16 +207,16 @@ class DisjunctionConstraintTestSuite : public CxxTest::TestSuite dc.notifyLowerBound( 2, -10 ); dc.notifyUpperBound( 2, 10 ); - TS_ASSERT( !dc.phaseFixed() ); + TS_ASSERT( !dc.isImplication() ); dc.notifyLowerBound( 0, -1 ); - TS_ASSERT( !dc.phaseFixed() ); + TS_ASSERT( !dc.isImplication() ); dc.notifyLowerBound( 0, 2 ); - TS_ASSERT( !dc.phaseFixed() ); + TS_ASSERT( !dc.isImplication() ); dc.notifyLowerBound( 0, 6 ); - TS_ASSERT( dc.phaseFixed() ); + TS_ASSERT( dc.isImplication() ); PiecewiseLinearCaseSplit validSplit = dc.getValidCaseSplit(); TS_ASSERT_EQUALS( validSplit, *cs3 ); @@ -222,6 +224,7 @@ class DisjunctionConstraintTestSuite : public CxxTest::TestSuite { DisjunctionConstraint dc( caseSplits ); + dc.initializeCDOs( &ctx ); dc.notifyLowerBound( 0, -10 ); dc.notifyUpperBound( 0, 10 ); @@ -230,16 +233,16 @@ class DisjunctionConstraintTestSuite : public CxxTest::TestSuite dc.notifyLowerBound( 2, -10 ); dc.notifyUpperBound( 2, 10 ); - TS_ASSERT( !dc.phaseFixed() ); + TS_ASSERT( !dc.isImplication() ); dc.notifyUpperBound( 0, 7 ); - TS_ASSERT( !dc.phaseFixed() ); + TS_ASSERT( !dc.isImplication() ); dc.notifyUpperBound( 0, 2 ); - TS_ASSERT( !dc.phaseFixed() ); + TS_ASSERT( !dc.isImplication() ); dc.notifyUpperBound( 0, -2 ); - TS_ASSERT( dc.phaseFixed() ); + TS_ASSERT( dc.isImplication() ); PiecewiseLinearCaseSplit validSplit = dc.getValidCaseSplit(); TS_ASSERT_EQUALS( validSplit, *cs1 ); @@ -261,6 +264,7 @@ class DisjunctionConstraintTestSuite : public CxxTest::TestSuite BoundManager boundManager( context ); boundManager.initialize( 11 ); dc.registerBoundManager( &boundManager ); + dc.initializeCDOs( &context ); dc.notifyLowerBound( 0, -10 ); dc.notifyUpperBound( 0, 10 ); @@ -269,16 +273,16 @@ class DisjunctionConstraintTestSuite : public CxxTest::TestSuite dc.notifyLowerBound( 2, -10 ); dc.notifyUpperBound( 2, 10 ); - TS_ASSERT( !dc.phaseFixed() ); + TS_ASSERT( !dc.isImplication() ); dc.notifyLowerBound( 0, -1 ); - TS_ASSERT( !dc.phaseFixed() ); + TS_ASSERT( !dc.isImplication() ); dc.notifyLowerBound( 0, 2 ); - TS_ASSERT( !dc.phaseFixed() ); + TS_ASSERT( !dc.isImplication() ); dc.notifyLowerBound( 0, 6 ); - TS_ASSERT( dc.phaseFixed() ); + TS_ASSERT( dc.isImplication() ); PiecewiseLinearCaseSplit validSplit = dc.getValidCaseSplit(); TS_ASSERT_EQUALS( validSplit, *cs3 ); @@ -290,6 +294,7 @@ class DisjunctionConstraintTestSuite : public CxxTest::TestSuite BoundManager boundManager( context ); boundManager.initialize( 11 ); dc.registerBoundManager( &boundManager ); + dc.initializeCDOs( &context ); dc.notifyLowerBound( 0, -10 ); dc.notifyUpperBound( 0, 10 ); @@ -298,16 +303,16 @@ class DisjunctionConstraintTestSuite : public CxxTest::TestSuite dc.notifyLowerBound( 2, -10 ); dc.notifyUpperBound( 2, 10 ); - TS_ASSERT( !dc.phaseFixed() ); + TS_ASSERT( !dc.isImplication() ); dc.notifyUpperBound( 0, 7 ); - TS_ASSERT( !dc.phaseFixed() ); + TS_ASSERT( !dc.isImplication() ); dc.notifyUpperBound( 0, 2 ); - TS_ASSERT( !dc.phaseFixed() ); + TS_ASSERT( !dc.isImplication() ); dc.notifyUpperBound( 0, -2 ); - TS_ASSERT( dc.phaseFixed() ); + TS_ASSERT( dc.isImplication() ); PiecewiseLinearCaseSplit validSplit = dc.getValidCaseSplit(); TS_ASSERT_EQUALS( validSplit, *cs1 ); @@ -322,15 +327,15 @@ class DisjunctionConstraintTestSuite : public CxxTest::TestSuite DisjunctionConstraint disjunction( caseSplits ); - TS_ASSERT_EQUALS( disjunction.getContext(), static_cast( nullptr ) ); - TS_ASSERT_EQUALS( disjunction.getActiveStatusCDO(), static_cast*>( nullptr ) ); - TS_ASSERT_EQUALS( disjunction.getPhaseStatusCDO(), static_cast*>( nullptr ) ); - TS_ASSERT_EQUALS( disjunction.getInfeasibleCasesCDList(), static_cast*>( nullptr ) ); + TS_ASSERT_EQUALS( disjunction.getContext(), static_cast( nullptr ) ); + TS_ASSERT_EQUALS( disjunction.getActiveStatusCDO(), static_cast *>( nullptr ) ); + TS_ASSERT_EQUALS( disjunction.getPhaseStatusCDO(), static_cast *>( nullptr ) ); + TS_ASSERT_EQUALS( disjunction.getInfeasibleCasesCDList(), static_cast *>( nullptr ) ); TS_ASSERT_THROWS_NOTHING( disjunction.initializeCDOs( &context ) ); TS_ASSERT_EQUALS( disjunction.getContext(), &context ); - TS_ASSERT_DIFFERS( disjunction.getActiveStatusCDO(), static_cast*>( nullptr ) ); - TS_ASSERT_DIFFERS( disjunction.getPhaseStatusCDO(), static_cast*>( nullptr ) ); - TS_ASSERT_DIFFERS( disjunction.getInfeasibleCasesCDList(), static_cast*>( nullptr ) ); + TS_ASSERT_DIFFERS( disjunction.getActiveStatusCDO(), static_cast *>( nullptr ) ); + TS_ASSERT_DIFFERS( disjunction.getPhaseStatusCDO(), static_cast *>( nullptr ) ); + TS_ASSERT_DIFFERS( disjunction.getInfeasibleCasesCDList(), static_cast *>( nullptr ) ); bool active = false; TS_ASSERT_THROWS_NOTHING( active = disjunction.isActive() ); @@ -449,7 +454,7 @@ class DisjunctionConstraintTestSuite : public CxxTest::TestSuite PiecewiseLinearCaseSplit validSplit = dc.getImpliedCaseSplit(); TS_ASSERT_EQUALS( validSplit, *cs3 ); - dc.markInfeasible( dc.getPhaseStatus() ); + dc.markInfeasible( dc.getImpliedCase() ); TS_ASSERT( !dc.isFeasible() ); TS_ASSERT_EQUALS( dc.nextFeasibleCase(), CONSTRAINT_INFEASIBLE ); } @@ -514,7 +519,7 @@ class DisjunctionConstraintTestSuite : public CxxTest::TestSuite Tightening t2( 0, 5, Tightening::UB ); Tightening t3( 3, 0, Tightening::UB ); // First aux introduced here. Tightening t4( 4, 0, Tightening::LB ); // Second aux introduced here. - for ( const auto &t : {t1, t2, t3, t4} ) + for ( const auto &t : { t1, t2, t3, t4 } ) TS_ASSERT( split->getBoundTightenings().exists( t ) ); } ++split; @@ -525,7 +530,7 @@ class DisjunctionConstraintTestSuite : public CxxTest::TestSuite Tightening t1( 0, 5, Tightening::LB ); Tightening t2( 5, 0, Tightening::UB ); // Third aux introduced here. Tightening t3( 6, 0, Tightening::LB ); // Fourth aux - for ( const auto &t : {t1, t2, t3} ) + for ( const auto &t : { t1, t2, t3 } ) TS_ASSERT( split->getBoundTightenings().exists( t ) ); } ++split; @@ -535,7 +540,7 @@ class DisjunctionConstraintTestSuite : public CxxTest::TestSuite TS_ASSERT( split->getEquations().empty() ); Tightening t1( 7, 0, Tightening::LB ); // 5th aux Tightening t2( 8, 0, Tightening::UB ); // 6th aux - for ( const auto &t : {t1, t2} ) + for ( const auto &t : { t1, t2 } ) TS_ASSERT( split->getBoundTightenings().exists( t ) ); } @@ -617,8 +622,8 @@ class DisjunctionConstraintTestSuite : public CxxTest::TestSuite List recoveredCaseSplits = recoveredDisj.getCaseSplits(); auto split = recoveredCaseSplits.begin(); - TS_ASSERT_EQUALS( *split++, *cs1); - TS_ASSERT_EQUALS( *split++, *cs2); - TS_ASSERT_EQUALS( *split, *cs3); + TS_ASSERT_EQUALS( *split++, *cs1 ); + TS_ASSERT_EQUALS( *split++, *cs2 ); + TS_ASSERT_EQUALS( *split, *cs3 ); } }; diff --git a/src/engine/tests/Test_SmtCore.h b/src/engine/tests/Test_SmtCore.h index 51a9f4404e..66853643f7 100644 --- a/src/engine/tests/Test_SmtCore.h +++ b/src/engine/tests/Test_SmtCore.h @@ -22,6 +22,7 @@ #include "PiecewiseLinearConstraint.h" #include "ReluConstraint.h" #include "SmtCore.h" +#include "context/context.h" #include @@ -107,25 +108,35 @@ class SmtCoreTestSuite : public CxxTest::TestSuite } List nextSplits; + void registerCaseSplit( PiecewiseLinearCaseSplit caseSplit ) + { + nextSplits.append( caseSplit ); + allCases.append( (PhaseStatus)(++_numCases) ); + } + List getCaseSplits() const { return nextSplits; } + List allCases; List getAllCases() const { - return List(); + return allCases; } bool phaseFixed() const { - return true; + return false; } - PiecewiseLinearCaseSplit getCaseSplit( PhaseStatus /*caseId*/ ) const + PiecewiseLinearCaseSplit getCaseSplit( PhaseStatus caseId ) const { - PiecewiseLinearCaseSplit dontCare; - return dontCare; + auto it = nextSplits.begin(); + for ( int i = 0; i < (int)caseId - 1; ++i ) + ++it; + + return *it; } PiecewiseLinearCaseSplit getValidCaseSplit() const @@ -169,6 +180,7 @@ class SmtCoreTestSuite : public CxxTest::TestSuite { return ""; } + }; void setUp() @@ -188,8 +200,10 @@ class SmtCoreTestSuite : public CxxTest::TestSuite ReluConstraint constraint1( 1, 2 ); ReluConstraint constraint2( 3, 4 ); - SmtCore smtCore( engine ); + CVC4::context::Context context; + SmtCore smtCore( engine, context ); + TS_ASSERT( !smtCore.needToSplit() ); for ( unsigned i = 0; i < ( unsigned ) Options::get()->getInt( Options::CONSTRAINT_VIOLATION_THRESHOLD ) - 1; ++i ) { smtCore.reportViolatedConstraint( &constraint1 ); @@ -204,7 +218,8 @@ class SmtCoreTestSuite : public CxxTest::TestSuite void test_perform_split() { - SmtCore smtCore( engine ); + CVC4::context::Context context; + SmtCore smtCore( engine, context ); MockConstraint constraint; @@ -231,9 +246,11 @@ class SmtCoreTestSuite : public CxxTest::TestSuite split3.storeBoundTightening( bound5 ); // Store the splits - constraint.nextSplits.append( split1 ); - constraint.nextSplits.append( split2 ); - constraint.nextSplits.append( split3 ); + constraint.registerCaseSplit( split1 ); + constraint.registerCaseSplit( split2 ); + constraint.registerCaseSplit( split3 ); + + constraint.initializeCDOs( &context ); for ( unsigned i = 0; i < ( unsigned ) Options::get()->getInt( Options::CONSTRAINT_VIOLATION_THRESHOLD ); ++i ) smtCore.reportViolatedConstraint( &constraint ); @@ -242,85 +259,30 @@ class SmtCoreTestSuite : public CxxTest::TestSuite engine->lastRestoredState = NULL; TS_ASSERT( smtCore.needToSplit() ); - TS_ASSERT_EQUALS( smtCore.getStackDepth(), 0U ); + TS_ASSERT_EQUALS( smtCore.getDecisionLevel(), 0U ); TS_ASSERT( !constraint.setActiveWasCalled ); - TS_ASSERT_THROWS_NOTHING( smtCore.performSplit() ); + TS_ASSERT_THROWS_NOTHING( smtCore.decide() ); TS_ASSERT( constraint.setActiveWasCalled ); TS_ASSERT( !smtCore.needToSplit() ); - TS_ASSERT_EQUALS( smtCore.getStackDepth(), 1U ); - - // Check that Split1 was performed and tableau state was stored - TS_ASSERT_EQUALS( engine->lastLowerBounds.size(), 1U ); - TS_ASSERT_EQUALS( engine->lastLowerBounds.begin()->_variable, 1U ); - TS_ASSERT_EQUALS( engine->lastLowerBounds.begin()->_bound, 3.0 ); - - TS_ASSERT_EQUALS( engine->lastUpperBounds.size(), 1U ); - TS_ASSERT_EQUALS( engine->lastUpperBounds.begin()->_variable, 1U ); - TS_ASSERT_EQUALS( engine->lastUpperBounds.begin()->_bound, 5.0 ); - - TS_ASSERT( engine->lastStoredState ); - TS_ASSERT( !engine->lastRestoredState ); - - EngineState *originalState = engine->lastStoredState; - engine->lastStoredState = NULL; - engine->lastLowerBounds.clear(); - engine->lastUpperBounds.clear(); - engine->lastEquations.clear(); - - // Pop Split1, check that the tableau was restored and that - // a Split2 was performed - TS_ASSERT( smtCore.popSplit() ); - TS_ASSERT_EQUALS( smtCore.getStackDepth(), 1U ); - - TS_ASSERT_EQUALS( engine->lastRestoredState, originalState ); - TS_ASSERT( !engine->lastStoredState ); - engine->lastRestoredState = NULL; - - TS_ASSERT( engine->lastLowerBounds.empty() ); - - TS_ASSERT_EQUALS( engine->lastUpperBounds.size(), 2U ); - auto it = engine->lastUpperBounds.begin(); - TS_ASSERT_EQUALS( it->_variable, 2U ); - TS_ASSERT_EQUALS( it->_bound, 13.0 ); - ++it; - TS_ASSERT_EQUALS( it->_variable, 3U ); - TS_ASSERT_EQUALS( it->_bound, 25.0 ); - - engine->lastRestoredState = NULL; - engine->lastLowerBounds.clear(); - engine->lastUpperBounds.clear(); - engine->lastEquations.clear(); - - // Pop Split2, check that the tableau was restored and that - // a Split3 was performed - TS_ASSERT( smtCore.popSplit() ); - TS_ASSERT_EQUALS( smtCore.getStackDepth(), 1U ); - - TS_ASSERT_EQUALS( engine->lastRestoredState, originalState ); - TS_ASSERT( !engine->lastStoredState ); - engine->lastRestoredState = NULL; - - TS_ASSERT_EQUALS( engine->lastLowerBounds.size(), 1U ); - it = engine->lastLowerBounds.begin(); - TS_ASSERT_EQUALS( it->_variable, 14U ); - TS_ASSERT_EQUALS( it->_bound, 2.3 ); + TS_ASSERT_EQUALS( smtCore.getDecisionLevel(), 1U ); - TS_ASSERT( engine->lastUpperBounds.empty() ); + // Pop Split1 and check that Split2 was decided + TS_ASSERT( smtCore.backtrackAndContinueSearch() ); + TS_ASSERT_EQUALS( smtCore.getDecisionLevel(), 1U ); - engine->lastRestoredState = NULL; - engine->lastLowerBounds.clear(); - engine->lastUpperBounds.clear(); - engine->lastEquations.clear(); + // Pop Split2, check that Split3 was implied + TS_ASSERT( smtCore.backtrackAndContinueSearch() ); + TS_ASSERT_EQUALS( smtCore.getDecisionLevel(), 0U ); // Final pop - TS_ASSERT( !smtCore.popSplit() ); - TS_ASSERT( !engine->lastRestoredState ); - TS_ASSERT_EQUALS( smtCore.getStackDepth(), 0U ); + TS_ASSERT( !smtCore.backtrackAndContinueSearch() ); + TS_ASSERT_EQUALS( smtCore.getDecisionLevel(), 0U ); } void test_perform_split__inactive_constraint() { - SmtCore smtCore( engine ); + CVC4::context::Context context; + SmtCore smtCore( engine, context ); MockConstraint constraint; @@ -347,9 +309,9 @@ class SmtCoreTestSuite : public CxxTest::TestSuite split3.storeBoundTightening( bound5 ); // Store the splits - constraint.nextSplits.append( split1 ); - constraint.nextSplits.append( split2 ); - constraint.nextSplits.append( split3 ); + constraint.registerCaseSplit( split1 ); + constraint.registerCaseSplit( split2 ); + constraint.registerCaseSplit( split3 ); for ( unsigned i = 0; i < ( unsigned ) Options::get()->getInt( Options::CONSTRAINT_VIOLATION_THRESHOLD ); ++i ) smtCore.reportViolatedConstraint( &constraint ); @@ -357,7 +319,7 @@ class SmtCoreTestSuite : public CxxTest::TestSuite constraint.nextIsActive = false; TS_ASSERT( smtCore.needToSplit() ); - TS_ASSERT_THROWS_NOTHING( smtCore.performSplit() ); + TS_ASSERT_THROWS_NOTHING( smtCore.decide() ); TS_ASSERT( !smtCore.needToSplit() ); // Check that no split was performed @@ -370,7 +332,8 @@ class SmtCoreTestSuite : public CxxTest::TestSuite void test_all_splits_so_far() { - SmtCore smtCore( engine ); + CVC4::context::Context context; + SmtCore smtCore( engine, context ); MockConstraint constraint; @@ -391,8 +354,9 @@ class SmtCoreTestSuite : public CxxTest::TestSuite split2.storeBoundTightening( bound4 ); // Store the splits - constraint.nextSplits.append( split1 ); - constraint.nextSplits.append( split2 ); + constraint.registerCaseSplit( split1 ); + constraint.registerCaseSplit( split2 ); + constraint.initializeCDOs( &context ); for ( unsigned i = 0; i < ( unsigned ) Options::get()->getInt( Options::CONSTRAINT_VIOLATION_THRESHOLD ); ++i ) smtCore.reportViolatedConstraint( &constraint ); @@ -400,16 +364,20 @@ class SmtCoreTestSuite : public CxxTest::TestSuite constraint.nextIsActive = true; TS_ASSERT( smtCore.needToSplit() ); - TS_ASSERT_THROWS_NOTHING( smtCore.performSplit() ); + TS_ASSERT_THROWS_NOTHING( smtCore.decide() ); TS_ASSERT( !smtCore.needToSplit() ); // Register a valid split // Split 3 + MockConstraint implication; PiecewiseLinearCaseSplit split3; Tightening bound5( 14, 2.3, Tightening::LB ); + split3.storeBoundTightening( bound5 ); + implication.registerCaseSplit( split3 ); + implication.initializeCDOs( &context ); - TS_ASSERT_THROWS_NOTHING( smtCore.recordImpliedValidSplit( split3 ) ); + TS_ASSERT_THROWS_NOTHING( smtCore.pushImplication( &implication ) ); // Do another real split @@ -424,8 +392,10 @@ class SmtCoreTestSuite : public CxxTest::TestSuite Tightening bound7( 8, 13.0, Tightening::UB ); split5.storeBoundTightening( bound7 ); - constraint2.nextSplits.append( split4 ); - constraint2.nextSplits.append( split5 ); + constraint2.registerCaseSplit( split4 ); + constraint2.registerCaseSplit( split5 ); + + constraint2.initializeCDOs( &context ); for ( unsigned i = 0; i < ( unsigned ) Options::get()->getInt( Options::CONSTRAINT_VIOLATION_THRESHOLD ); ++i ) smtCore.reportViolatedConstraint( &constraint2 ); @@ -433,7 +403,7 @@ class SmtCoreTestSuite : public CxxTest::TestSuite constraint2.nextIsActive = true; TS_ASSERT( smtCore.needToSplit() ); - TS_ASSERT_THROWS_NOTHING( smtCore.performSplit() ); + TS_ASSERT_THROWS_NOTHING( smtCore.decide() ); TS_ASSERT( !smtCore.needToSplit() ); // Check that everything is received in the correct order @@ -452,110 +422,9 @@ class SmtCoreTestSuite : public CxxTest::TestSuite TS_ASSERT_EQUALS( *it, split4 ); } - void test_store_smt_state() - { - // ReLU(x0, x1) - // ReLU(x2, x3) - // ReLU(x4, x5) - - InputQuery inputQuery; - inputQuery.setNumberOfVariables( 6 ); - - ReluConstraint relu1 = ReluConstraint( 0, 1 ); - ReluConstraint relu2 = ReluConstraint( 2, 3 ); - - relu1.transformToUseAuxVariables( inputQuery ); - relu2.transformToUseAuxVariables( inputQuery ); - - SmtCore smtCore( engine ); - - PiecewiseLinearCaseSplit split1; - Tightening bound1( 1, 0.5, Tightening::LB ); - split1.storeBoundTightening( bound1 ); - TS_ASSERT_THROWS_NOTHING( smtCore.recordImpliedValidSplit( split1 ) ); - - for ( unsigned i = 0; i < ( unsigned ) Options::get()->getInt( Options::CONSTRAINT_VIOLATION_THRESHOLD ); ++i ) - smtCore.reportViolatedConstraint( &relu1 ); - - TS_ASSERT( smtCore.needToSplit() ); - TS_ASSERT_THROWS_NOTHING( smtCore.performSplit() ); - TS_ASSERT( !smtCore.needToSplit() ); - - PiecewiseLinearCaseSplit split2; - Tightening bound2( 3, 2.3, Tightening::UB ); - split2.storeBoundTightening( bound2 ); - TS_ASSERT_THROWS_NOTHING( smtCore.recordImpliedValidSplit( split2 ) ); - - for ( unsigned i = 0; i < ( unsigned ) Options::get()->getInt( Options::CONSTRAINT_VIOLATION_THRESHOLD ); ++i ) - smtCore.reportViolatedConstraint( &relu2 ); - - TS_ASSERT( smtCore.needToSplit() ); - TS_ASSERT_THROWS_NOTHING( smtCore.performSplit() ); - TS_ASSERT( !smtCore.needToSplit() ); - - SmtState smtState; - smtCore.storeSmtState( smtState ); - TS_ASSERT( smtState._impliedValidSplitsAtRoot.size() == 1 ); - TS_ASSERT( *smtState._impliedValidSplitsAtRoot.begin() == split1 ); - - TS_ASSERT( smtState._stack.size() == 2 ); - // Examine the first stackEntry - SmtStackEntry *stackEntry = *( smtState._stack.begin() ); - TS_ASSERT( stackEntry->_activeSplit == *( relu1.getCaseSplits().begin() ) ); - TS_ASSERT( *( stackEntry->_alternativeSplits.begin() ) == *( ++relu1.getCaseSplits().begin() ) ); - TS_ASSERT( stackEntry->_impliedValidSplits.size() == 1 ); - TS_ASSERT( *( stackEntry->_impliedValidSplits.begin() ) == split2 ); - // Examine the second stackEntry - stackEntry = *( ++smtState._stack.begin() ); - TS_ASSERT( stackEntry->_activeSplit == *( relu2.getCaseSplits().begin() ) ); - TS_ASSERT( *( stackEntry->_alternativeSplits.begin() ) == *( ++relu2.getCaseSplits().begin() ) ); - TS_ASSERT( stackEntry->_impliedValidSplits.size() == 0 ); - - clearSmtState( smtState ); - - TS_ASSERT_THROWS_NOTHING( smtCore.popSplit() ); - - smtCore.storeSmtState( smtState ); - TS_ASSERT( smtState._impliedValidSplitsAtRoot.size() == 1 ); - TS_ASSERT( *smtState._impliedValidSplitsAtRoot.begin() == split1 ); - - TS_ASSERT( smtState._stack.size() == 2 ); - // Examine the first stackEntry - stackEntry = *( smtState._stack.begin() ); - TS_ASSERT( stackEntry->_activeSplit == *( relu1.getCaseSplits().begin() ) ); - TS_ASSERT( *( stackEntry->_alternativeSplits.begin() ) == *( ++relu1.getCaseSplits().begin() ) ); - TS_ASSERT( stackEntry->_impliedValidSplits.size() == 1 ); - TS_ASSERT( *( stackEntry->_impliedValidSplits.begin() ) == split2 ); - // Examine the second stackEntry - stackEntry = *( ++smtState._stack.begin() ); - TS_ASSERT( stackEntry->_activeSplit == *( ++relu2.getCaseSplits().begin() ) ); - TS_ASSERT( stackEntry->_alternativeSplits.empty() ); - TS_ASSERT( stackEntry->_impliedValidSplits.size() == 0 ); - - clearSmtState( smtState ); - - TS_ASSERT_THROWS_NOTHING( smtCore.popSplit() ); - } - - void clearSmtState( SmtState &smtState ) - { - for ( const auto &stackEntry : smtState._stack ) - delete stackEntry; - smtState._stack = List(); - smtState._impliedValidSplitsAtRoot = List(); - } - void test_todo() { // Reason: the inefficiency in resizing the tableau mutliple times TS_TRACE( "add support for adding multiple equations at once, not one-by-one" ); } }; - -// -// Local Variables: -// compile-command: "make -C ../../.. " -// tags-file-name: "../../../TAGS" -// c-basic-offset: 4 -// End: -//