diff options
Diffstat (limited to 'Source/Provers/SMTLib/SMTLibLineariser.cs')
-rw-r--r-- | Source/Provers/SMTLib/SMTLibLineariser.cs | 22 |
1 files changed, 20 insertions, 2 deletions
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index de8798b8..6df44c2f 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -34,7 +34,7 @@ namespace Microsoft.Boogie.SMTLib public class SMTLibExprLineariser : IVCExprVisitor<bool, LineariserOptions/*!*/> { - public static string ToString(VCExpr e, UniqueNamer namer, SMTLibProverOptions opts, IList<string> optReqs = null) + public static string ToString(VCExpr e, UniqueNamer namer, SMTLibProverOptions opts, ref bool containsNamedAssumes, IList<string> optReqs = null) { Contract.Requires(e != null); Contract.Requires(namer != null); @@ -44,6 +44,7 @@ namespace Microsoft.Boogie.SMTLib SMTLibExprLineariser lin = new SMTLibExprLineariser(sw, namer, opts, optReqs); Contract.Assert(lin != null); lin.Linearise(e, LineariserOptions.Default); + containsNamedAssumes |= lin.ContainsNamedAssumes; return cce.NonNull(sw.ToString()); } @@ -76,6 +77,12 @@ namespace Microsoft.Boogie.SMTLib readonly IList<string> OptimizationRequests; + bool containsNamedAssumes; + public bool ContainsNamedAssumes + { + get { return containsNamedAssumes; } + } + public SMTLibExprLineariser(TextWriter wr, UniqueNamer namer, SMTLibProverOptions opts, IList<string> optReqs = null) { Contract.Requires(wr != null); Contract.Requires(namer != null); @@ -270,7 +277,18 @@ namespace Microsoft.Boogie.SMTLib && (node.Op.Equals(VCExpressionGenerator.MinimizeOp) || node.Op.Equals(VCExpressionGenerator.MaximizeOp))) { string optOp = node.Op.Equals(VCExpressionGenerator.MinimizeOp) ? "minimize" : "maximize"; - OptimizationRequests.Add(string.Format("({0} {1})", optOp, ToString(node[0], Namer, ProverOptions))); + OptimizationRequests.Add(string.Format("({0} {1})", optOp, ToString(node[0], Namer, ProverOptions, ref containsNamedAssumes))); + Linearise(node[1], options); + return true; + } + if (node.Op.Equals(VCExpressionGenerator.SoftOp)) + { + Linearise(node[1], options); + return true; + } + if (node.Op.Equals(VCExpressionGenerator.NamedAssumeOp)) + { + containsNamedAssumes = true; Linearise(node[1], options); return true; } |