From 815c5f5fb885112a1b4d037e511336735acaa2f5 Mon Sep 17 00:00:00 2001 From: tabarbe Date: Tue, 20 Jul 2010 22:33:04 +0000 Subject: Boogie: Rename didn't work. Resetting to try again --- Source/Provers/Z3/Inspector.cs | 136 ----- Source/Provers/Z3/Prover.cs | 942 --------------------------------- Source/Provers/Z3/ProverInterface.cs | 344 ------------ Source/Provers/Z3/TypeDeclCollector.cs | 280 ---------- Source/Provers/Z3/Z3.csproj | 144 ----- 5 files changed, 1846 deletions(-) delete mode 100644 Source/Provers/Z3/Inspector.cs delete mode 100644 Source/Provers/Z3/Prover.cs delete mode 100644 Source/Provers/Z3/ProverInterface.cs delete mode 100644 Source/Provers/Z3/TypeDeclCollector.cs delete mode 100644 Source/Provers/Z3/Z3.csproj 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 { - public Dictionary! Labels = new Dictionary(); - - public static Dictionary! 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! 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! parms, string! option, string! value) - modifies parms.*; - { - OptionValue ov = new OptionValue(option, value); - Owner.AssignSame(ov, Owner.ElementProxy(parms)); - parms.Add(ov); - } - private List! parameterSettings; - - // [NotDelayed] - [Captured] - public Z3ProverProcess(Z3InstanceOptions! opts, Inspector? inspector) - requires inspector != null ==> Owner.Same(opts, inspector); - { // throws ProverException - string! z3args = OptionChar() + "si"; - List parms = new List(); - - 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! 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! 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 identifierToPartition = new Dictionary(); - // map each ZID to the set (in list form) of IDs belonging to it (possibly empty): - List> partitionToIdentifiers = new List>(); - // map each ZID to the number or boolean given, if any: - List partitionToValue = new List(); - // map each value (number or boolean) to the ZID, reverse map of partitionToValue - Dictionary valueToPartition = new Dictionary(); - 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 emptyList = new List(); - 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! identifierToPartition, - List>! partitionToIdentifiers, - List! partitionToValue, - Dictionary! 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!> arrayModel = new List!>(); - string array = s.Substring(j+1); - int index1, index2; - string from, to; - List tuple = new List(); - 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(); - } - 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! identifierToPartition, - List>! partitionToIdentifiers) - modifies identifierToPartition.*, partitionToIdentifiers.*; - ensures 0 <= result && result <= s.Length; - { - List identifiers = new List(); - 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! identifierToPartition, - List>! partitionToIdentifiers, - List! partitionToValue, - Dictionary! 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>!> definedFunctions = new Dictionary>!>(); - // 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> functionDefinition = new List>(); - // list of arguments, followed by the result, the last element of this list is always the result - List argumentsAndResult = new List(); - - // read F - while (true) - { - functionDefinition = new List>(); - 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(); - // 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(); - 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(); - 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! identifierToPartition, List>! partitionToIdentifiers, List! partitionToValue, Dictionary! valueToPartition, Dictionary>!>! 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! possible_names = new List(); - List 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>!> kv in definedFunctions) { - foreach (List! 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 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 funNames = new List(definedFunctions.Keys); - funNames.Sort(); - foreach (string! name in funNames) { - if (definedFunctions[name].Count == 1) continue; // skip functions with only the else-> clause - foreach (List! 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 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!> array = tempPTVI as List!>; - assume array != null; - writer.Write(" -> {"); - foreach(List 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>!> kvp in definedFunctions) { - writer.WriteLine(kvp.Key + " -> {"); - List> kvpValue = kvp.Value; - if (kvpValue != null) { - foreach(List 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 kvp in identifierToPartition) { - writer.WriteLine(kvp.Key + " : " + "*" + kvp.Value); - } - - writer.WriteLine("valueToPartition:"); - foreach (KeyValuePair 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! 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! LetVariablesAttr; - public override List! LetVariables { get { - return LetVariablesAttr; - } } - - public override LineariserOptions! AddLetVariable(VCExprVar! furtherVar) { - List! allVars = new List (); - allVars.AddRange(LetVariables); - allVars.Add(furtherVar); - return new Z3LineariserOptions(AsTerm, opts, allVars); - } - - public override LineariserOptions! AddLetVariables(List! furtherVars) { - List! allVars = new List (); - 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()); - - 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! proverCommands = new List (); - 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 { - - private readonly UniqueNamer! Namer; - - private readonly bool NativeBv; - - public TypeDeclCollector(UniqueNamer! namer, bool nativeBv) { - this.Namer = namer; - this.NativeBv = nativeBv; - AllDecls = new List (); - IncDecls = new List (); - KnownFunctions = new Dictionary (); - KnownVariables = new Dictionary (); - KnownTypes = new Dictionary (); - KnownBvOps = new Dictionary (); - - KnownStoreFunctions = new Dictionary (); - KnownSelectFunctions = new Dictionary (); - } - - internal TypeDeclCollector(UniqueNamer! namer, TypeDeclCollector! coll) { - this.Namer = namer; - this.NativeBv = coll.NativeBv; - AllDecls = new List (coll.AllDecls); - IncDecls = new List (coll.IncDecls); - KnownFunctions = new Dictionary (coll.KnownFunctions); - KnownVariables = new Dictionary (coll.KnownVariables); - KnownTypes = new Dictionary (coll.KnownTypes); - KnownBvOps = new Dictionary (coll.KnownBvOps); - - KnownStoreFunctions = new Dictionary (coll.KnownStoreFunctions); - KnownSelectFunctions = new Dictionary (coll.KnownSelectFunctions); - } - - // not used - protected override bool StandardResult(VCExpr! node, bool arg) { - return true; - } - - private readonly List! AllDecls; - private readonly List! IncDecls; - - private readonly IDictionary! KnownFunctions; - private readonly IDictionary! KnownVariables; - - // bitvector types have to be registered as well - private readonly IDictionary! KnownTypes; - - // the names of registered BvConcatOps and BvExtractOps - private readonly IDictionary! KnownBvOps; - - private readonly IDictionary! KnownStoreFunctions; - private readonly IDictionary! KnownSelectFunctions; - - public List! AllDeclarations { get { - List! res = new List (); - res.AddRange(AllDecls); - return res; - } } - - public List! GetNewDeclarations() { - List! res = new List (); - 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 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - \ No newline at end of file -- cgit v1.2.3