diff options
| author |  tabarbe <unknown> | 2010-07-20 22:22:12 +0000 |
|---|---|---|
| committer | tabarbe <unknown> | 2010-07-20 22:22:12 +0000 |
| commit | 5c84bac10a29c07a04e95734c07107423cf33c51 (patch) | |
| tree | 1f3f9cf236e4250763b3f066a3e44ace36b4faa4 /Source/Provers/Z3/Prover.cs | |
| parent | 88382bfc242a7f9d9ac0e698d97c123133ef57dc (diff) | |
Boogie/Z3: Renaming the sources for Z3 in preparation for commit of my port of the project.
Diffstat (limited to 'Source/Provers/Z3/Prover.cs')
| -rw-r--r-- | Source/Provers/Z3/Prover.cs | 942 |
1 files changed, 942 insertions, 0 deletions
diff --git a/Source/Provers/Z3/Prover.cs b/Source/Provers/Z3/Prover.cs new file mode 100644 index 00000000..dbf23a8a --- /dev/null +++ b/Source/Provers/Z3/Prover.cs @@ -0,0 +1,942 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.IO;
+using System.Diagnostics;
+using System.Collections;
+using System.Collections.Generic;
+using System.Text;
+using util;
+using Microsoft.Contracts;
+using Microsoft.Boogie;
+using Microsoft.Boogie.Simplify;
+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;
+ private readonly bool expectingModel = false;
+
+ private string! cmdLineArgs = "";
+ class OptionValue {
+ public readonly string! Option;
+ public readonly string! Value;
+ public OptionValue(string! option, string! value) { Option = option; Value = value; }
+ }
+ static void AddOption(List<OptionValue!>! parms, string! option, string! value)
+ modifies parms.*;
+ {
+ OptionValue ov = new OptionValue(option, value);
+ Owner.AssignSame(ov, Owner.ElementProxy(parms));
+ parms.Add(ov);
+ }
+ private List<OptionValue!>! parameterSettings;
+
+ // [NotDelayed]
+ [Captured]
+ public Z3ProverProcess(Z3InstanceOptions! opts, Inspector? inspector)
+ requires inspector != null ==> Owner.Same(opts, inspector);
+ { // throws ProverException
+ 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");
+ }
+
+ 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) {
+ 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);
+ psi.CreateNoWindow = true;
+ psi.UseShellExecute = false;
+ psi.RedirectStandardInput = true;
+ psi.RedirectStandardOutput = true;
+ psi.RedirectStandardError = true;
+
+ base(psi, opts.ExeName);
+
+ Owner.AssignSame(this, opts);
+ this.opts = opts;
+ this.inspector = inspector;
+ }
+
+ public override string! OptionComments()
+ {
+ StringBuilder sb = new StringBuilder();
+ sb.AppendFormat("Z3 command line: {0} {1}\nUser supplied Z3 options:",
+ opts.ExeName, cmdLineArgs);
+ assume CommandLineOptions.Clo.IsPeerConsistent;
+ foreach (string! opt in CommandLineOptions.Clo.Z3Options) {
+ sb.Append(" ").Append(opt);
+ }
+ sb.AppendFormat("\nProver options: {0}\n", opts.ToString());
+ return sb.ToString();
+ }
+
+ [Pure(false)]
+ public override IEnumerable<string!>! ParameterSettings {
+ get {
+ if (opts.V2) {
+ foreach (OptionValue opt in parameterSettings) {
+ yield return "(SETPARAMETER " + opt.Option + " " + opt.Value + ")";
+ }
+ }
+ }
+ }
+
+ // z3 uses different magic characters for options on linux/unix and on windows
+ private static string! OptionChar() {
+ assume Environment.OSVersion != null;
+ switch (Environment.OSVersion.Platform) {
+ case PlatformID.Unix:
+ return "-";
+ default:
+ return "/";
+ }
+ }
+
+ protected override void DoBeginCheck(string! descriptiveName, string! formula)
+ {
+ ToWriteLine(formula);
+ ToWriteLine(String.Format("; END OF FORMULA {0} - {1}", NumFormulasChecked.ToString(), descriptiveName));
+ ToFlush();
+ }
+
+ protected int TimedFromReadChar()
+ {
+ if (opts.Timeout > 0)
+ return FromReadChar((opts.Timeout + 1) * 1000);
+ else
+ return FromReadChar();
+ }
+
+ private void Trace(string! msg)
+ {
+ Console.WriteLine("Z3: " + msg);
+ }
+
+ public override ProverOutcome CheckOutcome(Microsoft.Boogie.ProverInterface.ErrorHandler! handler)
+ throws UnexpectedProverOutputException;
+ {
+ ProverOutcome outcome;
+ bool isInvalid = false;
+
+ if (this.simplify == null) {
+ return ProverOutcome.Inconclusive;
+ }
+
+
+ while (true) {
+ int ch = TimedFromReadChar();
+ if (ch == -1 && this.readTimedOut) {
+ handler.OnResourceExceeded("timeout (forced)");
+ return ProverOutcome.TimeOut;
+ }
+
+ string line = new string((char)ch, 1) + FromReadLine();
+
+ if (line.StartsWith("STATS ")) {
+ if (inspector != null) {
+ inspector.StatsLine(line);
+ }
+ continue;
+ }
+
+ if (opts.Verbosity > 2) {
+ Trace("INPUT: " + line);
+ }
+
+ if (line.StartsWith("WARNING: Out of allocated virtual memory.")) {
+ handler.OnResourceExceeded("memory");
+ return ProverOutcome.OutOfMemory;
+ }
+
+
+ if (line.StartsWith("WARNING: ")) {
+ string w = line.Substring(9);
+ handler.OnProverWarning(w);
+ continue;
+ }
+
+ if (line.ToUpper().StartsWith("ERROR")) {
+ Console.WriteLine("Z3 returns the following error:");
+ Console.WriteLine(" " + line);
+ return ProverOutcome.Inconclusive;
+ }
+
+ int beg = 0;
+ while (beg < line.Length && '0' <= line[beg] && line[beg] <= '9')
+ invariant beg <= line.Length;
+ {
+ beg++;
+ }
+
+ if (beg > 0 && line.Substring(beg).StartsWith(": ")) {
+ string status = line.Substring(beg + 2);
+
+ if (status.StartsWith("Valid")) {
+ return ProverOutcome.Valid;
+ }
+
+ if (status.StartsWith("Timeout")) {
+ handler.OnResourceExceeded("timeout");
+ return ProverOutcome.TimeOut;
+ }
+
+ if (status.StartsWith("Inconclusive")) {
+ return ProverOutcome.Inconclusive;
+ }
+
+ if (status.StartsWith("Memout")) {
+ handler.OnResourceExceeded("memory");
+ return ProverOutcome.OutOfMemory;
+ }
+
+ if (status.StartsWith("Invalid")) {
+ isInvalid = true;
+ continue;
+ }
+ }
+
+ if (isInvalid && line == ".") {
+ return ProverOutcome.NotValid;
+ }
+
+ if (isInvalid && line.StartsWith("labels: (")) {
+ List<string!>! l = ParseLabels(line);
+ Z3ErrorModel errModel = null;
+ if (expectingModel) {
+ if (opts.Verbosity > 2) {
+ Trace("waiting for model");
+ }
+ line = FromReadLine();
+ if (line.StartsWith("partitions:")) {
+ line = ParseModel(out errModel);
+ if (opts.Verbosity > 2) {
+ Trace("model parsed, final line " + line);
+ }
+ // Z3 always ends the model with END_OF_MODEL, not with labels: or .
+ assume line == "END_OF_MODEL";
+ } else {
+ throw new UnexpectedProverOutputException(string.Format("evil input from z3 (expecting partitions): '{0}'", line));
+ }
+ }
+ handler.OnModel(l, errModel);
+ continue;
+ }
+
+ 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:
+
+ Output ::= VC*
+ VC ::= number ": " "Valid." | number ": " "Inconclusive" | VCI
+ VCI ::= number ": " "Invalid"
+ ("labels: " "(" ID* ")"
+ [MODEL] "END_OF_MODEL")+
+ "."
+ MODEL ::= MBOOL MFUNC
+ MBOOL ::= "boolean assignment:"
+ "partitions:"
+ MAPPING*
+ MAPPING ::= ZID ["{" ID+"}"] ["->" "(" (number | false | true | BITVECTOR) ")"]
+ BITVECTOR ::= ulong ":bv" int
+ MFUNC ::= "function interpretations:"
+ F*
+ F ::= Id "->" "{"
+ MAPLET*
+ "else" "->" ZID
+ "}"
+ MAPLET ::= ZID* "->" ZID
+
+ -----------------------------------------------------------------------------*/
+ private string! ParseModel(out Z3ErrorModel errModel)
+ modifies this.*;
+ ensures result == "." || result.StartsWith("labels: (") || result == "END_OF_MODEL";
+ throws UnexpectedProverOutputException;
+ {
+ //Format in the grammar:
+ // ZID ["{" ID+"}"] ["->" "(" (number | false | true) ")"]
+ // storing the model:
+ // map each ID (a string) to the corresping ZID (an integer) in a dictionary:
+ Dictionary<string!, int> identifierToPartition = new Dictionary<string!, int>();
+ // map each ZID to the set (in list form) of IDs belonging to it (possibly empty):
+ List<List<string!>> partitionToIdentifiers = new List<List<string!>>();
+ // map each ZID to the number or boolean given, if any:
+ List<Object> partitionToValue = new List<Object>();
+ // map each value (number or boolean) to the ZID, reverse map of partitionToValue
+ Dictionary<Object, int> valueToPartition = new Dictionary<Object, int>();
+ Owner.AssignSame(Owner.ElementProxy(partitionToValue), Owner.ElementProxy(valueToPartition));
+
+ int ch;
+
+ // read the MAPPING
+ for (int zID = 0; true; zID++)
+ {
+ ch = FromReadChar();
+ if (ch == 'f') {
+ break;
+ }
+ ParseModelMapping(zID, identifierToPartition, partitionToIdentifiers, partitionToValue, valueToPartition);
+ }// end MAPPING
+
+ // add the fake partition for the 'else -> #undefined' clause
+ List<string!> emptyList = new List<string!>();
+ Owner.AssignSame(emptyList, Owner.ElementProxy(partitionToIdentifiers));
+ partitionToIdentifiers.Add(emptyList);
+ partitionToValue.Add(null);
+
+ // continue in ParseModelFunctions, which breaks up this long method and enables its verification
+ return ParseModelFunctions(ch, out errModel, identifierToPartition, partitionToIdentifiers, partitionToValue, valueToPartition);
+ }
+
+ private void ParseModelMapping(int zID,
+ Dictionary<string!, int>! identifierToPartition,
+ List<List<string!>>! partitionToIdentifiers,
+ List<Object>! partitionToValue,
+ Dictionary<Object, int>! valueToPartition)
+ requires Owner.Same(Owner.ElementProxy(partitionToValue), Owner.ElementProxy(valueToPartition));
+ modifies this.*, identifierToPartition.*, partitionToIdentifiers.*, partitionToValue.*, valueToPartition.*;
+ {
+ string s = FromReadLine();
+ {
+ // sanity check
+ int pos = s.IndexOf(' ');
+ string n = s;
+ int k;
+ if (pos >= 0) {
+ n = s.Substring(0,pos);
+ }
+ if (! (int.TryParse(n, out k) && zID == k)) {
+ System.Console.WriteLine("mismatch: {0}!={1} '{2}'", zID, k, s);
+ assume false;
+ }
+ }
+
+ int j = ParseModelZidAndIdentifiers(zID, s, identifierToPartition, partitionToIdentifiers);
+
+ j = s.IndexOf(" -> ", j);
+ if (0 <= j) {
+ j += 4;
+ }
+ 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) {
+ 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;
+ 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;
+ Owner.AssignSame(boxedFalse, Owner.ElementProxy(partitionToValue));
+ partitionToValue.Add(boxedFalse);
+ 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
+ partitionToValue.Add(null);
+ } else if (s[j] == '{') {
+ // array
+ List<List<int>!> arrayModel = new List<List<int>!>();
+ 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);
+ 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);
+ tuple.Add(int.Parse(to));
+ arrayModel.Add(tuple);
+ tuple = new List<int>();
+ }
+ assert array.StartsWith("else ->");
+ index1 = array.IndexOf('*') + 1;
+ index2 = array.IndexOf('}');
+ to = array.Substring(index1, index2-index1);
+ tuple.Add(int.Parse(to));
+ arrayModel.Add(tuple);
+ partitionToValue.Add(arrayModel);
+ } else {
+ string numberOrBv = s.Substring(j);
+ // make number an int, then store it:
+ BigNum bvVal;
+ int bvSize;
+ string number, type;
+
+ int l = numberOrBv.IndexOf(':', 0);
+ if (0 <= l) {
+ number = numberOrBv.Substring(0, l);
+ type = numberOrBv.Substring(l + 1);
+ } else {
+ l = numberOrBv.IndexOf('[', 0);
+ if (0 <= l) {
+ number = numberOrBv.Substring(2, l-2);
+ int closingBracePosition = numberOrBv.IndexOf(']', l);
+ if (l < closingBracePosition)
+ type = "bv" + numberOrBv.Substring(l + 1, closingBracePosition - l - 1);
+ else type = "int";
+ } else {
+ number = numberOrBv;
+ type = "int";
+ }
+ }
+
+ if (type == "int") {
+ object boxedN = BigNum.FromString(number);
+ assume Owner.None(boxedN);
+ Owner.AssignSame(boxedN, Owner.ElementProxy(partitionToValue));
+ partitionToValue.Add(boxedN);
+ 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);
+ Owner.AssignSame(bitV, Owner.ElementProxy(partitionToValue));
+ partitionToValue.Add(bitV);
+ 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);
+ assume false;
+ }
+
+ }
+ }
+
+ private static int ParseModelZidAndIdentifiers(int zID, string! s,
+ Dictionary<string!, int>! identifierToPartition,
+ List<List<string!>>! partitionToIdentifiers)
+ modifies identifierToPartition.*, partitionToIdentifiers.*;
+ ensures 0 <= result && result <= s.Length;
+ {
+ List<string!> identifiers = new List<string!>();
+ int arrowIndex = s.IndexOf('>');
+ 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.
+ assume j < s.Length; // there should be more characters; the ending '}', for one
+ //ID*
+ while (true)
+ invariant identifiers.IsPeerConsistent && identifierToPartition.IsPeerConsistent && partitionToIdentifiers.IsPeerConsistent;
+ invariant 0 <= j && j < s.Length;
+ {
+ int k = s.IndexOfAny(new char[]{' ', '}'}, j);
+ assume j <= k;
+ string id = s.Substring(j, k-j);
+ j = k+1;
+ 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;
+ }
+ assume j < s.Length; // there should be more characters; the ending '}', for one
+ }//end ID*
+ } else {
+ j = 0;
+ }
+ Owner.AssignSame(identifiers, Owner.ElementProxy(partitionToIdentifiers));
+ 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
+ )
+ modifies this.*;
+ ensures result == "." || result.StartsWith("labels: (") || result == "END_OF_MODEL";
+ throws UnexpectedProverOutputException;
+ {
+ // 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
+ // the last element here will always be a list with just one entry which corresponds to the else case
+ 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)
+ {
+ 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
+ // whenever there is a model this will end with "END_OF_MODEL", the other cases can only
+ // happen when there is no model printed!
+ if (s == "." || s.StartsWith("labels: (") || s == "END_OF_MODEL") {
+ errModel = new Z3ErrorModel(identifierToPartition, partitionToIdentifiers, partitionToValue, valueToPartition, definedFunctions);
+ return s;
+ }
+ int j = s.IndexOf(' ', 0);
+ 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)
+ {
+ // This function was a macro and we are not parsing its definition currently.
+ // Just move on to the next function.
+ while (true)
+ {
+ s = FromReadLine();
+ if (0 <= s.IndexOf("{" + id + "}"))
+ break;
+ }
+ continue;
+ }
+
+ // just ignore the "-> {" by dropping string s
+ string zIDstring;
+
+ // MAPLET
+ while (true)
+ {
+ argumentsAndResult = new List<int>();
+ // remove the 2 spaces that are here
+ FromReadChar();
+ FromReadChar();
+ s = FromReadLine();
+ if (s.StartsWith("else ->")) break;
+ j = 0;
+
+ //ZID*
+ while(true)
+ invariant 0 <= j && j <= s.Length;
+ {
+ j = s.IndexOfAny(new Char[]{'*', '-'}, j);
+ // true because this always ends with a "->":
+ 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:
+ assume j < s.Length;
+ int k = s.IndexOf(' ', j);
+ // by input string format:
+ 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:
+ assume j <= s.Length;
+ zIDstring = s.Substring(j);
+ // add the result
+ argumentsAndResult.Add(int.Parse(zIDstring));
+ // add the input line as another 'pointwise defined' element to the functions definition
+ functionDefinition.Add(argumentsAndResult);
+ }// end MAPLET
+
+ // this is the 'else -> #unspecified' case
+ // by input string format:
+ 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
+ // which is then added to the function definition, which is now complete
+ Owner.AssignSame(argumentsAndResult, 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); */
+
+ // and therefore added to the map of defined functions, together with the name 'id'
+ // which had been extracted before
+ 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, "}");
+ FromReadLine();
+ }// end F
+ }
+
+ }
+
+
+ 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)
+ {
+ this.partitionNames = new string?[partitionToIdentifiers.Count];
+ this.prevPartitionNames = new string?[partitionToIdentifiers.Count];
+ }
+
+ private string?[]! partitionNames;
+ private string?[]! prevPartitionNames;
+
+ private void SetNames()
+ {
+ int len = partitionToIdentifiers.Count;
+ for (int i = 0; i < 3; ++i) { // let the names stabilize a bit
+ prevPartitionNames = partitionNames;
+ partitionNames = new string?[len];
+ for (int pos = 0; pos < len; ++pos)
+ GetPartitionName(pos);
+ }
+ }
+
+ private int NameBadness(string! name)
+ {
+ int badness = name.Length;
+ if (name.StartsWith("call") && name.IndexOf("formal@") > 0)
+ badness += 1000;
+ if (name.IndexOf ("(") > 0)
+ badness += 500;
+ return badness;
+ }
+
+ private string! GetPartitionName(int pos)
+ {
+ string name = partitionNames[pos];
+ if (name != null) {
+ return name;
+ }
+
+ object tmp = partitionToValue[pos];
+ if (tmp != null) {
+ partitionNames[pos] = tmp is BvConst ? ((BvConst)tmp).ToReadableString() : tmp.ToString();
+ } else {
+ List<string!>! possible_names = new List<string!>();
+ List<string!> pti = partitionToIdentifiers[pos];
+
+ // make sure we're not called recursively
+ string prevName = prevPartitionNames[pos];
+ if (prevName == null) prevName = "*" + pos;
+ partitionNames[pos] = prevName;
+
+ if (pti != null && pti.Count > 0) {
+ // add identifiers
+ foreach (string! name in pti)
+ possible_names.Add(name);
+ }
+
+ // Then also look for functions,
+ // and then collect possible functional definitions
+ foreach (KeyValuePair<string!, List<List<int>>!> kv in definedFunctions) {
+ foreach (List<int>! parms in kv.Value) {
+ if (parms.Count > 1 && parms[parms.Count - 1] == pos) {
+ string! s = kv.Key + "(";
+ for (int i = 0; i < parms.Count - 1; ++i) {
+ if (i != 0) s += ", ";
+ s += GetPartitionName(parms[i]);
+ }
+ s += ")";
+ possible_names.Add(s);
+ }
+ }
+ }
+
+ // choose the shortest possible name
+ if (possible_names.Count > 0) {
+ string! best = possible_names[0];
+ foreach (string! s in possible_names)
+ if (NameBadness(s) < NameBadness(best)) best = s;
+ if (best.Length < 120)
+ partitionNames[pos] = best;
+ }
+ }
+
+ return (!)partitionNames[pos];
+ }
+
+ private void PrintReadableModel (TextWriter! writer) {
+ writer.WriteLine("Z3 error model: ");
+ SetNames();
+ writer.WriteLine("partitions:");
+ 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];
+ if (pti != null && (pti.Count > 1 || (pti.Count == 1 && partitionToValue[i] != null))) {
+ writer.Write("{");
+ 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
+ if (pti.Count != 0) {
+ writer.Write(pti[pti.Count - 1]);
+ }
+ writer.Write("}");
+ }
+ writer.WriteLine();
+ }
+
+ writer.WriteLine();
+ writer.WriteLine("function interpretations:");
+ List<string!> funNames = new List<string!>(definedFunctions.Keys);
+ funNames.Sort();
+ foreach (string! name in funNames) {
+ if (definedFunctions[name].Count == 1) continue; // skip functions with only the else-> clause
+ foreach (List<int>! parms in definedFunctions[name]) {
+ string! s = name + "(";
+ if (parms.Count == 1) {
+ continue;
+ // s += "*";
+ } else {
+ for (int i = 0; i < parms.Count - 1; ++i) {
+ if (i != 0) s += ", ";
+ s += GetPartitionName(parms[i]);
+ }
+ }
+ s += ")";
+ string! res = GetPartitionName(parms[parms.Count - 1]);
+ if (res == s)
+ res = "*" + parms[parms.Count - 1] + " (SELF)";
+ writer.WriteLine("{0} = {1}", s, res);
+ }
+ writer.WriteLine();
+ }
+ writer.WriteLine("The end.");
+ writer.WriteLine();
+ }
+
+ public override void Print (TextWriter! writer) {
+ if (CommandLineOptions.Clo.PrintErrorModel == 4) {
+ PrintReadableModel(writer);
+ return;
+ }
+
+ writer.WriteLine("Z3 error model: ");
+
+ writer.WriteLine("partitions:");
+ 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 ++) {
+ writer.Write(pti[k] + " ");
+ }
+ //extra work to make sure no " " is at the end of the list of identifiers
+ if (pti.Count != 0) {
+ writer.Write(pti[pti.Count - 1]);
+ }
+ writer.Write("}");
+ }
+ // temp object needed for non-null checking
+ object tempPTVI = partitionToValue[i];
+ if (tempPTVI != null) {
+ if (tempPTVI.ToString() == "True") {
+ writer.Write(" -> " + "true" + "");
+ } else if (tempPTVI.ToString() == "False") {
+ writer.Write(" -> " + "false" + "");
+ } else if (tempPTVI is BigNum) {
+ writer.Write(" -> " + tempPTVI + ":int");
+ } else if (tempPTVI is List<List<int>!>) {
+ List<List<int>!> array = tempPTVI as List<List<int>!>;
+ assume array != null;
+ writer.Write(" -> {");
+ foreach(List<int> l in array) {
+ if (l.Count == 2) {
+ writer.Write("*"+l[0] + " -> " + "*"+l[1] + "; ");
+ } else {
+ assert (l.Count == 1);
+ writer.Write("else -> *"+l[0]+"}");
+ }
+ }
+ } else {
+ writer.Write(" -> " + tempPTVI + "");
+ }
+ } else {
+ writer.Write(" ");
+ }
+ writer.WriteLine();
+ }
+
+ writer.WriteLine("function interpretations:");
+ foreach (KeyValuePair<string!, List<List<int>>!> kvp in definedFunctions) {
+ writer.WriteLine(kvp.Key + " -> {");
+ List<List<int>> kvpValue = kvp.Value;
+ if (kvpValue != null) {
+ foreach(List<int> l in kvpValue) {
+ writer.Write(" ");
+ if (l != null) {
+ for (int i = 0; i < l.Count - 1; i++) {
+ writer.Write("*"+l[i] + " ");
+ }
+ if (l.Count == 1) {
+ writer.WriteLine("else -> #unspecified");
+ } else {
+ writer.WriteLine("-> "+ "*" + l[l.Count - 1]);
+ }
+ }
+ }
+ }
+ writer.WriteLine("}");
+ }
+ writer.WriteLine("END_OF_MODEL");
+ writer.WriteLine(".");
+
+ if (CommandLineOptions.Clo.PrintErrorModel >= 2) {
+ writer.WriteLine("identifierToPartition:");
+ foreach (KeyValuePair<string!, int> kvp in identifierToPartition) {
+ writer.WriteLine(kvp.Key + " : " + "*" + kvp.Value);
+ }
+
+ writer.WriteLine("valueToPartition:");
+ foreach (KeyValuePair<object, int> kvp in valueToPartition) {
+ writer.WriteLine(kvp.Key + " : " + "*" + kvp.Value);
+ }
+ writer.WriteLine("End of model.");
+ }
+ }
+ }
+
+
+}
+
+
|