Skip to content

Commit 139b331

Browse files
OmriIsacHUJIOmriIsacHUJI
committed
Add convenient assumptions, support additional lemmas, use proof holes for delegation, bugfix in farkasStrings.
1 parent 6dea5e3 commit 139b331

File tree

6 files changed

+252
-161
lines changed

6 files changed

+252
-161
lines changed

‎src/configuration/GlobalConfiguration.cpp‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -120,7 +120,7 @@ const bool GlobalConfiguration::WRITE_ALETHE_PROOF = true;
120120
const unsigned GlobalConfiguration::BACKWARD_BOUND_PROPAGATION_DEPTH = 3;
121121
const unsigned GlobalConfiguration::MAX_ROUNDS_OF_BACKWARD_ANALYSIS = 10;
122122

123-
const bool GlobalConfiguration::ANALYZE_PROOF_DEPENDENCIES = false;
123+
const bool GlobalConfiguration::ANALYZE_PROOF_DEPENDENCIES = true;
124124
const bool GlobalConfiguration::MINIMIZE_PROOF_DEPENDENCIES = true;
125125

126126
#ifdef ENABLE_GUROBI

‎src/engine/Engine.cpp‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3721,7 +3721,7 @@ bool Engine::certifyUNSATCertificate()
37213721

37223722
if ( GlobalConfiguration::WRITE_ALETHE_PROOF )
37233723
{
3724-
String pref = Options::get()->getString( Options::INPUT_FILE_PATH ).tokenize("/").back();
3724+
String pref = Options::get()->getString( Options::INPUT_FILE_PATH ).tokenize( "/" ).back();
37253725
File file( pref + ".smt2.alethe" );
37263726
SmtLibWriter::writeToSmtLibFile( pref + ".smt2",
37273727
_tableau->getM(),

‎src/engine/ReluConstraint.cpp‎

Lines changed: 44 additions & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -168,7 +168,7 @@ void ReluConstraint::notifyLowerBound( unsigned variable, double newBound )
168168
createTighteningRow();
169169

170170
// A positive lower bound is always propagated between f and b
171-
if ( ( variable == _f || variable == _b ) && bound > 0 )
171+
if ( ( variable == _f || variable == _b ) && FloatUtils::isPositive( bound ) )
172172
{
173173
// If we're in the active phase, aux should be 0
174174
if ( proofs && _auxVarInUse )
@@ -194,11 +194,11 @@ void ReluConstraint::notifyLowerBound( unsigned variable, double newBound )
194194

195195
// A positive lower bound for aux means we're inactive: f is 0, b is
196196
// non-positive When inactive, b = -aux
197-
else if ( _auxVarInUse && variable == _aux && bound > 0 )
197+
else if ( _auxVarInUse && variable == _aux && FloatUtils::isPositive( bound ) )
198198
{
199199
if ( proofs )
200200
_boundManager->addLemmaExplanationAndTightenBound(
201-
_f, 0, Tightening::UB, { variable }, Tightening::LB, *this, true, 0 );
201+
_f, 0, Tightening::UB, { variable }, Tightening::LB, *this, true, bound );
202202
else
203203
_boundManager->tightenUpperBound( _f, 0 );
204204

@@ -214,23 +214,24 @@ void ReluConstraint::notifyLowerBound( unsigned variable, double newBound )
214214
// If already inactive, tightening is linear
215215
if ( getPhaseStatus() == RELU_PHASE_INACTIVE )
216216
_boundManager->tightenUpperBound( _aux, -bound, *_tighteningRow );
217-
// else if ( getPhaseStatus() == PHASE_NOT_FIXED )
218-
// _boundManager->addLemmaExplanationAndTightenBound( _aux,
219-
// -bound,
220-
// Tightening::UB,
221-
// { variable },
222-
// Tightening::LB,
223-
// *this,
224-
// false,
225-
// bound );
217+
else if ( getPhaseStatus() == PHASE_NOT_FIXED &&
218+
!GlobalConfiguration::WRITE_ALETHE_PROOF )
219+
_boundManager->addLemmaExplanationAndTightenBound( _aux,
220+
-bound,
221+
Tightening::UB,
222+
{ variable },
223+
Tightening::LB,
224+
*this,
225+
false,
226+
bound );
226227
}
227228
else
228229
_boundManager->tightenUpperBound( _aux, -bound );
229230
}
230231

231232
// Also, if for some reason we only know a negative lower bound for
232233
// f, we attempt to tighten it to 0
233-
else if ( bound < 0 && variable == _f )
234+
else if ( bound < 0 && variable == _f && !GlobalConfiguration::WRITE_ALETHE_PROOF )
234235
{
235236
if ( proofs )
236237
_boundManager->addLemmaExplanationAndTightenBound(
@@ -278,14 +279,15 @@ void ReluConstraint::notifyUpperBound( unsigned variable, double newBound )
278279
else
279280
{
280281
if ( !FloatUtils::isPositive( bound ) )
281-
_boundManager->addLemmaExplanationAndTightenBound( _b,
282-
0,
283-
Tightening::UB,
284-
{ variable },
285-
Tightening::UB,
286-
*this,
287-
true,
288-
0 );
282+
_boundManager->addLemmaExplanationAndTightenBound(
283+
_b,
284+
0,
285+
Tightening::UB,
286+
{ variable },
287+
Tightening::UB,
288+
*this,
289+
true,
290+
FloatUtils::isZero( bound ) ? 0 : bound );
289291
// Bound cannot be negative if ReLU is inactive
290292
if ( FloatUtils::isNegative( bound ) )
291293
throw InfeasibleQueryException();
@@ -301,7 +303,14 @@ void ReluConstraint::notifyUpperBound( unsigned variable, double newBound )
301303
// If b has a non-positive upper bound, f's upper bound is 0
302304
if ( proofs )
303305
_boundManager->addLemmaExplanationAndTightenBound(
304-
_f, 0, Tightening::UB, { variable }, Tightening::UB, *this, true, 0 );
306+
_f,
307+
0,
308+
Tightening::UB,
309+
{ variable },
310+
Tightening::UB,
311+
*this,
312+
true,
313+
FloatUtils::isZero( bound ) ? 0 : bound );
305314
else
306315
_boundManager->tightenUpperBound( _f, 0 );
307316

@@ -318,7 +327,8 @@ void ReluConstraint::notifyUpperBound( unsigned variable, double newBound )
318327
// If already inactive, tightening is linear
319328
if ( getPhaseStatus() == RELU_PHASE_ACTIVE )
320329
_boundManager->tightenUpperBound( _f, bound, *_tighteningRow );
321-
else if ( getPhaseStatus() == PHASE_NOT_FIXED )
330+
else if ( getPhaseStatus() == PHASE_NOT_FIXED &&
331+
!GlobalConfiguration::WRITE_ALETHE_PROOF )
322332
_boundManager->addLemmaExplanationAndTightenBound( _f,
323333
bound,
324334
Tightening::UB,
@@ -341,14 +351,15 @@ void ReluConstraint::notifyUpperBound( unsigned variable, double newBound )
341351
else
342352
{
343353
if ( !FloatUtils::isPositive( bound ) )
344-
_boundManager->addLemmaExplanationAndTightenBound( _b,
345-
0,
346-
Tightening::LB,
347-
{ variable },
348-
Tightening::UB,
349-
*this,
350-
true,
351-
0 );
354+
_boundManager->addLemmaExplanationAndTightenBound(
355+
_b,
356+
0,
357+
Tightening::LB,
358+
{ variable },
359+
Tightening::UB,
360+
*this,
361+
true,
362+
FloatUtils::isZero( bound ) ? 0 : bound );
352363
// Bound cannot be negative if ReLU is active
353364
if ( FloatUtils::isNegative( bound ) )
354365
throw InfeasibleQueryException();
@@ -574,8 +585,8 @@ List<PiecewiseLinearConstraint::Fix> ReluConstraint::getSmartFixes( ITableau *ta
574585

575586
List<PiecewiseLinearCaseSplit> ReluConstraint::getCaseSplits() const
576587
{
577-
// if ( getPhaseStatus() != PHASE_NOT_FIXED )
578-
// throw MarabouError( MarabouError::REQUESTED_CASE_SPLITS_FROM_FIXED_CONSTRAINT );
588+
// if ( getPhaseStatus() != PHASE_NOT_FIXED )
589+
// throw MarabouError( MarabouError::REQUESTED_CASE_SPLITS_FROM_FIXED_CONSTRAINT );
579590

580591
List<PiecewiseLinearCaseSplit> splits;
581592

0 commit comments

Comments
 (0)