Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

More stable ratio test #78

Merged
merged 73 commits into from
Jul 24, 2018
Merged
Changes from 1 commit
Commits
Show all changes
73 commits
Select commit Hold shift + click to select a range
97fa3eb
initial work on sparse matrix representation
GuyKatzHuji Jun 18, 2018
f67f40f
store/restore functionality
GuyKatzHuji Jun 18, 2018
9f1ad34
addLastRow functionality
GuyKatzHuji Jun 18, 2018
8315e89
getRow and getColumn
GuyKatzHuji Jun 18, 2018
9f96f81
column-merging functionality
GuyKatzHuji Jun 18, 2018
1ea9792
added an interface class
GuyKatzHuji Jun 19, 2018
1826116
introducing also sparse vectors
GuyKatzHuji Jun 19, 2018
a50b767
added addLastColumn functionality
GuyKatzHuji Jun 19, 2018
5394f30
another unittest
GuyKatzHuji Jun 19, 2018
c509909
get sparse columns/matrices in dense form
GuyKatzHuji Jun 19, 2018
66c00ce
WIP on storing the constraint matrix inside the tableau in sparse form
GuyKatzHuji Jun 19, 2018
b20cc6f
more WIP, fixed a few bugs, still have a couple of failing tests
GuyKatzHuji Jun 19, 2018
7f95cb1
fixed some test issues
GuyKatzHuji Jun 20, 2018
a90fd95
initialization
GuyKatzHuji Jun 20, 2018
dc2af7f
resize _a along with the rest
GuyKatzHuji Jun 20, 2018
4db0052
Merge branch 'master' into sparse_matrices
GuyKatzHuji Jul 8, 2018
f3683fb
sparse lu factors
GuyKatzHuji Jul 8, 2018
ea02f96
store also the transposed versions of F and V
GuyKatzHuji Jul 9, 2018
d3610b3
starting work on the sparse GE
GuyKatzHuji Jul 9, 2018
403decb
some work on changing the values within an existing sparse
GuyKatzHuji Jul 9, 2018
e05eb0e
refactoring and new functionality for CSRMatrix: any kind of
GuyKatzHuji Jul 10, 2018
2f3d16d
support for empty initialization and counting elements
GuyKatzHuji Jul 10, 2018
234b694
sparse GE is now working. minor bug fixes elsewhere
GuyKatzHuji Jul 10, 2018
36b9a60
compute Ft and Vt as part of the G-elimination process
GuyKatzHuji Jul 11, 2018
836d393
tests
GuyKatzHuji Jul 11, 2018
71b70c4
basis oracles can return also sparse columns, not just dense
GuyKatzHuji Jul 11, 2018
7408f3d
sparse LU factorization class
GuyKatzHuji Jul 11, 2018
f3b98ec
switch to using the sparse factorization in the engine/tableau
GuyKatzHuji Jul 11, 2018
64ae293
bug fix in mergeColumns, and nicer printing
GuyKatzHuji Jul 11, 2018
f583be0
bug fix
GuyKatzHuji Jul 11, 2018
d545f15
bug fix
GuyKatzHuji Jul 11, 2018
6120c31
bug fix: merging columns does not delete the actual column, just
GuyKatzHuji Jul 12, 2018
b667c26
configuration changes
GuyKatzHuji Jul 12, 2018
7364641
optimization: since the sparse columns of A are needed all the time,
GuyKatzHuji Jul 12, 2018
cb67ed9
a more efficient implementation of sparse vectors
GuyKatzHuji Jul 12, 2018
05e06de
comments and unit tests
GuyKatzHuji Jul 12, 2018
f0c9c68
cleanup
GuyKatzHuji Jul 12, 2018
ad79fac
Merge branch 'master' into sparse_matrices
GuyKatzHuji Jul 12, 2018
27b0f04
keep _A in dense column-major format, too, instead of repeatedly
GuyKatzHuji Jul 12, 2018
ad630e5
Merge branch 'master' into sparse_matrices
GuyKatzHuji Jul 12, 2018
7df63cd
bad deletes
GuyKatzHuji Jul 15, 2018
f3ab834
bug fix in test
GuyKatzHuji Jul 15, 2018
aa00bbc
bug fixes: relu constraint propagation, and the handling of merged
GuyKatzHuji Jul 15, 2018
b05229b
new test
GuyKatzHuji Jul 15, 2018
8421ff6
compute Ft incrementally, use it whenever sparse columns are required
GuyKatzHuji Jul 15, 2018
ce8968d
did the todo
GuyKatzHuji Jul 15, 2018
6da8e7f
valgrind fixes
GuyKatzHuji Jul 16, 2018
ab6e2a3
Merge branch 'master' into sparse_matrices
GuyKatzHuji Jul 16, 2018
1d42540
debugging
GuyKatzHuji Jul 16, 2018
089097e
un-initialized memory
GuyKatzHuji Jul 18, 2018
11bef7d
merge
GuyKatzHuji Jul 18, 2018
bca044d
cleanup
GuyKatzHuji Jul 18, 2018
518f157
fixing an issue with cost function degradation
GuyKatzHuji Jul 18, 2018
ee74206
Merge branch 'master' into sparse_matrices
GuyKatzHuji Jul 18, 2018
74d4648
reinstating the anti-looping trick
GuyKatzHuji Jul 18, 2018
4b2cb18
debug prints
GuyKatzHuji Jul 19, 2018
6a898f2
verify invariants
GuyKatzHuji Jul 19, 2018
72c2804
debug info for crash
GuyKatzHuji Jul 19, 2018
34eacff
fixing a numerical stability issue
guykatzz Jul 20, 2018
747297c
cleanup
guykatzz Jul 20, 2018
600339f
Merge branch 'master' into sparse_matrices
guykatzz Jul 20, 2018
7f50496
cleanup
guykatzz Jul 20, 2018
7e314e2
Merge branch 'master' into sparse_matrices
guykatzz Jul 21, 2018
45ef5c7
removing the code with the failing assertion
guykatzz Jul 22, 2018
0d187f8
weaken a couple of too-storng assertions
guykatzz Jul 22, 2018
d32f7cc
bug fix and some fine-tuning of PSE
guykatzz Jul 22, 2018
ee81a08
bug fix in LU factorization
guykatzz Jul 22, 2018
d5188bb
Merge branch 'master' into sparse_matrices
GuyKatzHuji Jul 23, 2018
5cb7976
WIP
GuyKatzHuji Jul 23, 2018
0005099
cleanup
guykatzz Jul 23, 2018
bfb8198
cleanup
guykatzz Jul 23, 2018
9eb834a
fine-tuning the computation of basic costs
GuyKatzHuji Jul 24, 2018
127d019
more robust comparisons
GuyKatzHuji Jul 24, 2018
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
more WIP, fixed a few bugs, still have a couple of failing tests
GuyKatzHuji committed Jun 19, 2018
commit b20cc6f9d42a7dacab076ef765dba5bd2e621670
2 changes: 2 additions & 0 deletions src/basis_factorization/CSRMatrix.cpp
Original file line number Diff line number Diff line change
@@ -51,6 +51,8 @@ void CSRMatrix::initialize( const double *M, unsigned m, unsigned n )
unsigned estimatedNumRowEntries = std::max( 2U, _n / ROW_DENSITY_ESTIMATE );
_estimatedNnz = estimatedNumRowEntries * _m;

