diff options
| author |  wuestholz <unknown> | 2014-10-17 10:11:47 +0200 |
|---|---|---|
| committer | wuestholz <unknown> | 2014-10-17 10:11:47 +0200 |
| commit | 96c50d521e9b9089bfc20389e589ac5f45705632 (patch) | |
| tree | 3b96432cff25c75b14bd7df4d8100b722719f269 /Source/Core/Absy.cs | |
| parent | 855a0095b2a22230a2791827b666d0073b24ad5b (diff) | |
Worked on the verification result caching.
Diffstat (limited to 'Source/Core/Absy.cs')
| -rw-r--r-- | Source/Core/Absy.cs | 39 |
1 files changed, 32 insertions, 7 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index a9466f8d..3325d742 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -3266,28 +3266,53 @@ namespace Microsoft.Boogie { }
}
- public List<LocalVariable> PossiblyFalseAssumptionVariables(Dictionary<Variable, Expr> incarnationMap)
+ IList<LocalVariable> doomedInjectedAssumptionVariables;
+ public IList<LocalVariable> DoomedInjectedAssumptionVariables
+ {
+ get
+ {
+ return doomedInjectedAssumptionVariables != null ? doomedInjectedAssumptionVariables : new List<LocalVariable>();
+ }
+ }
+
+ public List<LocalVariable> RelevantInjectedAssumptionVariables(Dictionary<Variable, Expr> incarnationMap)
{
return InjectedAssumptionVariables.Where(v => incarnationMap.ContainsKey(v)).ToList();
}
+ public List<LocalVariable> RelevantDoomedInjectedAssumptionVariables(Dictionary<Variable, Expr> incarnationMap)
+ {
+ return DoomedInjectedAssumptionVariables.Where(v => incarnationMap.ContainsKey(v)).ToList();
+ }
+
public Expr ConjunctionOfInjectedAssumptionVariables(Dictionary<Variable, Expr> incarnationMap, out bool isTrue)
{
Contract.Requires(incarnationMap != null);
- var vars = PossiblyFalseAssumptionVariables(incarnationMap).Select(v => incarnationMap[v]).ToList();
+ var vars = RelevantInjectedAssumptionVariables(incarnationMap).Select(v => incarnationMap[v]).ToList();
isTrue = vars.Count == 0;
return LiteralExpr.BinaryTreeAnd(vars);
}
- public void InjectAssumptionVariable(LocalVariable variable)
+ public void InjectAssumptionVariable(LocalVariable variable, bool isDoomed = false)
{
- if (injectedAssumptionVariables == null)
+ LocVars.Add(variable);
+ if (isDoomed)
{
- injectedAssumptionVariables = new List<LocalVariable>();
+ if (doomedInjectedAssumptionVariables == null)
+ {
+ doomedInjectedAssumptionVariables = new List<LocalVariable>();
+ }
+ doomedInjectedAssumptionVariables.Add(variable);
+ }
+ else
+ {
+ if (injectedAssumptionVariables == null)
+ {
+ injectedAssumptionVariables = new List<LocalVariable>();
+ }
+ injectedAssumptionVariables.Add(variable);
}
- injectedAssumptionVariables.Add(variable);
- LocVars.Add(variable);
}
public Implementation(IToken tok, string name, List<TypeVariable> typeParams, List<Variable> inParams, List<Variable> outParams, List<Variable> localVariables, [Captured] StmtList structuredStmts, QKeyValue kv)
|