Skip to content

Commit 5565a96

Browse files
liamjdavisliamjdavis
committed
Updated constraint files to use abstract lp solver
1 parent cf08630 commit 5565a96

10 files changed

Lines changed: 50 additions & 48 deletions

‎src/engine/AbsoluteValueConstraint.cpp‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -379,8 +379,8 @@ bool AbsoluteValueConstraint::satisfied() const
379379

380380
List<PiecewiseLinearConstraint::Fix> AbsoluteValueConstraint::getPossibleFixes() const
381381
{
382-
// Reluplex does not currently work with Gurobi.
383-
ASSERT( _gurobi == NULL );
382+
// Reluplex does not currently work with an external LP solver.
383+
ASSERT( _lpSolver == NULL );
384384

385385
ASSERT( !satisfied() );
386386

@@ -551,9 +551,9 @@ void AbsoluteValueConstraint::dump( String &output ) const
551551

552552
void AbsoluteValueConstraint::updateVariableIndex( unsigned oldIndex, unsigned newIndex )
553553
{
554-
// Variable reindexing can only occur in preprocessing before Gurobi is
555-
// registered.
556-
ASSERT( _gurobi == NULL );
554+
// Variable reindexing can only occur in preprocessing before the LP
555+
// solver is registered.
556+
ASSERT( _lpSolver == NULL );
557557

558558
ASSERT( oldIndex == _b || oldIndex == _f ||
559559
( _auxVarsInUse && ( oldIndex == _posAux || oldIndex == _negAux ) ) );

‎src/engine/DisjunctionConstraint.cpp‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -202,17 +202,17 @@ bool DisjunctionConstraint::satisfied() const
202202

203203
List<PiecewiseLinearConstraint::Fix> DisjunctionConstraint::getPossibleFixes() const
204204
{
205-
// Reluplex does not currently work with Gurobi.
206-
ASSERT( _gurobi == NULL );
205+
// Reluplex does not currently work with an external LP solver.
206+
ASSERT( _lpSolver == NULL );
207207

208208
return List<PiecewiseLinearConstraint::Fix>();
209209
}
210210

211211
List<PiecewiseLinearConstraint::Fix>
212212
DisjunctionConstraint::getSmartFixes( ITableau * /* tableau */ ) const
213213
{
214-
// Reluplex does not currently work with Gurobi.
215-
ASSERT( _gurobi == NULL );
214+
// Reluplex does not currently work with an external LP solver.
215+
ASSERT( _lpSolver == NULL );
216216

217217
return getPossibleFixes();
218218
}
@@ -343,9 +343,9 @@ void DisjunctionConstraint::dump( String &output ) const
343343

344344
void DisjunctionConstraint::updateVariableIndex( unsigned oldIndex, unsigned newIndex )
345345
{
346-
// Variable reindexing can only occur in preprocessing before Gurobi is
347-
// registered.
348-
ASSERT( _gurobi == NULL );
346+
// Variable reindexing can only occur in preprocessing before the LP
347+
// solver is registered.
348+
ASSERT( _lpSolver == NULL );
349349

350350
ASSERT( !participatingVariable( newIndex ) );
351351

‎src/engine/LeakyReluConstraint.cpp‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -357,8 +357,8 @@ bool LeakyReluConstraint::satisfied() const
357357

358358
List<PiecewiseLinearConstraint::Fix> LeakyReluConstraint::getPossibleFixes() const
359359
{
360-
// Reluplex does not currently work with Gurobi.
361-
ASSERT( _gurobi == NULL );
360+
// Reluplex does not currently work with an external LP solver.
361+
ASSERT( _lpSolver == NULL );
362362

363363
ASSERT( !satisfied() );
364364
ASSERT( existsAssignment( _b ) );
@@ -614,9 +614,9 @@ void LeakyReluConstraint::dump( String &output ) const
614614

615615
void LeakyReluConstraint::updateVariableIndex( unsigned oldIndex, unsigned newIndex )
616616
{
617-
// Variable reindexing can only occur in preprocessing before Gurobi is
618-
// registered.
619-
ASSERT( _gurobi == NULL );
617+
// Variable reindexing can only occur in preprocessing before the LP
618+
// solver is registered.
619+
ASSERT( _lpSolver == NULL );
620620

621621
ASSERT( participatingVariable( oldIndex ) );
622622
ASSERT( !_lowerBounds.exists( newIndex ) && !_upperBounds.exists( newIndex ) &&

‎src/engine/MaxConstraint.cpp‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -374,15 +374,15 @@ bool MaxConstraint::isCaseInfeasible( unsigned variable ) const
374374

375375
List<PiecewiseLinearConstraint::Fix> MaxConstraint::getPossibleFixes() const
376376
{
377-
// Reluplex does not currently work with Gurobi.
378-
ASSERT( _gurobi == NULL );
377+
// Reluplex does not currently work with an external LP solver.
378+
ASSERT( _lpSolver == NULL );
379379
return List<PiecewiseLinearConstraint::Fix>();
380380
}
381381

382382
List<PiecewiseLinearConstraint::Fix> MaxConstraint::getSmartFixes( ITableau * ) const
383383
{
384-
// Reluplex does not currently work with Gurobi.
385-
ASSERT( _gurobi == NULL );
384+
// Reluplex does not currently work with an external LP solver.
385+
ASSERT( _lpSolver == NULL );
386386
return getPossibleFixes();
387387
}
388388

@@ -462,9 +462,9 @@ PiecewiseLinearCaseSplit MaxConstraint::getCaseSplit( PhaseStatus phase ) const
462462

463463
void MaxConstraint::updateVariableIndex( unsigned oldIndex, unsigned newIndex )
464464
{
465-
// Variable re-indexing can only occur in preprocessing before Gurobi is
466-
// registered.
467-
ASSERT( _gurobi == NULL );
465+
// Variable re-indexing can only occur in preprocessing before the LP
466+
// solver is registered.
467+
ASSERT( _lpSolver == NULL );
468468

469469
_lowerBounds[newIndex] = _lowerBounds[oldIndex];
470470
_upperBounds[newIndex] = _upperBounds[oldIndex];

‎src/engine/PiecewiseLinearConstraint.cpp‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@ PiecewiseLinearConstraint::PiecewiseLinearConstraint()
2929
, _cdInfeasibleCases( nullptr )
3030
, _score( FloatUtils::negativeInfinity() )
3131
, _statistics( NULL )
32-
, _gurobi( NULL )
32+
, _lpSolver( NULL )
3333
, _cdPhaseFixingEntry( nullptr )
3434
, _tableauAuxVars()
3535
{
@@ -47,7 +47,7 @@ PiecewiseLinearConstraint::PiecewiseLinearConstraint( unsigned numCases )
4747
, _cdInfeasibleCases( nullptr )
4848
, _score( FloatUtils::negativeInfinity() )
4949
, _statistics( NULL )
50-
, _gurobi( NULL )
50+
, _lpSolver( NULL )
5151
, _cdPhaseFixingEntry( nullptr )
5252
, _tableauAuxVars()
5353
{

‎src/engine/PiecewiseLinearConstraint.h‎

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -49,7 +49,7 @@
4949

5050
#include "FloatUtils.h"
5151
#include "GroundBoundManager.h"
52-
#include "GurobiWrapper.h"
52+
#include "LPSolver.h"
5353
#include "IBoundManager.h"
5454
#include "ITableau.h"
5555
#include "LinearExpression.h"
@@ -356,11 +356,11 @@ class PiecewiseLinearConstraint : public ITableau::VariableWatcher
356356
}
357357

358358
/*
359-
Register the GurobiWrapper object. We will query it for assignment.
359+
Register the LPSolver object. We will query it for assignment.
360360
*/
361-
inline void registerGurobi( GurobiWrapper *gurobi )
361+
inline void registerLPSolver( LPSolver *lpSolver )
362362
{
363-
_gurobi = gurobi;
363+
_lpSolver = lpSolver;
364364
}
365365

366366
inline void registerTableau( ITableau *tableau )
@@ -555,9 +555,9 @@ class PiecewiseLinearConstraint : public ITableau::VariableWatcher
555555
Statistics *_statistics;
556556

557557
/*
558-
The gurobi object for solving the LPs during the search.
558+
The LP solver object for solving the LPs during the search.
559559
*/
560-
GurobiWrapper *_gurobi;
560+
LPSolver *_lpSolver;
561561

562562
CVC4::context::CDO<std::shared_ptr<GroundBoundManager::GroundBoundEntry>> *_cdPhaseFixingEntry;
563563

@@ -646,8 +646,8 @@ class PiecewiseLinearConstraint : public ITableau::VariableWatcher
646646
/**********************************************************************/
647647
inline bool existsAssignment( unsigned variable ) const
648648
{
649-
if ( _gurobi )
650-
return _gurobi->existsAssignment( Stringf( "x%u", variable ) );
649+
if ( _lpSolver )
650+
return _lpSolver->existsAssignment( Stringf( "x%u", variable ) );
651651
else if ( _tableau )
652652
return _tableau->existsValue( variable );
653653
else
@@ -656,12 +656,12 @@ class PiecewiseLinearConstraint : public ITableau::VariableWatcher
656656

657657
inline double getAssignment( unsigned variable ) const
658658
{
659-
if ( _gurobi == nullptr )
659+
if ( _lpSolver == nullptr )
660660
{
661661
return _tableau->getValue( variable );
662662
}
663663
else
664-
return _gurobi->getAssignment( Stringf( "x%u", variable ) );
664+
return _lpSolver->getAssignment( Stringf( "x%u", variable ) );
665665
}
666666

667667
List<unsigned> _tableauAuxVars;

‎src/engine/ReluConstraint.cpp‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -391,8 +391,8 @@ bool ReluConstraint::satisfied() const
391391

392392
List<PiecewiseLinearConstraint::Fix> ReluConstraint::getPossibleFixes() const
393393
{
394-
// Reluplex does not currently work with Gurobi.
395-
ASSERT( _gurobi == NULL );
394+
// Reluplex does not currently work with an external LP solver.
395+
ASSERT( _lpSolver == NULL );
396396

397397
ASSERT( !satisfied() );
398398
ASSERT( existsAssignment( _b ) );
@@ -450,8 +450,8 @@ List<PiecewiseLinearConstraint::Fix> ReluConstraint::getPossibleFixes() const
450450

451451
List<PiecewiseLinearConstraint::Fix> ReluConstraint::getSmartFixes( ITableau *tableau ) const
452452
{
453-
// Reluplex does not currently work with Gurobi.
454-
ASSERT( _gurobi == NULL );
453+
// Reluplex does not currently work with an external LP solver.
454+
ASSERT( _lpSolver == NULL );
455455

456456
ASSERT( !satisfied() );
457457
ASSERT( existsAssignment( _f ) && existsAssignment( _b ) );
@@ -733,9 +733,9 @@ void ReluConstraint::dump( String &output ) const
733733

734734
void ReluConstraint::updateVariableIndex( unsigned oldIndex, unsigned newIndex )
735735
{
736-
// Variable reindexing can only occur in preprocessing before Gurobi is
737-
// registered.
738-
ASSERT( _gurobi == NULL );
736+
// Variable reindexing can only occur in preprocessing before the LP
737+
// solver is registered.
738+
ASSERT( _lpSolver == NULL );
739739

740740
ASSERT( oldIndex == _b || oldIndex == _f || ( _auxVarInUse && oldIndex == _aux ) );
741741
ASSERT( !_lowerBounds.exists( newIndex ) && !_upperBounds.exists( newIndex ) &&

‎src/engine/SignConstraint.cpp‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -485,8 +485,8 @@ void SignConstraint::notifyUpperBound( unsigned variable, double bound )
485485

486486
List<PiecewiseLinearConstraint::Fix> SignConstraint::getPossibleFixes() const
487487
{
488-
// This should never be called when we are using Gurobi to solve LPs.
489-
ASSERT( _gurobi == NULL );
488+
// This should never be called when we are using an external LP solver.
489+
ASSERT( _lpSolver == NULL );
490490

491491
ASSERT( !satisfied() );
492492
ASSERT( existsAssignment( _b ) );
@@ -537,9 +537,9 @@ void SignConstraint::getEntailedTightenings( List<Tightening> &tightenings ) con
537537

538538
void SignConstraint::updateVariableIndex( unsigned oldIndex, unsigned newIndex )
539539
{
540-
// Variable reindexing can only occur in preprocessing before Gurobi is
541-
// registered.
542-
ASSERT( _gurobi == NULL );
540+
// Variable reindexing can only occur in preprocessing before the LP
541+
// solver is registered.
542+
ASSERT( _lpSolver == NULL );
543543

544544
ASSERT( oldIndex == _b || oldIndex == _f );
545545
ASSERT( !_boundManager );

‎src/engine/tests/Test_IncrementalLinearization.h‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@
1414
**/
1515

1616
#include "FloatUtils.h"
17+
#include "GurobiWrapper.h"
1718
#include "IncrementalLinearization.h"
1819
#include "MILPEncoder.h"
1920
#include "MarabouError.h"

‎src/engine/tests/Test_MILPEncoder.h‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@
1515

1616
#include "FloatUtils.h"
1717
#include "GlobalConfiguration.h"
18+
#include "GurobiWrapper.h"
1819
#include "MILPEncoder.h"
1920
#include "MarabouError.h"
2021
#include "MockTableau.h"

0 commit comments

Comments
 (0)