Skip to content

Commit a7e2f78

Browse files
denis-bogdanasdenis-bogdanas
authored
Java Backend logging: log cases of ConjunctiveFormula evaluating to false, for final implication and spec rule application. (runtimeverification#851)
1 parent 4497aa7 commit a7e2f78

1 file changed

Lines changed: 40 additions & 21 deletions

File tree

‎java-backend/src/main/java/org/kframework/backend/java/symbolic/ConjunctiveFormula.java‎

Lines changed: 40 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -271,7 +271,8 @@ public ConjunctiveFormula unsafeAddVariableBinding(Variable variable, Term term)
271271
} else if (previousTerm.equals(term)) {
272272
return this;
273273
} else {
274-
return falsify(substitution, equalities, disjunctions, new Equality(previousTerm, term, global));
274+
Equality debugEquality = new Equality(previousTerm, term, global);
275+
return falsify(substitution, equalities, disjunctions, debugEquality, debugEquality, false);
275276
}
276277
}
277278

@@ -386,15 +387,15 @@ public ConjunctiveFormula retainSubstitutionVars(Set<Variable> variablesToRetain
386387
}
387388

388389
public ConjunctiveFormula simplify() {
389-
return simplify(false, true, TermContext.builder(global).build(), Collections.emptySet(), false);
390+
return simplify(false, true, TermContext.builder(global).build(), Collections.emptySet(), false, false);
390391
}
391392

392393
/**
393394
* Simplifies this conjunctive formula as much as possible.
394395
* Decomposes equalities by using unification.
395396
*/
396397
public ConjunctiveFormula simplify(TermContext context) {
397-
return simplify(false, true, context, Collections.emptySet(), false);
398+
return simplify(false, true, context, Collections.emptySet(), false, false);
398399
}
399400

400401
/**
@@ -404,11 +405,13 @@ public ConjunctiveFormula simplify(TermContext context) {
404405
*/
405406
public ConjunctiveFormula simplifyBeforePatternFolding(TermContext context, Set<Variable> rhsOnlyVariables,
406407
boolean logFailures) {
407-
return simplify(false, false, context, rhsOnlyVariables, logFailures);
408+
return simplify(false, false, context, rhsOnlyVariables, logFailures,
409+
logFailures || global.javaExecutionOptions.logImplications);
408410
}
409411

410412
public ConjunctiveFormula simplifyModuloPatternFolding(TermContext context, Set<Variable> rhsOnlyVariables) {
411-
return simplify(true, true, context, rhsOnlyVariables, false);
413+
return simplify(true, true, context, rhsOnlyVariables, false,
414+
global.javaExecutionOptions.logImplications);
412415
}
413416

414417
/**
@@ -421,24 +424,27 @@ public ConjunctiveFormula simplifyModuloPatternFolding(TermContext context, Set<
421424
* @param rhsOnlyVariables When generating substitutions, substitutions for these vars will be preferred. A
422425
* wrong/empty set here won't affect soundness but will affect completeness.
423426
* @param logFailures
427+
* @param logFormulaFalsify
424428
* @return
425429
*/
426430
private ConjunctiveFormula simplify(boolean patternFolding, boolean partialSimplification,
427-
TermContext context, Set<Variable> rhsOnlyVariables, boolean logFailures) {
431+
TermContext context, Set<Variable> rhsOnlyVariables, boolean logFailures,
432+
boolean logFormulaFalsify) {
428433
ConjunctiveFormula cachedResult = global.formulaCache
429434
.cacheGet(this, patternFolding, partialSimplification, rhsOnlyVariables, context);
430435
if (cachedResult != null) {
431436
return cachedResult;
432437
}
433438

434439
ConjunctiveFormula result = simplifyImpl(patternFolding, partialSimplification, context, rhsOnlyVariables,
435-
logFailures);
440+
logFailures, logFormulaFalsify);
436441
global.formulaCache.cachePut(this, patternFolding, partialSimplification, context, rhsOnlyVariables, result);
437442
return result;
438443
}
439444

