| 17 | using namespace CVC4::context; |
| 18 | |
| 19 | BoundExplainer::BoundExplainer( unsigned numberOfVariables, unsigned numberOfRows, Context &ctx ) |
| 20 | : _context( ctx ) |
| 21 | , _numberOfVariables( numberOfVariables ) |
| 22 | , _numberOfRows( numberOfRows ) |
| 23 | , _upperBoundExplanations( 0 ) |
| 24 | , _lowerBoundExplanations( 0 ) |
| 25 | , _trivialUpperBoundExplanation( 0 ) |
| 26 | , _trivialLowerBoundExplanation( 0 ) |
| 27 | { |
| 28 | for ( unsigned i = 0; i < _numberOfVariables; ++i ) |
| 29 | { |
| 30 | _upperBoundExplanations.append( new ( true ) CDO<SparseUnsortedList>( &ctx ) ); |
| 31 | _lowerBoundExplanations.append( new ( true ) CDO<SparseUnsortedList>( &ctx ) ); |
| 32 | |
| 33 | _trivialUpperBoundExplanation.append( new ( true ) CDO<bool>( &ctx, true ) ); |
| 34 | _trivialLowerBoundExplanation.append( new ( true ) CDO<bool>( &ctx, true ) ); |
| 35 | } |
| 36 | } |
| 37 | |
| 38 | BoundExplainer::~BoundExplainer() |
| 39 | { |