diff options
author | Valentin Wüstholz <wuestholz@gmail.com> | 2015-11-18 15:46:24 -0600 |
---|---|---|
committer | Valentin Wüstholz <wuestholz@gmail.com> | 2015-11-18 15:46:24 -0600 |
commit | a51f4e6cba57b6711e36ef482f4e320c9cf0542f (patch) | |
tree | b0142b762f2eb094dec09d40a1b7d449f2d8e076 /Source/Provers/SMTLib/SMTLibLineariser.cs | |
parent | 9a4448732895ffe451642b2bebd95dcf1ed371d4 (diff) |
Add experimental support for optimization (requires Z3 build after changeset 9cba63c31f6f1466dd4ef442bb840d1ab84539c7).
Diffstat (limited to 'Source/Provers/SMTLib/SMTLibLineariser.cs')
-rw-r--r-- | Source/Provers/SMTLib/SMTLibLineariser.cs | 17 |
1 files changed, 14 insertions, 3 deletions
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index dcf95bd2..de8798b8 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -34,14 +34,14 @@ namespace Microsoft.Boogie.SMTLib public class SMTLibExprLineariser : IVCExprVisitor<bool, LineariserOptions/*!*/> { - public static string ToString(VCExpr e, UniqueNamer namer, SMTLibProverOptions opts) + public static string ToString(VCExpr e, UniqueNamer namer, SMTLibProverOptions opts, IList<string> optReqs = null) { Contract.Requires(e != null); Contract.Requires(namer != null); Contract.Ensures(Contract.Result<string>() != null); StringWriter sw = new StringWriter(); - SMTLibExprLineariser lin = new SMTLibExprLineariser(sw, namer, opts); + SMTLibExprLineariser lin = new SMTLibExprLineariser(sw, namer, opts, optReqs); Contract.Assert(lin != null); lin.Linearise(e, LineariserOptions.Default); return cce.NonNull(sw.ToString()); @@ -74,12 +74,15 @@ namespace Microsoft.Boogie.SMTLib internal int UnderQuantifier = 0; internal readonly SMTLibProverOptions ProverOptions; - public SMTLibExprLineariser(TextWriter wr, UniqueNamer namer, SMTLibProverOptions opts) + readonly IList<string> OptimizationRequests; + + public SMTLibExprLineariser(TextWriter wr, UniqueNamer namer, SMTLibProverOptions opts, IList<string> optReqs = null) { Contract.Requires(wr != null); Contract.Requires(namer != null); this.wr = wr; this.Namer = namer; this.ProverOptions = opts; + this.OptimizationRequests = optReqs; } public void Linearise(VCExpr expr, LineariserOptions options) @@ -263,6 +266,14 @@ namespace Microsoft.Boogie.SMTLib } return true; } + if (OptimizationRequests != null + && (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))); + Linearise(node[1], options); + return true; + } return node.Accept<bool, LineariserOptions/*!*/>(OpLineariser, options); } |