diff options
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 50 | ||||
| -rw-r--r-- | Source/Core/VCExp.cs | 2 | ||||
| -rw-r--r-- | Source/Houdini/AbstractHoudini.cs | 2 |
3 files changed, 46 insertions, 8 deletions
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 6bed4e75..215e17da 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -509,7 +509,7 @@ namespace Microsoft.Boogie { Contract.Invariant(0 <= EnhancedErrorMessages && EnhancedErrorMessages < 2);
Contract.Invariant(0 <= StepsBeforeWidening && StepsBeforeWidening <= 9);
Contract.Invariant(-1 <= BracketIdsInVC && BracketIdsInVC < 2);
- Contract.Invariant(cce.NonNullElements(ProverOptions));
+ Contract.Invariant(cce.NonNullElements(this.proverOptions));
}
public int LoopUnrollCount = -1; // -1 means don't unroll loops
@@ -573,7 +573,28 @@ namespace Microsoft.Boogie { public ProverFactory TheProverFactory;
public string ProverName;
[Peer]
- public List<string/*!*/>/*!*/ ProverOptions = new List<string/*!*/>();
+ private List<string> proverOptions = new List<string>();
+
+ public IEnumerable<string> ProverOptions
+ {
+ get
+ {
+ Contract.Ensures(Contract.Result<IEnumerable<string>>() != null);
+ foreach (string s in this.proverOptions)
+ yield return s;
+ }
+ }
+
+ public void AddProverOption(string option)
+ {
+ Contract.Requires(option != null);
+ this.proverOptions.Add(option);
+ }
+
+ public void RemoveAllProverOptions(Predicate<string> match)
+ {
+ this.proverOptions.RemoveAll(match);
+ }
public int BracketIdsInVC = -1; // -1 - not specified, 0 - no, 1 - yes
public bool CausalImplies = false;
@@ -609,12 +630,29 @@ namespace Microsoft.Boogie { }
[ContractInvariantMethod]
void ObjectInvariant4() {
- Contract.Invariant(cce.NonNullElements(Z3Options));
+ Contract.Invariant(cce.NonNullElements(this.z3Options));
Contract.Invariant(0 <= Z3lets && Z3lets < 4);
}
[Peer]
- public List<string/*!*/>/*!*/ Z3Options = new List<string/*!*/>();
+ private List<string> z3Options = new List<string>();
+
+ public IEnumerable<string> Z3Options
+ {
+ get
+ {
+ Contract.Ensures(Contract.Result<IEnumerable<string>>() != null);
+ foreach (string s in z3Options)
+ yield return s;
+ }
+ }
+
+ public void AddZ3Option(string option)
+ {
+ Contract.Requires(option != null);
+ this.z3Options.Add(option);
+ }
+
public bool Z3types = false;
public int Z3lets = 3; // 0 - none, 1 - only LET TERM, 2 - only LET FORMULA, 3 - (default) any
@@ -1099,7 +1137,7 @@ namespace Microsoft.Boogie { case "p":
case "proverOpt":
if (ps.ConfirmArgumentCount(1)) {
- ProverOptions.Add(cce.NonNull(args[ps.i]));
+ AddProverOption(cce.NonNull(args[ps.i]));
}
return true;
@@ -1392,7 +1430,7 @@ namespace Microsoft.Boogie { case "z3opt":
if (ps.ConfirmArgumentCount(1)) {
- Z3Options.Add(cce.NonNull(args[ps.i]));
+ AddZ3Option(cce.NonNull(args[ps.i]));
}
return true;
diff --git a/Source/Core/VCExp.cs b/Source/Core/VCExp.cs index 5a8100a7..87b8f3e6 100644 --- a/Source/Core/VCExp.cs +++ b/Source/Core/VCExp.cs @@ -81,7 +81,7 @@ The generic options may or may not be used by the prover plugin. }
}
- public virtual void Parse(List<string/*!*/>/*!*/ opts) {
+ public virtual void Parse(IEnumerable<string/*!*/>/*!*/ opts) {
Contract.Requires(cce.NonNullElements(opts));
StringBuilder sb = new StringBuilder(stringRepr);
Contract.Assert(sb != null);
diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs index cc8298b3..b49107a0 100644 --- a/Source/Houdini/AbstractHoudini.cs +++ b/Source/Houdini/AbstractHoudini.cs @@ -2199,7 +2199,7 @@ namespace Microsoft.Boogie.Houdini { this.name2Impl = SimpleUtil.nameImplMapping(program);
if (CommandLineOptions.Clo.ProverKillTime > 0)
- CommandLineOptions.Clo.ProverOptions.Add(string.Format("TIME_LIMIT={0}", CommandLineOptions.Clo.ProverKillTime));
+ CommandLineOptions.Clo.AddProverOption(string.Format("TIME_LIMIT={0}", CommandLineOptions.Clo.ProverKillTime));
this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, new List<Checker>());
this.prover = ProverInterface.CreateProver(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, -1);
|