Skip to content

Apply simplification to Imp and Iff connectives #4533

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.

Sign up for GitHub

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

Merged
merged 37 commits into from
Apr 2, 2024
Merged

Apply simplification to Imp and Iff connectives #4533

Show file tree
Hide file tree
Changes from 32 commits
Commits
Show all changes
37 commits
Select commit Hold shift + click to select a range
4235832
Optimize uses clauses added by Translator.cs
zafer-esen Aug 16, 2023
7ac0fbe
Add trigger to an axiom that was incorrectly being pruned away.
zafer-esen Aug 16, 2023
943ade9
Revert change in Translator for Boogie compatibility.
zafer-esen Aug 16, 2023
b52e014
Update integration tests. Minor changes in the prelude.
zafer-esen Aug 17, 2023
99a24cc
Simplify certain formulas with literals.
zafer-esen Aug 21, 2023
0f76db6
Fixes some issues introduced during merge with upstream.
zafer-esen Sep 8, 2023
81ce40e
Fixes another issue introduced during merge.
zafer-esen Sep 8, 2023
1224fd2
Simplify F in BplAnd.
zafer-esen Sep 8, 2023
80bde0a
Make BplIff static.
zafer-esen Sep 8, 2023
09dcb06
Merge branch 'master' into simplify-imp-iff
zafer-esen Sep 8, 2023
ec7b088
Adds a few more and replacements.
zafer-esen Sep 8, 2023
56ebbf7
Merge branch 'master' into simplify-imp-iff
zafer-esen Sep 11, 2023
7234e99
More simplification for BplIff
zafer-esen Sep 11, 2023
4228f5c
Merge branch 'master' into simplify-imp-iff
zafer-esen Sep 25, 2023
4dc1c0e
Consider Lit when simplifying and update expected test results.
zafer-esen Sep 25, 2023
4ffe6d0
Merge remote-tracking branch 'upstream/master' into simplify-imp-iff
atomb Nov 8, 2023
bd17def
Merge branch 'master' into simplify-imp-iff
atomb Nov 15, 2023
915c68e
Merge remote-tracking branch 'upstream/master' into simplify-imp-iff
atomb Jan 31, 2024
1ce4aeb
Fix overzealous conversion to BplImp, BplAnd
atomb Jan 31, 2024
85f0ee1
Fix some expected test outputs
atomb Jan 31, 2024
493b912
Get one more test to pass
atomb Feb 1, 2024
33b2b97
Fix misunderstanding of for-each-compiler
atomb Feb 1, 2024
30677dd
Make dafny4/gcd.dfy less brittle
atomb Feb 1, 2024
3289695
Make VSComp2010/Problem2-Invert.dfy less brittle
atomb Feb 1, 2024
082e19a
Merge remote-tracking branch 'upstream/master' into simplify-imp-iff
atomb Feb 9, 2024
2d973cf
Fix tests
atomb Feb 10, 2024
77443c1
Merge remote-tracking branch 'upstream/master' into simplify-imp-iff
atomb Feb 10, 2024
16b77c2
Merge branch 'master' into simplify-imp-iff
atomb Mar 28, 2024
e6bda87
Merge remote-tracking branch 'upstream/master' into simplify-imp-iff
atomb Mar 29, 2024
fad1c8d
Fix CI
atomb Mar 29, 2024
b08ffef
One more test fix
atomb Apr 1, 2024
0c3c0a3
Merge remote-tracking branch 'upstream/master' into simplify-imp-iff
atomb Apr 1, 2024
9ed2257
Remove unneeded resource limit increase
atomb Apr 2, 2024
e7ee237
Merge branch 'master' into simplify-imp-iff
atomb Apr 2, 2024
2b769f9
Rebuild standard libraries
atomb Apr 2, 2024
08daf27
Merge remote-tracking branch 'upstream/master' into simplify-imp-iff
atomb Apr 2, 2024
e53ed77
Update expected test output
atomb Apr 2, 2024
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
46 changes: 36 additions & 10 deletions Source/DafnyCore/Verifier/BoogieGenerator.BoogieFactory.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -628,7 +628,7 @@ public Bpl.Expr ProperPrefix(Bpl.IToken tok, Bpl.Expr e0, Bpl.Expr e1) {
Contract.Ensures(Contract.Result<Bpl.Expr>() != null);
Bpl.Expr len0 = FunctionCall(tok, BuiltinFunction.SeqLength, null, e0);
Bpl.Expr len1 = FunctionCall(tok, BuiltinFunction.SeqLength, null, e1);
var result = Bpl.Expr.And(
var result = BplAnd(
Bpl.Expr.Lt(len0, len1),
FunctionCall(tok, BuiltinFunction.SeqSameUntil, null, e0, e1, len0));
result.tok = tok;
Expand Down Expand Up @@ -698,10 +698,15 @@ static Bpl.Expr BplAnd(Bpl.Expr a, Bpl.Expr b) {
Contract.Requires(b != null);
Contract.Ensures(Contract.Result<Bpl.Expr>() != null);

if (a == Bpl.Expr.True) {
var aNoLit = RemoveLit(a);
var bNoLit = RemoveLit(b);

if (aNoLit == Bpl.Expr.True) {
return b;
} else if (b == Bpl.Expr.True) {
} else if (bNoLit == Bpl.Expr.True) {
return a;
} else if (aNoLit == Bpl.Expr.False || bNoLit == Bpl.Expr.False) {
return Bpl.Expr.False;
} else {
return Bpl.Expr.Binary(a.tok, Bpl.BinaryOperator.Opcode.And, a, b);
}
Expand All @@ -721,24 +726,42 @@ static Bpl.Expr BplOr(Bpl.Expr a, Bpl.Expr b) {
Contract.Requires(b != null);
Contract.Ensures(Contract.Result<Bpl.Expr>() != null);

if (a == Bpl.Expr.False) {
var aNoLit = RemoveLit(a);
var bNoLit = RemoveLit(b);

if (aNoLit == Bpl.Expr.False) {
return b;
} else if (b == Bpl.Expr.False) {
} else if (bNoLit == Bpl.Expr.False) {
return a;
} else if (aNoLit == Bpl.Expr.True) {
return a;
} else if (bNoLit == Bpl.Expr.True) {
return b;
} else {
return Bpl.Expr.Binary(a.tok, Bpl.BinaryOperator.Opcode.Or, a, b);
}
}

Bpl.Expr BplIff(Bpl.Expr a, Bpl.Expr b) {
static Bpl.Expr BplIff(Bpl.Expr a, Bpl.Expr b) {
Contract.Requires(a != null);
Contract.Requires(b != null);
Contract.Ensures(Contract.Result<Bpl.Expr>() != null);

if (a == Bpl.Expr.True) {
var aNoLit = RemoveLit(a);
var bNoLit = RemoveLit(b);

if (aNoLit == Bpl.Expr.True) {
return b;
} else if (b == Bpl.Expr.True) {
} else if (bNoLit == Bpl.Expr.True) {
return a;
} else if (aNoLit == Bpl.Expr.False) {
return Bpl.Expr.Not(b);
} else if (bNoLit == Bpl.Expr.False) {
return Bpl.Expr.Not(a);
} else if (aNoLit == bNoLit) {
return Bpl.Expr.True;
} else if (aNoLit == Bpl.Expr.Not(b) || bNoLit == Bpl.Expr.Not(a)) {
return Bpl.Expr.False;
} else {
return Bpl.Expr.Iff(a, b);
}
Expand All @@ -749,9 +772,12 @@ static Bpl.Expr BplImp(Bpl.Expr a, Bpl.Expr b) {
Contract.Requires(b != null);
Contract.Ensures(Contract.Result<Bpl.Expr>() != null);

if (a == Bpl.Expr.True || b == Bpl.Expr.True) {
var aNoLit = RemoveLit(a);
var bNoLit = RemoveLit(b);

if (aNoLit == Bpl.Expr.True || bNoLit == Bpl.Expr.True) {
return b;
} else if (a == Bpl.Expr.False) {
} else if (aNoLit == Bpl.Expr.False) {
return Bpl.Expr.True;
} else {
return Bpl.Expr.Imp(a, b);
Expand Down
20 changes: 10 additions & 10 deletions Source/DafnyCore/Verifier/BoogieGenerator.DataTypes.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,7 +43,7 @@ void AddDatatype(DatatypeDecl dt) {
cases_body = BplOr(cases_body, disj);
tr = new Bpl.Trigger(ctor.tok, true, new List<Bpl.Expr> { disj, isPredicate }, tr);
}
var body = Bpl.Expr.Imp(isPredicate, cases_body);
var body = BplImp(isPredicate, cases_body);
var ax = BplForall(boundVariables, tr, body);
var axiom = new Bpl.Axiom(dt.tok, ax, "Questionmark data type disjunctivity");
sink.AddTopLevelDeclaration(axiom);
Expand Down Expand Up @@ -124,7 +124,7 @@ private void AddInductiveDatatypeAxioms(Dictionary<DatatypeCtor, Bpl.Function> c
eqs = BplAnd(eqs, eq);
}

var ax = BplForall(new List<Variable> { aVar, bVar }, trigger, Bpl.Expr.Imp(ante, Bpl.Expr.Iff(dtEqual, eqs)));
var ax = BplForall(new List<Variable> { aVar, bVar }, trigger, BplImp(ante, BplIff(dtEqual, eqs)));
AddOtherDefinition(constructorFunctions[ctor], new Bpl.Axiom(dt.tok, ax, $"Datatype extensional equality definition: {ctor.FullName}"));
}
}
Expand All @@ -143,7 +143,7 @@ private void AddExtensionalityAxiom(IndDatatypeDecl dt) {
var lhs = FunctionCall(dt.tok, dtEqualName, Bpl.Type.Bool, a, b);
var rhs = Bpl.Expr.Eq(a, b);

var ax = BplForall(new List<Variable> { aVar, bVar }, BplTrigger(lhs), Bpl.Expr.Iff(lhs, rhs));
var ax = BplForall(new List<Variable> { aVar, bVar }, BplTrigger(lhs), BplIff(lhs, rhs));
sink.AddTopLevelDeclaration(new Bpl.Axiom(dt.tok, ax, $"Datatype extensionality axiom: {dt.FullName}"));
}
}
Expand Down Expand Up @@ -423,7 +423,7 @@ private Bpl.Function AddDataTypeConstructor(DatatypeDecl dt, DatatypeCtor ctor,
var queryPredicate = FunctionCall(ctor.tok, queryField.Name, Bpl.Type.Bool, th);
var ctorId = FunctionCall(ctor.tok, BuiltinFunction.DatatypeCtorId, null, th);
var rhs = Bpl.Expr.Eq(ctorId, constructorIdReference);
var body = Bpl.Expr.Iff(queryPredicate, rhs);
var body = BplIff(queryPredicate, rhs);
var tr = BplTrigger(queryPredicate);
var ax = BplForall(thVar, tr, body);
sink.AddTopLevelDeclaration(new Bpl.Axiom(ctor.tok, ax, "Questionmark and identifier"));
Expand Down Expand Up @@ -517,7 +517,7 @@ private Bpl.Function AddDataTypeConstructor(DatatypeDecl dt, DatatypeCtor ctor,
Bpl.Variable iVar = new Bpl.BoundVariable(arg.tok, new Bpl.TypedIdent(arg.tok, "i", Bpl.Type.Int));
bvs.Add(iVar);
Bpl.IdentifierExpr ie = new Bpl.IdentifierExpr(arg.tok, iVar);
Bpl.Expr ante = Bpl.Expr.And(
Bpl.Expr ante = BplAnd(
Bpl.Expr.Le(Bpl.Expr.Literal(0), ie),
Bpl.Expr.Lt(ie, FunctionCall(arg.tok, BuiltinFunction.SeqLength, null, args[i])));
var seqIndex = FunctionCall(arg.tok, BuiltinFunction.SeqIndex, predef.DatatypeType, args[i], ie);
Expand All @@ -526,7 +526,7 @@ private Bpl.Function AddDataTypeConstructor(DatatypeDecl dt, DatatypeCtor ctor,
var ct = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);
var rhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, ct);
q = new Bpl.ForallExpr(ctor.tok, bvs, new Trigger(lhs.tok, true, new List<Bpl.Expr> { seqIndex, ct }),
Bpl.Expr.Imp(ante, Bpl.Expr.Lt(lhs, rhs)));
BplImp(ante, Bpl.Expr.Lt(lhs, rhs)));
sink.AddTopLevelDeclaration(new Bpl.Axiom(ctor.tok, q, "Inductive seq element rank"));
}

Expand All @@ -553,7 +553,7 @@ private Bpl.Function AddDataTypeConstructor(DatatypeDecl dt, DatatypeCtor ctor,
var ct = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);
var rhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, ct);
var trigger = new Bpl.Trigger(ctor.tok, true, new List<Bpl.Expr> { inSet, ct });
q = new Bpl.ForallExpr(ctor.tok, bvs, trigger, Bpl.Expr.Imp(inSet, Bpl.Expr.Lt(lhs, rhs)));
q = new Bpl.ForallExpr(ctor.tok, bvs, trigger, BplImp(inSet, Bpl.Expr.Lt(lhs, rhs)));
sink.AddTopLevelDeclaration(new Bpl.Axiom(ctor.tok, q, "Inductive set element rank"));
} else if (argType is MultiSetType) {
// axiom (forall params, d: Datatype {arg[d], #dt.ctor(params)} :: 0 < arg[d] ==> DtRank(d) < DtRank(#dt.ctor(params)));
Expand All @@ -569,7 +569,7 @@ private Bpl.Function AddDataTypeConstructor(DatatypeDecl dt, DatatypeCtor ctor,
var ct = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);
var rhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, ct);
var trigger = new Bpl.Trigger(ctor.tok, true, new List<Bpl.Expr> { inMultiset, ct });
q = new Bpl.ForallExpr(ctor.tok, bvs, trigger, Bpl.Expr.Imp(ante, Bpl.Expr.Lt(lhs, rhs)));
q = new Bpl.ForallExpr(ctor.tok, bvs, trigger, BplImp(ante, Bpl.Expr.Lt(lhs, rhs)));
sink.AddTopLevelDeclaration(new Bpl.Axiom(ctor.tok, q, "Inductive multiset element rank"));
} else if (argType is MapType) {
var finite = ((MapType)argType).Finite;
Expand All @@ -589,7 +589,7 @@ private Bpl.Function AddDataTypeConstructor(DatatypeDecl dt, DatatypeCtor ctor,
var ct = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);
var rhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, ct);
var trigger = new Bpl.Trigger(ctor.tok, true, new List<Bpl.Expr> { inDomain, ct });
q = new Bpl.ForallExpr(ctor.tok, bvs, trigger, Bpl.Expr.Imp(inDomain, Bpl.Expr.Lt(lhs, rhs)));
q = new Bpl.ForallExpr(ctor.tok, bvs, trigger, BplImp(inDomain, Bpl.Expr.Lt(lhs, rhs)));
sink.AddTopLevelDeclaration(new Bpl.Axiom(ctor.tok, q, "Inductive map key rank"));
}
{
Expand All @@ -613,7 +613,7 @@ private Bpl.Function AddDataTypeConstructor(DatatypeDecl dt, DatatypeCtor ctor,
var ct = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);
var rhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, ct);
var trigger = new Bpl.Trigger(ctor.tok, true, new List<Bpl.Expr> { inDomain, ct });
q = new Bpl.ForallExpr(ctor.tok, bvs, trigger, Bpl.Expr.Imp(inDomain, Bpl.Expr.Lt(lhs, rhs)));
q = new Bpl.ForallExpr(ctor.tok, bvs, trigger, BplImp(inDomain, Bpl.Expr.Lt(lhs, rhs)));
sink.AddTopLevelDeclaration(new Bpl.Axiom(ctor.tok, q, "Inductive map value rank"));
}
}
Expand Down
32 changes: 16 additions & 16 deletions Source/DafnyCore/Verifier/BoogieGenerator.Decreases.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -82,7 +82,7 @@ void CheckCallTermination(IToken tok, List<Expression> contextDecreases, List<Ex
bool endsWithWinningTopComparison = N == contextDecreases.Count && N < calleeDecreases.Count;
Bpl.Expr decrExpr = DecreasesCheck(toks, types0, types1, callee, caller, builder, "", endsWithWinningTopComparison, false);
if (allowance != null) {
decrExpr = Bpl.Expr.Or(allowance, decrExpr);
decrExpr = BplOr(allowance, decrExpr);
}
builder.Add(Assert(tok, decrExpr, new PODesc.Terminates(inferredDecreases, false, hint)));
}
Expand Down Expand Up @@ -125,7 +125,7 @@ Bpl.Expr DecreasesCheck(List<IToken> toks, List<Type> types0, List<Type> types1,
// we only need to check lower bound for integers--sets, sequences, booleans, references, and datatypes all have natural lower bounds
Bpl.Expr prefixIsLess = Bpl.Expr.False;
for (int i = 0; i < k; i++) {
prefixIsLess = Bpl.Expr.Or(prefixIsLess, Less[i]);
prefixIsLess = BplOr(prefixIsLess, Less[i]);
};

Bpl.Expr zero = null;
Expand All @@ -140,9 +140,9 @@ Bpl.Expr DecreasesCheck(List<IToken> toks, List<Type> types0, List<Type> types1,
if (zero != null) {
Bpl.Expr bounded = Bpl.Expr.Le(zero, ee1[k]);
for (int i = 0; i < k; i++) {
bounded = Bpl.Expr.Or(bounded, Less[i]);
bounded = BplOr(bounded, Less[i]);
}
Bpl.Cmd cmd = Assert(toks[k], Bpl.Expr.Or(bounded, Eq[k]), new PODesc.DecreasesBoundedBelow(N, k, zeroStr, suffixMsg));
Bpl.Cmd cmd = Assert(toks[k], BplOr(bounded, Eq[k]), new PODesc.DecreasesBoundedBelow(N, k, zeroStr, suffixMsg));
builder.Add(cmd);
}
}
Expand All @@ -154,10 +154,10 @@ Bpl.Expr DecreasesCheck(List<IToken> toks, List<Type> types0, List<Type> types1,
Bpl.Expr eq = Eq[i];
if (allowNoChange) {
// decrCheck = atmost && (eq ==> decrCheck)
decrCheck = Bpl.Expr.And(less, Bpl.Expr.Imp(eq, decrCheck));
decrCheck = BplAnd(less, BplImp(eq, decrCheck));
} else {
// decrCheck = less || (eq && decrCheck)
decrCheck = Bpl.Expr.Or(less, Bpl.Expr.And(eq, decrCheck));
decrCheck = BplOr(less, BplAnd(eq, decrCheck));
}
}
return decrCheck;
Expand Down Expand Up @@ -236,9 +236,9 @@ void ComputeLessEq(IToken tok, Type ty0, Type ty1, Bpl.Expr e0, Bpl.Expr e1, out
less = Bpl.Expr.Lt(b0, b1);
atmost = Bpl.Expr.Le(b0, b1);
} else if (ty0 is BoolType) {
eq = Bpl.Expr.Iff(e0, e1);
less = Bpl.Expr.And(Bpl.Expr.Not(e0), e1);
atmost = Bpl.Expr.Imp(e0, e1);
eq = BplIff(e0, e1);
less = BplAnd(Bpl.Expr.Not(e0), e1);
atmost = BplImp(e0, e1);
} else if (ty0 is CharType) {
eq = Bpl.Expr.Eq(e0, e1);
var operand0 = FunctionCall(e0.tok, BuiltinFunction.CharToInt, null, e0);
Expand All @@ -263,17 +263,17 @@ void ComputeLessEq(IToken tok, Type ty0, Type ty1, Bpl.Expr e0, Bpl.Expr e1, out
less = Bpl.Expr.Lt(b0, b1);
atmost = Bpl.Expr.Le(b0, b1);
if (ty0.IsNumericBased(Type.NumericPersuasion.Int) && includeLowerBound) {
less = Bpl.Expr.And(Bpl.Expr.Le(Bpl.Expr.Literal(0), b0), less);
atmost = Bpl.Expr.And(Bpl.Expr.Le(Bpl.Expr.Literal(0), b0), atmost);
less = BplAnd(Bpl.Expr.Le(Bpl.Expr.Literal(0), b0), less);
atmost = BplAnd(Bpl.Expr.Le(Bpl.Expr.Literal(0), b0), atmost);
}

} else if (ty0.IsNumericBased(Type.NumericPersuasion.Real)) {
eq = Bpl.Expr.Eq(e0, e1);
less = Bpl.Expr.Le(e0, Bpl.Expr.Sub(e1, Bpl.Expr.Literal(BaseTypes.BigDec.FromInt(1))));
atmost = Bpl.Expr.Le(e0, e1);
if (includeLowerBound) {
less = Bpl.Expr.And(Bpl.Expr.Le(Bpl.Expr.Literal(BaseTypes.BigDec.ZERO), e0), less);
atmost = Bpl.Expr.And(Bpl.Expr.Le(Bpl.Expr.Literal(BaseTypes.BigDec.ZERO), e0), atmost);
less = BplAnd(Bpl.Expr.Le(Bpl.Expr.Literal(BaseTypes.BigDec.ZERO), e0), less);
atmost = BplAnd(Bpl.Expr.Le(Bpl.Expr.Literal(BaseTypes.BigDec.ZERO), e0), atmost);
}

} else if (ty0 is IteratorDecl.EverIncreasingType) {
Expand Down Expand Up @@ -342,9 +342,9 @@ void ComputeLessEq(IToken tok, Type ty0, Type ty1, Bpl.Expr e0, Bpl.Expr e1, out
Contract.Assert(ty0.IsRefType); // otherwise, unexpected type
var b0 = Bpl.Expr.Neq(e0, predef.Null);
var b1 = Bpl.Expr.Neq(e1, predef.Null);
eq = Bpl.Expr.Iff(b0, b1);
less = Bpl.Expr.And(Bpl.Expr.Not(b0), b1);
atmost = Bpl.Expr.Imp(b0, b1);
eq = BplIff(b0, b1);
less = BplAnd(Bpl.Expr.Not(b0), b1);
atmost = BplImp(b0, b1);
}
}
}
Loading