diff options
| -rw-r--r-- | Source/Provers/Z3/Prover.cs | 654 |
1 files changed, 266 insertions, 388 deletions
diff --git a/Source/Provers/Z3/Prover.cs b/Source/Provers/Z3/Prover.cs index 208f934b..c431b5af 100644 --- a/Source/Provers/Z3/Prover.cs +++ b/Source/Provers/Z3/Prover.cs @@ -18,39 +18,41 @@ using Microsoft.Basetypes; // Simplified interface to an external prover like Simplify or the z3 process, taken from Bird.
namespace Microsoft.Boogie.Z3
{
- internal class Z3ProverProcess : ProverProcess {
- [Peer] private Z3InstanceOptions opts;
- [Peer] private readonly Inspector/*?*/ inspector;
+ internal class Z3ProverProcess : ProverProcess
+ {
+ [Peer]
+ private Z3InstanceOptions opts;
+ [Peer]
+ private readonly Inspector/*?*/ inspector;
private readonly bool expectingModel = false;
private string cmdLineArgs = "";
[ContractInvariantMethod]
- void ObjectInvariant()
- {
- Contract.Invariant(cmdLineArgs!=null);
+ void ObjectInvariant() {
+ Contract.Invariant(cmdLineArgs != null);
Contract.Invariant(opts != null);
Contract.Invariant(cce.NonNullElements(parameterSettings));
}
-
- class OptionValue {
+ class OptionValue
+ {
public readonly string Option;
public readonly string Value;
[ContractInvariantMethod]
-void ObjectInvariant()
-{
- Contract.Invariant(Option!=null);
+ void ObjectInvariant() {
+ Contract.Invariant(Option != null);
Contract.Invariant(Value != null);
-}
+ }
- public OptionValue(string option, string value) {Contract.Requires(option != null);Contract.Requires(value != null); Option = option; Value = value; }
+ public OptionValue(string option, string value) { Contract.Requires(option != null); Contract.Requires(value != null); Option = option; Value = value; }
}
+
static void AddOption(List<OptionValue> parms, string option, string value)
//modifies parms.*; TODO:
{
- Contract.Requires(option != null);
- Contract.Requires(value != null);
+ Contract.Requires(option != null);
+ Contract.Requires(value != null);
Contract.Requires(cce.NonNullElements(parms));
OptionValue ov = new OptionValue(option, value);
cce.Owner.AssignSame(ov, cce.Owner.ElementProxy(parms));
@@ -59,224 +61,102 @@ void ObjectInvariant() private List<OptionValue/*!>!*/> parameterSettings;
- //[NotDelayed]
- [Captured]
- public Z3ProverProcess(Z3InstanceOptions opts, Inspector inspector)
- : base(ComputeProcessStartInfo(opts), opts.ExeName)
- { // throws ProverException
- Contract.Requires(opts != null);
- Contract.Requires(inspector == null || cce.Owner.Same(opts, inspector));
- string z3args = OptionChar() + "si";
- List<OptionValue/*!*/> parms = new List<OptionValue/*!*/>();
-
- if (opts.V2) {
- AddOption(parms, "MODEL_PARTIAL", "true");
- AddOption(parms, "MODEL_VALUE_COMPLETION", "false");
- AddOption(parms, "MODEL_HIDE_UNUSED_PARTITIONS", "false");
- AddOption(parms, "MODEL_V1", "true");
- AddOption(parms, "ASYNC_COMMANDS", "false");
- } else {
- AddOption(parms, "PARTIAL_MODELS", "true");
- AddOption(parms, "MODEL_VALUE_COMPLETION", "false");
- AddOption(parms, "HIDE_UNUSED_PARTITIONS", "false");
+ static void AppendCmdLineOption(StringBuilder cmdLineBldr, string name, object value) {
+ cmdLineBldr.Append(' ').Append(OptionChar()).Append(name).Append(':').Append(value);
}
- if (opts.V2) {
- // Phase selection means to always try the negative literal polarity first, seems to be good for Boogie.
- // The restart parameters change the restart behavior to match Z3 v1, which also seems to be good.
- AddOption(parms, "PHASE_SELECTION", "0");
- AddOption(parms, "RESTART_STRATEGY", "0");
- AddOption(parms, "RESTART_FACTOR", "|1.5|");
-
- // This is used by VCC, but could be also useful for others, if sk_hack(foo(x)) is included as trigger,
- // the foo(x0) will be activated for e-matching when x is skolemized to x0.
- AddOption(parms, "NNF_SK_HACK", "true");
-
- // More or less like MAM=0.
- AddOption(parms, "QI_EAGER_THRESHOLD", "100");
- // Complex proof attempts in VCC (and likely elsewhere) require matching depth of 20 or more.
-
- // the following will make the :weight option more usable
- AddOption(parms, "QI_COST", "|\"(+ weight generation)\"|");
-
- // Make the integer model more diverse by default, speeds up some benchmarks a lot.
- AddOption(parms, "ARITH_RANDOM_INITIAL_VALUE", "true");
-
- // The left-to-right structural case-splitting strategy.
- AddOption(parms, "SORT_AND_OR", "false");
- AddOption(parms, "CASE_SPLIT", "3");
-
- // In addition delay adding unit conflicts.
- AddOption(parms, "DELAY_UNITS", "true");
- AddOption(parms, "DELAY_UNITS_THRESHOLD", "16");
-
- if (opts.Inspector != null) {
- AddOption(parms, "PROGRESS_SAMPLING_FREQ", "100");
- }
- } else {
- z3args += " " + OptionChar() + "mam:" + CommandLineOptions.Clo.Z3mam;
- }
-
- if (CommandLineOptions.Clo.z3AtFlag) {
- z3args += " " + OptionChar() + "@ ";
- }
- if (0 <= CommandLineOptions.Clo.ProverCCLimit) {
- z3args += " " + OptionChar() + "cex:" + CommandLineOptions.Clo.ProverCCLimit;
- }
- if (0 <= opts.Timeout) {
- z3args += " " + OptionChar() + "t:" + opts.Timeout;
- }
- if (opts.Typed) {
- AddOption(parms, "TYPE_CHECK", "true");
- if (opts.BitVectors == CommandLineOptions.BvHandling.Z3Native) {
- if (opts.V2) {
- AddOption(parms, "BV_REFLECT", "true");
- } else {
- AddOption(parms, "REFLECT_BV_OPS", "true");
- }
- }
- }
- if (CommandLineOptions.Clo.PrintErrorModel >= 1 ||
- CommandLineOptions.Clo.EnhancedErrorMessages == 1 ||
- CommandLineOptions.Clo.ContractInfer ||
- CommandLineOptions.Clo.LazyInlining > 0 ||
- CommandLineOptions.Clo.StratifiedInlining > 0) {
- z3args += " " + OptionChar() + "m";
- expectingModel = true;
- }
- if (CommandLineOptions.Clo.LazyInlining == 2) {
- z3args += " " + OptionChar() + "nw";
- AddOption(parms, "MACRO_EXPANSION", "true");
- }
-
- // Z3 version 1.3 does not support SETPARAMETER in the input, so we tack on the OPTION=value pairs to z3args
- if (opts.V1) {
- foreach (OptionValue opt in parms) {
- z3args += string.Format(" \"{0}={1}\"", opt.Option, opt.Value);
- }
- }
-
- foreach (string opt in CommandLineOptions.Clo.Z3Options) {
- Contract.Assert(opt != null);
- int eq = opt.IndexOf("=");
- // we add them both to command line and the input file:
- // - allow for overriding default options
- // - some options (like TRACE) work only from command line
- // Also options with spaces do not work with (SETPARAMETER ...)
- if (eq > 0 && opt.IndexOf(" ") < 0 && 'A' <= opt[0] && opt[0] <= 'Z') {
- AddOption(parms, opt.Substring(0, eq), opt.Substring(eq + 1));
- }
- z3args += " \"" + opt + "\"";
- }
-
-
- cmdLineArgs = z3args;
- parameterSettings = parms;
-
- // ProcessStartInfo psi = new ProcessStartInfo(opts.ExeName, z3args);
- // Contract.Assert(psi!=null);
- // psi.CreateNoWindow = true;
- // psi.UseShellExecute = false;
- // psi.RedirectStandardInput = true;
- // psi.RedirectStandardOutput = true;
- // psi.RedirectStandardError = true;
-
- //base(psi, opts.ExeName);
-
- cce.Owner.AssignSame(this, opts);
- this.opts = opts;
- this.inspector = inspector;
+ static void AppendCmdLineOption(StringBuilder cmdLineBldr, string name) {
+ cmdLineBldr.Append(' ').Append(OptionChar()).Append(name);
}
- private static ProcessStartInfo ComputeProcessStartInfo(Z3InstanceOptions opts) {
- string z3args = OptionChar() + "si";
- List<OptionValue/*!*/> parms = new List<OptionValue/*!*/>();
+ static List<OptionValue/*!*/>/*!*/ CreateParameterListForOptions(Z3InstanceOptions opts, Inspector inspector, out string cmdLineArgs, out bool expectingModel)
+ {
+ List<OptionValue/*!*/>/*!*/ result = new List<OptionValue/*!*/>();
+ StringBuilder cmdLineArgsBldr = new StringBuilder();
+ AppendCmdLineOption(cmdLineArgsBldr, "si");
+ expectingModel = false;
- if (opts.V2) {
- AddOption(parms, "MODEL_PARTIAL", "true");
- AddOption(parms, "MODEL_VALUE_COMPLETION", "false");
- AddOption(parms, "MODEL_HIDE_UNUSED_PARTITIONS", "false");
- AddOption(parms, "MODEL_V1", "true");
- AddOption(parms, "ASYNC_COMMANDS", "false");
+ if (opts.V1) {
+ AddOption(result, "PARTIAL_MODELS", "true");
+ AddOption(result, "MODEL_VALUE_COMPLETION", "false");
+ AddOption(result, "HIDE_UNUSED_PARTITIONS", "false");
+ AppendCmdLineOption(cmdLineArgsBldr, "mam", CommandLineOptions.Clo.Z3mam);
} else {
- AddOption(parms, "PARTIAL_MODELS", "true");
- AddOption(parms, "MODEL_VALUE_COMPLETION", "false");
- AddOption(parms, "HIDE_UNUSED_PARTITIONS", "false");
- }
+ AddOption(result, "MODEL_PARTIAL", "true");
+ AddOption(result, "MODEL_VALUE_COMPLETION", "false");
+ AddOption(result, "MODEL_HIDE_UNUSED_PARTITIONS", "false");
+ AddOption(result, "MODEL_V1", "true");
+ AddOption(result, "ASYNC_COMMANDS", "false");
- if (opts.V2) {
// Phase selection means to always try the negative literal polarity first, seems to be good for Boogie.
// The restart parameters change the restart behavior to match Z3 v1, which also seems to be good.
- AddOption(parms, "PHASE_SELECTION", "0");
- AddOption(parms, "RESTART_STRATEGY", "0");
- AddOption(parms, "RESTART_FACTOR", "|1.5|");
+ AddOption(result, "PHASE_SELECTION", "0");
+ AddOption(result, "RESTART_STRATEGY", "0");
+ AddOption(result, "RESTART_FACTOR", "|1.5|");
// This is used by VCC, but could be also useful for others, if sk_hack(foo(x)) is included as trigger,
// the foo(x0) will be activated for e-matching when x is skolemized to x0.
- AddOption(parms, "NNF_SK_HACK", "true");
+ AddOption(result, "NNF_SK_HACK", "true");
// More or less like MAM=0.
- AddOption(parms, "QI_EAGER_THRESHOLD", "100");
+ AddOption(result, "QI_EAGER_THRESHOLD", "100");
// Complex proof attempts in VCC (and likely elsewhere) require matching depth of 20 or more.
// the following will make the :weight option more usable
- AddOption(parms, "QI_COST", "|\"(+ weight generation)\"|");
+ AddOption(result, "QI_COST", "|\"(+ weight generation)\"|");
// Make the integer model more diverse by default, speeds up some benchmarks a lot.
- AddOption(parms, "ARITH_RANDOM_INITIAL_VALUE", "true");
+ AddOption(result, "ARITH_RANDOM_INITIAL_VALUE", "true");
// The left-to-right structural case-splitting strategy.
- AddOption(parms, "SORT_AND_OR", "false");
- AddOption(parms, "CASE_SPLIT", "3");
+ AddOption(result, "SORT_AND_OR", "false");
+ AddOption(result, "CASE_SPLIT", "3");
// In addition delay adding unit conflicts.
- AddOption(parms, "DELAY_UNITS", "true");
- AddOption(parms, "DELAY_UNITS_THRESHOLD", "16");
+ AddOption(result, "DELAY_UNITS", "true");
+ AddOption(result, "DELAY_UNITS_THRESHOLD", "16");
if (opts.Inspector != null) {
- AddOption(parms, "PROGRESS_SAMPLING_FREQ", "100");
+ AddOption(result, "PROGRESS_SAMPLING_FREQ", "100");
}
- } else {
- z3args += " " + OptionChar() + "mam:" + CommandLineOptions.Clo.Z3mam;
}
- if (CommandLineOptions.Clo.z3AtFlag) {
- z3args += " " + OptionChar() + "@ ";
+ if (opts.Typed) {
+ AddOption(result, "TYPE_CHECK", "true");
+ if (opts.BitVectors == CommandLineOptions.BvHandling.Z3Native)
+ if (opts.V2)
+ AddOption(result, "BV_REFLECT", "true");
+ else
+ AddOption(result, "REFLECT_BV_OPS", "true");
}
- if (0 <= CommandLineOptions.Clo.ProverCCLimit) {
- z3args += " " + OptionChar() + "cex:" + CommandLineOptions.Clo.ProverCCLimit;
+
+ if (CommandLineOptions.Clo.LazyInlining == 2) {
+ AddOption(result, "MACRO_EXPANSION", "true");
+ AppendCmdLineOption(cmdLineArgsBldr, "nw");
}
+
+ if (CommandLineOptions.Clo.z3AtFlag)
+ AppendCmdLineOption(cmdLineArgsBldr, "@ ");
+
+ if (0 <= CommandLineOptions.Clo.ProverCCLimit)
+ AppendCmdLineOption(cmdLineArgsBldr, "cex", CommandLineOptions.Clo.ProverCCLimit);
+
if (0 <= opts.Timeout) {
- z3args += " " + OptionChar() + "t:" + opts.Timeout;
- }
- if (opts.Typed) {
- AddOption(parms, "TYPE_CHECK", "true");
- if (opts.BitVectors == CommandLineOptions.BvHandling.Z3Native) {
- if (opts.V2) {
- AddOption(parms, "BV_REFLECT", "true");
- } else {
- AddOption(parms, "REFLECT_BV_OPS", "true");
- }
- }
+ AppendCmdLineOption(cmdLineArgsBldr, "t", opts.Timeout);
}
if (CommandLineOptions.Clo.PrintErrorModel >= 1 ||
CommandLineOptions.Clo.EnhancedErrorMessages == 1 ||
CommandLineOptions.Clo.ContractInfer ||
CommandLineOptions.Clo.LazyInlining > 0 ||
CommandLineOptions.Clo.StratifiedInlining > 0) {
- z3args += " " + OptionChar() + "m";
- //expectingModel = true;
- }
- if (CommandLineOptions.Clo.LazyInlining == 2) {
- z3args += " " + OptionChar() + "nw";
- AddOption(parms, "MACRO_EXPANSION", "true");
+ AppendCmdLineOption(cmdLineArgsBldr, "m");
+ expectingModel = true;
}
-
+
// Z3 version 1.3 does not support SETPARAMETER in the input, so we tack on the OPTION=value pairs to z3args
if (opts.V1) {
- foreach (OptionValue opt in parms) {
- z3args += string.Format(" \"{0}={1}\"", opt.Option, opt.Value);
- }
+ foreach (OptionValue opt in result)
+ cmdLineArgsBldr.Append(" \"").Append(opt.Option).Append('=').Append(opt.Value).Append('\"');
}
foreach (string opt in CommandLineOptions.Clo.Z3Options) {
@@ -287,36 +167,51 @@ void ObjectInvariant() // - some options (like TRACE) work only from command line
// Also options with spaces do not work with (SETPARAMETER ...)
if (eq > 0 && opt.IndexOf(" ") < 0 && 'A' <= opt[0] && opt[0] <= 'Z') {
- AddOption(parms, opt.Substring(0, eq), opt.Substring(eq + 1));
+ AddOption(result, opt.Substring(0, eq), opt.Substring(eq + 1));
}
- z3args += " \"" + opt + "\"";
+ cmdLineArgsBldr.Append(" \"").Append(opt).Append('\"');
}
+ cmdLineArgs = cmdLineArgsBldr.ToString();
+ return result;
+ }
- //cmdLineArgs = z3args;
- //parameterSettings = parms;
-
- ProcessStartInfo psi = new ProcessStartInfo(opts.ExeName, z3args);
- Contract.Assert(psi != null);
- psi.CreateNoWindow = true;
- psi.UseShellExecute = false;
- psi.RedirectStandardInput = true;
- psi.RedirectStandardOutput = true;
- psi.RedirectStandardError = true;
-
- return psi;
+ //[NotDelayed]
+ [Captured]
+ public Z3ProverProcess(Z3InstanceOptions opts, Inspector inspector)
+ : base(ComputeProcessStartInfo(opts), opts.ExeName) { // throws ProverException
+ Contract.Requires(opts != null);
+ Contract.Requires(inspector == null || cce.Owner.Same(opts, inspector));
+ this.parameterSettings = CreateParameterListForOptions(opts, inspector, out this.cmdLineArgs, out expectingModel);
+ cce.Owner.AssignSame(this, opts);
+ this.opts = opts;
+ this.inspector = inspector;
}
-
- public override string OptionComments()
+
+ private static ProcessStartInfo ComputeProcessStartInfo(Z3InstanceOptions opts)
{
+ string cmdLineArgs;
+ bool dummy;
+ CreateParameterListForOptions(opts, null, out cmdLineArgs, out dummy);
+ return new ProcessStartInfo(opts.ExeName, cmdLineArgs)
+ {
+ CreateNoWindow = true,
+ UseShellExecute = false,
+ RedirectStandardInput = true,
+ RedirectStandardOutput = true,
+ RedirectStandardError = true
+ };
+ }
+
+ public override string OptionComments() {
Contract.Ensures(Contract.Result<string>() != null);
StringBuilder sb = new StringBuilder();
sb.AppendFormat("Z3 command line: {0} {1}\nUser supplied Z3 options:",
opts.ExeName, cmdLineArgs);
- Contract.Assume( cce.IsPeerConsistent(CommandLineOptions.Clo));
+ Contract.Assume(cce.IsPeerConsistent(CommandLineOptions.Clo));
foreach (string opt in CommandLineOptions.Clo.Z3Options) {
- Contract.Assert(opt!=null);
+ Contract.Assert(opt != null);
sb.Append(" ").Append(opt);
}
sb.AppendFormat("\nProver options: {0}\n", opts.ToString());
@@ -326,7 +221,7 @@ void ObjectInvariant() //[Pure(false)]
public override IEnumerable<string/*!>!*/> ParameterSettings {
get {
- Contract.Ensures(cce.NonNullElements( Contract.Result<IEnumerable<string>>()));
+ Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<string>>()));
if (opts.V2) {
foreach (OptionValue opt in parameterSettings) {
@@ -340,7 +235,7 @@ void ObjectInvariant() private static string OptionChar() {
Contract.Ensures(Contract.Result<string>() != null);
- Contract.Assume( Environment.OSVersion != null);
+ Contract.Assume(Environment.OSVersion != null);
switch (Environment.OSVersion.Platform) {
case PlatformID.Unix:
return "-";
@@ -349,8 +244,7 @@ void ObjectInvariant() }
}
- protected override void DoBeginCheck(string descriptiveName, string formula)
- {
+ protected override void DoBeginCheck(string descriptiveName, string formula) {
Contract.Requires(descriptiveName != null);
Contract.Requires(formula != null);
ToWriteLine(formula);
@@ -358,24 +252,21 @@ void ObjectInvariant() ToFlush();
}
- protected int TimedFromReadChar()
- {
+ protected int TimedFromReadChar() {
if (opts.Timeout > 0)
return FromReadChar((opts.Timeout + 1) * 1000);
else
return FromReadChar();
}
- private void Trace(string msg)
- {
+ private void Trace(string msg) {
Contract.Requires(msg != null);
Console.WriteLine("Z3: " + msg);
}
- public override ProverOutcome CheckOutcome(Microsoft.Boogie.ProverInterface.ErrorHandler handler)
- {
- Contract.Requires(handler != null);
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
+ public override ProverOutcome CheckOutcome(Microsoft.Boogie.ProverInterface.ErrorHandler handler) {
+ Contract.Requires(handler != null);
+ Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
//ProverOutcome outcome;
bool isInvalid = false;
@@ -404,10 +295,10 @@ void ObjectInvariant() Trace("INPUT: " + line);
}
- if (line.StartsWith("WARNING: Out of allocated virtual memory.")) {
- handler.OnResourceExceeded("memory");
- return ProverOutcome.OutOfMemory;
- }
+ if (line.StartsWith("WARNING: Out of allocated virtual memory.")) {
+ handler.OnResourceExceeded("memory");
+ return ProverOutcome.OutOfMemory;
+ }
if (line.StartsWith("WARNING: ")) {
@@ -423,8 +314,7 @@ void ObjectInvariant() }
int beg = 0;
- while (beg < line.Length && '0' <= line[beg] && line[beg] <= '9')
- {
+ while (beg < line.Length && '0' <= line[beg] && line[beg] <= '9') {
cce.LoopInvariant(beg <= line.Length);
beg++;
}
@@ -475,7 +365,7 @@ void ObjectInvariant() Trace("model parsed, final line " + line);
}
// Z3 always ends the model with END_OF_MODEL, not with labels: or .
- Contract.Assume( line == "END_OF_MODEL");
+ Contract.Assume(line == "END_OF_MODEL");
} else {
throw new UnexpectedProverOutputException(string.Format("evil input from z3 (expecting partitions): '{0}'", line));
}
@@ -487,7 +377,7 @@ void ObjectInvariant() throw new UnexpectedProverOutputException(string.Format("evil input from z3: '{0}'", line));
}
}
-
+
/* ----------------------------------------------------------------------------
BNF Grammar to parse Z3 output, including the model generated when using the /m /si switch:
@@ -516,8 +406,8 @@ void ObjectInvariant() //TODO: modifies this.*;
//throws UnexpectedProverOutputException;
{
- Contract.Ensures(Contract.Result<string>() == "." || Contract.Result<string>().StartsWith("labels: (") || Contract.Result<string>() == "END_OF_MODEL");
- Contract.Ensures(Contract.Result<string>() != null);
+ Contract.Ensures(Contract.Result<string>() == "." || Contract.Result<string>().StartsWith("labels: (") || Contract.Result<string>() == "END_OF_MODEL");
+ Contract.Ensures(Contract.Result<string>() != null);
//Format in the grammar:
// ZID ["{" ID+"}"] ["->" "(" (number | false | true) ")"]
@@ -535,8 +425,7 @@ void ObjectInvariant() int ch;
// read the MAPPING
- for (int zID = 0; true; zID++)
- {
+ for (int zID = 0; true; zID++) {
ch = FromReadChar();
if (ch == 'f') {
break;
@@ -559,13 +448,13 @@ void ObjectInvariant() List<List<string/*!*/>>/*!*/ partitionToIdentifiers,
List<Object>/*!*/ partitionToValue,
Dictionary<Object, int>/*!*/ valueToPartition)
- //TODO: modifies this.*, identifierToPartition.*, partitionToIdentifiers.*, partitionToValue.*, valueToPartition.*;
+ //TODO: modifies this.*, identifierToPartition.*, partitionToIdentifiers.*, partitionToValue.*, valueToPartition.*;
{
- Contract.Requires(partitionToValue != null);
+ Contract.Requires(partitionToValue != null);
Contract.Requires(valueToPartition != null);
Contract.Requires(cce.NonNullElements(identifierToPartition));
Contract.Requires(cce.NonNullElements(partitionToIdentifiers));
- Contract.Requires(cce.Owner.Same(cce.Owner.ElementProxy(partitionToValue), cce.Owner.ElementProxy(valueToPartition)));
+ Contract.Requires(cce.Owner.Same(cce.Owner.ElementProxy(partitionToValue), cce.Owner.ElementProxy(valueToPartition)));
string s = FromReadLine();
{
// sanity check
@@ -573,44 +462,44 @@ void ObjectInvariant() string n = s;
int k;
if (pos >= 0) {
- n = s.Substring(0,pos);
+ n = s.Substring(0, pos);
}
- if (! (int.TryParse(n, out k) && zID == k)) {
+ if (!(int.TryParse(n, out k) && zID == k)) {
System.Console.WriteLine("mismatch: {0}!={1} '{2}'", zID, k, s);
- Contract.Assume( false);
+ Contract.Assume(false);
}
}
-
+
int j = ParseModelZidAndIdentifiers(zID, s, identifierToPartition, partitionToIdentifiers);
-
+
j = s.IndexOf(" -> ", j);
if (0 <= j) {
j += 4;
}
- Contract.Assume( j == -1 || j < s.Length); // if ' -> ' is present, then more should remain of the line
+ Contract.Assume(j == -1 || j < s.Length); // if ' -> ' is present, then more should remain of the line
if (j == -1) {
// no "-> " found, end of this line, store that there is no value:
partitionToValue.Add(null);
int idForNull;
if (identifierToPartition.TryGetValue("nullObject", out idForNull) && idForNull == zID) {
- Contract.Assume( !valueToPartition.ContainsKey("nullObject")); // a RHS value should occur only once in the Z3 output
+ Contract.Assume(!valueToPartition.ContainsKey("nullObject")); // a RHS value should occur only once in the Z3 output
valueToPartition.Add("nullObject", zID);
// In this case partitionToValue (as the reverse of valueToPartition) should include
// a map from zID -> "nullObject", but doing that breaks printing out the model as
// it is printed out by Z3. Also, that information is not required, valueToPartition
// works well enough by itself.
}
-
+
} else if (s[j] == 't'/*rue*/) {
partitionToValue.Add(true);
object boxedTrue = true;
- Contract.Assume( !valueToPartition.ContainsKey(boxedTrue)); // a RHS value should occur only once in the Z3 output
+ Contract.Assume(!valueToPartition.ContainsKey(boxedTrue)); // a RHS value should occur only once in the Z3 output
valueToPartition.Add(boxedTrue, zID);
} else if (s[j] == 'f'/*alse*/) {
object boxedFalse = false;
cce.Owner.AssignSame(boxedFalse, cce.Owner.ElementProxy(partitionToValue));
partitionToValue.Add(boxedFalse);
- Contract.Assume( !valueToPartition.ContainsKey(boxedFalse)); // a RHS value should occur only once in the Z3 output
+ Contract.Assume(!valueToPartition.ContainsKey(boxedFalse)); // a RHS value should occur only once in the Z3 output
valueToPartition.Add(boxedFalse, zID);
} else if (s[j] == 'v') {
// -> val!..., i.e. no value
@@ -618,29 +507,29 @@ void ObjectInvariant() } else if (s[j] == '{') {
// array
List<List<int>/*!*/> arrayModel = new List<List<int>/*!*/>();
- Contract.Assert(Contract.ForAll(arrayModel,a=>cce.NonNullElements(a)));
- string array = s.Substring(j+1);
+ Contract.Assert(Contract.ForAll(arrayModel, a => cce.NonNullElements(a)));
+ string array = s.Substring(j + 1);
int index1, index2;
string from, to;
List<int> tuple = new List<int>();
while (0 <= array.IndexOf(';')) {
index1 = array.IndexOf('*') + 1;
index2 = array.IndexOf(' ');
- from = array.Substring(index1, index2-index1);
+ from = array.Substring(index1, index2 - index1);
tuple.Add(int.Parse(from));
array = array.Substring(index2);
index1 = array.IndexOf('*') + 1;
index2 = array.IndexOf(';');
- to = array.Substring(index1, index2-index1);
- array = array.Substring(index2+2);
+ to = array.Substring(index1, index2 - index1);
+ array = array.Substring(index2 + 2);
tuple.Add(int.Parse(to));
arrayModel.Add(tuple);
tuple = new List<int>();
}
- Contract.Assert(array.StartsWith("else ->"));
+ Contract.Assert(array.StartsWith("else ->"));
index1 = array.IndexOf('*') + 1;
index2 = array.IndexOf('}');
- to = array.Substring(index1, index2-index1);
+ to = array.Substring(index1, index2 - index1);
tuple.Add(int.Parse(to));
arrayModel.Add(tuple);
partitionToValue.Add(arrayModel);
@@ -658,7 +547,7 @@ void ObjectInvariant() } else {
l = numberOrBv.IndexOf('[', 0);
if (0 <= l) {
- number = numberOrBv.Substring(2, l-2);
+ number = numberOrBv.Substring(2, l - 2);
int closingBracePosition = numberOrBv.IndexOf(']', l);
if (l < closingBracePosition)
type = "bv" + numberOrBv.Substring(l + 1, closingBracePosition - l - 1);
@@ -671,20 +560,20 @@ void ObjectInvariant() if (type == "int") {
object boxedN = BigNum.FromString(number);
- Contract.Assume( cce.Owner.None(boxedN));
+ Contract.Assume(cce.Owner.None(boxedN));
cce.Owner.AssignSame(boxedN, cce.Owner.ElementProxy(partitionToValue));
partitionToValue.Add(boxedN);
- Contract.Assume( !valueToPartition.ContainsKey(boxedN)); // a RHS value should occur only once in the Z3 output
- valueToPartition.Add(boxedN, zID); + Contract.Assume(!valueToPartition.ContainsKey(boxedN)); // a RHS value should occur only once in the Z3 output
+ valueToPartition.Add(boxedN, zID);
} else if (type.StartsWith("bv") && BigNum.TryParse(number, out bvVal) && int.TryParse(type.Substring(2), out bvSize)) {
BvConst bitV = new BvConst(bvVal, bvSize);
cce.Owner.AssignSame(bitV, cce.Owner.ElementProxy(partitionToValue));
partitionToValue.Add(bitV);
- Contract.Assume( !valueToPartition.ContainsKey(bitV)); // a RHS value should occur only once in the Z3 output
+ Contract.Assume(!valueToPartition.ContainsKey(bitV)); // a RHS value should occur only once in the Z3 output
valueToPartition.Add(bitV, zID);
} else {
System.Console.WriteLine("cannot parse type: '{0}':'{1}'", number, type);
- Contract.Assume( false);
+ Contract.Assume(false);
}
}
@@ -696,34 +585,34 @@ void ObjectInvariant() //TODO: modifies identifierToPartition.*, partitionToIdentifiers.*;
//TODO: Find all modifies statements
{
- Contract.Requires(identifierToPartition!=null&&cce.NonNullElements(identifierToPartition.Keys));
- Contract.Requires(partitionToIdentifiers!=null&& Contract.ForAll(partitionToIdentifiers, identifier=>cce.NonNullElements(identifier)));
- Contract.Requires(s != null);
- Contract.Ensures(0 <= Contract.Result<int>() && Contract.Result<int>() <= s.Length);
-
+ Contract.Requires(identifierToPartition != null && cce.NonNullElements(identifierToPartition.Keys));
+ Contract.Requires(partitionToIdentifiers != null && Contract.ForAll(partitionToIdentifiers, identifier => cce.NonNullElements(identifier)));
+ Contract.Requires(s != null);
+ Contract.Ensures(0 <= Contract.Result<int>() && Contract.Result<int>() <= s.Length);
+
List<string/*!*/> identifiers = new List<string/*!*/>();
int arrowIndex = s.IndexOf('>');
- Contract.Assert(0 < arrowIndex);
+ Contract.Assert(0 < arrowIndex);
int j = s.IndexOf('{', 0) + 1; // skip the '{', if present, and set j to 0 otherwise
if (1 <= j && j < arrowIndex) {
// There is a list of ID's.
- Contract.Assume( j < s.Length); // there should be more characters; the ending '}', for one
+ Contract.Assume(j < s.Length); // there should be more characters; the ending '}', for one
//ID*
- while (true)
- {Contract.Invariant(cce.IsPeerConsistent( identifiers) && cce.IsPeerConsistent(identifierToPartition) && cce.IsPeerConsistent(partitionToIdentifiers));
+ while (true) {
+ Contract.Invariant(cce.IsPeerConsistent(identifiers) && cce.IsPeerConsistent(identifierToPartition) && cce.IsPeerConsistent(partitionToIdentifiers));
Contract.Invariant(0 <= j && j < s.Length);
- int k = s.IndexOfAny(new char[]{' ', '}'}, j);
- Contract.Assume( j <= k);
- string id = s.Substring(j, k-j);
- j = k+1;
- Contract.Assume( !identifierToPartition.ContainsKey(id)); // an ID is listed only once in this list, and an ID can only belong to one ZID equivalence class
+ int k = s.IndexOfAny(new char[] { ' ', '}' }, j);
+ Contract.Assume(j <= k);
+ string id = s.Substring(j, k - j);
+ j = k + 1;
+ Contract.Assume(!identifierToPartition.ContainsKey(id)); // an ID is listed only once in this list, and an ID can only belong to one ZID equivalence class
identifierToPartition.Add(id, zID);
identifiers.Add(id);
if (s[k] == '}') {
// end of reading ID*
break;
}
- Contract.Assume( j < s.Length); // there should be more characters; the ending '}', for one
+ Contract.Assume(j < s.Length); // there should be more characters; the ending '}', for one
}//end ID*
} else {
j = 0;
@@ -732,27 +621,26 @@ void ObjectInvariant() partitionToIdentifiers.Add(identifiers);
return j;
}
-
+
private string ParseModelFunctions(int ch, out Z3ErrorModel errModel,
Dictionary<string/*!*/, int>/*!*/ identifierToPartition,
List<List<string/*!*/>>/*!*/ partitionToIdentifiers,
List<Object>/*!*/ partitionToValue,
Dictionary<Object, int>/*!*/ valueToPartition
- )
+ )
//TODO: modifies this.*;
-
{
- Contract.Requires(identifierToPartition!=null&&cce.NonNullElements(identifierToPartition.Keys));
- Contract.Requires(partitionToIdentifiers!=null&& Contract.ForAll(partitionToIdentifiers, identifier=>cce.NonNullElements(identifier)));
- Contract.Requires(partitionToValue!=null);
- Contract.Requires(valueToPartition!=null);
- Contract.Ensures(Contract.Result<string>() != null);
- Contract.Ensures(Contract.Result<string>() == "." || Contract.Result<string>().StartsWith("labels: (") || Contract.Result<string>() == "END_OF_MODEL");
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
+ Contract.Requires(identifierToPartition != null && cce.NonNullElements(identifierToPartition.Keys));
+ Contract.Requires(partitionToIdentifiers != null && Contract.ForAll(partitionToIdentifiers, identifier => cce.NonNullElements(identifier)));
+ Contract.Requires(partitionToValue != null);
+ Contract.Requires(valueToPartition != null);
+ Contract.Ensures(Contract.Result<string>() != null);
+ Contract.Ensures(Contract.Result<string>() == "." || Contract.Result<string>().StartsWith("labels: (") || Contract.Result<string>() == "END_OF_MODEL");
+ Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
// read the function F
Expect(ch, "function interpretations:");
FromReadLine();
-
+
// mapping of function names to function definitions
Dictionary<string/*!*/, List<List<int>>/*!*/> definedFunctions = new Dictionary<string/*!*/, List<List<int>>/*!*/>();
// function definition given as list of 'pointwise definitions' in the form of the arguments and result
@@ -760,10 +648,9 @@ void ObjectInvariant() List<List<int>> functionDefinition = new List<List<int>>();
// list of arguments, followed by the result, the last element of this list is always the result
List<int> argumentsAndResult = new List<int>();
-
+
// read F
- while (true)
- {
+ while (true) {
functionDefinition = new List<List<int>>();
string s = FromReadLine();
// end of F, "END_OF_MODEL" ends model, '.' ends whole VC, 'l' starts a new set of labels and model
@@ -774,30 +661,27 @@ void ObjectInvariant() return s;
}
int j = s.IndexOf(' ', 0);
- Contract.Assume( 0 <= j);
+ Contract.Assume(0 <= j);
string id = s.Substring(0, j);
// id is stored into definedFunctions once the function definition for it has
// been completely parsed.
-
- if (s.IndexOf("-> {") < 0)
- {
+
+ if (s.IndexOf("-> {") < 0) {
// This function was a macro and we are not parsing its definition currently.
// Just move on to the next function.
- while (true)
- {
+ while (true) {
s = FromReadLine();
if (0 <= s.IndexOf("{" + id + "}"))
break;
}
continue;
}
-
+
// just ignore the "-> {" by dropping string s
string zIDstring;
-
+
// MAPLET
- while (true)
- {
+ while (true) {
argumentsAndResult = new List<int>();
// remove the 2 spaces that are here
FromReadChar();
@@ -805,35 +689,35 @@ void ObjectInvariant() s = FromReadLine();
if (s.StartsWith("else ->")) break;
j = 0;
-
+
//ZID*
- while(true)
- {Contract.Invariant( 0 <= j && j <= s.Length);
-
- j = s.IndexOfAny(new Char[]{'*', '-'}, j);
+ while (true) {
+ Contract.Invariant(0 <= j && j <= s.Length);
+
+ j = s.IndexOfAny(new Char[] { '*', '-' }, j);
// true because this always ends with a "->":
- Contract.Assume( 0 <= j);
-
+ Contract.Assume(0 <= j);
+
// reading -> means end of ZID*
if (s[j] == '-'/*>*/) break;
-
+
// start reading the ZID* with the number, not the *
j = j + 1;
// by input string format:
- Contract.Assume( j < s.Length);
+ Contract.Assume(j < s.Length);
int k = s.IndexOf(' ', j);
// by input string format:
- Contract.Assume( j <= k);
- zIDstring = s.Substring(j, k-j);
+ Contract.Assume(j <= k);
+ zIDstring = s.Substring(j, k - j);
// add the arguments
argumentsAndResult.Add(int.Parse(zIDstring));
j = k;
}// end ZID*
-
+
// j is the beginning of "-> *", we want the first character after this
j = j + 4;
// by input string format:
- Contract.Assume( j <= s.Length);
+ Contract.Assume(j <= s.Length);
zIDstring = s.Substring(j);
// add the result
argumentsAndResult.Add(int.Parse(zIDstring));
@@ -843,7 +727,7 @@ void ObjectInvariant() // this is the 'else -> #unspecified' case
// by input string format:
- Contract.Assume( s.IndexOf("#unspec") >= 0);
+ Contract.Assume(s.IndexOf("#unspec") >= 0);
// this stores the else line as another argumentsAndResult list
argumentsAndResult = new List<int>();
argumentsAndResult.Add(partitionToIdentifiers.Count - 1); // use the fake partition we have created before
@@ -851,23 +735,23 @@ void ObjectInvariant() cce.Owner.AssignSame(argumentsAndResult, cce.Owner.ElementProxy(functionDefinition));
functionDefinition.Add(argumentsAndResult);
- /*
- // this is the 'else -> *' case, that string is already in s
- j = s.IndexOf('*', 0) + 1;
- // by input string format:
- assume 0 < j && j < s.Length;
- zIDstring = s.Substring(j);
- // this stores the else line as another argumentsAndResult list
- argumentsAndResult = new List<int>();
- argumentsAndResult.Add(int.Parse(zIDstring));
- // which is then added to the function definition, which is now complete
- functionDefinition.Add(argumentsAndResult); */
+ /*
+ // this is the 'else -> *' case, that string is already in s
+ j = s.IndexOf('*', 0) + 1;
+ // by input string format:
+ assume 0 < j && j < s.Length;
+ zIDstring = s.Substring(j);
+ // this stores the else line as another argumentsAndResult list
+ argumentsAndResult = new List<int>();
+ argumentsAndResult.Add(int.Parse(zIDstring));
+ // which is then added to the function definition, which is now complete
+ functionDefinition.Add(argumentsAndResult); */
// and therefore added to the map of defined functions, together with the name 'id'
// which had been extracted before
- Contract.Assume( !definedFunctions.ContainsKey(id)); // each function name in the model is listed only once
+ Contract.Assume(!definedFunctions.ContainsKey(id)); // each function name in the model is listed only once
definedFunctions.Add(id, functionDefinition);
-
+
// read the line with "}"
ch = FromReadChar();
Expect(ch, "}");
@@ -878,20 +762,19 @@ void ObjectInvariant() }
- public class Z3ErrorModel : ErrorModel
+ public class Z3ErrorModel : ErrorModel
{
public Z3ErrorModel(Dictionary<string/*!*/, int>/*!*/ identifierToPartition,
List<List<string/*!*/>>/*!*/ partitionToIdentifiers,
List<Object>/*!*/ partitionToValue,
Dictionary<object, int>/*!*/ valueToPartition,
Dictionary<string/*!*/, List<List<int>>/*!*/>/*!*/ definedFunctions)
- : base(identifierToPartition, partitionToIdentifiers, partitionToValue, valueToPartition, definedFunctions)
- {
- Contract.Requires(identifierToPartition!=null&&cce.NonNullElements(identifierToPartition.Keys));
- Contract.Requires(partitionToIdentifiers!=null&&Contract.ForAll(partitionToIdentifiers,x=>cce.NonNullElements(x)));
+ : base(identifierToPartition, partitionToIdentifiers, partitionToValue, valueToPartition, definedFunctions) {
+ Contract.Requires(identifierToPartition != null && cce.NonNullElements(identifierToPartition.Keys));
+ Contract.Requires(partitionToIdentifiers != null && Contract.ForAll(partitionToIdentifiers, x => cce.NonNullElements(x)));
Contract.Requires(partitionToValue != null);
- Contract.Requires(valueToPartition!=null);
- Contract.Requires(definedFunctions!=null&&cce.NonNullElements(definedFunctions.Keys)&&cce.NonNullElements(definedFunctions.Values));
+ Contract.Requires(valueToPartition != null);
+ Contract.Requires(definedFunctions != null && cce.NonNullElements(definedFunctions.Keys) && cce.NonNullElements(definedFunctions.Values));
this.partitionNames = new string/*?*/[partitionToIdentifiers.Count];
this.prevPartitionNames = new string/*?*/[partitionToIdentifiers.Count];
@@ -901,15 +784,13 @@ void ObjectInvariant() private string/*?*/[]/*!*/ prevPartitionNames;
[ContractInvariantMethod]
-void ObjectInvariant()
-{
- Contract.Invariant(partitionNames!=null);
- Contract.Invariant(prevPartitionNames!=null);
-}
+ void ObjectInvariant() {
+ Contract.Invariant(partitionNames != null);
+ Contract.Invariant(prevPartitionNames != null);
+ }
- private void SetNames()
- {
+ private void SetNames() {
int len = partitionToIdentifiers.Count;
for (int i = 0; i < 3; ++i) { // let the names stabilize a bit
prevPartitionNames = partitionNames;
@@ -919,19 +800,17 @@ void ObjectInvariant() }
}
- private int NameBadness(string name)
- {
- Contract.Requires(name!=null);
+ private int NameBadness(string name) {
+ Contract.Requires(name != null);
int badness = name.Length;
if (name.StartsWith("call") && name.IndexOf("formal@") > 0)
badness += 1000;
- if (name.IndexOf ("(") > 0)
+ if (name.IndexOf("(") > 0)
badness += 500;
return badness;
}
- private string GetPartitionName(int pos)
- {
+ private string GetPartitionName(int pos) {
Contract.Ensures(Contract.Result<string>() != null);
string name = partitionNames[pos];
@@ -941,7 +820,7 @@ void ObjectInvariant() object tmp = partitionToValue[pos];
if (tmp != null) {
- partitionNames[pos] = tmp is BvConst ? ((BvConst)tmp).ToReadableString() : tmp.ToString();
+ partitionNames[pos] = tmp is BvConst ? ((BvConst)tmp).ToReadableString() : tmp.ToString();
} else {
List<string/*!*/>/*!*/ possible_names = new List<string/*!*/>();
List<string/*!*/> pti = partitionToIdentifiers[pos];
@@ -954,17 +833,17 @@ void ObjectInvariant() if (pti != null && pti.Count > 0) {
// add identifiers
- foreach (string n in pti)
- {
- Contract.Assert(n!=null);
- possible_names.Add(n);}
+ foreach (string n in pti) {
+ Contract.Assert(n != null);
+ possible_names.Add(n);
+ }
}
// Then also look for functions,
// and then collect possible functional definitions
foreach (KeyValuePair<string/*!*/, List<List<int>>/*!*/> kv in definedFunctions) {
- Contract.Assert(kv.Key!=null);
- Contract.Assert(kv.Value!=null);
+ Contract.Assert(kv.Key != null);
+ Contract.Assert(kv.Value != null);
foreach (List<int> parms in kv.Value) {
if (parms.Count > 1 && parms[parms.Count - 1] == pos) {
string s = kv.Key + "(";
@@ -981,9 +860,10 @@ void ObjectInvariant() // choose the shortest possible name
if (possible_names.Count > 0) {
string best = possible_names[0];
- foreach (string s in possible_names){
- Contract.Assert(s!=null);
- if (NameBadness(s) < NameBadness(best)) best = s;}
+ foreach (string s in possible_names) {
+ Contract.Assert(s != null);
+ if (NameBadness(s) < NameBadness(best)) best = s;
+ }
if (best.Length < 120)
partitionNames[pos] = best;
}
@@ -991,20 +871,20 @@ void ObjectInvariant() return cce.NonNull(partitionNames[pos]);
}
-
- private void PrintReadableModel (TextWriter writer) {
- Contract.Requires(writer!=null);
+
+ private void PrintReadableModel(TextWriter writer) {
+ Contract.Requires(writer != null);
writer.WriteLine("Z3 error model: ");
SetNames();
writer.WriteLine("partitions:");
- Contract.Assert(partitionToIdentifiers.Count == partitionToValue.Count);
- for (int i = 0; i < partitionToIdentifiers.Count; i++){
- writer.Write("{0,5}: {1} ", "*"+i, GetPartitionName(i));
+ Contract.Assert(partitionToIdentifiers.Count == partitionToValue.Count);
+ for (int i = 0; i < partitionToIdentifiers.Count; i++) {
+ writer.Write("{0,5}: {1} ", "*" + i, GetPartitionName(i));
List<string/*!*/> pti = partitionToIdentifiers[i];
Contract.Assert(cce.NonNullElements(pti));
if (pti != null && (pti.Count > 1 || (pti.Count == 1 && partitionToValue[i] != null))) {
writer.Write("{");
- for (int k = 0; k < pti.Count - 1; k ++) {
+ for (int k = 0; k < pti.Count - 1; k++) {
writer.Write(pti[k] + " ");
}
//extra work to make sure no " " is at the end of the list of identifiers
@@ -1021,10 +901,10 @@ void ObjectInvariant() List<string> funNames = new List<string>(definedFunctions.Keys);
funNames.Sort();
foreach (string name in funNames) {
- Contract.Assert(name!=null);
+ Contract.Assert(name != null);
if (definedFunctions[name].Count == 1) continue; // skip functions with only the else-> clause
foreach (List<int> parms in definedFunctions[name]) {
- Contract.Assert(parms!=null);
+ Contract.Assert(parms != null);
string s = name + "(";
if (parms.Count == 1) {
continue;
@@ -1047,8 +927,8 @@ void ObjectInvariant() writer.WriteLine();
}
- public override void Print (TextWriter writer) {
- Contract.Requires(writer!=null);
+ public override void Print(TextWriter writer) {
+ Contract.Requires(writer != null);
if (CommandLineOptions.Clo.PrintErrorModel == 4) {
PrintReadableModel(writer);
return;
@@ -1057,13 +937,13 @@ void ObjectInvariant() writer.WriteLine("Z3 error model: ");
writer.WriteLine("partitions:");
- Contract.Assert(partitionToIdentifiers.Count == partitionToValue.Count);
- for (int i = 0; i < partitionToIdentifiers.Count; i++){
- writer.Write("*"+i);
+ Contract.Assert(partitionToIdentifiers.Count == partitionToValue.Count);
+ for (int i = 0; i < partitionToIdentifiers.Count; i++) {
+ writer.Write("*" + i);
List<string> pti = partitionToIdentifiers[i];
if (pti != null && pti.Count != 0) {
writer.Write(" {");
- for (int k = 0; k < pti.Count - 1; k ++) {
+ for (int k = 0; k < pti.Count - 1; k++) {
writer.Write(pti[k] + " ");
}
//extra work to make sure no " " is at the end of the list of identifiers
@@ -1083,15 +963,15 @@ void ObjectInvariant() writer.Write(" -> " + tempPTVI + ":int");
} else if (tempPTVI is List<List<int>>) {
List<List<int>> array = tempPTVI as List<List<int>>;
- Contract.Assume( array != null);
+ Contract.Assume(array != null);
writer.Write(" -> {");
- foreach(List<int> l in array) {
+ foreach (List<int> l in array) {
if (l.Count == 2) {
- writer.Write("*"+l[0] + " -> " + "*"+l[1] + "; ");
+ writer.Write("*" + l[0] + " -> " + "*" + l[1] + "; ");
} else {
- Contract.Assert((l.Count == 1));
- writer.Write("else -> *"+l[0]+"}");
- }
+ Contract.Assert((l.Count == 1));
+ writer.Write("else -> *" + l[0] + "}");
+ }
}
} else {
writer.Write(" -> " + tempPTVI + "");
@@ -1104,20 +984,20 @@ void ObjectInvariant() writer.WriteLine("function interpretations:");
foreach (KeyValuePair<string, List<List<int>>> kvp in definedFunctions) {
- Contract.Assert(kvp.Key!=null);
+ Contract.Assert(kvp.Key != null);
writer.WriteLine(kvp.Key + " -> {");
List<List<int>> kvpValue = kvp.Value;
if (kvpValue != null) {
- foreach(List<int> l in kvpValue) {
+ foreach (List<int> l in kvpValue) {
writer.Write(" ");
if (l != null) {
for (int i = 0; i < l.Count - 1; i++) {
- writer.Write("*"+l[i] + " ");
+ writer.Write("*" + l[i] + " ");
}
if (l.Count == 1) {
writer.WriteLine("else -> #unspecified");
} else {
- writer.WriteLine("-> "+ "*" + l[l.Count - 1]);
+ writer.WriteLine("-> " + "*" + l[l.Count - 1]);
}
}
}
@@ -1126,14 +1006,14 @@ void ObjectInvariant() }
writer.WriteLine("END_OF_MODEL");
writer.WriteLine(".");
-
+
if (CommandLineOptions.Clo.PrintErrorModel >= 2) {
writer.WriteLine("identifierToPartition:");
foreach (KeyValuePair<string, int> kvp in identifierToPartition) {
- Contract.Assert(kvp.Key!=null);
- writer.WriteLine(kvp.Key + " : " + "*" + kvp.Value); + Contract.Assert(kvp.Key != null);
+ writer.WriteLine(kvp.Key + " : " + "*" + kvp.Value);
}
-
+
writer.WriteLine("valueToPartition:");
foreach (KeyValuePair<object, int> kvp in valueToPartition) {
writer.WriteLine(kvp.Key + " : " + "*" + kvp.Value);
@@ -1142,8 +1022,6 @@ void ObjectInvariant() }
}
}
-
-
}
|