Put Model.cs in separate assembly. Fix signing/versioning with it.

1 files changed, 0 insertions, 546 deletions

diff --git a/Source/VCGeneration/Model.cs b/Source/VCGeneration/Model.cs
deleted file mode 100644
index d309c01d..00000000
--- a/Source/VCGeneration/Model.cs
+++ /dev/null
@@ -1,546 +0,0 @@
-//-----------------------------------------------------------------------------

-//

-// Copyright (C) Microsoft Corporation.  All Rights Reserved.

-//

-//-----------------------------------------------------------------------------

-using System;

-using System.Collections.Generic;

-

-namespace Microsoft.Boogie

-{

-  public class Model

-  {

-    #region Elements and functions (inner classes)

-    public enum ElementKind

-    {

-      Integer,

-      BitVector,

-      Boolean,

-      Uninterpreted

-    }

-

-    abstract public class Element

-    {

-      public readonly Model Model;

-      internal List<FuncTuple> references = new List<FuncTuple>();

-      public readonly int Id;

-

-      public IEnumerable<FuncTuple> References { get { return references; } }

-      

-      public IEnumerable<FuncTuple> Names { 

-        get {

-          foreach (var f in references)

-            if (f.Result == this) yield return f;

-        } 

-      }

-

-      public IEnumerable<FuncTuple> ArgReferences

-      {

-        get

-        {

-          foreach (var f in references) {

-            if (f.Result != this)

-              yield return f;

-            else

-              foreach (var r in f.Args)

-                if (r == this) { yield return f; break; }

-          }

-        }

-      }

-

-      protected Element(Model p) { Model = p; }

-      public abstract ElementKind Kind { get; }

-      public virtual int AsInt() { throw new NotImplementedException(); }

-    }

-

-    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 Func

-    {

-      public readonly Model Model;

-      public readonly string Name;

-      public readonly int Arity;

-      internal readonly List<FuncTuple> apps = new List<FuncTuple>();

-      public IEnumerable<FuncTuple> Apps { get { return apps; } }

-      public int AppCount { get { return apps.Count; } }

-

-      internal Func(Model p, string n, int a) { Model = p;  Name = n; Arity = a; }

-

-      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);

-      }

-

-      public Element GetConstant()

-      {

-        if (Arity != 0)

-          throw new ArgumentException();

-        if (apps.Count == 0)

-          SetConstant(Model.MkElement("**" + Name));

-        return apps[0].Result;

-      }

-

-      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<Element>();

-          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];

-

-      public readonly Func Func;

-      public readonly 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;

-      }

-    }

-    #endregion

-

-    private List<Func> functions = new List<Func>();

-    private List<Element> elements = new List<Element>();

-    private List<CapturedState> states = new List<CapturedState>();

-    private Dictionary<string, Func> functionsByName = new Dictionary<string, Func>();

-    private Dictionary<string, Element> elementsByName = new Dictionary<string, Element>();

-

-    #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!")) {

-        return new Uninterpreted(this, name);

-      } else {

-        return null;

-      }

-    }

-

-    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<string> vars = new List<string>();

-      Dictionary<string, Element> valuations = new Dictionary<string, Element>();

-      readonly CapturedState previous;

-      public readonly string Name;

-

-      public IEnumerable<string> Variables { get { return vars; } }

-      public int VariableCount { get { return vars.Count; } }

-      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);

-      }

-

-      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;

-    }

-    #endregion

-

-    public Model()

-    {

-      InitialState = new CapturedState("<initial>", null);

-      states.Add(InitialState);

-      True = new Boolean(this, true);

-      False = new Boolean(this, false);

-      elements.Add(True);

-      elements.Add(False);

-      elementsByName.Add("true", True);

-      elementsByName.Add("false", False);

-    }

-

-    public IEnumerable<Func> Functions { get { return functions; } }

-    public IEnumerable<Element> Elements { get { return elements; } }

-    public IEnumerable<CapturedState> 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 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 void Write(System.IO.TextWriter wr)

-    {

-      wr.WriteLine("*** MODEL");

-      foreach (var f in Functions)

-        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);

-          }

-          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");

-    }

-

-    class Parser

