Skip to content

Commit 931575e

Browse files
OmriIsacHUJIOmriIsacHUJI
committed
minor
1 parent 9246431 commit 931575e

File tree

2 files changed

+98
-71
lines changed

2 files changed

+98
-71
lines changed

‎src/proofs/AletheProofWriter.cpp‎

Lines changed: 86 additions & 63 deletions
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,7 @@ AletheProofWriter::AletheProofWriter( unsigned explanationSize,
2626
, _n( upperBounds.size() )
2727
, _m( explanationSize )
2828
, _stepCounter( 1 )
29+
, _varToPLC()
2930
{
3031
for ( unsigned i = 0; i < _n; ++i )
3132
{
@@ -36,6 +37,10 @@ AletheProofWriter::AletheProofWriter( unsigned explanationSize,
3637
_currentUpperBounds[i].push( std::tuple<int, double>( 0, upperBounds[i] ) );
3738
}
3839

40+
for ( const auto &plc : problemConstraints )
41+
for ( const auto var : plc->getParticipatingVariables() )
42+
_varToPLC.insert( var, plc );
43+
3944
// Write only necessary lines upon initialization
4045
writeTableauAssumptions();
4146
}
@@ -295,9 +300,9 @@ void AletheProofWriter::applyContradiction( const UnsatCertificateNode *node )
295300
" :rule la_generic :args " + farkasArgs;
296301

297302
String res = String( "( step res" + std::to_string( node->getId() ) ) + " (cl " +
298-
getPathClause( node ) + ") :rule resolution :premises (" +
299-
getPathResSteps( node ) + " t" + std::to_string( node->getId() ) + " " +
300-
farkasParticipants + " ) ) \n";
303+
getNegatedSplitsClause( getPathSplits( node ) ) + ") :rule resolution :premises (" +
304+
getSplitsResSteps( getPathSplits( node ) ) + " t" +
305+
std::to_string( node->getId() ) + " " + farkasParticipants + " ) ) \n";
301306

302307

303308
_proof.append( { laGeneric, res } );
@@ -334,34 +339,33 @@ void AletheProofWriter::concludeChildrenUnsat( const UnsatCertificateNode *node,
334339
ASSERT( childrenIndices.size() == 2 )
335340
PiecewiseLinearCaseSplit firstChildSplit = node->getChildren().front()->getSplit();
336341
String resLine = String( "( step res" + std::to_string( node->getId() ) + " (cl " ) +
337-
getPathClause( node ) + ") :rule resolution :premises ( split" +
342+
getNegatedSplitsClause( getPathSplits( node ) ) +
343+
") :rule resolution :premises ( split" +
338344
std::to_string( node->getChildren().front()->getSplitNum() ) + " res" +
339345
std::to_string( childrenIndices.front() ) + " res" +
340346
std::to_string( childrenIndices.back() ) + ") )\n";
341347

342348
_proof.append( resLine );
343349
}
344350

345-
String AletheProofWriter::getPathClause( const UnsatCertificateNode *node )
351+
String
352+
AletheProofWriter::getNegatedSplitsClause( const List<PiecewiseLinearCaseSplit> &splits ) const
346353
{
347-
if ( !node->getParent() )
354+
if ( splits.empty() )
348355
return "";
349356

350357
String clause = "";
351-
const UnsatCertificateNode *cur = node;
352-
while ( !cur->getSplit().getBoundTightenings().empty() )
358+
for ( const auto &split : splits )
353359
{
354360
clause += "( not ( and ";
355-
const PiecewiseLinearCaseSplit &headSplit = cur->getSplit();
356-
for ( const auto bound : headSplit.getBoundTightenings() )
361+
for ( const auto bound : split.getBoundTightenings() )
357362
clause += getBoundAsClause( bound );
358-
cur = cur->getParent();
359363
clause += " ) )";
360364
}
361365
return clause;
362366
}
363367

364-
String AletheProofWriter::getBoundAsClause( const Tightening &bound )
368+
String AletheProofWriter::getBoundAsClause( const Tightening &bound ) const
365369
{
366370
if ( bound._type == Tightening::UB )
367371
return String( "( <= x" + std::to_string( bound._variable ) + " " ) +
@@ -372,7 +376,7 @@ String AletheProofWriter::getBoundAsClause( const Tightening &bound )
372376
}
373377

374378

375-
String AletheProofWriter::getSplitAsClause( const PiecewiseLinearCaseSplit &split )
379+
String AletheProofWriter::getSplitAsClause( const PiecewiseLinearCaseSplit &split ) const
376380
{
377381
ASSERT( split.getEquations().empty() );
378382
String clause = "( and ";
@@ -383,38 +387,51 @@ String AletheProofWriter::getSplitAsClause( const PiecewiseLinearCaseSplit &spli
383387
return clause;
384388
}
385389

386-
String AletheProofWriter::getSplitsAsClause( const List<PiecewiseLinearCaseSplit> &splits )
390+
String AletheProofWriter::getSplitsAsClause( const List<PiecewiseLinearCaseSplit> &splits ) const
387391
{
388392
String clause = "";
389393
for ( const auto &split : splits )
390394
clause += getSplitAsClause( split );
391395
return clause;
392396
}
393397

394-
bool AletheProofWriter::isSplitActive( const PiecewiseLinearCaseSplit &split )
398+
bool AletheProofWriter::isSplitActive( const PiecewiseLinearCaseSplit &split ) const
395399
{
396400
ASSERT( split.getEquations().empty() )
397401
return split.getBoundTightenings().back()._type == Tightening::LB ||
398402
split.getBoundTightenings().front()._type == Tightening::LB;
399403
}
400404

401-
String AletheProofWriter::getPathResSteps( const UnsatCertificateNode *node )
405+
List<PiecewiseLinearCaseSplit>
406+
AletheProofWriter::getPathSplits( const UnsatCertificateNode *node ) const
402407
{
403-
if ( !node->getParent() )
408+
List<PiecewiseLinearCaseSplit> pathSplits = List<PiecewiseLinearCaseSplit>();
409+
const UnsatCertificateNode *cur = node;
410+
while ( cur && !cur->getSplit().getBoundTightenings().empty() )
411+
{
412+
pathSplits.append( cur->getSplit() );
413+
cur = cur->getParent();
414+
}
415+
416+
return pathSplits;
417+
}
418+
419+
String AletheProofWriter::getSplitsResSteps( const List<PiecewiseLinearCaseSplit> &splits ) const
420+
{
421+
if ( splits.empty() )
404422
return "";
405423

406424
String resSteps = " ";
407-
const UnsatCertificateNode *cur = node;
408-
while ( !cur->getSplit().getBoundTightenings().empty() )
425+
for ( const auto &split : splits )
409426
{
410-
String currentStep = " split" + std::to_string( cur->getSplitNum() );
411-
const PiecewiseLinearCaseSplit &headSplit = cur->getSplit();
412-
String isActive = isSplitActive( headSplit ) ? "a" : "i";
413-
414-
for ( unsigned i = 0; i < headSplit.getBoundTightenings().size(); ++i )
415-
currentStep += String( " split" + std::to_string( cur->getSplitNum() ) + "_" ) +
416-
isActive + std::to_string( i );
417-
cur = cur->getParent();
427+
unsigned splitNum =
428+
_varToPLC[split.getBoundTightenings().front()._variable]->getTableauAuxVars().front();
429+
String currentStep = " split" + std::to_string( splitNum );
430+
String isActive = isSplitActive( split ) ? "a" : "i";
431+
432+
for ( unsigned i = 0; i < split.getBoundTightenings().size(); ++i )
433+
currentStep += String( " split" + std::to_string( splitNum ) + "_" ) + isActive +
434+
std::to_string( i );
418435
// Add steps to the left
419436
resSteps = currentStep + resSteps;
420437
}
@@ -489,11 +506,10 @@ List<String> AletheProofWriter::applyReluLemma( const UnsatCertificateNode *node
489506
String laGeneric = String( "( step farkasLem" ) + id + " " + farkasClause +
490507
" :rule la_generic :args " + farkasArgs;
491508

492-
String res = String( "( step causResLem" ) + id + " (cl " + getPathClause( node ) + causeBound +
493-
") :rule resolution :premises (" + getPathResSteps( node ) + " farkasLem" + id +
494-
" " + farkasParticipants + " ) ) \n";
495-
496-
// TODO consider writing the causing var ground bound
509+
String res = String( "( step causResLem" ) + id + " (cl " +
510+
getNegatedSplitsClause( getPathSplits( node ) ) + causeBound +
511+
") :rule resolution :premises (" + getSplitsResSteps( getPathSplits( node ) ) +
512+
" farkasLem" + id + " " + farkasParticipants + " ) ) \n";
497513

498514
unsigned b = plc->getB();
499515
unsigned f = plc->getF();
@@ -527,29 +543,31 @@ List<String> AletheProofWriter::applyReluLemma( const UnsatCertificateNode *node
527543
{
528544
matched = true;
529545
String splitrule = causingVar == f ? "_i1" : "_i0";
530-
proofRuleRes = String( "( step resLem" ) + id + " ( cl " + getPathClause( node ) +
531-
conclusion + ") :rule resolution :premises ( causResLem" + id +
532-
" tautSplit" + id + " split" + identifier + splitrule + " split" +
533-
identifier + " split" + identifier + "_a1 ) ) \n";
546+
proofRuleRes = String( "( step resLem" ) + id + " ( cl " +
547+
getNegatedSplitsClause( getPathSplits( node ) ) + conclusion +
548+
") :rule resolution :premises ( causResLem" + id + " tautSplit" + id +
549+
" split" + identifier + splitrule + " split" + identifier + " split" +
550+
identifier + "_a1 ) ) \n";
534551
}
535552
else if ( causingVar == b && causingVarBound == Tightening::LB && affectedVar == aux &&
536553
affectedVarBound == Tightening::UB && targetBound == 0 )
537554
{
538555
matched = true;
539-
proofRuleRes = String( "( step resLem" ) + id + " ( cl " + getPathClause( node ) +
540-
conclusion + ") :rule resolution :premises ( causResLem" + id + " equiv" +
541-
identifier + "_a0) ) \n";
556+
proofRuleRes = String( "( step resLem" ) + id + " ( cl " +
557+
getNegatedSplitsClause( getPathSplits( node ) ) + conclusion +
558+
") :rule resolution :premises ( causResLem" + id + " equiv" + identifier +
559+
"_a0) ) \n";
542560
}
543561
// If lb of aux is positive, then ub of f is 0
544562
else if ( causingVar == aux && causingVarBound == Tightening::LB && affectedVar == f &&
545563
affectedVarBound == Tightening::UB && targetBound > 0 )
546564
{
547565
matched = true;
548566

549-
proofRuleRes = String( "( step resLem" ) + id + " ( cl " + getPathClause( node ) +
550-
conclusion + ") :rule resolution :premises ( causResLem" + id +
551-
" tautSplit" + id + " split" + identifier + "_a1 split" + identifier +
552-
" split" + identifier + "_i1 ) ) \n";
567+
proofRuleRes =
568+
String( "( step resLem" ) + id + " ( cl " + getNegatedSplitsClause( getPathSplits( node ) ) +
569+
conclusion + ") :rule resolution :premises ( causResLem" + id + " tautSplit" + id +
570+
" split" + identifier + "_a1 split" + identifier + " split" + identifier + "_i1 ) ) \n";
553571
}
554572

555573
// If ub of b is non positive, then ub of f is 0
@@ -558,37 +576,40 @@ List<String> AletheProofWriter::applyReluLemma( const UnsatCertificateNode *node
558576
{
559577
matched = true;
560578

561-
proofRuleRes = String( "( step resLem" ) + id + " ( cl " + getPathClause( node ) +
562-
conclusion + ") :rule resolution :premises ( causResLem" + id +
563-
" tautSplit" + id + " split" + identifier + "_a0 split" + identifier +
564-
" split" + identifier + "_i1 ) ) \n";
579+
proofRuleRes =
580+
String( "( step resLem" ) + id + " ( cl " + getNegatedSplitsClause( getPathSplits( node ) ) +
581+
conclusion + ") :rule resolution :premises ( causResLem" + id + " tautSplit" + id +
582+
" split" + identifier + "_a0 split" + identifier + " split" + identifier + "_i1 ) ) \n";
565583
}
566584
// Propagate 0 ub from f to b
567585
else if ( causingVar == f && causingVarBound == Tightening::UB && affectedVar == b &&
568586
affectedVarBound == Tightening::UB && targetBound == 0 )
569587
{
570588
matched = true;
571-
getPathClause( node ) + conclusion + proofRuleRes =
572-
String( "( step resLem" ) + id + " ( cl " +
573-
") :rule resolution :premises ( causResLem" + id + " equiv" + identifier + "_i1) ) \n";
589+
proofRuleRes = String( "( step resLem" ) + id + " ( cl " +
590+
getNegatedSplitsClause( getPathSplits( node ) ) + conclusion +
591+
") :rule resolution :premises ( causResLem" + id + " equiv" + identifier +
592+
"_i1) ) \n";
574593
}
575594
else if ( causingVar == b && causingVarBound == Tightening::UB && affectedVar == f &&
576595
affectedVarBound == Tightening::UB && targetBound == 0 )
577596
{
578597
matched = true;
579-
proofRuleRes = String( "( step resLem" ) + id + " ( cl " + getPathClause( node ) +
580-
conclusion + ") :rule resolution :premises ( causResLem" + id + " equiv" +
581-
identifier + "_i0) ) \n";
598+
proofRuleRes = String( "( step resLem" ) + id + " ( cl " +
599+
getNegatedSplitsClause( getPathSplits( node ) ) + conclusion +
600+
") :rule resolution :premises ( causResLem" + id + " equiv" + identifier +
601+
"_i0) ) \n";
582602
}
583603
// If ub of aux is 0, then lb of b is 0
584604
else if ( causingVar == aux && causingVarBound == Tightening::UB && affectedVar == b &&
585605
affectedVarBound == Tightening::LB && targetBound == 0 )
586606

587607
{
588608
matched = true;
589-
proofRuleRes = String( "( step resLem" ) + id + " ( cl " + getPathClause( node ) +
590-
conclusion + ") :rule resolution :premises ( causResLem" + id + " equiv" +
591-
identifier + "_a1) ) \n";
609+
proofRuleRes = String( "( step resLem" ) + id + " ( cl " +
610+
getNegatedSplitsClause( getPathSplits( node ) ) + conclusion +
611+
") :rule resolution :premises ( causResLem" + id + " equiv" + identifier +
612+
"_a1) ) \n";
592613
}
593614
// If lb of b is negative x, then ub of aux is -x
594615
else if ( causingVar == b && causingVarBound == Tightening::LB && affectedVar == aux &&
@@ -618,8 +639,9 @@ List<String> AletheProofWriter::applyReluLemma( const UnsatCertificateNode *node
618639
proofRule += String( "( step aFarkasLem" ) + id + " " + subFarkasClause +
619640
") :rule la_generic :args (1 1 -1 1 -1) )\n";
620641

621-
proofRuleRes += String( "( step resLem" ) + id + " ( cl " + getPathClause( node ) +
622-
conclusion + ") :rule resolution :premises ( causResLem" + id + " e" +
642+
proofRuleRes += String( "( step resLem" ) + id + " ( cl " +
643+
getNegatedSplitsClause( getPathSplits( node ) ) + conclusion +
644+
") :rule resolution :premises ( causResLem" + id + " e" +
623645
std::to_string( identifierInt - ( _n - _m ) ) + " l" + identifier +
624646
" aFarkasLem" + id + " tautSplit" + id + " split" + identifier +
625647
"_a1 split" + identifier + " split" + identifier + "_i1 ) ) \n";
@@ -652,8 +674,9 @@ List<String> AletheProofWriter::applyReluLemma( const UnsatCertificateNode *node
652674
proofRule += String( "( step aFarkasLem" ) + id + " " + subFarkasClause +
653675
") :rule la_generic :args (1 1 -1 1 1) )\n";
654676

655-
proofRuleRes += String( "( step resLem" ) + id + " ( cl " + getPathClause( node ) +
656-
conclusion + ") :rule resolution :premises ( causResLem" + id + " e" +
677+
proofRuleRes += String( "( step resLem" ) + id + " ( cl " +
678+
getNegatedSplitsClause( getPathSplits( node ) ) + conclusion +
679+
") :rule resolution :premises ( causResLem" + id + " e" +
657680
std::to_string( identifierInt - ( _n - _m ) ) + " u" + identifier +
658681
" aFarkasLem" + id + " tautSplit" + id + " split" + identifier +
659682
"_a1 split" + identifier + " split" + identifier + "_i1 ) ) \n";
@@ -679,7 +702,7 @@ List<String> AletheProofWriter::applyReluLemma( const UnsatCertificateNode *node
679702
}
680703

681704
void AletheProofWriter::linearCombinationMpq( const std::vector<mpq_t> &explainedRow,
682-
const SparseUnsortedList &expl )
705+
const SparseUnsortedList &expl ) const
683706
{
684707
SparseUnsortedList tableauRow( _n );
685708
for ( const auto &entry : expl )
@@ -789,7 +812,7 @@ void AletheProofWriter::farkasStrings( const SparseUnsortedList &expl,
789812
}
790813

791814

792-
String AletheProofWriter::convertTableauAssumptionToClause( unsigned index )
815+
String AletheProofWriter::convertTableauAssumptionToClause( unsigned index ) const
793816
{
794817
String assumption( _tableauAssumptions[index] );
795818
unsigned begin = assumption.find( "=" );
@@ -800,7 +823,7 @@ String AletheProofWriter::convertTableauAssumptionToClause( unsigned index )
800823
void AletheProofWriter::writeDelegatedLeaf( const UnsatCertificateNode *node )
801824
{
802825
String proofHole = String( "( step res" + std::to_string( node->getId() ) ) + " (cl " +
803-
getPathClause( node ) + ") :rule hole ) \n";
826+
getNegatedSplitsClause( getPathSplits( node ) ) + ") :rule hole ) \n";
804827
_proof.append( proofHole );
805828
}
806829

‎src/proofs/AletheProofWriter.h‎

Lines changed: 12 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -59,6 +59,8 @@ class AletheProofWriter
5959
unsigned _m;
6060
unsigned _stepCounter;
6161

62+
Map<unsigned, PiecewiseLinearConstraint *> _varToPLC;
63+
6264
void writeBoundAssumptions();
6365

6466
void writePLCAssumption();
@@ -76,22 +78,24 @@ class AletheProofWriter
7678

7779
void insertCurrentBoundsToVec( bool isUpper, Vector<double> &boundsVec );
7880

79-
String getPathClause( const UnsatCertificateNode *node );
81+
String getNegatedSplitsClause( const List<PiecewiseLinearCaseSplit> &splits ) const;
82+
83+
String getSplitsResSteps( const List<PiecewiseLinearCaseSplit> &splits )const;
8084

81-
String getPathResSteps( const UnsatCertificateNode *node );
85+
List<PiecewiseLinearCaseSplit> getPathSplits( const UnsatCertificateNode *node )const;
8286

83-
String getSplitsAsClause( const List<PiecewiseLinearCaseSplit> &splits );
87+
String getSplitsAsClause( const List<PiecewiseLinearCaseSplit> &splits )const;
8488

85-
String getSplitAsClause( const PiecewiseLinearCaseSplit &splits );
89+
String getSplitAsClause( const PiecewiseLinearCaseSplit &split ) const;
8690

87-
String getBoundAsClause( const Tightening &bound );
91+
String getBoundAsClause( const Tightening &bound ) const;
8892

89-
String convertTableauAssumptionToClause( unsigned index );
93+
String convertTableauAssumptionToClause( unsigned index ) const;
9094

91-
bool isSplitActive( const PiecewiseLinearCaseSplit &split );
95+
bool isSplitActive( const PiecewiseLinearCaseSplit &split )const ;
9296

9397
void linearCombinationMpq( const std::vector<mpq_t> &explainedRow,
94-
const SparseUnsortedList &expl );
98+
const SparseUnsortedList &expl )const ;
9599

96100
void farkasStrings( const SparseUnsortedList &expl,
97101
String &farkasArgs,

0 commit comments

Comments
 (0)