freeMemoryIfNeeded();

_A = new double[_estimatedNnz];
if ( !_A )
throw BasisFactorizationError( BasisFactorizationError::ALLOCATION_FAILED, "CSRMatrix::A" );
21 changes: 21 additions & 0 deletions src/engine/Equation.cpp
Original file line number Diff line number Diff line change
@@ -12,6 +12,7 @@

#include "Equation.h"
#include "FloatUtils.h"
#include "Map.h"

Equation::Addend::Addend( double coefficient, unsigned variable )
: _coefficient( coefficient )
@@ -83,6 +84,26 @@ bool Equation::operator==( const Equation &other ) const
( _type == other._type );
}

bool Equation::equivalent( const Equation &other ) const
{
if ( _scalar != other._scalar )
return false;

if ( _type != other._type )
return false;

Map<unsigned, double> us;
Map<unsigned, double> them;

for ( const auto &addend : _addends )
us[addend._variable] = addend._coefficient;

for ( const auto &addend : other._addends )
them[addend._variable] = addend._coefficient;

return us == them;
}

void Equation::dump() const
{
for ( const auto &addend : _addends )
1 change: 1 addition & 0 deletions src/engine/Equation.h
Original file line number Diff line number Diff line change
@@ -64,6 +64,7 @@ class Equation
EquationType _type;

bool operator==( const Equation &other ) const;
bool equivalent( const Equation &other ) const;

void dump() const;
};
64 changes: 42 additions & 22 deletions src/engine/Tableau.cpp
Original file line number Diff line number Diff line change
@@ -34,7 +34,8 @@ Tableau::Tableau()
, _changeColumn( NULL )
, _pivotRow( NULL )
, _b( NULL )
, _work( NULL )
, _workM( NULL )
, _workN( NULL )
, _unitVector( NULL )
, _basisFactorization( NULL )
, _multipliers( NULL )
@@ -51,7 +52,6 @@ Tableau::Tableau()
, _statistics( NULL )
, _costFunctionManager( NULL )
{
_A = new CSRMatrix();
}