440445
private ConjunctiveFormula simplifyImpl(boolean patternFolding, boolean partialSimplification, TermContext context,
441-
Set<Variable> rhsOnlyVariables, boolean logFailures) {
446+
Set<Variable> rhsOnlyVariables, boolean logFailures,
447+
boolean logFormulaFalsify) {
442448
assert !isFalse();
443449
ConjunctiveFormula originalTopConstraint = context.getTopConstraint();
444450
Substitution<Variable, Term> substitution = this.substitution;
@@ -459,15 +465,16 @@ private ConjunctiveFormula simplifyImpl(boolean patternFolding, boolean partialS
459465
//loss can happen. Details: https://github.com/kframework/k-legacy/pull/2399#issuecomment-360680618
460466
context.setTopConstraint(minus(originalTopConstraint, equality));
461467

462-
Term leftHandSide = equality.leftHandSide().substituteAndEvaluate(substitution, context);
463-
Term rightHandSide = equality.rightHandSide().substituteAndEvaluate(substitution, context);
468+
Equality oldEquality = equality; //for debug
469+
Term leftHandSide = oldEquality.leftHandSide().substituteAndEvaluate(substitution, context);
470+
Term rightHandSide = oldEquality.rightHandSide().substituteAndEvaluate(substitution, context);
464471
equality = new Equality(leftHandSide, rightHandSide, global);
465472
//noinspection StatementWithEmptyBody
466473
if (equality.isTrue()) {
467474
// delete
468475
} else if (equality.truthValue() == TruthValue.FALSE) {
469476
// conflict
470-
return falsify(substitution, equalities, disjunctions, equality);
477+
return falsify(substitution, equalities, disjunctions, equality, oldEquality, logFormulaFalsify);
471478
} else if (equality.isSimplifiableByCurrentAlgorithm()) {
472479
// (decompose + conflict)*
473480
FastRuleMatcher unifier = new FastRuleMatcher(global, 1);
@@ -479,7 +486,7 @@ private ConjunctiveFormula simplifyImpl(boolean patternFolding, boolean partialS
479486
new Equality(
480487
unifier.unificationFailureLeftHandSide(),
481488
unifier.unificationFailureRightHandSide(),
482-
global));
489+
global), equality, logFormulaFalsify);
483490
}
484491

485492
// TODO(AndreiS): fix this in a general way
@@ -494,7 +501,7 @@ private ConjunctiveFormula simplifyImpl(boolean patternFolding, boolean partialS
494501

495502
} else if (varToNormalTermNonSubstitutable(leftHandSide, rightHandSide)
496503
|| varToNormalTermNonSubstitutable(rightHandSide, leftHandSide)) {
497-
return falsify(substitution, equalities, disjunctions, equality);
504+
return falsify(substitution, equalities, disjunctions, equality, oldEquality, logFormulaFalsify);
498505
} else { //Attempt to replace equality by substitution, RHS to LHS only
499506
ImmutableMapSubstitution<Variable, Term> newVarSubstitution =
500507
getSubstitutionIfPossibleUnoriented(leftHandSide, rightHandSide, rhsOnlyVariables);
@@ -504,7 +511,8 @@ private ConjunctiveFormula simplifyImpl(boolean patternFolding, boolean partialS
504511
context);
505512
change = true;
506513
if (substitution.isFalse(global)) {
507-
return falsify(substitution, equalities, disjunctions, equality);
514+
return falsify(substitution, equalities, disjunctions, equality, null,
515+
logFormulaFalsify);
508516
}
509517
} else {
510518
pendingEqualities = pendingEqualities.plus(equality);
@@ -537,7 +545,8 @@ private ConjunctiveFormula simplifyImpl(boolean patternFolding, boolean partialS
537545
context);
538546
change = true;
539547
if (substitution.isFalse(global)) {
540-
return falsify(substitution, equalities, disjunctions, equality);
548+
return falsify(substitution, equalities, disjunctions, equality, null,
549+
logFormulaFalsify);
541550
}
542551
} else {
543552
pendingEqualities = pendingEqualities.plus(equality);
@@ -557,12 +566,8 @@ private ConjunctiveFormula falsify(
557566
Substitution<Variable, Term> substitution,
558567
PersistentUniqueList<Equality> equalities,
559568
PersistentUniqueList<DisjunctiveFormula> disjunctions,
560-
Equality equality) {
561-
if ((RuleAuditing.isAuditBegun() || global.javaExecutionOptions.debugZ3)
562-
&& !(equality.leftHandSide() instanceof BoolToken && equality.rightHandSide() instanceof BoolToken)) {
563-
global.log().format("Unification failure: %s does not unify with %s\n",
564-
equality.leftHandSide(), equality.rightHandSide());
565-
}
569+
Equality equality, Equality oldEquality, boolean logFormulaFalsify) {
570+
logFalsify(substitution, equalities, disjunctions, equality, oldEquality, logFormulaFalsify);
566571
return new ConjunctiveFormula(
567572
substitution,
568573
equalities,
@@ -572,6 +577,20 @@ private ConjunctiveFormula falsify(
572577
global);
573578
}
574579

580+
private void logFalsify(Substitution<Variable, Term> substitution, PersistentUniqueList<Equality> equalities,
581+
PersistentUniqueList<DisjunctiveFormula> disjunctions,
582+
Equality equality, Equality oldEquality, boolean logFormulaFalsify) {
583+
if (logFormulaFalsify || RuleAuditing.isAuditBegun()) {
584+
Substitution<Variable, Term> debugSubstitution = oldEquality != null
585+
? substitution.retainAll(
586+
Sets.union(oldEquality.leftHandSide().variableSet(),
587+
oldEquality.rightHandSide().variableSet()))
588+
: substitution;
589+
global.log().format("Unification failure: %s\nOld Equality: %s\nRelevant substitution: %s\n",
590+
equality, oldEquality, debugSubstitution);
591+
}
592+
}
593+
575594
/**
576595
* Apply projection lemmas over equalities:
577596
* proj(X,0,N) == proj(Y,0,N) /\ ... /\ proj(X,N-1,N) == proj(Y,N-1,N)

0 commit comments

Comments
 (0)