From 4ad4d6a0c0d1e275b3678d09501581b246b4bfae Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Wed, 15 Nov 2023 10:47:49 -0800 Subject: [PATCH] Major simplifications --- Source/Provers/SMTLib/ProverInterface.cs | 4 +++- Source/Provers/SMTLib/ProverUtil.cs | 2 -- .../SMTLib/SMTLibProcessTheoremProver.cs | 16 +++------------- Source/VCGeneration/Checker.cs | 18 +++++++++++++++++- Source/VCGeneration/SmokeTester.cs | 6 ++---- Source/VCGeneration/Split.cs | 6 ++---- 6 files changed, 27 insertions(+), 25 deletions(-) diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index 842f81785..c5da1ff8a 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -270,10 +270,12 @@ public virtual void SetRlimit(uint limit) { } - public virtual void SetOtherSMTOption(string name, string value) + // Sets a local SMT option (cleared with ClearLocalSMTOptions) + public virtual void SetLocalSMTOption(string name, string value) { } + // Clear options set with SetLocalSMTOption public virtual void ClearLocalSMTOptions() { } diff --git a/Source/Provers/SMTLib/ProverUtil.cs b/Source/Provers/SMTLib/ProverUtil.cs index daaacae34..689f229e4 100644 --- a/Source/Provers/SMTLib/ProverUtil.cs +++ b/Source/Provers/SMTLib/ProverUtil.cs @@ -20,8 +20,6 @@ public class ProverOptions public bool ForceLogStatus = false; public uint TimeLimit = 0; public uint ResourceLimit = 0; - // Other options suitable for (set-option :key value) - // TODO: put ResourceLimit in here? 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 cc216e204..9c8040712 100644 --- a/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs +++ b/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs @@ -1,7 +1,6 @@ using System; using System.Collections.Concurrent; using System.Collections.Generic; -using System.ComponentModel.Design; using System.IO; using System.Linq; using System.Diagnostics; @@ -434,6 +433,7 @@ 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 + ")"); @@ -1162,27 +1162,17 @@ 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; } - // Don't use SetOtherSMTOption directly, because we want a - // connection to TimeLimit. public override void SetRlimit(uint limit) { - if (options.Solver == SolverKind.Z3) { - SetOtherSMTOption(Z3.RlimitOption, limit.ToString()); - if (limit > 0) { - SetTimeout(0); - } - } + options.ResourceLimit = limit; } - // Note: must be re-set for every query - public override void SetOtherSMTOption(string name, string value) + public override void SetLocalSMTOption(string name, string value) { options.SmtOptions.Add(new OptionValue(name, value)); } diff --git a/Source/VCGeneration/Checker.cs b/Source/VCGeneration/Checker.cs index 0f5a0ad14..b07d62e9d 100644 --- a/Source/VCGeneration/Checker.cs +++ b/Source/VCGeneration/Checker.cs @@ -143,6 +143,16 @@ public void Target(Program prog, ProverContext ctx, Split split) } } + private void SetTimeout(uint timeout) + { + TheoremProver.SetTimeout(Util.BoundedMultiply(timeout, 1000)); + } + + private void SetRlimit(uint rlimit) + { + TheoremProver.SetRlimit(rlimit); + } + /// /// Set up the context. /// @@ -306,7 +316,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, CancellationToken cancellationToken) + public async Task BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler, uint timeout, uint rlimit, CancellationToken cancellationToken) { Contract.Requires(descriptiveName != null); Contract.Requires(vc != null); @@ -319,6 +329,12 @@ public async Task BeginCheck(string descriptiveName, VCExpr vc, ProverInterface. this.handler = handler; await thmProver.Reset(gen); + if (0 < rlimit) + { + timeout = 0; + } + SetTimeout(timeout); + SetRlimit(rlimit); ProverStart = DateTime.UtcNow; ProverStopwatch.Restart(); diff --git a/Source/VCGeneration/SmokeTester.cs b/Source/VCGeneration/SmokeTester.cs index f4a69728a..f449cce68 100644 --- a/Source/VCGeneration/SmokeTester.cs +++ b/Source/VCGeneration/SmokeTester.cs @@ -305,10 +305,8 @@ async Task CheckUnreachable(TextWriter traceWriter, Block cur, List s Emit(); } } - - 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.BeginCheck(cce.NonNull(Implementation.Name + "_smoke" + id++), vc, new ErrorHandler(Options, absyIds, callback), + Options.SmokeTimeout, Options.ResourceLimit, CancellationToken.None); await checker.ProverTask; diff --git a/Source/VCGeneration/Split.cs b/Source/VCGeneration/Split.cs index 4b0ed4567..81645ed94 100644 --- a/Source/VCGeneration/Split.cs +++ b/Source/VCGeneration/Split.cs @@ -1353,12 +1353,10 @@ public async Task BeginCheck(TextWriter traceWriter, Checker checker, VerifierCa Print(); } - checker.TheoremProver.SetTimeout(Util.BoundedMultiply(timeout, 1000)); - checker.TheoremProver.SetRlimit(rlimit); foreach (var entry in Implementation.GetExtraSMTOptions()) { - checker.TheoremProver.SetOtherSMTOption(entry.Key, entry.Value); + checker.TheoremProver.SetLocalSMTOption(entry.Key, entry.Value); } - await checker.BeginCheck(Description, vc, reporter, cancellationToken); + await checker.BeginCheck(Description, vc, reporter, timeout, rlimit, cancellationToken); } public string Description