Tableau::~Tableau()
@@ -157,10 +157,16 @@ void Tableau::freeMemoryIfNeeded()
_basisFactorization = NULL;
}

if ( _work )
if ( _workM )
{
delete[] _workM;
_workM = NULL;
}

if ( _workN )
{
delete[] _work;
_work = NULL;
delete[] _workN;
_workN = NULL;
}
}

@@ -169,6 +175,10 @@ void Tableau::setDimensions( unsigned m, unsigned n )
_m = m;
_n = n;

_A = new CSRMatrix();
if ( !_A )
throw ReluplexError( ReluplexError::ALLOCATION_FAILED, "Tableau::A" );

_a = new double[m];
if ( !_a )
throw ReluplexError( ReluplexError::ALLOCATION_FAILED, "Tableau::a" );
@@ -231,8 +241,12 @@ void Tableau::setDimensions( unsigned m, unsigned n )
if ( !_basisFactorization )
throw ReluplexError( ReluplexError::ALLOCATION_FAILED, "Tableau::basisFactorization" );

_work = new double[m];
if ( !_work )
_workM = new double[m];
if ( !_workM )
throw ReluplexError( ReluplexError::ALLOCATION_FAILED, "Tableau::work" );

_workN = new double[n];
if ( !_workN )
throw ReluplexError( ReluplexError::ALLOCATION_FAILED, "Tableau::work" );

if ( _statistics )
@@ -312,7 +326,7 @@ void Tableau::computeAssignment()
We first compute y (stored in _work), and then do an FTRAN pass to solve B*xB = y
*/

memcpy( _work, _b, sizeof(double) * _m );
memcpy( _workM, _b, sizeof(double) * _m );

// Compute a linear combination of the columns of AN
for ( unsigned i = 0; i < _n - _m; ++i )
@@ -322,11 +336,11 @@ void Tableau::computeAssignment()

_A->getColumn( var, &_sparseWorkVector );
for ( const auto entry : _sparseWorkVector._values )
_work[entry.first] -= entry.second * value;
_workM[entry.first] -= entry.second * value;
}

// Solve B*xB = y by performing a forward transformation
_basisFactorization->forwardTransformation( _work, _basicAssignment );
_basisFactorization->forwardTransformation( _workM, _basicAssignment );

computeBasicStatus();