-    {

-      internal System.IO.TextReader rd;

-      string lastLine = "";

-      int lineNo;

-      bool v1model = false;

-      Dictionary<string, Element> partitionMapping = new Dictionary<string, Element>(); // only used when v1model is true

-      internal List<Model> resModels = new List<Model>();

-      Model currModel;

-

-      void BadModel(string msg)

-      {

-        throw new ArgumentException(string.Format("Invalid model: {0}, at line {1} ({2})", msg, lineNo, lastLine));

-      }

-

-      static char[] seps = new char[] { ' ' };

-

-      string[] GetWords(string line)

-      {

-        if (line == null)

-          return null;

-        var words = line.Split(seps, StringSplitOptions.RemoveEmptyEntries);

-        return words;

-      }

-

-      string ReadLine()

-      {

-        var l = rd.ReadLine();

-        if (l != null) {

-          lineNo++;

-          lastLine = l;

-        }

-        return l;

-      }

-

-      Element GetElt(string name)

-      {

-        Element ret;

-

-        if (v1model) {

-          if (!partitionMapping.TryGetValue(name, out ret))

-            BadModel("undefined partition " + name);

-        } else {

-          ret = currModel.TryMkElement(name);

-          if (ret == null)

-            BadModel("invalid element name " + name);

-        }

-

-        return ret;

-      }

-

-      void NewModel()

-      {

-        v1model = false;

-        partitionMapping.Clear();

-        lastLine = "";

-        currModel = new Model();

-        resModels.Add(currModel);

-      }

-

-      internal void Run()

-      {

-        for (; ; ) {

-          var line = ReadLine();

-          if (line == null) break; // end of model, everything fine

-

-          if (line == "Counterexample:" || line == "Z3 error model: " || line == "*** MODEL") {

-            NewModel();

-            continue;

-          }

-

-          if (line.EndsWith(": Invalid.") || line.EndsWith(": Valid.")|| line.StartsWith("labels:"))

-            continue;

-          if (line == "END_OF_MODEL" || line == "." || line == "*** END_MODEL")

-            continue;

-          if (line == "partitions:" || line == "function interpretations:") {

-            v1model = true;

-            continue;

-          }

-

-          var words = GetWords(line);

-          if (words.Length == 0) continue;

-          var lastWord = words[words.Length - 1];

-

-          if (currModel == null)

-            BadModel("model begin marker not found");

-

-          if (line.StartsWith("*** STATE ")) {

-            var name = line.Substring(10);

-            CapturedState cs;

-            if (name == "<initial>")

-              cs = currModel.InitialState;

-            else

-              cs = currModel.MkState(name);

-            for (; ; ) {

-              var tmpline = ReadLine();

-              if (tmpline == "*** END_STATE") break;

-              var tuple = GetWords(tmpline);

-              if (tuple == null) BadModel("EOF in state table");

-              if (tuple.Length == 0) continue;

-              if (tuple.Length != 3 || tuple[1] != "->") BadModel("invalid state tuple definition");

-              cs.AddBinding(tuple[0], GetElt(tuple[2]));

-            }

-            continue;

-          }

-

-          if (v1model && words[0][0] == '*') {

-            var partName = words[0];

-            var len = words.Length;

-            Element elt;

-            if (len >= 3 && words[len - 2] == "->") {

-              elt = currModel.TryMkElement(lastWord);

-              if (elt == null) BadModel("bad parition value " + lastWord);

-              len -= 2;

-            } else {

-              elt = currModel.MkElement(words[0]);

-            }

-            partitionMapping.Add(partName, elt);

-            for (int i = 1; i < len; ++i) {

-              var name = words[i];

-              if (i == 1 && name[0] == '{')

-                name = name.Substring(1);

-              if (i == len - 1 && name.EndsWith("}"))

-                name = name.Substring(0, name.Length - 1);

-              var cnst = currModel.MkFunc(name, 0);

-              cnst.SetConstant(elt);

-            }

-

-          } else if (words.Length == 3 && words[1] == "->") {

-            Func fn = null;

-            var funName = words[0];

-

-            if (lastWord == "{") {

-              for (; ; ) {

-                var tuple = GetWords(ReadLine());

-                if (tuple == null) BadModel("EOF in function table");

-                if (tuple.Length == 0) continue;

-                if (tuple.Length == 1 && tuple[0] == "}") break;

-                if (tuple.Length < 3 || tuple[tuple.Length - 2] != "->") BadModel("invalid function tuple definition");

-                if (tuple[0] == "else") continue;

-                if (fn == null)

-                  fn = currModel.MkFunc(funName, tuple.Length - 2);

-                var args = new Element[fn.Arity];

-                for (int i = 0; i < fn.Arity; ++i)

-                  args[i] = GetElt(tuple[i]);

-                fn.AddApp(GetElt(tuple[tuple.Length - 1]), args);

-              }

-            } else {

-              fn = currModel.MkFunc(funName, 0);

-              fn.SetConstant(GetElt(lastWord));

-            }

-          } else {

-            BadModel("unidentified line");

-          }

-        }

-      }

-    }

-

-    public static List<Model> ParseModels(System.IO.TextReader rd)

-    {

-      var p = new Parser();

-      p.rd = rd;

-      p.Run();

-      return p.resModels;

-    }

-

-  }

-}