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

Handle MalformedBasis exceptions when adding a new equation #50

Merged
merged 21 commits into from
May 23, 2018
Merged
Changes from 1 commit
Commits
Show all changes
21 commits
Select commit Hold shift + click to select a range
f318b4f
a more efficient computation of the explicit basis:
GuyKatzHuji May 8, 2018
f4af79f
Merge branch 'master' into ft_opt
GuyKatzHuji May 8, 2018
11796ab
pivoting stats
GuyKatzHuji May 8, 2018
a32d35f
bug fix in store/restore
GuyKatzHuji May 8, 2018
f0193cd
Merge branch 'master' into ft_opt
GuyKatzHuji May 8, 2018
e53123c
supprt for a "basis column oracle", which allows the basis
GuyKatzHuji May 9, 2018
6c7e6e3
cleanup in FT factorization
GuyKatzHuji May 9, 2018
450a302
grab a fresh basis from the oracle instead of condensing th etas
GuyKatzHuji May 9, 2018
bdf5954
Merge branch 'master' into ft_opt
GuyKatzHuji May 9, 2018
23ba33a
bug fix in test
GuyKatzHuji May 10, 2018
8c1440b
Merge branch 'master' into ft_opt
GuyKatzHuji May 10, 2018
ca7f01e
Merge branch 'master' into ft_opt
GuyKatzHuji May 21, 2018
701a3c2
started separating out the gaussian elimination functionality from the
GuyKatzHuji May 21, 2018
c66587b
Merge branch 'master' into ft_opt
GuyKatzHuji May 22, 2018
ab0a98c
error when adding an equation
GuyKatzHuji May 22, 2018
5a04155
handle the initial assignment of basic variables as part of Tableau::…
GuyKatzHuji May 23, 2018
0815323
make RowBoundTightener remember the tableau, instead of passing the
GuyKatzHuji May 23, 2018
e4e5089
Tableau's addRow() informs objects registered as "resizeWatchers" that
GuyKatzHuji May 23, 2018
b023d47
oops
GuyKatzHuji May 23, 2018
0c2a2d0
Merge branch 'master' into ft_opt
GuyKatzHuji May 23, 2018
a672601
oops
GuyKatzHuji May 23, 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
oops
GuyKatzHuji committed May 23, 2018
commit a67260121f3ddb7fcd6367ad1b4dafcd7b318161
11 changes: 0 additions & 11 deletions src/engine/Tableau.cpp
Original file line number Diff line number Diff line change
@@ -1331,17 +1331,6 @@ void Tableau::addEquation( const Equation &equation )
if ( FloatUtils::isZero( _basicAssignment[_m - 1] ) )
_basicAssignment[_m - 1] = 0.0;

// Refactorize the basis
try
{
_basisFactorization->refactorizeBasis();
}
catch ( MalformedBasisException & )
{
log( "addEquation failed - could not refactorize basis" );
throw ReluplexError( ReluplexError::FAILURE_TO_ADD_NEW_EQUATION );
}

// Notify about the new variable's assignment and compute its status
notifyVariableValue( _basicIndexToVariable[_m - 1], _basicAssignment[_m - 1] );
computeBasicStatus( _m - 1 );