@@ -1054,8 +1068,8 @@ void Tableau::getTableauRow( unsigned index, TableauRow *row )
row->_row[i]._coefficient -= ( _multipliers[entry.first] * entry.second );
}

_basisFactorization->forwardTransformation( _b, _work );
row->_scalar = _work[index];
_basisFactorization->forwardTransformation( _b, _workM );
row->_scalar = _workM[index];

row->_lhs = _basicIndexToVariable[index];
}
@@ -1281,11 +1295,11 @@ unsigned Tableau::addEquation( const Equation &equation )

// Adjust the constraint matrix
_A->addEmptyColumn();
std::fill_n( _work, _m, 0.0 );
std::fill_n( _workN, _n, 0.0 );
for ( const auto &addend : equation._addends )
_work[addend._variable] = addend._coefficient;
_work[_m - 1] = 1;
_A->addLastRow( _work );
_workN[addend._variable] = addend._coefficient;
_workN[auxVariable] = 1;
_A->addLastRow( _workN );

// Invalidate the cost function, so that it is recomputed in the next iteration.
_costFunctionManager->invalidateCostFunction();
@@ -1476,12 +1490,18 @@ void Tableau::addRow()
delete _basisFactorization;
_basisFactorization = newBasisFactorization;

// Allocate a larger _work. Don't need to initialize.
double *newWork = new double[newM];
if ( !newWork )
throw ReluplexError( ReluplexError::ALLOCATION_FAILED, "Tableau::newWork" );
delete[] _work;
_work = newWork;
// Allocate a larger _workM and _workN. Don't need to initialize.
double *newWorkM = new double[newM];
if ( !newWorkM )
throw ReluplexError( ReluplexError::ALLOCATION_FAILED, "Tableau::newWorkM" );
delete[] _workM;
_workM = newWorkM;

double *newWorkN = new double[newN];
if ( !newWorkN )
throw ReluplexError( ReluplexError::ALLOCATION_FAILED, "Tableau::newWorkN" );
delete[] _workN;
_workN = newWorkN;

_m = newM;
_n = newN;
5 changes: 3 additions & 2 deletions src/engine/Tableau.h
Original file line number Diff line number Diff line change
@@ -457,9 +457,10 @@ class Tableau : public ITableau, public IBasisFactorization::BasisColumnOracle
double *_b;

/*
Working memory (of size m).
Working memory (of size m and n).
*/
double *_work;
double *_workM;
double *_workN;

/*
Working memory for extracting information from
8 changes: 6 additions & 2 deletions src/engine/tests/MockTableau.h
Original file line number Diff line number Diff line change
@@ -423,9 +423,13 @@ class MockTableau : public ITableau
return NULL;
}

void getSparseARow( unsigned /* row */, SparseVector */* result */ ) const
void getSparseARow( unsigned row, SparseVector *result ) const
{
TS_ASSERT( false );
for ( unsigned i = 0; i < lastN; ++i )
{
if ( !FloatUtils::isZero( A[row*lastN + i] ) )
result->_values[i] = A[row*lastN + i];
}
}

void performDegeneratePivot()
3 changes: 0 additions & 3 deletions src/engine/tests/Test_Preprocessor.h
Original file line number Diff line number Diff line change
@@ -420,10 +420,7 @@ class PreprocessorTestSuite : public CxxTest::TestSuite
equation1.setScalar( 10 );
inputQuery.addEquation( equation1 );

TS_TRACE( "Start" );

InputQuery processed = Preprocessor().preprocess( inputQuery, false );
TS_TRACE( "End" );

TS_ASSERT_EQUALS( processed.getNumberOfVariables(), 4U );

189 changes: 110 additions & 79 deletions src/engine/tests/Test_Tableau.h
Original file line number Diff line number Diff line change
@@ -1395,91 +1395,122 @@ class TableauTestSuite : public CxxTest::TestSuite
3x3 + x7 + 4x1 + 3x2 + 4x4 = 420
*/

