From 752978545d17c2f8b001b0865c58f7d208a4786b Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Wed, 15 Nov 2023 10:25:39 -0800 Subject: [PATCH] Simplify use of SMT options --- Source/Provers/SMTLib/ProverInterface.cs | 2 +- Source/Provers/SMTLib/ProverUtil.cs | 1 - .../SMTLib/SMTLibProcessTheoremProver.cs | 26 +++++++++++++------ Source/VCGeneration/Checker.cs | 12 +-------- Source/VCGeneration/SmokeTester.cs | 6 +++-- Source/VCGeneration/Split.cs | 8 ++++-- Source/VCGeneration/SplitAndVerifyWorker.cs | 2 +- 7 files changed, 31 insertions(+), 26 deletions(-) diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index fc25d865a..842f81785 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -274,7 +274,7 @@ public virtual void SetOtherSMTOption(string name, string value) { } - public virtual void ClearOtherSMTOptions() + public virtual void ClearLocalSMTOptions() { } diff --git a/Source/Provers/SMTLib/ProverUtil.cs b/Source/Provers/SMTLib/ProverUtil.cs index 5145815bc..daaacae34 100644 --- a/Source/Provers/SMTLib/ProverUtil.cs +++ b/Source/Provers/SMTLib/ProverUtil.cs @@ -22,7 +22,6 @@ public class ProverOptions public uint ResourceLimit = 0; // Other options suitable for (set-option :key value) // TODO: put ResourceLimit in here? - public Dictionary OtherOptions = new(); public int? RandomSeed = null; public int MemoryLimit = 0; public int Verbosity = 0; diff --git a/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs b/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs index a0c9b64b8..cc216e204 100644 --- a/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs +++ b/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs @@ -1,6 +1,7 @@ using System; using System.Collections.Concurrent; using System.Collections.Generic; +using System.ComponentModel.Design; using System.IO; using System.Linq; using System.Diagnostics; @@ -433,15 +434,14 @@ protected void SendVCOptions() if (options.Solver == SolverKind.Z3 || options.Solver == SolverKind.NoOpWithZ3Options) { SendThisVC("(set-option :" + Z3.TimeoutOption + " " + options.TimeLimit + ")"); - SendThisVC("(set-option :" + Z3.RlimitOption + " " + options.ResourceLimit + ")"); if (options.RandomSeed != null) { SendThisVC("(set-option :" + Z3.SmtRandomSeed + " " + options.RandomSeed.Value + ")"); SendThisVC("(set-option :" + Z3.SatRandomSeed + " " + options.RandomSeed.Value + ")"); } } - foreach (var entry in options.OtherOptions) { - SendThisVC("(set-option :" + entry.Key + " " + entry.Value + ")"); + foreach (var entry in options.SmtOptions) { + SendThisVC("(set-option :" + entry.Option + " " + entry.Value + ")"); } } @@ -1162,26 +1162,36 @@ public override void AssertAxioms() FlushAxioms(); } + // This doesn't use SetOtherSMTOption because it may be set using + // different mechanisms than set-option in some cases. public override void SetTimeout(uint ms) { options.TimeLimit = ms; } - // TODO: make this use SetOtherSMTOption? + // Don't use SetOtherSMTOption directly, because we want a + // connection to TimeLimit. public override void SetRlimit(uint limit) { - options.ResourceLimit = limit; + if (options.Solver == SolverKind.Z3) { + SetOtherSMTOption(Z3.RlimitOption, limit.ToString()); + if (limit > 0) { + SetTimeout(0); + } + } } // Note: must be re-set for every query public override void SetOtherSMTOption(string name, string value) { - options.OtherOptions[name] = value; + options.SmtOptions.Add(new OptionValue(name, value)); } - public override void ClearOtherSMTOptions() + public override void ClearLocalSMTOptions() { - options.OtherOptions.Clear(); + // Go back to global options + options.SmtOptions.Clear(); + options.Parse(libOptions.ProverOptions); } protected Outcome ParseOutcome(SExpr resp, out bool wasUnknown) diff --git a/Source/VCGeneration/Checker.cs b/Source/VCGeneration/Checker.cs index c9f6c750b..0f5a0ad14 100644 --- a/Source/VCGeneration/Checker.cs +++ b/Source/VCGeneration/Checker.cs @@ -306,7 +306,7 @@ private async Task Check(string descriptiveName, VCExpr vc, CancellationToken ca proverRunTime = ProverStopwatch.Elapsed; } - public async Task BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler, uint timeout, uint rlimit, Dictionary otherSMTOptions, CancellationToken cancellationToken) + public async Task BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler, CancellationToken cancellationToken) { Contract.Requires(descriptiveName != null); Contract.Requires(vc != null); @@ -319,16 +319,6 @@ public async Task BeginCheck(string descriptiveName, VCExpr vc, ProverInterface. this.handler = handler; await thmProver.Reset(gen); - if (0 < rlimit) - { - timeout = 0; - } - - thmProver.SetTimeout(timeout); - thmProver.SetRlimit(rlimit); - foreach (var entry in otherSMTOptions) { - thmProver.SetOtherSMTOption(entry.Key, entry.Value); - } ProverStart = DateTime.UtcNow; ProverStopwatch.Restart(); diff --git a/Source/VCGeneration/SmokeTester.cs b/Source/VCGeneration/SmokeTester.cs index 5066a4e1f..f4a69728a 100644 --- a/Source/VCGeneration/SmokeTester.cs +++ b/Source/VCGeneration/SmokeTester.cs @@ -305,8 +305,10 @@ async Task CheckUnreachable(TextWriter traceWriter, Block cur, List s Emit(); } } - await checker.BeginCheck(cce.NonNull(Implementation.Name + "_smoke" + id++), vc, new ErrorHandler(Options, absyIds, callback), - Options.SmokeTimeout, Options.ResourceLimit, new(), CancellationToken.None); + + checker.TheoremProver.SetTimeout(Options.SmokeTimeout); + checker.TheoremProver.SetRlimit(Options.ResourceLimit); + await checker.BeginCheck(cce.NonNull(Implementation.Name + "_smoke" + id++), vc, new ErrorHandler(Options, absyIds, callback), CancellationToken.None); await checker.ProverTask; diff --git a/Source/VCGeneration/Split.cs b/Source/VCGeneration/Split.cs index 994efaa87..4b0ed4567 100644 --- a/Source/VCGeneration/Split.cs +++ b/Source/VCGeneration/Split.cs @@ -1353,8 +1353,12 @@ public async Task BeginCheck(TextWriter traceWriter, Checker checker, VerifierCa Print(); } - var extraSMTOpts = Implementation.GetExtraSMTOptions(); - await checker.BeginCheck(Description, vc, reporter, timeout, rlimit, extraSMTOpts, cancellationToken); + checker.TheoremProver.SetTimeout(Util.BoundedMultiply(timeout, 1000)); + checker.TheoremProver.SetRlimit(rlimit); + foreach (var entry in Implementation.GetExtraSMTOptions()) { + checker.TheoremProver.SetOtherSMTOption(entry.Key, entry.Value); + } + await checker.BeginCheck(Description, vc, reporter, cancellationToken); } public string Description diff --git a/Source/VCGeneration/SplitAndVerifyWorker.cs b/Source/VCGeneration/SplitAndVerifyWorker.cs index a325d79fd..a83a7bf47 100644 --- a/Source/VCGeneration/SplitAndVerifyWorker.cs +++ b/Source/VCGeneration/SplitAndVerifyWorker.cs @@ -194,7 +194,7 @@ private async Task ProcessResultAndReleaseChecker(int iteration, Split split, Ch await checker.GoBackToIdle(); } - checker.TheoremProver.ClearOtherSMTOptions(); + checker.TheoremProver.ClearLocalSMTOptions(); } private static bool IsProverFailed(ProverInterface.Outcome outcome)