diff options
| author |  tabarbe <unknown> | 2010-07-20 22:33:04 +0000 |
|---|---|---|
| committer | tabarbe <unknown> | 2010-07-20 22:33:04 +0000 |
| commit | 815c5f5fb885112a1b4d037e511336735acaa2f5 (patch) | |
| tree | 38dd141d530dfb2469cd26e946af7d0ba28c89cb /Source | |
| parent | 5c84bac10a29c07a04e95734c07107423cf33c51 (diff) | |
Boogie: Rename didn't work. Resetting to try again
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Provers/Z3/Inspector.cs | 136 | ||||
| -rw-r--r-- | Source/Provers/Z3/Prover.cs | 942 | ||||
| -rw-r--r-- | Source/Provers/Z3/ProverInterface.cs | 344 | ||||
| -rw-r--r-- | Source/Provers/Z3/TypeDeclCollector.cs | 280 | ||||
| -rw-r--r-- | Source/Provers/Z3/Z3.csproj | 144 |
5 files changed, 0 insertions, 1846 deletions
diff --git a/Source/Provers/Z3/Inspector.cs b/Source/Provers/Z3/Inspector.cs deleted file mode 100644 index fa1b844e..00000000 --- a/Source/Provers/Z3/Inspector.cs +++ /dev/null @@ -1,136 +0,0 @@ -//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-using System;
-using System.IO;
-using System.Diagnostics;
-using System.Collections;
-using System.Collections.Generic;
-using util;
-using Microsoft.Contracts;
-using Microsoft.Boogie;
-using Microsoft.Boogie.Simplify;
-using Microsoft.Basetypes;
-using Microsoft.Boogie.VCExprAST;
-
-namespace Microsoft.Boogie.Z3
-{
- internal class FindLabelsVisitor : TraversingVCExprVisitor<bool, bool> {
- public Dictionary<string!,bool>! Labels = new Dictionary<string!,bool>();
-
- public static Dictionary<string!,bool>! FindLabels(VCExpr! expr) {
- FindLabelsVisitor! visitor = new FindLabelsVisitor();
- visitor.Traverse(expr, true);
- return visitor.Labels;
- }
-
- protected override bool StandardResult(VCExpr! node, bool arg) {
- VCExprNAry nary = node as VCExprNAry;
- if (nary != null) {
- VCExprLabelOp lab = nary.Op as VCExprLabelOp;
- if (lab != null) {
- Labels[lab.label] = lab.pos;
- }
- }
- return true;
- }
- }
-
- internal class Inspector {
- [Rep] protected readonly Process! inspector;
- [Rep] readonly TextReader! fromInspector;
- [Rep] readonly TextWriter! toInspector;
-
- public Inspector(Z3InstanceOptions! opts)
- {
- ProcessStartInfo! psi = new ProcessStartInfo(opts.Inspector);
- psi.CreateNoWindow = true;
- psi.UseShellExecute = false;
- psi.RedirectStandardInput = true;
- psi.RedirectStandardOutput = true;
- psi.RedirectStandardError = false;
-
- try
- {
- Process inspector = Process.Start(psi);
- this.inspector = inspector;
- fromInspector = inspector.StandardOutput;
- toInspector = inspector.StandardInput;
- }
- catch (System.ComponentModel.Win32Exception e)
- {
- throw new Exception(string.Format("Unable to start the inspector process {0}: {1}", opts.Inspector, e.Message));
- }
- }
-
- public void NewProver()
- {
- }
-
- public void NewProblem(string! descriptiveName, VCExpr! vc, ProverInterface.ErrorHandler! handler)
- {
- Dictionary<string!,bool>! labels = FindLabelsVisitor.FindLabels(vc);
- toInspector.WriteLine("PROBLEM " + descriptiveName);
- toInspector.WriteLine("TOKEN BEGIN");
- foreach (string! lab in labels.Keys) {
- string! no = lab.Substring(1);
- Absy! absy = handler.Label2Absy(no);
- IToken tok = absy.tok;
- AssertCmd assrt = absy as AssertCmd;
- Block blk = absy as Block;
- string val = tok.val; // might require computation, so cache it
- if (val == "foo" || tok.filename == null) continue; // no token
-
- toInspector.Write("TOKEN ");
- toInspector.Write(lab);
- toInspector.Write(" ");
-
- if (assrt != null) {
- toInspector.Write("ASSERT");
- string errData = assrt.ErrorData as string;
- if (errData != null) {
- val = errData;
- } else if (assrt.ErrorMessage != null) {
- val = assrt.ErrorMessage;
- }
- } else if (blk != null) {
- toInspector.Write("BLOCK ");
- toInspector.Write(blk.Label);
- } else {
- assume false;
- }
- if (val == null || val == "assert" || val == "ensures") { val = ""; }
-
- if (absy is LoopInitAssertCmd) {
- val += " (loop entry)";
- } else if (absy is LoopInvMaintainedAssertCmd) {
- val += " (loop body)";
- } else if (val.IndexOf("#VCCERR") >= 0) {
- // skip further transformations
- } else if (absy is AssertRequiresCmd) {
- AssertRequiresCmd req = (AssertRequiresCmd)absy;
- IToken t2 = req.Requires.tok;
- string tval = t2.val;
- if (tval == "requires")
- tval = string.Format("{0}({1},{2}))", t2.filename, t2.line, t2.col);
- string call = "";
- if (val != "call") call = " in call to " + val;
- val = string.Format("precondition {0}{1}", tval, call);
- }
-
- val = val.Replace("\r", "").Replace("\n", " ");
-
- toInspector.WriteLine(string.Format(" {0} {1} :@:{2}:@:{3}", tok.line, tok.col, tok.filename, val));
- }
- toInspector.WriteLine("TOKEN END");
- }
-
- public void StatsLine(string! line)
- {
- toInspector.WriteLine(line);
- toInspector.Flush();
- }
- }
-}
diff --git a/Source/Provers/Z3/Prover.cs b/Source/Provers/Z3/Prover.cs deleted file mode 100644 index dbf23a8a..00000000 --- a/Source/Provers/Z3/Prover.cs +++ /dev/null @@ -1,942 +0,0 @@ -//-----------------------------------------------------------------------------
-//
-// 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.");
- }
- }
- }
-
-
-}
-
-
diff --git a/Source/Provers/Z3/ProverInterface.cs b/Source/Provers/Z3/ProverInterface.cs deleted file mode 100644 index 3473a139..00000000 --- a/Source/Provers/Z3/ProverInterface.cs +++ /dev/null @@ -1,344 +0,0 @@ -//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-using System;
-using System.Collections;
-using System.Collections.Generic;
-using System.Threading;
-using System.IO;
-using System.Text;
-using ExternalProver;
-using System.Diagnostics;
-using Microsoft.Contracts;
-using Microsoft.Boogie.AbstractInterpretation;
-using Microsoft.Boogie;
-using Microsoft.Boogie.VCExprAST;
-using Microsoft.Boogie.Clustering;
-using Microsoft.Boogie.TypeErasure;
-using Microsoft.Boogie.Z3;
-using Microsoft.Boogie.Simplify;
-
-namespace Microsoft.Boogie.Z3
-{
- public class Z3ProcessTheoremProver : ProcessTheoremProver
- {
- private Z3InstanceOptions! opts;
- private Inspector inspector;
-
- [NotDelayed]
- public Z3ProcessTheoremProver(VCExpressionGenerator! gen,
- DeclFreeProverContext! ctx, Z3InstanceOptions! opts)
- throws UnexpectedProverOutputException;
- {
- this.opts = opts;
- string! backPred = opts.Typed ? "TypedUnivBackPred2.sx" : "UnivBackPred2.sx";
- base(opts, gen, ctx, opts.ExeName, backPred);
- }
-
- private void FireUpInspector()
- {
- if (inspector == null && opts.Inspector != null) {
- inspector = new Inspector(opts);
- }
- }
-
- protected override Microsoft.Boogie.Simplify.ProverProcess! CreateProverProcess(string! proverPath) {
- opts.ExeName = proverPath;
- FireUpInspector();
- if (inspector != null) {
- inspector.NewProver();
- }
- return new Z3ProverProcess(opts, inspector);
- }
-
- protected override AxiomVCExprTranslator! SpawnVCExprTranslator() {
- return new Z3VCExprTranslator(gen, opts);
- }
-
- public override void BeginCheck(string! descriptiveName, VCExpr! vc, ErrorHandler! handler)
- {
- FireUpInspector();
- if (inspector != null) {
- inspector.NewProblem(descriptiveName, vc, handler);
- }
- base.BeginCheck(descriptiveName, vc, handler);
- }
- }
-
- public class Z3InstanceOptions : ProverOptions
- {
- public int Timeout { get { return TimeLimit / 1000; } }
- public bool Typed {
- get {
- return CommandLineOptions.Clo.Z3types || BitVectors == CommandLineOptions.BvHandling.Z3Native;
- }
- }
- public int Lets {
- get
- ensures 0 <= result && result < 4;
- {
- return CommandLineOptions.Clo.Z3lets;
- }
- }
- public bool V1 = false;
- public bool V2 = false; // default set in PostParse
- public bool DistZ3 = false;
- public string! ExeName = "z3.exe";
- public bool InverseImplies = false;
- public string? Inspector = null;
-
- protected override bool Parse(string! opt)
- {
- return ParseBool(opt, "V1", ref V1) ||
- ParseBool(opt, "V2", ref V2) ||
- ParseBool(opt, "REVERSE_IMPLIES", ref InverseImplies) ||
- ParseString(opt, "INSPECTOR", ref Inspector) ||
- ParseBool(opt, "DIST", ref DistZ3) ||
- base.Parse(opt);
- }
-
- protected override void PostParse()
- {
- base.PostParse();
-
- if (!V1 && !V2) {
- V2 = true; // default
- } else if (V1 && V2) {
- ReportError("V1 and V2 requested at the same time");
- } else if (V1 && DistZ3) {
- ReportError("V1 and DistZ3 requested at the same time");
- }
- if (V1) {
- ExeName = "z3-v1.3.exe";
- }
- if (DistZ3) {
- ExeName = "z3-dist.exe";
- CommandLineOptions.Clo.RestartProverPerVC = true;
- }
-
- }
- }
-
- internal class Z3LineariserOptions : LineariserOptions {
- private readonly Z3InstanceOptions! opts;
-
- public override CommandLineOptions.BvHandling Bitvectors { get {
- return opts.BitVectors;
- } }
-
- internal Z3LineariserOptions(bool asTerm, Z3InstanceOptions! opts, List<VCExprVar!>! letVariables) {
- base(asTerm);
- this.opts = opts;
- this.LetVariablesAttr = letVariables;
- }
-
- public override bool UseWeights { get {
- return opts.V2;
- } }
-
- public override bool UseTypes { get {
- return opts.Typed;
- } }
-
- public override bool QuantifierIds { get {
- return true;
- } }
-
- public override bool InverseImplies { get {
- return opts.InverseImplies;
- } }
-
- public override LineariserOptions! SetAsTerm(bool newVal) {
- if (newVal == AsTerm)
- return this;
- return new Z3LineariserOptions(newVal, opts, LetVariables);
- }
-
- // variables representing formulas in let-bindings have to be
- // printed in a different way than other variables
- private readonly List<VCExprVar!>! LetVariablesAttr;
- public override List<VCExprVar!>! LetVariables { get {
- return LetVariablesAttr;
- } }
-
- public override LineariserOptions! AddLetVariable(VCExprVar! furtherVar) {
- List<VCExprVar!>! allVars = new List<VCExprVar!> ();
- allVars.AddRange(LetVariables);
- allVars.Add(furtherVar);
- return new Z3LineariserOptions(AsTerm, opts, allVars);
- }
-
- public override LineariserOptions! AddLetVariables(List<VCExprVar!>! furtherVars) {
- List<VCExprVar!>! allVars = new List<VCExprVar!> ();
- allVars.AddRange(LetVariables);
- allVars.AddRange(furtherVars);
- return new Z3LineariserOptions(AsTerm, opts, allVars);
- }
- }
-
- // -----------------------------------------------------------------------------------------------
- // -----------------------------------------------------------------------------------------------
- // -----------------------------------------------------------------------------------------------
-
- public class Z3VCExprTranslator : AxiomVCExprTranslator {
- public Z3VCExprTranslator(VCExpressionGenerator! gen, Z3InstanceOptions! opts) {
- Gen = gen;
- Opts = opts;
- TypeAxiomBuilder! axBuilder;
- switch (CommandLineOptions.Clo.TypeEncodingMethod) {
- case CommandLineOptions.TypeEncoding.Arguments:
- axBuilder = new TypeAxiomBuilderArguments (gen);
- break;
- default:
- axBuilder = new TypeAxiomBuilderPremisses (gen);
- break;
- }
- axBuilder.Setup();
- AxBuilder = axBuilder;
- UniqueNamer namer = new UniqueNamer ();
- Namer = namer;
- this.DeclCollector =
- new TypeDeclCollector (namer, opts.BitVectors == CommandLineOptions.BvHandling.Z3Native);
- }
-
- private Z3VCExprTranslator(Z3VCExprTranslator! tl) {
- base(tl);
- Gen = tl.Gen;
- Opts = tl.Opts; // we assume that the options have not changed
- AxBuilder = (TypeAxiomBuilder)tl.AxBuilder.Clone();
- UniqueNamer namer = (UniqueNamer)tl.Namer.Clone();
- Namer = namer;
- DeclCollector = new TypeDeclCollector (namer, tl.DeclCollector);
- }
-
- public override Object! Clone() {
- return new Z3VCExprTranslator(this);
- }
-
- private readonly Z3InstanceOptions! Opts;
- private readonly VCExpressionGenerator! Gen;
- private readonly TypeAxiomBuilder! AxBuilder;
- private readonly UniqueNamer! Namer;
- private readonly TypeDeclCollector! DeclCollector;
-
- public override string! Lookup(VCExprVar! var)
- {
- return Namer.Lookup(var);
- }
-
- public override string! translate(VCExpr! expr, int polarity) {
- DateTime start = DateTime.Now;
- if (CommandLineOptions.Clo.Trace)
- Console.Write("Linearising ... ");
-
- // handle the types in the VCExpr
- TypeEraser eraser;
- switch (CommandLineOptions.Clo.TypeEncodingMethod) {
- case CommandLineOptions.TypeEncoding.Arguments:
- eraser = new TypeEraserArguments((TypeAxiomBuilderArguments)AxBuilder, Gen);
- break;
- case CommandLineOptions.TypeEncoding.Monomorphic:
- eraser = null;
- break;
- default:
- eraser = new TypeEraserPremisses((TypeAxiomBuilderPremisses)AxBuilder, Gen);
- break;
- }
- VCExpr! exprWithoutTypes = eraser != null ? eraser.Erase(expr, polarity) : expr;
-
- LetBindingSorter! letSorter = new LetBindingSorter(Gen);
- VCExpr! sortedExpr = letSorter.Mutate(exprWithoutTypes, true);
- VCExpr! sortedAxioms = letSorter.Mutate(AxBuilder.GetNewAxioms(), true);
-
- if (Opts.Typed) {
- DeclCollector.Collect(sortedAxioms);
- DeclCollector.Collect(sortedExpr);
- FeedTypeDeclsToProver();
- } else {
- TermFormulaFlattener! flattener = new TermFormulaFlattener (Gen);
- sortedExpr = flattener.Flatten(sortedExpr);
- sortedAxioms = flattener.Flatten(sortedAxioms);
- }
- if (Opts.Lets != 3) {
- // replace let expressions with implies
- Let2ImpliesMutator letImplier = new Let2ImpliesMutator(Gen, Opts.Lets == 1, Opts.Lets == 2);
- sortedExpr = letImplier.Mutate(sortedExpr);
- sortedAxioms = letImplier.Mutate(sortedAxioms);
- }
-
- //////////////////////////////////////////////////////////////////////////
- //SubtermCollector! coll = new SubtermCollector (gen);
- //coll.Traverse(sortedExpr, true);
- //coll.Traverse(sortedAxioms, true);
- //coll.UnifyClusters();
- //Console.WriteLine(coll);
- //////////////////////////////////////////////////////////////////////////
-
- LineariserOptions linOptions = new Z3LineariserOptions(false, Opts, new List<VCExprVar!>());
-
- AddAxiom(SimplifyLikeExprLineariser.ToString(sortedAxioms, linOptions, Namer));
-
- string! res = SimplifyLikeExprLineariser.ToString(sortedExpr, linOptions, Namer);
-
- if (CommandLineOptions.Clo.Trace) {
- TimeSpan elapsed = DateTime.Now - start;
- Console.WriteLine("finished [{0} s] ", elapsed.TotalSeconds);
- }
- return res;
- }
-
- private void FeedTypeDeclsToProver() {
- foreach (string! s in DeclCollector.GetNewDeclarations())
- AddTypeDecl(s);
- }
- }
-
- // -----------------------------------------------------------------------------------------------
- // -----------------------------------------------------------------------------------------------
- // -----------------------------------------------------------------------------------------------
-
- public class Factory : ProverFactory
- {
-
- public override object! SpawnProver(ProverOptions! popts, object! ctxt)
- {
- Z3InstanceOptions opts = (Z3InstanceOptions!)popts;
- return this.SpawnProver(((DeclFreeProverContext!)ctxt).ExprGen,
- (DeclFreeProverContext!)ctxt,
- opts);
- }
-
- public override object! NewProverContext(ProverOptions! options) {
- if (CommandLineOptions.Clo.BracketIdsInVC < 0) {
- CommandLineOptions.Clo.BracketIdsInVC = 0;
- }
-
- Z3InstanceOptions opts = (Z3InstanceOptions!)options;
- VCExpressionGenerator! gen = new VCExpressionGenerator ();
- List<string!>! proverCommands = new List<string!> ();
- proverCommands.Add("all");
- proverCommands.Add("z3");
- proverCommands.Add("simplifyLike");
- if (opts.BitVectors == CommandLineOptions.BvHandling.Z3Native)
- proverCommands.Add("bvDefSem");
- if (opts.BitVectors == CommandLineOptions.BvHandling.ToInt)
- proverCommands.Add("bvInt");
- VCGenerationOptions! genOptions = new VCGenerationOptions(proverCommands);
-
- return new DeclFreeProverContext(gen, genOptions);
- }
-
- public override ProverOptions! BlankProverOptions()
- {
- return new Z3InstanceOptions();
- }
-
- protected virtual Z3ProcessTheoremProver! SpawnProver(VCExpressionGenerator! gen,
- DeclFreeProverContext! ctx,
- Z3InstanceOptions! opts) {
- return new Z3ProcessTheoremProver(gen, ctx, opts);
- }
- }
-}
diff --git a/Source/Provers/Z3/TypeDeclCollector.cs b/Source/Provers/Z3/TypeDeclCollector.cs deleted file mode 100644 index 4d6accaf..00000000 --- a/Source/Provers/Z3/TypeDeclCollector.cs +++ /dev/null @@ -1,280 +0,0 @@ -//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-using System;
-using System.Collections;
-using System.Collections.Generic;
-using System.Diagnostics;
-using Microsoft.Contracts;
-using Microsoft.Boogie.VCExprAST;
-
-namespace Microsoft.Boogie.Z3
-{
- // Visitor for collecting the occurring function symbols in a VCExpr,
- // and for creating the corresponding declarations that can be fed into
- // Z3
-
- // (should this be rather done by Context.DeclareFunction? right now,
- // the TypeErasure visitor introduces new function symbols that are
- // not passed to this method)
-
- public class TypeDeclCollector : BoundVarTraversingVCExprVisitor<bool, bool> {
-
- private readonly UniqueNamer! Namer;
-
- private readonly bool NativeBv;
-
- public TypeDeclCollector(UniqueNamer! namer, bool nativeBv) {
- this.Namer = namer;
- this.NativeBv = nativeBv;
- AllDecls = new List<string!> ();
- IncDecls = new List<string!> ();
- KnownFunctions = new Dictionary<Function!, bool> ();
- KnownVariables = new Dictionary<VCExprVar!, bool> ();
- KnownTypes = new Dictionary<Type!, bool> ();
- KnownBvOps = new Dictionary<string!, bool> ();
-
- KnownStoreFunctions = new Dictionary<string!, bool> ();
- KnownSelectFunctions = new Dictionary<string!, bool> ();
- }
-
- internal TypeDeclCollector(UniqueNamer! namer, TypeDeclCollector! coll) {
- this.Namer = namer;
- this.NativeBv = coll.NativeBv;
- AllDecls = new List<string!> (coll.AllDecls);
- IncDecls = new List<string!> (coll.IncDecls);
- KnownFunctions = new Dictionary<Function!, bool> (coll.KnownFunctions);
- KnownVariables = new Dictionary<VCExprVar!, bool> (coll.KnownVariables);
- KnownTypes = new Dictionary<Type!, bool> (coll.KnownTypes);
- KnownBvOps = new Dictionary<string!, bool> (coll.KnownBvOps);
-
- KnownStoreFunctions = new Dictionary<string!, bool> (coll.KnownStoreFunctions);
- KnownSelectFunctions = new Dictionary<string!, bool> (coll.KnownSelectFunctions);
- }
-
- // not used
- protected override bool StandardResult(VCExpr! node, bool arg) {
- return true;
- }
-
- private readonly List<string!>! AllDecls;
- private readonly List<string!>! IncDecls;
-
- private readonly IDictionary<Function!, bool>! KnownFunctions;
- private readonly IDictionary<VCExprVar!, bool>! KnownVariables;
-
- // bitvector types have to be registered as well
- private readonly IDictionary<Type!, bool>! KnownTypes;
-
- // the names of registered BvConcatOps and BvExtractOps
- private readonly IDictionary<string!, bool>! KnownBvOps;
-
- private readonly IDictionary<string!, bool>! KnownStoreFunctions;
- private readonly IDictionary<string!, bool>! KnownSelectFunctions;
-
- public List<string!>! AllDeclarations { get {
- List<string!>! res = new List<string!> ();
- res.AddRange(AllDecls);
- return res;
- } }
-
- public List<string!>! GetNewDeclarations() {
- List<string!>! res = new List<string!> ();
- res.AddRange(IncDecls);
- IncDecls.Clear();
- return res;
- }
-
- private void AddDeclaration(string! decl) {
- AllDecls.Add(decl);
- IncDecls.Add(decl);
- }
-
- public void Collect(VCExpr! expr) {
- Traverse(expr, true);
- }
-
- ///////////////////////////////////////////////////////////////////////////
-
- private static string! TypeToString(Type! t) {
- return SimplifyLikeExprLineariser.TypeToString(t);
- }
-
- private void RegisterType(Type! type)
- {
- if (KnownTypes.ContainsKey(type)) return;
-
- if (type.IsMap && CommandLineOptions.Clo.UseArrayTheory) {
- KnownTypes.Add(type, true);
- string declString = "";
- MapType! mapType = type.AsMap;
-
- declString += "(DEFTYPE " + TypeToString(type) + " :BUILTIN Array ";
- foreach (Type! t in mapType.Arguments) {
- RegisterType(t);
- declString += TypeToString(t);
- declString += " ";
- }
- RegisterType(mapType.Result);
- declString += TypeToString(mapType.Result);
- declString += ")";
- AddDeclaration(declString);
- return;
- }
-
- if (type.IsBv && NativeBv) {
- int bits = type.BvBits;
- string name = TypeToString(type);
-
- AddDeclaration("(DEFTYPE " + name + " :BUILTIN BitVec " + bits + ")");
- // If we add the BUILTIN then the conversion axiom does not work
- AddDeclaration("(DEFOP " + name + "_to_int " + name + " $int)"); // :BUILTIN bv2int $int)");
- AddDeclaration("(DEFOP $make_bv" + bits + " $int " + name + " :BUILTIN int2bv " + bits + ")");
- string! expr = "($make_bv" + bits + " (" + name + "_to_int x))";
- AddDeclaration("(BG_PUSH (FORALL (x :TYPE " + name + ") (PATS "
- + expr + ") (QID bvconv" + bits + ") (EQ " + expr + " x)))");
-
- KnownTypes.Add(type, true);
- }
- }
-
- public override bool Visit(VCExprNAry! node, bool arg) {
- // there are a couple cases where operators have to be
- // registered by generating appropriate Z3 statements
-
- if (node.Op is VCExprBvConcatOp) {
- //
- if (NativeBv) {
- RegisterType(node[0].Type);
- RegisterType(node[1].Type);
- RegisterType(node.Type);
-
- string name = SimplifyLikeExprLineariser.BvConcatOpName(node);
- if (!KnownBvOps.ContainsKey(name)) {
- AddDeclaration("(DEFOP " + name +
- " " + TypeToString(node[0].Type) +
- " " + TypeToString(node[1].Type) +
- " " + TypeToString(node.Type) +
- " :BUILTIN concat)");
- KnownBvOps.Add(name, true);
- }
- }
- //
- } else if (node.Op is VCExprBvExtractOp) {
- //
- if (NativeBv) {
- RegisterType(node[0].Type);
- RegisterType(node.Type);
-
- VCExprBvExtractOp! op = (VCExprBvExtractOp)node.Op;
- string name = SimplifyLikeExprLineariser.BvExtractOpName(node);
- if (!KnownBvOps.ContainsKey(name)) {
- AddDeclaration("(DEFOP " + name +
- " " + TypeToString(node[0].Type) +
- " " + TypeToString(node.Type) +
- " :BUILTIN extract " +
- (op.End - 1) + " " + op.Start + ")");
- KnownBvOps.Add(name, true);
- }
- }
- //
- } else if (node.Op is VCExprStoreOp) {
- //
- RegisterType(node[0].Type);
- RegisterType(node[1].Type);
- RegisterType(node[2].Type);
- RegisterType(node.Type);
- string name = SimplifyLikeExprLineariser.StoreOpName(node);
- if (!KnownStoreFunctions.ContainsKey(name)) {
- AddDeclaration("(DEFOP " + name +
- " " + TypeToString(node[0].Type) +
- " " + TypeToString(node[1].Type) +
- " " + TypeToString(node[2].Type) +
- " " + TypeToString(node.Type) +
- " :BUILTIN store)");
- KnownStoreFunctions.Add(name, true);
- }
- //
- } else if (node.Op is VCExprSelectOp) {
- //
- RegisterType(node[0].Type);
- RegisterType(node[1].Type);
- RegisterType(node.Type);
- string name = SimplifyLikeExprLineariser.SelectOpName(node);
- if (!KnownSelectFunctions.ContainsKey(name)) {
- AddDeclaration("(DEFOP " + name +
- " " + TypeToString(node[0].Type) +
- " " + TypeToString(node[1].Type) +
- " " + TypeToString(node.Type) +
- " :BUILTIN select)");
- KnownSelectFunctions.Add(name, true);
- }
- //
- } else {
- //
- VCExprBoogieFunctionOp op = node.Op as VCExprBoogieFunctionOp;
- if (op != null && !KnownFunctions.ContainsKey(op.Func)) {
- Function! f = op.Func;
- string! printedName = Namer.GetName(f, f.Name);
- string! decl = "(DEFOP " + SimplifyLikeExprLineariser.MakeIdPrintable(printedName);
-
- foreach (Variable! v in f.InParams) {
- decl += " " + TypeToString(v.TypedIdent.Type);
- RegisterType(v.TypedIdent.Type);
- }
- assert f.OutParams.Length == 1;
- foreach (Variable! v in f.OutParams) {
- decl += " " + TypeToString(v.TypedIdent.Type);
- RegisterType(v.TypedIdent.Type);
- }
-
- string? builtin = ExtractBuiltin(f);
- if (builtin != null)
- decl += " :BUILTIN " + builtin;
-
- decl += ")";
-
- AddDeclaration(decl);
- KnownFunctions.Add(f, true);
- }
- //
- }
-
- return base.Visit(node, arg);
- }
-
- private string? ExtractBuiltin(Function! f) {
- string? retVal = null;
- if (NativeBv) {
- retVal = f.FindStringAttribute("bvbuiltin");
- }
- if (retVal == null) {
- retVal = f.FindStringAttribute("builtin");
- }
- return retVal;
- }
-
- public override bool Visit(VCExprVar! node, bool arg) {
- if (!BoundTermVars.Contains(node) && !KnownVariables.ContainsKey(node)) {
- RegisterType(node.Type);
- string! printedName = Namer.GetName(node, node.Name);
- string! decl =
- "(DEFOP " + SimplifyLikeExprLineariser.MakeIdPrintable(printedName)
- + " " + TypeToString(node.Type) + ")";
- AddDeclaration(decl);
- KnownVariables.Add(node, true);
- }
-
- return base.Visit(node, arg);
- }
-
- public override bool Visit(VCExprQuantifier! node, bool arg) {
- foreach (VCExprVar! v in node.BoundVars)
- RegisterType(v.Type);
-
- return base.Visit(node, arg);
- }
- }
-}
\ No newline at end of file diff --git a/Source/Provers/Z3/Z3.csproj b/Source/Provers/Z3/Z3.csproj deleted file mode 100644 index 4d7b3ee6..00000000 --- a/Source/Provers/Z3/Z3.csproj +++ /dev/null @@ -1,144 +0,0 @@ -<?xml version="1.0" encoding="utf-8"?>
-<VisualStudioProject>
- <XEN ProjectType="Local"
- SchemaVersion="1.0"
- Name="Z3"
- ProjectGuid="f75666de-cd56-457c-8782-09be243450fc"
- >
- <Build>
- <Settings ApplicationIcon=""
- AssemblyName="Provers.Z3"
- OutputType="Library"
- RootNamespace="Microsoft.Boogie.Z3"
- StartupObject=""
- StandardLibraryLocation=""
- TargetPlatform="v2"
- TargetPlatformLocation=""
- ShadowedAssembly=""
- NoStandardLibraries="False"
- >
- <Config Name="Debug"
- AllowUnsafeBlocks="False"
- BaseAddress="285212672"
- CheckForOverflowUnderflow="False"
- ConfigurationOverrideFile=""
- DefineConstants="DEBUG;TRACE"
- DocumentationFile=""
- DebugSymbols="True"
- FileAlignment="4096"
- IncrementalBuild="True"
- Optimize="False"
- OutputPath="bin\debug"
- RegisterForComInterop="False"
- RemoveIntegerChecks="false"
- TreatWarningsAsErrors="False"
- WarningLevel="4"
- ReferenceTypesAreNonNullByDefault="False"
- RunProgramVerifier="False"
- RunProgramVerifierWhileEditing="False"
- ProgramVerifierCommandLineOptions=""
- AllowPointersToManagedStructures="False"
- CheckContractAdmissibility="True"
- CheckPurity="False"
- />
- <Config Name="Release"
- AllowUnsafeBlocks="false"
- BaseAddress="285212672"
- CheckForOverflowUnderflow="false"
- ConfigurationOverrideFile=""
- DefineConstants="TRACE"
- DocumentationFile=""
- DebugSymbols="false"
- FileAlignment="4096"
- IncrementalBuild="false"
- Optimize="true"
- OutputPath="bin\release"
- RegisterForComInterop="false"
- RemoveIntegerChecks="false"
- TreatWarningsAsErrors="false"
- WarningLevel="4"
- />
- </Settings>
- <References>
- <Reference Name="System"
- AssemblyName="System"
- Private="false"
- />
- <Reference Name="System.Data"
- AssemblyName="System.Data"
- Private="false"
- />
- <Reference Name="System.Xml"
- AssemblyName="System.Xml"
- Private="false"
- />
- <Reference Name="Core"
- Project="{47BC34F1-A173-40BE-84C2-9332B4418387}"
- Private="true"
- />
- <Reference Name="AIFramework"
- Project="{24B55172-AD8B-47D1-8952-5A95CFDB9B31}"
- Private="true"
- />
- <Reference Name="Graph"
- Project="{4C28FB90-630E-4B55-A937-11A011B79765}"
- Private="true"
- />
- <Reference Name="Mscorlib.Contracts"
- AssemblyName="Mscorlib.Contracts"
- Private="false"
- HintPath="../../../Binaries/Mscorlib.Contracts.dll"
- />
- <Reference Name="System.Contracts"
- AssemblyName="System.Contracts"
- Private="false"
- HintPath="../../../Binaries/System.Contracts.dll"
- />
- <Reference Name="VCGeneration"
- Project="{F65666DE-FB56-457C-8782-09BE243450FC}"
- Private="true"
- />
- <Reference Name="Simplify"
- Project="{F75666DE-FB56-457C-8782-09BE243450FC}"
- Private="true"
- />
- <Reference Name="Basetypes"
- Project="{0C692837-77EC-415F-BF04-395E3ED06E9A}"
- Private="true"
- />
- <Reference Name="VCExpr"
- Project="{CF42B700-10AA-4DA9-8992-48A800251C11}"
- Private="true"
- />
- </References>
- </Build>
- <Files>
- <Include>
- <File BuildAction="Compile"
- SubType="Code"
- RelPath="Prover.ssc"
- />
- <File BuildAction="Compile"
- SubType="Code"
- RelPath="ProverInterface.ssc"
- />
- <File BuildAction="Compile"
- SubType="Code"
- RelPath="..\..\version.ssc"
- />
- <File BuildAction="Compile"
- SubType="Code"
- RelPath="TypeDeclCollector.ssc"
- />
- <File BuildAction="Compile"
- SubType="Code"
- RelPath="Inspector.ssc"
- />
- <File BuildAction="Compile"
- SubType="Code"
- RelPath="AssemblyInfo.ssc"
- />
- </Include>
- </Files>
- </XEN>
-</VisualStudioProject>
\ No newline at end of file |