From 962f8d5252b3f5ec4d19e0cd2a430934bd55cc6d Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sun, 28 Jun 2015 01:44:30 +0100 Subject: Normalise line endings using a .gitattributes file. Unfortunately this required that this commit globally modify most files. If you want to use git blame to see the real author of a line use the ``-w`` flag so that whitespace changes are ignored. --- Source/Model/Model.cs | 1412 +++++++++++++++---------------- Source/Model/Model.csproj | 218 ++--- Source/Model/ModelParser.cs | 4 +- Source/Model/Properties/AssemblyInfo.cs | 46 +- 4 files changed, 840 insertions(+), 840 deletions(-) (limited to 'Source/Model') diff --git a/Source/Model/Model.cs b/Source/Model/Model.cs index 76b7cb4a..1e71d6c2 100644 --- a/Source/Model/Model.cs +++ b/Source/Model/Model.cs @@ -1,706 +1,706 @@ -//----------------------------------------------------------------------------- -// -// Copyright (C) Microsoft Corporation. All Rights Reserved. -// -//----------------------------------------------------------------------------- - -/* -An instance of the Model class represents a single model returned from the SMT solver. This usually -corresponds to a single verification error. The model consists of elements and function interpretations. -Additionally the model may contain a number of captured states, each consisting of a user-supplied name -a mapping from Boogie variable names to model elements. - -Model elements (which used to be called “partitions” in Z3) are represented by instances of the -Model.Element class. Each element has an integer identity. The Element class has subclasses -Uninterpreted, Boolean, Integer, BitVector, and Array. The classes correspond to different sorts of -elements that the SMT solver may use. Each of these has properties for returning the actual -value (true/false or a number; for bitvectors also size). For an array the interpretation is a -particular function defined elsewhere in the model. - -A function interpretation is represented by Model.Func class. It consists of a name, arity, and -a list of defining tuples. A defining tuple (Model.FuncTuple) for a function of arity N has -N model elements as arguments and a single element as the result. A constant is a function -of arity 0, with just one defining tuple. Given a constant function f, the result element of -the defining tuple is retrieved with f.GetConstant(). - -The Model.Element class exposes methods to look up all the functions that reference it in their -defining tuples. Additionally Model.Func allows lookup of specific tuples, based on the elements. - -An instance of the Model class represents a single model returned from the SMT solver. - - */ - -using System; -using System.Linq; -using System.Collections.Generic; -using System.Text; -using System.Diagnostics; -using System.Text.RegularExpressions; - -namespace Microsoft.Boogie -{ - public class Model - { - #region Elements and functions (inner classes) - public enum ElementKind - { - Integer, - BitVector, - Boolean, - Uninterpreted, - Array, - DataValue - } - - abstract public class Element - { - public readonly Model Model; - internal List references = new List(); - public readonly int Id; - - public IEnumerable References { get { return references; } } - - public IEnumerable Names { - get { - foreach (var f in references) - if (f.Result == this) yield return f; - } - } - - protected Element(Model p) - { - Model = p; - Id = Model.elements.Count; - } - public abstract ElementKind Kind { get; } - public virtual int AsInt() { throw new NotImplementedException(); } - - public override int GetHashCode() { - return Id; - } - - public override bool Equals(object obj) { - return obj == this; - } - } - - #region element kinds - public class Uninterpreted : Element - { - public override ElementKind Kind { get { return ElementKind.Uninterpreted; } } - public override string ToString() { return Name; } - - internal Uninterpreted(Model p, string n) : base(p) { Name = n; } - public readonly string Name; - } - - abstract public class Number : Element - { - protected Number(Model p, string n) : base(p) { Numeral = n; } - public readonly string Numeral; - public override int AsInt() { return int.Parse(Numeral); } - } - - public class Integer : Number - { - internal Integer(Model p, string n) : base(p, n) { } - public override ElementKind Kind { get { return ElementKind.Integer; } } - public override string ToString() { return Numeral.ToString(); } - } - - public class BitVector : Number - { - internal BitVector(Model p, string n, int sz) : base(p, n) { Size = sz; } - public readonly int Size; - public override ElementKind Kind { get { return ElementKind.BitVector; } } - public override string ToString() { return string.Format("{0}bv{1}", Numeral, Size); } - } - - public class Boolean : Element - { - public bool Value; - internal Boolean(Model p, bool v) : base(p) { Value = v; } - public override ElementKind Kind { get { return ElementKind.Boolean; } } - public override string ToString() { return Value ? "true" : "false"; } - } - - public class Array : Element - { - public Func Value; - internal Array(Model p, Func v) : base(p) { Value = v; } - public override ElementKind Kind { get { return ElementKind.Array; } } - public override string ToString() { return string.Format("as-array[{0}]", Value.Name); } - } - - public class DatatypeValue : Element - { - public readonly string ConstructorName; - public readonly Element[] Arguments; - internal DatatypeValue(Model p, string name, List args) : base(p) { - ConstructorName = name; - Arguments = args.ToArray(); - } - public override ElementKind Kind { get { return ElementKind.DataValue; } } - public override string ToString() { - StringBuilder builder = new StringBuilder(); - builder.Append("(").Append(ConstructorName); - foreach (Element arg in Arguments) { - builder.Append(" ").Append(arg); - } - builder.Append(")"); - return builder.ToString(); - } - } - #endregion - - public class Func - { - public readonly Model Model; - public readonly string Name; - public readonly int Arity; - internal readonly List apps = new List(); - public IEnumerable Apps { get { return apps; } } - public int AppCount { get { return apps.Count; } } - private Element @else; - - internal Func(Model p, string n, int a) { Model = p; Name = n; Arity = a; } - - public override string ToString() - { - return string.Format("{0}/{1}", Name, Arity); - } - - internal void Substitute(Dictionary mapping) { - Element e; - if (@else != null && mapping.TryGetValue(@else, out e)) - @else = e; - foreach (var ft in apps) { - if (mapping.TryGetValue(ft.Result, out e)) ft.Result = e; - for (var i = 0; i < ft.Args.Length; ++i) - if (mapping.TryGetValue(ft.Args[i], out e)) ft.Args[i] = e; - } - } - - public Element Else - { - get - { - return @else; - } - set - { - if (@else != null) - throw new ArgumentException(); - @else = value; - } - } - - public void SetConstant(Element res) - { - if (Arity != 0 || apps.Count > 0) - throw new ArgumentException(); - var t = new FuncTuple(this, res, null); - apps.Add(t); - res.references.Add(t); - } - - /// - /// Return the first application where the argument at position argIdx is elt. - /// - public FuncTuple AppWithArg(int argIdx, Element elt) - { - foreach (var a in AppsWithArg(argIdx, elt)) - return a; - return null; - } - - /// - /// Return the first application with the result elt. - /// - public FuncTuple AppWithResult(Element elt) - { - foreach (var a in AppsWithResult(elt)) - return a; - return null; - } - - /// - /// Return all applications where the argument at position argIdx is elt. - /// - public IEnumerable AppsWithArg(int argIdx, Element elt) - { - foreach (var r in elt.References) { - if (r.Func == this && r.Args[argIdx] == elt) - yield return r; - } - } - - /// - /// Return all applications where the argument at position argIdx0 is elt0 and argument at argIdx1 is elt1. - /// - public IEnumerable AppsWithArgs(int argIdx0, Element elt0, int argIdx1, Element elt1) - { - foreach (var r in elt0.References) { - if (r.Func == this && r.Args[argIdx0] == elt0 && r.Args[argIdx1] == elt1) - yield return r; - } - } - - /// - /// Return all the applications with the result elt. - /// - public IEnumerable AppsWithResult(Element elt) - { - foreach (var r in elt.References) { - if (r.Func == this && r.Result == elt) - yield return r; - } - } - - /// - /// For a nullary function, return its value. - /// - public Element GetConstant() - { - if (Arity != 0) - throw new ArgumentException(); - if (apps.Count == 0) - SetConstant(Model.MkElement("**" + Name)); - return apps[0].Result; - } - - /// - /// If all arguments are non-null, and function application for them exists return the value, otherwise return null. - /// - public Element OptEval(params Element[] args) - { - if (args.Any(a => a == null)) return null; - return TryEval(args); - } - - /// - /// Look for function application with given arguments and return its value or null if no such application exists. - /// - public Element TryEval(params Element[] args) - { - for (int i = 0; i < args.Length; ++i) - if(args[i]==null) - throw new ArgumentException(); - - if (apps.Count > 10) { - var best = apps; - for (int i = 0; i < args.Length; ++i) - if (args[i].references.Count < best.Count) - best = args[i].references; - if (best != apps) { - foreach (var tpl in best) { - bool same = true; - if (tpl.Func != this) - continue; - for (int i = 0; i < args.Length; ++i) - if (tpl.Args[i] != args[i]) { - same = false; - break; - } - if (same) return tpl.Result; - } - return null; - } - } - - foreach (var tpl in apps) { - bool same = true; - for (int i = 0; i < args.Length; ++i) - if (tpl.Args[i] != args[i]) { - same = false; - break; - } - if (same) return tpl.Result; - } - return null; - } - - /// - /// Look for function application with a subsequence of given arguments and return its value or null if no such application exists. - /// - public Element TryPartialEval(params Element[] args) - { - foreach (var tpl in apps) { - int j = 0; - for (int i = 0; i < args.Length; ++i) { - if (tpl.Args[j] == args[i]) { - j++; - if (j == tpl.Args.Length) - return tpl.Result; - } - } - } - return null; - } - - /// - /// Short for TryEval(args) == (Element)true - /// - public bool IsTrue(params Element[] args) - { - var r = TryEval(args) as Boolean; - return r != null && r.Value; - } - - /// - /// Short for TryEval(args) == (Element)false - /// - public bool IsFalse(params Element[] args) - { - var r = TryEval(args) as Boolean; - return r != null && !r.Value; - } - - public void AddApp(Element res, params Element[] args) - { - if (Arity == 0) - SetConstant(res); - else { - if (args.Length != Arity) - throw new ArgumentException(); - var t = new FuncTuple(this, res, (Element[])args.Clone()); - apps.Add(t); - var u = new HashSet(); - res.references.Add(t); - u.Add(res); - foreach (var a in args) - if (!u.Contains(a)) { - u.Add(a); - a.references.Add(t); - } - } - } - } - - public class FuncTuple - { - static readonly Element[] EmptyArgs = new Element[0]; - - // These should be immutable, except when Substituting the entire model - public readonly Func Func; - public Element Result; - public readonly Element[] Args; - - internal FuncTuple(Func func, Element res, Element[] args) - { - if (args == null) Args = EmptyArgs; - else Args = args; - Func = func; - Result = res; - } - - public override string ToString() - { - var res = new StringBuilder(); - res.Append("(").Append(Func.Name); - for (int i = 0; i < Args.Length; ++i) { - res.Append(" ").Append(Args[i]); - } - res.Append(") -> ").Append(Result); - return res.ToString(); - } - } - #endregion - - private List functions = new List(); - private List elements = new List(); - private List states = new List(); - private Dictionary functionsByName = new Dictionary(); - private Dictionary elementsByName = new Dictionary(); - - #region factory methods - Element ConstructElement(string name) - { - if (name.ToLower() == "true") return True; - if (name.ToLower() == "false") return False; - - if (name.StartsWith("bv") && name.Length > 4 && Char.IsDigit(name[2])) - name = name.Substring(2); - - if (Char.IsDigit(name[0]) || name[0] == '-') { - int col = name.IndexOf("bv"); - int szi = -1; - - if (name.EndsWith(":int")) - name = name.Substring(0, name.Length - 4); - - if (col > 0) { - if (int.TryParse(name.Substring(col + 2), out szi) && szi > 0) { - name = name.Substring(0, col); - } else { - return null; - } - } else if (name.EndsWith("]")) { - col = name.IndexOf("["); - if (col > 0 && int.TryParse(name.Substring(col + 1, name.Length - col - 2), out szi) && szi > 0) { - name = name.Substring(0, col); - } else { - return null; - } - } - - for (int i = 1; i < name.Length; ++i) - if (!Char.IsDigit(name[i])) - return null; - - if (szi > 0) - return new BitVector(this, name, szi); - else - return new Integer(this, name); - } else if (name[0] == '*' || name.StartsWith("val!") || name.Contains("!val!")) { - return new Uninterpreted(this, name); - } else if (name.StartsWith("as-array[") && name.EndsWith("]")) { - var fnName = name.Substring(9, name.Length - 10); - return new Array(this, MkFunc(fnName, 1)); - } else { - return new DatatypeValue(this, name, new List()); - } - } - - public Element TryMkElement(string name) - { - Element res; - - if (elementsByName.TryGetValue(name, out res)) - return res; - - var tmp = ConstructElement(name); - if (tmp == null) return null; - - name = tmp.ToString(); - if (elementsByName.TryGetValue(name, out res)) - return res; - - elementsByName.Add(name, tmp); - elements.Add(tmp); - return tmp; - } - - public Element MkElement(string name) - { - Element res = TryMkElement(name); - if (res == null) - throw new ArgumentException("invalid element name: '" + name + "'"); - return res; - } - - public Func MkFunc(string name, int arity) - { - Func res; - if (functionsByName.TryGetValue(name, out res)) { - if (res.Arity != arity) - throw new ArgumentException(string.Format("function '{0}' previously created with arity {1}, now trying to recreate with arity {2}", name, res.Arity, arity)); - return res; - } - res = new Func(this, name, arity); - functionsByName.Add(name, res); - functions.Add(res); - return res; - } - #endregion - - #region state management - public class CapturedState - { - List vars = new List(); - Dictionary valuations = new Dictionary(); - readonly CapturedState previous; - // AL: Dropping "readonly" for corral - public /* readonly */ string Name { get; private set; } - - public IEnumerable Variables { get { return vars; } } - public IEnumerable AllVariables { - get { - if (previous != null) - return previous.AllVariables.Concat(Variables).Distinct(); - else - return Variables; - } - } - public int VariableCount { get { return vars.Count; } } - public bool HasBinding(string varname) - { - return valuations.ContainsKey(varname); - } - public Element TryGet(string varname) - { - CapturedState curr = this; - while (curr != null) { - Element res; - if (curr.valuations.TryGetValue(varname, out res)) - return res; - curr = curr.previous; - } - return null; - } - - public void AddBinding(string varname, Element value) - { - vars.Add(varname); - valuations.Add(varname, value); - } - - // Change name of the state - public void ChangeName(string newName) - { - Name = newName; - } - - // Change names of variables in this state - // (Used by corral) - internal void ChangeVariableNames(Dictionary varNameMap) - { - var oldVars = vars; - var oldValuations = valuations; - - vars = new List(); - valuations = new Dictionary(); - - foreach (var v in oldVars) - { - if (varNameMap.ContainsKey(v)) vars.Add(varNameMap[v]); - else vars.Add(v); - } - - foreach (var kvp in oldValuations) - { - if (varNameMap.ContainsKey(kvp.Key)) valuations.Add(varNameMap[kvp.Key], kvp.Value); - else valuations.Add(kvp.Key, kvp.Value); - } - } - - internal CapturedState(string name, CapturedState prev) - { - Name = name; - previous = prev; - } - } - - public CapturedState MkState(string name) - { - var last = states[states.Count - 1]; - var s = new CapturedState(name, last); - states.Add(s); - return s; - } - - // Change names of variables in all captured states - // (Used by corral) - public void ChangeVariableNames(Dictionary varNameMap) - { - foreach (var s in states) - { - s.ChangeVariableNames(varNameMap); - } - } - - #endregion - - public Model() - { - InitialState = new CapturedState("", null); - states.Add(InitialState); - True = new Boolean(this, true); - elements.Add(True); - elementsByName.Add("true", True); - False = new Boolean(this, false); - elements.Add(False); - elementsByName.Add("false", False); - } - - public IEnumerable Functions { get { return functions; } } - public IEnumerable Elements { get { return elements; } } - public IEnumerable States { get { return states; } } - public readonly Element True, False; - public readonly CapturedState InitialState; - - public bool HasFunc(string name) - { - return functionsByName.ContainsKey(name); - } - - public Func TryGetFunc(string name) - { - Func res; - if (functionsByName.TryGetValue(name, out res)) - return res; - else - return null; - } - - public Func GetFunc(string name) - { - Func res = TryGetFunc(name); - if (res == null) - throw new KeyNotFoundException("function '" + name + "' undefined in the model"); - return res; - } - - public Func TryGetSkolemFunc(string name) - { - return Functions.Where(f => f.Name.StartsWith(name + "!")).FirstOrDefault(); - } - - public Element GetElement(string name) - { - Element res; - if (elementsByName.TryGetValue(name, out res)) - return res; - else - throw new KeyNotFoundException("element '" + name + "' undefined in the model"); - } - - public Element MkIntElement(int v) - { - return MkElement(v.ToString()); - } - - public void Write(System.IO.TextWriter wr) - { - wr.WriteLine("*** MODEL"); - foreach (var f in Functions.OrderBy(f => f.Name)) - if (f.Arity == 0) { - wr.WriteLine("{0} -> {1}", f.Name, f.GetConstant()); - } - foreach (var f in Functions) - if (f.Arity != 0) { - wr.WriteLine("{0} -> {1}", f.Name, "{"); - foreach (var app in f.Apps) { - wr.Write(" "); - foreach (var a in app.Args) - wr.Write("{0} ", a); - wr.WriteLine("-> {0}", app.Result); - } - if (f.Else != null) - wr.WriteLine(" else -> {0}", f.Else); - wr.WriteLine("}"); - } - foreach (var s in States) { - if (s == InitialState && s.VariableCount == 0) - continue; - wr.WriteLine("*** STATE {0}", s.Name); - foreach (var v in s.Variables) - wr.WriteLine(" {0} -> {1}", v, s.TryGet(v)); - wr.WriteLine("*** END_STATE", s.Name); - } - wr.WriteLine("*** END_MODEL"); - } - - public void Substitute(Dictionary mapping) { - foreach (var f in functions) f.Substitute(mapping); - } - - public static List ParseModels(System.IO.TextReader rd) - { - ModelParser p = new ParserZ3(); - p.rd = rd; - p.Run(); - return p.resModels; - } - } -} +//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- + +/* +An instance of the Model class represents a single model returned from the SMT solver. This usually +corresponds to a single verification error. The model consists of elements and function interpretations. +Additionally the model may contain a number of captured states, each consisting of a user-supplied name +a mapping from Boogie variable names to model elements. + +Model elements (which used to be called “partitions” in Z3) are represented by instances of the +Model.Element class. Each element has an integer identity. The Element class has subclasses +Uninterpreted, Boolean, Integer, BitVector, and Array. The classes correspond to different sorts of +elements that the SMT solver may use. Each of these has properties for returning the actual +value (true/false or a number; for bitvectors also size). For an array the interpretation is a +particular function defined elsewhere in the model. + +A function interpretation is represented by Model.Func class. It consists of a name, arity, and +a list of defining tuples. A defining tuple (Model.FuncTuple) for a function of arity N has +N model elements as arguments and a single element as the result. A constant is a function +of arity 0, with just one defining tuple. Given a constant function f, the result element of +the defining tuple is retrieved with f.GetConstant(). + +The Model.Element class exposes methods to look up all the functions that reference it in their +defining tuples. Additionally Model.Func allows lookup of specific tuples, based on the elements. + +An instance of the Model class represents a single model returned from the SMT solver. + + */ + +using System; +using System.Linq; +using System.Collections.Generic; +using System.Text; +using System.Diagnostics; +using System.Text.RegularExpressions; + +namespace Microsoft.Boogie +{ + public class Model + { + #region Elements and functions (inner classes) + public enum ElementKind + { + Integer, + BitVector, + Boolean, + Uninterpreted, + Array, + DataValue + } + + abstract public class Element + { + public readonly Model Model; + internal List references = new List(); + public readonly int Id; + + public IEnumerable References { get { return references; } } + + public IEnumerable Names { + get { + foreach (var f in references) + if (f.Result == this) yield return f; + } + } + + protected Element(Model p) + { + Model = p; + Id = Model.elements.Count; + } + public abstract ElementKind Kind { get; } + public virtual int AsInt() { throw new NotImplementedException(); } + + public override int GetHashCode() { + return Id; + } + + public override bool Equals(object obj) { + return obj == this; + } + } + + #region element kinds + public class Uninterpreted : Element + { + public override ElementKind Kind { get { return ElementKind.Uninterpreted; } } + public override string ToString() { return Name; } + + internal Uninterpreted(Model p, string n) : base(p) { Name = n; } + public readonly string Name; + } + + abstract public class Number : Element + { + protected Number(Model p, string n) : base(p) { Numeral = n; } + public readonly string Numeral; + public override int AsInt() { return int.Parse(Numeral); } + } + + public class Integer : Number + { + internal Integer(Model p, string n) : base(p, n) { } + public override ElementKind Kind { get { return ElementKind.Integer; } } + public override string ToString() { return Numeral.ToString(); } + } + + public class BitVector : Number + { + internal BitVector(Model p, string n, int sz) : base(p, n) { Size = sz; } + public readonly int Size; + public override ElementKind Kind { get { return ElementKind.BitVector; } } + public override string ToString() { return string.Format("{0}bv{1}", Numeral, Size); } + } + + public class Boolean : Element + { + public bool Value; + internal Boolean(Model p, bool v) : base(p) { Value = v; } + public override ElementKind Kind { get { return ElementKind.Boolean; } } + public override string ToString() { return Value ? "true" : "false"; } + } + + public class Array : Element + { + public Func Value; + internal Array(Model p, Func v) : base(p) { Value = v; } + public override ElementKind Kind { get { return ElementKind.Array; } } + public override string ToString() { return string.Format("as-array[{0}]", Value.Name); } + } + + public class DatatypeValue : Element + { + public readonly string ConstructorName; + public readonly Element[] Arguments; + internal DatatypeValue(Model p, string name, List args) : base(p) { + ConstructorName = name; + Arguments = args.ToArray(); + } + public override ElementKind Kind { get { return ElementKind.DataValue; } } + public override string ToString() { + StringBuilder builder = new StringBuilder(); + builder.Append("(").Append(ConstructorName); + foreach (Element arg in Arguments) { + builder.Append(" ").Append(arg); + } + builder.Append(")"); + return builder.ToString(); + } + } + #endregion + + public class Func + { + public readonly Model Model; + public readonly string Name; + public readonly int Arity; + internal readonly List apps = new List(); + public IEnumerable Apps { get { return apps; } } + public int AppCount { get { return apps.Count; } } + private Element @else; + + internal Func(Model p, string n, int a) { Model = p; Name = n; Arity = a; } + + public override string ToString() + { + return string.Format("{0}/{1}", Name, Arity); + } + + internal void Substitute(Dictionary mapping) { + Element e; + if (@else != null && mapping.TryGetValue(@else, out e)) + @else = e; + foreach (var ft in apps) { + if (mapping.TryGetValue(ft.Result, out e)) ft.Result = e; + for (var i = 0; i < ft.Args.Length; ++i) + if (mapping.TryGetValue(ft.Args[i], out e)) ft.Args[i] = e; + } + } + + public Element Else + { + get + { + return @else; + } + set + { + if (@else != null) + throw new ArgumentException(); + @else = value; + } + } + + public void SetConstant(Element res) + { + if (Arity != 0 || apps.Count > 0) + throw new ArgumentException(); + var t = new FuncTuple(this, res, null); + apps.Add(t); + res.references.Add(t); + } + + /// + /// Return the first application where the argument at position argIdx is elt. + /// + public FuncTuple AppWithArg(int argIdx, Element elt) + { + foreach (var a in AppsWithArg(argIdx, elt)) + return a; + return null; + } + + /// + /// Return the first application with the result elt. + /// + public FuncTuple AppWithResult(Element elt) + { + foreach (var a in AppsWithResult(elt)) + return a; + return null; + } + + /// + /// Return all applications where the argument at position argIdx is elt. + /// + public IEnumerable AppsWithArg(int argIdx, Element elt) + { + foreach (var r in elt.References) { + if (r.Func == this && r.Args[argIdx] == elt) + yield return r; + } + } + + /// + /// Return all applications where the argument at position argIdx0 is elt0 and argument at argIdx1 is elt1. + /// + public IEnumerable AppsWithArgs(int argIdx0, Element elt0, int argIdx1, Element elt1) + { + foreach (var r in elt0.References) { + if (r.Func == this && r.Args[argIdx0] == elt0 && r.Args[argIdx1] == elt1) + yield return r; + } + } + + /// + /// Return all the applications with the result elt. + /// + public IEnumerable AppsWithResult(Element elt) + { + foreach (var r in elt.References) { + if (r.Func == this && r.Result == elt) + yield return r; + } + } + + /// + /// For a nullary function, return its value. + /// + public Element GetConstant() + { + if (Arity != 0) + throw new ArgumentException(); + if (apps.Count == 0) + SetConstant(Model.MkElement("**" + Name)); + return apps[0].Result; + } + + /// + /// If all arguments are non-null, and function application for them exists return the value, otherwise return null. + /// + public Element OptEval(params Element[] args) + { + if (args.Any(a => a == null)) return null; + return TryEval(args); + } + + /// + /// Look for function application with given arguments and return its value or null if no such application exists. + /// + public Element TryEval(params Element[] args) + { + for (int i = 0; i < args.Length; ++i) + if(args[i]==null) + throw new ArgumentException(); + + if (apps.Count > 10) { + var best = apps; + for (int i = 0; i < args.Length; ++i) + if (args[i].references.Count < best.Count) + best = args[i].references; + if (best != apps) { + foreach (var tpl in best) { + bool same = true; + if (tpl.Func != this) + continue; + for (int i = 0; i < args.Length; ++i) + if (tpl.Args[i] != args[i]) { + same = false; + break; + } + if (same) return tpl.Result; + } + return null; + } + } + + foreach (var tpl in apps) { + bool same = true; + for (int i = 0; i < args.Length; ++i) + if (tpl.Args[i] != args[i]) { + same = false; + break; + } + if (same) return tpl.Result; + } + return null; + } + + /// + /// Look for function application with a subsequence of given arguments and return its value or null if no such application exists. + /// + public Element TryPartialEval(params Element[] args) + { + foreach (var tpl in apps) { + int j = 0; + for (int i = 0; i < args.Length; ++i) { + if (tpl.Args[j] == args[i]) { + j++; + if (j == tpl.Args.Length) + return tpl.Result; + } + } + } + return null; + } + + /// + /// Short for TryEval(args) == (Element)true + /// + public bool IsTrue(params Element[] args) + { + var r = TryEval(args) as Boolean; + return r != null && r.Value; + } + + /// + /// Short for TryEval(args) == (Element)false + /// + public bool IsFalse(params Element[] args) + { + var r = TryEval(args) as Boolean; + return r != null && !r.Value; + } + + public void AddApp(Element res, params Element[] args) + { + if (Arity == 0) + SetConstant(res); + else { + if (args.Length != Arity) + throw new ArgumentException(); + var t = new FuncTuple(this, res, (Element[])args.Clone()); + apps.Add(t); + var u = new HashSet(); + res.references.Add(t); + u.Add(res); + foreach (var a in args) + if (!u.Contains(a)) { + u.Add(a); + a.references.Add(t); + } + } + } + } + + public class FuncTuple + { + static readonly Element[] EmptyArgs = new Element[0]; + + // These should be immutable, except when Substituting the entire model + public readonly Func Func; + public Element Result; + public readonly Element[] Args; + + internal FuncTuple(Func func, Element res, Element[] args) + { + if (args == null) Args = EmptyArgs; + else Args = args; + Func = func; + Result = res; + } + + public override string ToString() + { + var res = new StringBuilder(); + res.Append("(").Append(Func.Name); + for (int i = 0; i < Args.Length; ++i) { + res.Append(" ").Append(Args[i]); + } + res.Append(") -> ").Append(Result); + return res.ToString(); + } + } + #endregion + + private List functions = new List(); + private List elements = new List(); + private List states = new List(); + private Dictionary functionsByName = new Dictionary(); + private Dictionary elementsByName = new Dictionary(); + + #region factory methods + Element ConstructElement(string name) + { + if (name.ToLower() == "true") return True; + if (name.ToLower() == "false") return False; + + if (name.StartsWith("bv") && name.Length > 4 && Char.IsDigit(name[2])) + name = name.Substring(2); + + if (Char.IsDigit(name[0]) || name[0] == '-') { + int col = name.IndexOf("bv"); + int szi = -1; + + if (name.EndsWith(":int")) + name = name.Substring(0, name.Length - 4); + + if (col > 0) { + if (int.TryParse(name.Substring(col + 2), out szi) && szi > 0) { + name = name.Substring(0, col); + } else { + return null; + } + } else if (name.EndsWith("]")) { + col = name.IndexOf("["); + if (col > 0 && int.TryParse(name.Substring(col + 1, name.Length - col - 2), out szi) && szi > 0) { + name = name.Substring(0, col); + } else { + return null; + } + } + + for (int i = 1; i < name.Length; ++i) + if (!Char.IsDigit(name[i])) + return null; + + if (szi > 0) + return new BitVector(this, name, szi); + else + return new Integer(this, name); + } else if (name[0] == '*' || name.StartsWith("val!") || name.Contains("!val!")) { + return new Uninterpreted(this, name); + } else if (name.StartsWith("as-array[") && name.EndsWith("]")) { + var fnName = name.Substring(9, name.Length - 10); + return new Array(this, MkFunc(fnName, 1)); + } else { + return new DatatypeValue(this, name, new List()); + } + } + + public Element TryMkElement(string name) + { + Element res; + + if (elementsByName.TryGetValue(name, out res)) + return res; + + var tmp = ConstructElement(name); + if (tmp == null) return null; + + name = tmp.ToString(); + if (elementsByName.TryGetValue(name, out res)) + return res; + + elementsByName.Add(name, tmp); + elements.Add(tmp); + return tmp; + } + + public Element MkElement(string name) + { + Element res = TryMkElement(name); + if (res == null) + throw new ArgumentException("invalid element name: '" + name + "'"); + return res; + } + + public Func MkFunc(string name, int arity) + { + Func res; + if (functionsByName.TryGetValue(name, out res)) { + if (res.Arity != arity) + throw new ArgumentException(string.Format("function '{0}' previously created with arity {1}, now trying to recreate with arity {2}", name, res.Arity, arity)); + return res; + } + res = new Func(this, name, arity); + functionsByName.Add(name, res); + functions.Add(res); + return res; + } + #endregion + + #region state management + public class CapturedState + { + List vars = new List(); + Dictionary valuations = new Dictionary(); + readonly CapturedState previous; + // AL: Dropping "readonly" for corral + public /* readonly */ string Name { get; private set; } + + public IEnumerable Variables { get { return vars; } } + public IEnumerable AllVariables { + get { + if (previous != null) + return previous.AllVariables.Concat(Variables).Distinct(); + else + return Variables; + } + } + public int VariableCount { get { return vars.Count; } } + public bool HasBinding(string varname) + { + return valuations.ContainsKey(varname); + } + public Element TryGet(string varname) + { + CapturedState curr = this; + while (curr != null) { + Element res; + if (curr.valuations.TryGetValue(varname, out res)) + return res; + curr = curr.previous; + } + return null; + } + + public void AddBinding(string varname, Element value) + { + vars.Add(varname); + valuations.Add(varname, value); + } + + // Change name of the state + public void ChangeName(string newName) + { + Name = newName; + } + + // Change names of variables in this state + // (Used by corral) + internal void ChangeVariableNames(Dictionary varNameMap) + { + var oldVars = vars; + var oldValuations = valuations; + + vars = new List(); + valuations = new Dictionary(); + + foreach (var v in oldVars) + { + if (varNameMap.ContainsKey(v)) vars.Add(varNameMap[v]); + else vars.Add(v); + } + + foreach (var kvp in oldValuations) + { + if (varNameMap.ContainsKey(kvp.Key)) valuations.Add(varNameMap[kvp.Key], kvp.Value); + else valuations.Add(kvp.Key, kvp.Value); + } + } + + internal CapturedState(string name, CapturedState prev) + { + Name = name; + previous = prev; + } + } + + public CapturedState MkState(string name) + { + var last = states[states.Count - 1]; + var s = new CapturedState(name, last); + states.Add(s); + return s; + } + + // Change names of variables in all captured states + // (Used by corral) + public void ChangeVariableNames(Dictionary varNameMap) + { + foreach (var s in states) + { + s.ChangeVariableNames(varNameMap); + } + } + + #endregion + + public Model() + { + InitialState = new CapturedState("", null); + states.Add(InitialState); + True = new Boolean(this, true); + elements.Add(True); + elementsByName.Add("true", True); + False = new Boolean(this, false); + elements.Add(False); + elementsByName.Add("false", False); + } + + public IEnumerable Functions { get { return functions; } } + public IEnumerable Elements { get { return elements; } } + public IEnumerable States { get { return states; } } + public readonly Element True, False; + public readonly CapturedState InitialState; + + public bool HasFunc(string name) + { + return functionsByName.ContainsKey(name); + } + + public Func TryGetFunc(string name) + { + Func res; + if (functionsByName.TryGetValue(name, out res)) + return res; + else + return null; + } + + public Func GetFunc(string name) + { + Func res = TryGetFunc(name); + if (res == null) + throw new KeyNotFoundException("function '" + name + "' undefined in the model"); + return res; + } + + public Func TryGetSkolemFunc(string name) + { + return Functions.Where(f => f.Name.StartsWith(name + "!")).FirstOrDefault(); + } + + public Element GetElement(string name) + { + Element res; + if (elementsByName.TryGetValue(name, out res)) + return res; + else + throw new KeyNotFoundException("element '" + name + "' undefined in the model"); + } + + public Element MkIntElement(int v) + { + return MkElement(v.ToString()); + } + + public void Write(System.IO.TextWriter wr) + { + wr.WriteLine("*** MODEL"); + foreach (var f in Functions.OrderBy(f => f.Name)) + if (f.Arity == 0) { + wr.WriteLine("{0} -> {1}", f.Name, f.GetConstant()); + } + foreach (var f in Functions) + if (f.Arity != 0) { + wr.WriteLine("{0} -> {1}", f.Name, "{"); + foreach (var app in f.Apps) { + wr.Write(" "); + foreach (var a in app.Args) + wr.Write("{0} ", a); + wr.WriteLine("-> {0}", app.Result); + } + if (f.Else != null) + wr.WriteLine(" else -> {0}", f.Else); + wr.WriteLine("}"); + } + foreach (var s in States) { + if (s == InitialState && s.VariableCount == 0) + continue; + wr.WriteLine("*** STATE {0}", s.Name); + foreach (var v in s.Variables) + wr.WriteLine(" {0} -> {1}", v, s.TryGet(v)); + wr.WriteLine("*** END_STATE", s.Name); + } + wr.WriteLine("*** END_MODEL"); + } + + public void Substitute(Dictionary mapping) { + foreach (var f in functions) f.Substitute(mapping); + } + + public static List ParseModels(System.IO.TextReader rd) + { + ModelParser p = new ParserZ3(); + p.rd = rd; + p.Run(); + return p.resModels; + } + } +} diff --git a/Source/Model/Model.csproj b/Source/Model/Model.csproj index c6a1d047..dc0ae5e1 100644 --- a/Source/Model/Model.csproj +++ b/Source/Model/Model.csproj @@ -1,109 +1,109 @@ - - - - Debug - AnyCPU - 8.0.30703 - 2.0 - {ACEF88D5-DADD-46DA-BAE1-2144D63F4C83} - Library - Properties - Microsoft.Boogie - Model - v4.0 - 512 - Client - 0 - - - true - full - false - ..\..\Binaries\ - DEBUG;TRACE - prompt - 4 - - - pdbonly - true - ..\..\Binaries\ - TRACE - prompt - 4 - - - true - - - ..\InterimKey.snk - - - true - ..\..\Binaries\ - DEBUG;TRACE - full - AnyCPU - bin\Debug\Model.dll.CodeAnalysisLog.xml - true - GlobalSuppressions.cs - prompt - MinimumRecommendedRules.ruleset - ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets - ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules - True - False - True - False - False - False - False - False - False - False - False - False - True - False - False - False - - - - - - - False - Full - Build - 0 - 4 - false - - - true - bin\QED\ - DEBUG;TRACE - full - AnyCPU - prompt - MinimumRecommendedRules.ruleset - - - - - - - - - - - - - + + + + Debug + AnyCPU + 8.0.30703 + 2.0 + {ACEF88D5-DADD-46DA-BAE1-2144D63F4C83} + Library + Properties + Microsoft.Boogie + Model + v4.0 + 512 + Client + 0 + + + true + full + false + ..\..\Binaries\ + DEBUG;TRACE + prompt + 4 + + + pdbonly + true + ..\..\Binaries\ + TRACE + prompt + 4 + + + true + + + ..\InterimKey.snk + + + true + ..\..\Binaries\ + DEBUG;TRACE + full + AnyCPU + bin\Debug\Model.dll.CodeAnalysisLog.xml + true + GlobalSuppressions.cs + prompt + MinimumRecommendedRules.ruleset + ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets + ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules + True + False + True + False + False + False + False + False + False + False + False + False + True + False + False + False + + + + + + + False + Full + Build + 0 + 4 + false + + + true + bin\QED\ + DEBUG;TRACE + full + AnyCPU + prompt + MinimumRecommendedRules.ruleset + + + + + + + + + + + + + diff --git a/Source/Model/ModelParser.cs b/Source/Model/ModelParser.cs index 3b9fbb6f..b966d649 100644 --- a/Source/Model/ModelParser.cs +++ b/Source/Model/ModelParser.cs @@ -66,8 +66,8 @@ namespace Microsoft.Boogie string s = o as string; if (s != null) return GetElt (s); - List os = (List)o; - if (!(os[0] is string)) + List os = (List)o; + if (!(os[0] is string)) os.Insert(0, "_"); // KLM: fix crash on ((as const (Array Int Int)) 0) List args = new List (); for (int i = 1; i < os.Count; i++) { diff --git a/Source/Model/Properties/AssemblyInfo.cs b/Source/Model/Properties/AssemblyInfo.cs index 80c3907a..d69add5b 100644 --- a/Source/Model/Properties/AssemblyInfo.cs +++ b/Source/Model/Properties/AssemblyInfo.cs @@ -1,23 +1,23 @@ -using System.Reflection; -using System.Runtime.CompilerServices; -using System.Runtime.InteropServices; - -// General Information about an assembly is controlled through the following -// set of attributes. Change these attribute values to modify the information -// associated with an assembly. -[assembly: AssemblyTitle("Model")] -[assembly: AssemblyDescription("")] -[assembly: AssemblyConfiguration("")] -[assembly: AssemblyCompany("Microsoft")] -[assembly: AssemblyProduct("Model")] -[assembly: AssemblyCopyright("Copyright © Microsoft 2010-2011")] -[assembly: AssemblyTrademark("")] -[assembly: AssemblyCulture("")] - -// Setting ComVisible to false makes the types in this assembly not visible -// to COM components. If you need to access a type in this assembly from -// COM, set the ComVisible attribute to true on that type. -[assembly: ComVisible(false)] - -// The following GUID is for the ID of the typelib if this project is exposed to COM -[assembly: Guid("24299c94-99db-46c5-8671-5f91faac167e")] +using System.Reflection; +using System.Runtime.CompilerServices; +using System.Runtime.InteropServices; + +// General Information about an assembly is controlled through the following +// set of attributes. Change these attribute values to modify the information +// associated with an assembly. +[assembly: AssemblyTitle("Model")] +[assembly: AssemblyDescription("")] +[assembly: AssemblyConfiguration("")] +[assembly: AssemblyCompany("Microsoft")] +[assembly: AssemblyProduct("Model")] +[assembly: AssemblyCopyright("Copyright © Microsoft 2010-2011")] +[assembly: AssemblyTrademark("")] +[assembly: AssemblyCulture("")] + +// Setting ComVisible to false makes the types in this assembly not visible +// to COM components. If you need to access a type in this assembly from +// COM, set the ComVisible attribute to true on that type. +[assembly: ComVisible(false)] + +// The following GUID is for the ID of the typelib if this project is exposed to COM +[assembly: Guid("24299c94-99db-46c5-8671-5f91faac167e")] -- cgit v1.2.3