Equation expected1( Equation::EQ );
expected1.setScalar( 225 );
expected1.addAddend( 1, 4 );
expected1.addAddend( 1, 2 );
expected1.addAddend( 3, 0 );
expected1.addAddend( 2, 1 );
expected1.addAddend( 2, 3 );

Equation expected2( Equation::EQ );
expected2.setScalar( 117 );
expected2.addAddend( 1, 2 );
expected2.addAddend( 1, 0 );
expected2.addAddend( 1, 1 );
expected2.addAddend( 1, 5 );
expected2.addAddend( 1, 3 );

Equation expected3( Equation::EQ );
expected3.setScalar( 420 );
expected3.addAddend( 3, 2 );
expected3.addAddend( 1, 6 );
expected3.addAddend( 4, 0 );
expected3.addAddend( 3, 1 );
expected3.addAddend( 4, 3 );

List<Equation *> equations;
TS_ASSERT_THROWS_NOTHING( tableau->makeBasisMatrixAvailable() );
TS_ASSERT_THROWS_NOTHING( tableau->getBasisEquations( equations ) );
TS_ASSERT_EQUALS( equations.size(), 3u );

auto it = equations.begin();
Equation *eq1 = *it;
++it;
Equation *eq2 = *it;
++it;
Equation *eq3 = *it;

eq1->dump();

// Check equation 1
TS_ASSERT_EQUALS( eq1->_scalar, 225.0 );
TS_ASSERT_EQUALS( eq1->_addends.size(), 5u );

auto addend = eq1->_addends.begin();
TS_ASSERT_EQUALS( addend->_coefficient, 1.0 );
TS_ASSERT_EQUALS( addend->_variable, 4u );

++addend;
TS_ASSERT_EQUALS( addend->_coefficient, 1.0 );
TS_ASSERT_EQUALS( addend->_variable, 2u );

++addend;
TS_ASSERT_EQUALS( addend->_coefficient, 3.0 );
TS_ASSERT_EQUALS( addend->_variable, 0u );

++addend;
TS_ASSERT_EQUALS( addend->_coefficient, 2.0 );
TS_ASSERT_EQUALS( addend->_variable, 1u );

++addend;
TS_ASSERT_EQUALS( addend->_coefficient, 2.0 );
TS_ASSERT_EQUALS( addend->_variable, 3u );

// Check equation 2
TS_ASSERT_EQUALS( eq2->_scalar, 117.0 );
TS_ASSERT_EQUALS( eq2->_addends.size(), 5u );

addend = eq2->_addends.begin();
TS_ASSERT_EQUALS( addend->_coefficient, 1.0 );
TS_ASSERT_EQUALS( addend->_variable, 2u );

++addend;
TS_ASSERT_EQUALS( addend->_coefficient, 1.0 );
TS_ASSERT_EQUALS( addend->_variable, 0u );

++addend;
TS_ASSERT_EQUALS( addend->_coefficient, 1.0 );
TS_ASSERT_EQUALS( addend->_variable, 1u );

++addend;
TS_ASSERT_EQUALS( addend->_coefficient, 1.0 );
TS_ASSERT_EQUALS( addend->_variable, 5u );

++addend;
TS_ASSERT_EQUALS( addend->_coefficient, 1.0 );
TS_ASSERT_EQUALS( addend->_variable, 3u );

// Check equation 3
TS_ASSERT_EQUALS( eq3->_scalar, 420.0 );
TS_ASSERT_EQUALS( eq3->_addends.size(), 5u );

addend = eq3->_addends.begin();
TS_ASSERT_EQUALS( addend->_coefficient, 3.0 );
TS_ASSERT_EQUALS( addend->_variable, 2u );

++addend;
TS_ASSERT_EQUALS( addend->_coefficient, 1.0 );
TS_ASSERT_EQUALS( addend->_variable, 6u );

++addend;
TS_ASSERT_EQUALS( addend->_coefficient, 4.0 );
TS_ASSERT_EQUALS( addend->_variable, 0u );

