From 96861beb1b7d47bc0b940ff83d5a721d5e67d924 Mon Sep 17 00:00:00 2001 From: wuestholz Date: Fri, 2 Jan 2015 22:54:49 +0100 Subject: Minor changes --- Source/Core/AbsyCmd.cs | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) (limited to 'Source/Core/AbsyCmd.cs') diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index 746e70c0..900d1c7a 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -2640,18 +2640,21 @@ namespace Microsoft.Boogie { Substitution substOldCombined = v => { Expr s; if (oldSubst.TryGetValue(v, out s)) { return s; } return calleeSubstitutionOld(v); }; var clauses = procedure.Ensures.Select(e => Substituter.FunctionCallReresolvingApplyReplacingOldExprs(calleeSubstitution, substOldCombined, e.Condition, program)).Concat(modifies); - var conj = Conjunction(clauses); // TODO(wuestholz): Try extracting a function for each clause: - // var conj = Conjunction(clauses.Select(c => extract(c))); + // return Conjunction(clauses.Select(c => extract(c))); + var conj = Conjunction(clauses); return conj != null ? extract(conj) : conj; } - public Expr CheckedPrecondition(Procedure procedure, Program program) + public Expr CheckedPrecondition(Procedure procedure, Program program, Func extract) { - Contract.Requires(calleeSubstitution != null && calleeSubstitutionOld != null && program != null); + Contract.Requires(calleeSubstitution != null && calleeSubstitutionOld != null && program != null && extract != null); - var requires = procedure.Requires.Where(r => !r.Free).Select(r => Substituter.FunctionCallReresolvingApplyReplacingOldExprs(calleeSubstitution, calleeSubstitutionOld, r.Condition, program)); - return Conjunction(requires); + var clauses = procedure.Requires.Where(r => !r.Free).Select(r => Substituter.FunctionCallReresolvingApplyReplacingOldExprs(calleeSubstitution, calleeSubstitutionOld, r.Condition, program)); + // TODO(wuestholz): Try extracting a function for each clause: + // return Conjunction(clauses.Select(c => extract(c))); + var conj = Conjunction(clauses); + return conj != null ? extract(conj) : conj; } private static Expr Conjunction(IEnumerable conjuncts) -- cgit v1.2.3