Skip to content

Commit

Permalink
Rename Outcome to SolverOutcome (#842)
Browse files Browse the repository at this point in the history
  • Loading branch information
@keyboardDrummer
keyboardDrummer authored Jan 26, 2024
1 parent 0efcb0b commit a09ff24
Show file tree
Hide file tree
Showing 20 changed files with 171 additions and 172 deletions.
4 changes: 2 additions & 2 deletions Source/ExecutionEngine/ExecutionEngine.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@

namespace Microsoft.Boogie
{
public record ProcessedProgram(Program Program, Action<VCGen, Implementation, ImplementationRunResult> PostProcessResult) {
public record ProcessedProgram(Program Program, Action<VerificationConditionGenerator, Implementation, ImplementationRunResult> PostProcessResult) {
public ProcessedProgram(Program program) : this(program, (_, _, _) => { }) {
}
}
Expand Down Expand Up @@ -880,7 +880,7 @@ private IObservable<IVerificationStatus> VerifyImplementationWithoutCaching(Proc
var batchCompleted = new Subject<(Split split, VerificationRunResult vcResult)>();
var completeVerification = largeThreadTaskFactory.StartNew(async () =>
{
var vcgen = new VCGen(processedProgram.Program, checkerPool);
var vcgen = new VerificationConditionGenerator(processedProgram.Program, checkerPool);
vcgen.CachingActionCounts = stats.CachingActionCounts;
verificationResult.ProofObligationCountBefore = vcgen.CumulativeAssertionCount;
verificationResult.Start = DateTime.UtcNow;
Expand Down
38 changes: 19 additions & 19 deletions Source/Houdini/Houdini.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -52,7 +52,7 @@ public virtual void UpdateAssignment(Dictionary<Variable, bool> assignment)
{
}

public virtual void UpdateOutcome(Outcome outcome)
public virtual void UpdateOutcome(SolverOutcome outcome)
{
}

Expand Down Expand Up @@ -158,7 +158,7 @@ public override void UpdateImplementation(Implementation implementation)
curImp = implementation;
}

public override void UpdateOutcome(Outcome o)
public override void UpdateOutcome(SolverOutcome o)
{
Contract.Assert(curImp != null);
DateTime endT = DateTime.UtcNow;
Expand Down Expand Up @@ -237,7 +237,7 @@ public override void UpdateAssignment(Dictionary<Variable, bool> assignment)
wr.Flush();
}

public override void UpdateOutcome(Outcome outcome)
public override void UpdateOutcome(SolverOutcome outcome)
{
wr.WriteLine("analysis outcome :" + outcome);
wr.Flush();
Expand Down Expand Up @@ -335,7 +335,7 @@ protected void NotifyAssignment(Dictionary<Variable, bool> assignment)
Notify((NotifyDelegate) delegate(HoudiniObserver r) { r.UpdateAssignment(assignment); });
}

protected void NotifyOutcome(Outcome outcome)
protected void NotifyOutcome(SolverOutcome outcome)
{
Notify((NotifyDelegate) delegate(HoudiniObserver r) { r.UpdateOutcome(outcome); });
}
Expand Down Expand Up @@ -393,7 +393,7 @@ public class Houdini : ObservableHoudini
{
protected Program program;
protected HashSet<Variable> houdiniConstants;
protected VCGen vcgen;
protected VerificationConditionGenerator vcgen;
protected ProverInterface proverInterface;
protected Graph<Implementation> callGraph;
protected HashSet<Implementation> vcgenFailures;
Expand Down Expand Up @@ -470,7 +470,7 @@ protected void Initialize(TextWriter traceWriter, Program program, HoudiniSessio
*/

var checkerPool = new CheckerPool(Options);
this.vcgen = new VCGen(program, checkerPool);
this.vcgen = new VerificationConditionGenerator(program, checkerPool);
this.proverInterface = ProverInterface.CreateProver(Options, program, Options.ProverLogFilePath,
Options.ProverLogFileAppend, Options.TimeLimit, taskID: GetTaskID());

Expand Down Expand Up @@ -837,13 +837,13 @@ protected Dictionary<Variable, bool> BuildAssignment(HashSet<Variable> constants
return initial;
}

private bool IsOutcomeNotHoudini(Outcome outcome, List<Counterexample> errors)
private bool IsOutcomeNotHoudini(SolverOutcome outcome, List<Counterexample> errors)
{
switch (outcome)
{
case Outcome.Valid:
case SolverOutcome.Valid:
return false;
case Outcome.Invalid:
case SolverOutcome.Invalid:
Contract.Assume(errors != null);
foreach (Counterexample error in errors)
{
Expand All @@ -863,14 +863,14 @@ private bool IsOutcomeNotHoudini(Outcome outcome, List<Counterexample> errors)
// Return true if there was at least one non-candidate error
protected bool UpdateHoudiniOutcome(HoudiniOutcome houdiniOutcome,
Implementation implementation,
Outcome outcome,
SolverOutcome outcome,
List<Counterexample> errors)
{
string implName = implementation.Name;
houdiniOutcome.implementationOutcomes.Remove(implName);
List<Counterexample> nonCandidateErrors = new List<Counterexample>();

if (outcome == Outcome.Invalid)
if (outcome == SolverOutcome.Invalid)
{
foreach (Counterexample error in errors)
{
Expand Down Expand Up @@ -937,19 +937,19 @@ protected void AddRelatedToWorkList(RefutedAnnotation refutedAnnotation)

// Updates the worklist and current assignment
// @return true if the current function is dequeued
protected bool UpdateAssignmentWorkList(Outcome outcome,
protected bool UpdateAssignmentWorkList(SolverOutcome outcome,
List<Counterexample> errors)
{
Contract.Assume(currentHoudiniState.Implementation != null);
bool dequeue = true;

switch (outcome)
{
case Outcome.Valid:
case SolverOutcome.Valid:
//yeah, dequeue
break;

case Outcome.Invalid:
case SolverOutcome.Invalid:
Contract.Assume(errors != null);

foreach (Counterexample error in errors)
Expand Down Expand Up @@ -1489,15 +1489,15 @@ private RefutedAnnotation ExtractRefutedAnnotation(Counterexample error)
return null;
}

private async Task<(Outcome, List<Counterexample> errors)> TryCatchVerify(HoudiniSession session, int stage, IReadOnlyList<int> completedStages)
private async Task<(SolverOutcome, List<Counterexample> errors)> TryCatchVerify(HoudiniSession session, int stage, IReadOnlyList<int> completedStages)
{
try {
return await session.Verify(proverInterface, GetAssignmentWithStages(stage, completedStages), GetErrorLimit());
}
catch (UnexpectedProverOutputException upo)
{
Contract.Assume(upo != null);
return (Outcome.Undetermined, null);
return (SolverOutcome.Undetermined, null);
}

}
Expand Down Expand Up @@ -1551,7 +1551,7 @@ private async Task HoudiniVerifyCurrent(HoudiniSession session, int stage, IRead

#region Explain Houdini

if (Options.ExplainHoudini && outcome == Outcome.Invalid)
if (Options.ExplainHoudini && outcome == SolverOutcome.Invalid)
{
Contract.Assume(errors != null);
// make a copy of this variable
Expand Down Expand Up @@ -1587,7 +1587,7 @@ private async Task HoudiniVerifyCurrent(HoudiniSession session, int stage, IRead

if (UpdateAssignmentWorkList(outcome, errors))
{
if (Options.UseUnsatCoreForContractInfer && outcome == Outcome.Valid)
if (Options.UseUnsatCoreForContractInfer && outcome == SolverOutcome.Valid)
{
await session.UpdateUnsatCore(proverInterface, currentHoudiniState.Assignment);
}
Expand Down Expand Up @@ -1707,7 +1707,7 @@ public class VCGenOutcome
public VcOutcome VcOutcome;
public List<Counterexample> errors;

public VCGenOutcome(Outcome outcome, List<Counterexample> errors)
public VCGenOutcome(SolverOutcome outcome, List<Counterexample> errors)
{
this.VcOutcome = ConditionGeneration.ProverInterfaceOutcomeToConditionGenerationOutcome(outcome);
this.errors = errors;
Expand Down
24 changes: 12 additions & 12 deletions Source/Houdini/HoudiniSession.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -156,7 +156,7 @@ public bool InUnsatCore(Variable constant)
return false;
}

public HoudiniSession(Houdini houdini, VCGen vcgen, ProverInterface proverInterface, Program program,
public HoudiniSession(Houdini houdini, VerificationConditionGenerator vcgen, ProverInterface proverInterface, Program program,
ImplementationRun run, HoudiniStatistics stats, int taskID = -1)
{
var impl = run.Implementation;
Expand Down Expand Up @@ -195,7 +195,7 @@ public HoudiniSession(Houdini houdini, VCGen vcgen, ProverInterface proverInterf
new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Type.Bool), false));
proverInterface.DefineMacro(macro, conjecture);
conjecture = exprGen.Function(macro);
handler = new VCGen.ErrorReporter(this.houdini.Options, gotoCmdOrigins, absyIds, impl.Blocks, impl.debugInfos, collector,
handler = new VerificationConditionGenerator.ErrorReporter(this.houdini.Options, gotoCmdOrigins, absyIds, impl.Blocks, impl.debugInfos, collector,
mvInfo, proverInterface.Context, program, this);
}

Expand Down Expand Up @@ -252,7 +252,7 @@ private VCExpr BuildAxiom(ProverInterface proverInterface, Dictionary<Variable,

public HoudiniOptions Options => houdini.Options;

public async Task<(Outcome, List<Counterexample> errors)> Verify(
public async Task<(SolverOutcome, List<Counterexample> errors)> Verify(
ProverInterface proverInterface,
Dictionary<Variable, bool> assignment,
int errorLimit)
Expand Down Expand Up @@ -393,7 +393,7 @@ public async Task Explain(ProverInterface proverInterface,
var el = Options.ErrorLimit;
Options.ErrorLimit = 1;

var outcome = Outcome.Undetermined;
var outcome = SolverOutcome.Undetermined;

do
{
Expand All @@ -402,8 +402,8 @@ public async Task Explain(ProverInterface proverInterface,
handler, CancellationToken.None);
hardAssumptions.RemoveAt(hardAssumptions.Count - 1);

if (outcome == Outcome.TimeOut || outcome == Outcome.OutOfMemory ||
outcome == Outcome.OutOfResource || outcome == Outcome.Undetermined)
if (outcome == SolverOutcome.TimeOut || outcome == SolverOutcome.OutOfMemory ||
outcome == SolverOutcome.OutOfResource || outcome == SolverOutcome.Undetermined)
{
break;
}
Expand Down Expand Up @@ -436,8 +436,8 @@ public async Task Explain(ProverInterface proverInterface,
(outcome, var unsatisfiedSoftAssumptions2) = await proverInterface.CheckAssumptions(hardAssumptions, softAssumptions2,
handler, CancellationToken.None);

if (outcome == Outcome.TimeOut || outcome == Outcome.OutOfMemory ||
outcome == Outcome.OutOfResource || outcome == Outcome.Undetermined)
if (outcome == SolverOutcome.TimeOut || outcome == SolverOutcome.OutOfMemory ||
outcome == SolverOutcome.OutOfResource || outcome == SolverOutcome.Undetermined)
{
break;
}
Expand Down Expand Up @@ -467,8 +467,8 @@ public async Task Explain(ProverInterface proverInterface,
}
} while (false);

if (outcome == Outcome.TimeOut || outcome == Outcome.OutOfMemory ||
outcome == Outcome.OutOfResource || outcome == Outcome.Undetermined)
if (outcome == SolverOutcome.TimeOut || outcome == SolverOutcome.OutOfMemory ||
outcome == SolverOutcome.OutOfResource || outcome == SolverOutcome.Undetermined)
{
Houdini.explainHoudiniDottyFile.WriteLine("{0} -> {1} [ label = \"{2}\" color=red ];", refutedConstant.Name,
"TimeOut", Description);
Expand Down Expand Up @@ -515,8 +515,8 @@ public async Task UpdateUnsatCore(ProverInterface proverInterface, Dictionary<Va
assumptionExprs.Add(exprTranslator.LookupVariable(v));
}

(Outcome tmp, var unsatCore) = await proverInterface.CheckAssumptions(assumptionExprs, handler, CancellationToken.None);
System.Diagnostics.Debug.Assert(tmp == Outcome.Valid);
(SolverOutcome tmp, var unsatCore) = await proverInterface.CheckAssumptions(assumptionExprs, handler, CancellationToken.None);
System.Diagnostics.Debug.Assert(tmp == SolverOutcome.Valid);
unsatCoreSet = new HashSet<Variable>();
foreach (int i in unsatCore)
{
Expand Down
10 changes: 5 additions & 5 deletions Source/Provers/SMTLib/ProverInterface.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -112,7 +112,7 @@ public virtual int StartingProcId()
return 0;
}

public virtual void OnModel(IList<string> labels, Model model, Outcome proverOutcome)
public virtual void OnModel(IList<string> labels, Model model, SolverOutcome proverOutcome)
{
Contract.Requires(cce.NonNullElements(labels));
}
Expand Down Expand Up @@ -157,7 +157,7 @@ public virtual Absy Label2Absy(string label)
}
}

public abstract Task<Outcome> Check(string descriptiveName, VCExpr vc, ErrorHandler handler, int errorLimit, CancellationToken cancellationToken);
public abstract Task<SolverOutcome> Check(string descriptiveName, VCExpr vc, ErrorHandler handler, int errorLimit, CancellationToken cancellationToken);

public virtual void LogComment(string comment)
{
Expand Down Expand Up @@ -232,13 +232,13 @@ public virtual void Check()
}

// (check-sat + get-unsat-core + checkOutcome)
public virtual Task<(Outcome, List<int>)> CheckAssumptions(List<VCExpr> assumptions, ErrorHandler handler,
public virtual Task<(SolverOutcome, List<int>)> CheckAssumptions(List<VCExpr> assumptions, ErrorHandler handler,
CancellationToken cancellationToken)
{
throw new NotImplementedException();
}

public virtual Task<(Outcome, List<int>)> CheckAssumptions(List<VCExpr> hardAssumptions, List<VCExpr> softAssumptions,
public virtual Task<(SolverOutcome, List<int>)> CheckAssumptions(List<VCExpr> hardAssumptions, List<VCExpr> softAssumptions,
ErrorHandler handler, CancellationToken cancellationToken)
{
throw new NotImplementedException();
Expand Down Expand Up @@ -295,7 +295,7 @@ public virtual void AssertNamed(VCExpr vc, bool polarity, string name)
public abstract Task GoBackToIdle();
}

public enum Outcome
public enum SolverOutcome
{
Valid,
Invalid,
Expand Down
22 changes: 11 additions & 11 deletions Source/Provers/SMTLib/SMTLibBatchTheoremProver.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -62,7 +62,7 @@ public override int FlushAxiomsToTheoremProver()
return 0;
}

public override async Task<Outcome> Check(string descriptiveName, VCExpr vc, ErrorHandler handler, int errorLimit,
public override async Task<SolverOutcome> Check(string descriptiveName, VCExpr vc, ErrorHandler handler, int errorLimit,
CancellationToken cancellationToken)
{
currentErrorHandler = handler;
Expand Down Expand Up @@ -134,7 +134,7 @@ private Task<IReadOnlyList<SExpr>> SendRequestsAndClose(IReadOnlyList<string> re
return Process.SendRequestsAndCloseInput(sanitizedRequests, cancellationToken);
}

private async Task<Outcome> CheckSat(CancellationToken cancellationToken)
private async Task<SolverOutcome> CheckSat(CancellationToken cancellationToken)
{
var requests = new List<string>();
requests.Add("(check-sat)");
Expand All @@ -148,7 +148,7 @@ private async Task<Outcome> CheckSat(CancellationToken cancellationToken)
}

if (Process == null || HadErrors) {
return Outcome.Undetermined;
return SolverOutcome.Undetermined;
}

try {
Expand All @@ -159,7 +159,7 @@ private async Task<Outcome> CheckSat(CancellationToken cancellationToken)
catch (TimeoutException) {
currentErrorHandler.OnResourceExceeded("hard solver timeout");
resourceCount = -1;
return Outcome.TimeOut;
return SolverOutcome.TimeOut;
}
var responseStack = new Stack<SExpr>(responses.Reverse());

Expand All @@ -176,8 +176,8 @@ private async Task<Outcome> CheckSat(CancellationToken cancellationToken)
resourceCount = ParseRCount(rlimitSExp);

// Sometimes Z3 doesn't tell us that it ran out of resources
if (result != Outcome.Valid && resourceCount > options.ResourceLimit && options.ResourceLimit > 0) {
result = Outcome.OutOfResource;
if (result != SolverOutcome.Valid && resourceCount > options.ResourceLimit && options.ResourceLimit > 0) {
result = SolverOutcome.OutOfResource;
}
}

Expand All @@ -186,16 +186,16 @@ private async Task<Outcome> CheckSat(CancellationToken cancellationToken)

if (options.LibOptions.ProduceUnsatCores) {
var unsatCoreSExp = responseStack.Pop();
if (result == Outcome.Valid) {
if (result == SolverOutcome.Valid) {
ReportCoveredElements(unsatCoreSExp);
}
}

if (result == Outcome.Invalid) {
if (result == SolverOutcome.Invalid) {
var labels = CalculatePath(currentErrorHandler.StartingProcId(), errorModel);
if (labels.Length == 0) {
// Without a path to an error, we don't know what to report
result = Outcome.Undetermined;
result = SolverOutcome.Undetermined;
} else {
currentErrorHandler.OnModel(labels, errorModel, result);
}
Expand Down Expand Up @@ -294,13 +294,13 @@ public override Task<List<string>> UnsatCore()
throw new NotSupportedException("Batch mode solver interface does not support unsat cores.");
}

public override Task<(Outcome, List<int>)> CheckAssumptions(List<VCExpr> assumptions,
public override Task<(SolverOutcome, List<int>)> CheckAssumptions(List<VCExpr> assumptions,
ErrorHandler handler, CancellationToken cancellationToken)
{
throw new NotSupportedException("Batch mode solver interface does not support checking assumptions.");
}

public override Task<(Outcome, List<int>)> CheckAssumptions(List<VCExpr> hardAssumptions, List<VCExpr> softAssumptions,
public override Task<(SolverOutcome, List<int>)> CheckAssumptions(List<VCExpr> hardAssumptions, List<VCExpr> softAssumptions,
ErrorHandler handler, CancellationToken cancellationToken)
{
throw new NotSupportedException("Batch mode solver interface does not support checking assumptions.");
Expand Down
Loading

0 comments on commit a09ff24

Please sign in to comment.