++addend;
TS_ASSERT_EQUALS( addend->_coefficient, 3.0 );
TS_ASSERT_EQUALS( addend->_variable, 1u );

++addend;
TS_ASSERT_EQUALS( addend->_coefficient, 4.0 );
TS_ASSERT_EQUALS( addend->_variable, 3u );
TS_ASSERT( expected1.equivalent( **it++ ) );
TS_ASSERT( expected2.equivalent( **it++ ) );
TS_ASSERT( expected3.equivalent( **it++ ) );

// Equation *eq1 = *it;
// ++it;
// Equation *eq2 = *it;
// ++it;
// Equation *eq3 = *it;

// TS_TRACE( "Here" );
// eq1->dump();
// eq2->dump();
// eq3->dump();

// // Check equation 1
// TS_ASSERT_EQUALS( eq1->_scalar, 225.0 );
// TS_ASSERT_EQUALS( eq1->_addends.size(), 5u );

// auto addend = eq1->_addends.begin();
// TS_ASSERT_EQUALS( addend->_coefficient, 1.0 );
// TS_ASSERT_EQUALS( addend->_variable, 4u );

// ++addend;
// TS_ASSERT_EQUALS( addend->_coefficient, 1.0 );
// TS_ASSERT_EQUALS( addend->_variable, 2u );

// ++addend;
// TS_ASSERT_EQUALS( addend->_coefficient, 3.0 );
// TS_ASSERT_EQUALS( addend->_variable, 0u );

// ++addend;
// TS_ASSERT_EQUALS( addend->_coefficient, 2.0 );
// TS_ASSERT_EQUALS( addend->_variable, 1u );

// ++addend;
// TS_ASSERT_EQUALS( addend->_coefficient, 2.0 );
// TS_ASSERT_EQUALS( addend->_variable, 3u );

// // Check equation 2
// TS_ASSERT_EQUALS( eq2->_scalar, 117.0 );
// TS_ASSERT_EQUALS( eq2->_addends.size(), 5u );

// addend = eq2->_addends.begin();
// TS_ASSERT_EQUALS( addend->_coefficient, 1.0 );
// TS_ASSERT_EQUALS( addend->_variable, 2u );

// ++addend;
// TS_ASSERT_EQUALS( addend->_coefficient, 1.0 );
// TS_ASSERT_EQUALS( addend->_variable, 0u );

// ++addend;
// TS_ASSERT_EQUALS( addend->_coefficient, 1.0 );
// TS_ASSERT_EQUALS( addend->_variable, 1u );

// ++addend;
// TS_ASSERT_EQUALS( addend->_coefficient, 1.0 );
// TS_ASSERT_EQUALS( addend->_variable, 5u );

// ++addend;
// TS_ASSERT_EQUALS( addend->_coefficient, 1.0 );
// TS_ASSERT_EQUALS( addend->_variable, 3u );

// // Check equation 3
// TS_ASSERT_EQUALS( eq3->_scalar, 420.0 );
// TS_ASSERT_EQUALS( eq3->_addends.size(), 5u );

// addend = eq3->_addends.begin();
// TS_ASSERT_EQUALS( addend->_coefficient, 3.0 );
// TS_ASSERT_EQUALS( addend->_variable, 2u );

// ++addend;
// TS_ASSERT_EQUALS( addend->_coefficient, 1.0 );
// TS_ASSERT_EQUALS( addend->_variable, 6u );

// ++addend;
// TS_ASSERT_EQUALS( addend->_coefficient, 4.0 );
// TS_ASSERT_EQUALS( addend->_variable, 0u );

// ++addend;
// TS_ASSERT_EQUALS( addend->_coefficient, 3.0 );
// TS_ASSERT_EQUALS( addend->_variable, 1u );

// ++addend;
// TS_ASSERT_EQUALS( addend->_coefficient, 4.0 );
// TS_ASSERT_EQUALS( addend->_variable, 3u );

TS_ASSERT_THROWS_NOTHING( delete tableau );
}