fix failing tests

NeuralNetworkVerification · Jan 6, 2024 · 9a9cb8f · 9a9cb8f
1 parent 83fbff7
commit 9a9cb8f
Show file tree

Hide file tree

Showing 3 changed files with 13 additions and 7 deletions.
diff --git a/src/configuration/GlobalConfiguration.cpp b/src/configuration/GlobalConfiguration.cpp
@@ -114,7 +114,7 @@ const bool GlobalConfiguration::GUROBI_LOGGING = false;
 // Logging - note that it is enabled only in Debug mode
 const bool GlobalConfiguration::DNC_MANAGER_LOGGING = true;
 const bool GlobalConfiguration::ENGINE_LOGGING = true;
-const bool GlobalConfiguration::TABLEAU_LOGGING = false;
+const bool GlobalConfiguration::TABLEAU_LOGGING = true;
 const bool GlobalConfiguration::SMT_CORE_LOGGING = true;
 const bool GlobalConfiguration::DANTZIGS_RULE_LOGGING = false;
 const bool GlobalConfiguration::BASIS_FACTORIZATION_LOGGING = false;

diff --git a/src/engine/Engine.cpp b/src/engine/Engine.cpp
@@ -283,11 +283,9 @@ bool Engine::solve( unsigned timeoutInSeconds )
             // If true, we just entered a new subproblem
             if ( splitJustPerformed )
             {
-                std::cout << "bt" << std::endl;
                 performBoundTighteningAfterCaseSplit();
                 informLPSolverOfBounds();
                 splitJustPerformed = false;
-                std::cout << "bt - done" << std::endl;
             }
 
             // Perform any SmtCore-initiated case splits
@@ -306,6 +304,13 @@ bool Engine::solve( unsigned timeoutInSeconds )
 
             if ( allVarsWithinBounds() )
             {
+                // It's possible that a disjunction constraint is fixed and additional constraints
+                // are introduced, making the linear portion unsatisfied. So we need to make sure
+                // there are no valid case splits that we do not know of.
+                applyAllBoundTightenings();
+                if ( applyAllValidConstraintCaseSplits() )
+                    continue;
+
                 // The linear portion of the problem has been solved.
                 // Check the status of the PL constraints
                 bool solutionFound =

diff --git a/src/engine/tests/Test_RowBoundTightener.h b/src/engine/tests/Test_RowBoundTightener.h
@@ -16,6 +16,7 @@
 #include <cxxtest/TestSuite.h>
 
 #include "MockTableau.h"
+#include "GlobalConfiguration.h"
 #include "RowBoundTightener.h"
 
 class MockForRowBoundTightener
@@ -105,8 +106,8 @@ class RowBoundTightenerTestSuite : public CxxTest::TestSuite
 
         // LB -> 1 - 10 - 4 -100
         // UB -> 1 - 5 + 6 + 100
-        TS_ASSERT_EQUALS( lower->_value, -113 );
-        TS_ASSERT_EQUALS( upper->_value, 102 );
+        TS_ASSERT_EQUALS( lower->_value, -113 - GlobalConfiguration::EXPLICIT_BASIS_BOUND_TIGHTENING_ROUNDING_CONSTANT );
+        TS_ASSERT_EQUALS( upper->_value, 102 + GlobalConfiguration::EXPLICIT_BASIS_BOUND_TIGHTENING_ROUNDING_CONSTANT );
     }
 
     void test_pivot_row_just_upper_tightend()
@@ -166,7 +167,7 @@ class RowBoundTightenerTestSuite : public CxxTest::TestSuite
         TS_ASSERT_EQUALS( upper->_type, Tightening::UB );
 
         // Lower: 1 - 10 - 4, Upper: 1 - 5 + 6
-        TS_ASSERT_EQUALS( upper->_value, 2 );
+        TS_ASSERT_EQUALS( upper->_value, 2 + GlobalConfiguration::EXPLICIT_BASIS_BOUND_TIGHTENING_ROUNDING_CONSTANT );
     }
 
     void test_pivot_row__just_lower_tightend()
@@ -219,7 +220,7 @@ class RowBoundTightenerTestSuite : public CxxTest::TestSuite
         TS_ASSERT_EQUALS( lower._type, Tightening::LB );
 
         // Lower: 1 - 10 - 4, Lower: 1 - 5 + 6
-        TS_ASSERT_EQUALS( lower._value, -13 );
+        TS_ASSERT_EQUALS( lower._value, -13 - GlobalConfiguration::EXPLICIT_BASIS_BOUND_TIGHTENING_ROUNDING_CONSTANT );
     }
 
     void test_pivot_row__nothing_tightened()