the cvc4 parser can now parse nested array expressions

1 files changed, 471 insertions, 457 deletions

diff --git a/Source/Model/ModelParser.cs b/Source/Model/ModelParser.cs
index 9a455662..5de903ab 100644
--- a/Source/Model/ModelParser.cs
+++ b/Source/Model/ModelParser.cs
@@ -3,7 +3,6 @@
 // Copyright (C) Microsoft Corporation.  All Rights Reserved.
 //
 //-----------------------------------------------------------------------------
-
 using System;
 using System.Linq;
 using System.Collections.Generic;
@@ -17,28 +16,27 @@ namespace Microsoft.Boogie
 	{
 		protected Model currModel;
 		int lineNo;
-		internal List<Model> resModels = new List<Model>();
+		internal List<Model> resModels = new List<Model> ();
 		internal System.IO.TextReader rd;
-
 		string lastLine = "";
 		protected static char[] seps = new char[] { ' ' };
-		protected static Regex bv = new Regex(@"\(_ BitVec (\d+)\)");
+		protected static Regex bv = new Regex (@"\(_ BitVec (\d+)\)");
 
-		protected void NewModel()
+		protected void NewModel ()
 		{
 			lastLine = "";
-			currModel = new Model();
-			resModels.Add(currModel);
+			currModel = new Model ();
+			resModels.Add (currModel);
 		}
 
-		protected void BadModel(string msg)
+		protected void BadModel (string msg)
 		{
-			throw new ArgumentException(string.Format("Invalid model: {0}, at line {1} ({2})", msg, lineNo, lastLine));
+			throw new ArgumentException (string.Format ("Invalid model: {0}, at line {1} ({2})", msg, lineNo, lastLine));
 		}
 
-		protected string ReadLine()
+		protected string ReadLine ()
 		{
-			var l = rd.ReadLine();
+			var l = rd.ReadLine ();
 			if (l != null) {
 				lineNo++;
 				lastLine = l;
@@ -46,34 +44,36 @@ namespace Microsoft.Boogie
 			return l;
 		}
 
-		string[] GetWords(string line)
+		string[] GetWords (string line)
 		{
 			if (line == null)
 				return null;
-			var words = line.Split(seps, StringSplitOptions.RemoveEmptyEntries);
+			var words = line.Split (seps, StringSplitOptions.RemoveEmptyEntries);
 			return words;
 		}
 
-		Model.Element GetElt(string name) {
-			Model.Element ret = currModel.TryMkElement(name);
+		Model.Element GetElt (string name)
+		{
+			Model.Element ret = currModel.TryMkElement (name);
 			if (ret == null)
-				BadModel("invalid element name " + name);
+				BadModel ("invalid element name " + name);
 			return ret;
 		}
 
-		protected Model.Element GetElt(object o) {
+		protected Model.Element GetElt (object o)
+		{
 			string s = o as string;
 			if (s != null)
-				return GetElt(s);
+				return GetElt (s);
 			List<object> os = (List<object>)o;
-			List<Model.Element> args = new List<Model.Element>();
+			List<Model.Element> args = new List<Model.Element> ();
 			for (int i = 1; i < os.Count; i++) {
-				args.Add(GetElt(os[i]));
+				args.Add (GetElt (os [i]));
 			}
-			return new Model.DatatypeValue(currModel, (string)os[0], args);
+			return new Model.DatatypeValue (currModel, (string)os [0], args);
 		}
 
-		protected int CountOpenParentheses(string s, int n)
+		protected int CountOpenParentheses (string s, int n)
 		{
 			int f = n;
 			foreach (char c in s) {
@@ -82,182 +82,175 @@ namespace Microsoft.Boogie
 				else if (c == ')')
 					f--;
 			}
-			if (f < 0) BadModel("mismatched parentheses in datatype term");
+			if (f < 0)
+				BadModel ("mismatched parentheses in datatype term");
 			return f;
 		}
 
-		abstract internal void Run();
+		abstract internal void Run ();
 	}
 
 	class ParserZ3 : ModelParser
 	{
-		List<object> GetFunctionTokens(string newLine)
+		List<object> GetFunctionTokens (string newLine)
 		{
 			if (newLine == null)
 				return null;
-			newLine = bv.Replace(newLine, "bv${1}");
+			newLine = bv.Replace (newLine, "bv${1}");
 			string line = newLine;
-			int openParenCounter = CountOpenParentheses(newLine, 0);
-			if (!newLine.Contains("}"))
-			{
-				while (openParenCounter > 0)
-				{
-					newLine = ReadLine();
-					if (newLine == null)
-					{
+			int openParenCounter = CountOpenParentheses (newLine, 0);
+			if (!newLine.Contains ("}")) {
+				while (openParenCounter > 0) {
+					newLine = ReadLine ();
+					if (newLine == null) {
 						return null;
 					}
 					line += newLine;
-					openParenCounter = CountOpenParentheses(newLine, openParenCounter);
+					openParenCounter = CountOpenParentheses (newLine, openParenCounter);
 				}
 			}
 
-			line = line.Replace("(", " ( ");
-			line = line.Replace(")", " ) ");
-			var tuple = line.Split(seps, StringSplitOptions.RemoveEmptyEntries);
-
-			List<object> newTuple = new List<object>();
-			Stack<List<object>> wordStack = new Stack<List<object>>();
-			for (int i = 0; i < tuple.Length; i++)
-			{
-				string elem = tuple[i];
-				if (elem == "(")
-				{
-					List<object> ls = new List<object>();
-					wordStack.Push(ls);
-				}
-				else if (elem == ")")
-				{
-					List<object> ls = wordStack.Pop();
-					if (wordStack.Count > 0)
-					{
-						wordStack.Peek().Add(ls);
-					}
-					else
-					{
-						newTuple.Add(ls);
+			line = line.Replace ("(", " ( ");
+			line = line.Replace (")", " ) ");
+			var tuple = line.Split (seps, StringSplitOptions.RemoveEmptyEntries);
+
+			List<object> newTuple = new List<object> ();
+			Stack<List<object>> wordStack = new Stack<List<object>> ();
+			for (int i = 0; i < tuple.Length; i++) {
+				string elem = tuple [i];
+				if (elem == "(") {
+					List<object> ls = new List<object> ();
+					wordStack.Push (ls);
+				} else if (elem == ")") {
+					List<object> ls = wordStack.Pop ();
+					if (wordStack.Count > 0) {
+						wordStack.Peek ().Add (ls);
+					} else {
+						newTuple.Add (ls);
 					}
-				}
-				else if (wordStack.Count > 0)
-				{
-					wordStack.Peek().Add(elem);
-				}
-				else
-				{
-					newTuple.Add(elem);
+				} else if (wordStack.Count > 0) {
+					wordStack.Peek ().Add (elem);
+				} else {
+					newTuple.Add (elem);
 				}
 			}
 			return newTuple;
 		}
 
-		internal override void Run()
+		internal override void Run ()
 		{
-			var selectFunctions = new Dictionary<int, Model.Func>();
-			var storeFunctions = new Dictionary<int, Model.Func>();
-			for (; ; ) {
-				var line = ReadLine();
-				if (line == null) break; // end of model, everything fine
+			var selectFunctions = new Dictionary<int, Model.Func> ();
+			var storeFunctions = new Dictionary<int, Model.Func> ();
+			for (; ;) {
+				var line = ReadLine ();
+				if (line == null)
+					break; // end of model, everything fine
 
 				if (line == "Counterexample:" || line == "Error model: " || line == "*** MODEL") {
-					NewModel();
+					NewModel ();
 					continue;
 				}
 
-				if (line.EndsWith(": Invalid.") || line.EndsWith(": Valid.")|| line.StartsWith("labels:"))
+				if (line.EndsWith (": Invalid.") || line.EndsWith (": Valid.") || line.StartsWith ("labels:"))
 					continue;
 				if (line == "END_OF_MODEL" || line == "." || line == "*** END_MODEL")
 					continue;
 
-				var words = GetFunctionTokens(line);
-				if (words.Count == 0) continue;
-				var lastWord = words[words.Count - 1];
+				var words = GetFunctionTokens (line);
+				if (words.Count == 0)
+					continue;
+				var lastWord = words [words.Count - 1];
 
 				if (currModel == null)
-					BadModel("model begin marker not found");
+					BadModel ("model begin marker not found");
 
-				if (line.StartsWith("*** STATE ")) {
-					var name = line.Substring(10);
+				if (line.StartsWith ("*** STATE ")) {
+					var name = line.Substring (10);
 					Model.CapturedState cs;
 					if (name == "<initial>")
 						cs = currModel.InitialState;
 					else
-						cs = currModel.MkState(name);
-					for (; ; ) {
-						var tmpline = ReadLine();
-						if (tmpline == "*** END_STATE") break;
-						var tuple = GetFunctionTokens(tmpline);
-						if (tuple == null) BadModel("EOF in state table");
-						if (tuple.Count == 0) continue;
-						if (tuple.Count == 3 && tuple[0] is string && tuple[1] is string && ((string) tuple[1]) == "->")
-						{
-							cs.AddBinding((string)tuple[0], GetElt(tuple[2]));
-						}
-						else
-						{
-							BadModel("invalid state tuple definition");
+						cs = currModel.MkState (name);
+					for (; ;) {
+						var tmpline = ReadLine ();
+						if (tmpline == "*** END_STATE")
+							break;
+						var tuple = GetFunctionTokens (tmpline);
+						if (tuple == null)
+							BadModel ("EOF in state table");
+						if (tuple.Count == 0)
+							continue;
+						if (tuple.Count == 3 && tuple [0] is string && tuple [1] is string && ((string)tuple [1]) == "->") {
+							cs.AddBinding ((string)tuple [0], GetElt (tuple [2]));
+						} else {
+							BadModel ("invalid state tuple definition");
 						}
 					}
 					continue;
 				}
 
-				if (words.Count == 3 && words[1] is string && ((string) words[1]) == "->") {
-					var funName = (string) words[0];
+				if (words.Count == 3 && words [1] is string && ((string)words [1]) == "->") {
+					var funName = (string)words [0];
 					Model.Func fn = null;
 
-					if (lastWord is string && ((string) lastWord) == "{") {
-						fn = currModel.TryGetFunc(funName);
-						for ( ; ; ) {
-							var tuple = GetFunctionTokens(ReadLine());
-							if (tuple == null) BadModel("EOF in function table");
-							if (tuple.Count == 0) continue;
-							string tuple0 = tuple[0] as string;
+					if (lastWord is string && ((string)lastWord) == "{") {
+						fn = currModel.TryGetFunc (funName);
+						for (; ;) {
+							var tuple = GetFunctionTokens (ReadLine ());
+							if (tuple == null)
+								BadModel ("EOF in function table");
+							if (tuple.Count == 0)
+								continue;
+							string tuple0 = tuple [0] as string;
 							if (tuple.Count == 1) {
 								if (fn == null)
-									fn = currModel.MkFunc(funName, 1);
-								if (tuple0 == "}") break;
+									fn = currModel.MkFunc (funName, 1);
+								if (tuple0 == "}")
+									break;
 								if (fn.Else == null)
-									fn.Else = GetElt(tuple[0]);
+									fn.Else = GetElt (tuple [0]);
 								continue;
 							}
-							string tuplePenultimate = tuple[tuple.Count - 2] as string;
-							if (tuplePenultimate != "->") BadModel("invalid function tuple definition");
-							var resultName = tuple[tuple.Count - 1];
+							string tuplePenultimate = tuple [tuple.Count - 2] as string;
+							if (tuplePenultimate != "->")
+								BadModel ("invalid function tuple definition");
+							var resultName = tuple [tuple.Count - 1];
 							if (tuple0 == "else") {
 								if (fn != null && !(resultName is string && ((string)resultName) == "#unspecified") && fn.Else == null) {
-									fn.Else = GetElt(resultName);
+									fn.Else = GetElt (resultName);
 								}
 								continue;
 							}
 
 							if (fn == null) {
 								var arity = tuple.Count - 2;
-								if (Regex.IsMatch(funName, "^MapType[0-9]*Select$")) {
-									funName = string.Format("[{0}]", arity);
-									if (!selectFunctions.TryGetValue(arity, out fn)) {
-										fn = currModel.MkFunc(funName, arity);
-										selectFunctions.Add(arity, fn);
+								if (Regex.IsMatch (funName, "^MapType[0-9]*Select$")) {
+									funName = string.Format ("[{0}]", arity);
+									if (!selectFunctions.TryGetValue (arity, out fn)) {
+										fn = currModel.MkFunc (funName, arity);
+										selectFunctions.Add (arity, fn);
 									}
-								} else if (Regex.IsMatch(funName, "^MapType[0-9]*Store$")) {
-									funName = string.Format("[{0}:=]", arity);
-									if (!storeFunctions.TryGetValue(arity, out fn)) {
-										fn = currModel.MkFunc(funName, arity);
-										storeFunctions.Add(arity, fn);
+								} else if (Regex.IsMatch (funName, "^MapType[0-9]*Store$")) {
+									funName = string.Format ("[{0}:=]", arity);
+									if (!storeFunctions.TryGetValue (arity, out fn)) {
+										fn = currModel.MkFunc (funName, arity);
+										storeFunctions.Add (arity, fn);
 									}
 								} else {
-									fn = currModel.MkFunc(funName, arity);
+									fn = currModel.MkFunc (funName, arity);
 								}
 							}
 							var args = new Model.Element[fn.Arity];
 							for (int i = 0; i < fn.Arity; ++i)
-								args[i] = GetElt(tuple[i]);
-							fn.AddApp(GetElt(resultName), args);
+								args [i] = GetElt (tuple [i]);
+							fn.AddApp (GetElt (resultName), args);
 						}
 					} else {
-						fn = currModel.MkFunc(funName, 0);
-						fn.SetConstant(GetElt(lastWord));
+						fn = currModel.MkFunc (funName, 0);
+						fn.SetConstant (GetElt (lastWord));
 					}
 				} else {
-					BadModel("unidentified line");
+					BadModel ("unidentified line");
 				}
 			}
 		}
@@ -270,23 +263,22 @@ namespace Microsoft.Boogie
 		protected int arity;
 		protected int arrayNum;
 
-		abstract protected void ParseArray(ref int i);
-		abstract protected void ParseITE(ref int i);
+		abstract protected void ParseArray (ref int i);
 
-		protected void FindArity()
+		abstract protected void ParseITE (ref int i);
+
+		protected void FindArity ()
 		{
 			arity = 0;
 			int p_count = 1;
 			int i = 4;
 
-			while (p_count > 0)
-			{
+			while (p_count > 0) {
 				if (i == tokens.Length - 1)
 					break;
-				else if (tokens[i] == ")")
+				else if (tokens [i] == ")")
 					p_count--;
-				else if (tokens[i] == "(" && tokens[i + 1] != "ite")
-				{
+				else if (tokens [i] == "(" && tokens [i + 1] != "ite") {
 					p_count++;
 					arity++;
 				}
@@ -295,108 +287,96 @@ namespace Microsoft.Boogie
 			}
 		}
 
-		protected string GetValue(int idx)
+		protected string GetValue (int idx)
 		{
-			string value = tokens[idx];
+			string value = tokens [idx];
 
-			if (tokens[idx - 1] == "-")
-			{
+			if (tokens [idx - 1] == "-") {
 				value = "(- " + value + ")";
-			}
-			else if (tokens[idx - 2] == "_")
-			{
-				value = tokens[idx - 1] + "[" + tokens[idx] + "]";
+			} else if (tokens [idx - 2] == "_") {
+				value = tokens [idx - 1] + "[" + tokens [idx] + "]";
 			}
 
 			return value;
 		}
 
-		void ParseEndOfExpression(ref int i)
+		void ParseEndOfExpression (ref int i)
 		{
 			i++;
 
-			if (i == tokens.Length && output.Count == 2)
-			{
+			if (i == tokens.Length && output.Count == 2) {
 				i += -2;
 
-				if (tokens[i] == ")")
-				{
+				if (tokens [i] == ")") {
 					i += -1;
-					output.Add(GetValue(i));
-				}
-				else
-				{
-					output.Add(GetValue(i));
+					output.Add (GetValue (i));
+				} else {
+					output.Add (GetValue (i));
 				}
 			}
 
-			if (i == tokens.Length && output.Contains("{"))
-			{
-				output.Add(" ");
-				output.Add("}");
+			if (i == tokens.Length && output.Contains ("{")) {
+				output.Add (" ");
+				output.Add ("}");
 			}
 		}
 
-		List<string> GetParsedTokens(string newLine)
+		List<string> GetParsedTokens (string newLine)
 		{
 			if (newLine == null)
 				return null;
 
-			newLine = bv.Replace(newLine, "bv${1}");
+			newLine = bv.Replace (newLine, "bv${1}");
 
 			string line = newLine;
-			int openParenCounter = CountOpenParentheses(newLine, 0);
+			int openParenCounter = CountOpenParentheses (newLine, 0);
 
-			while (openParenCounter > 0)
-			{
-				newLine = ReadLine();
-				if (newLine == null)
-				{
+			while (openParenCounter > 0) {
+				newLine = ReadLine ();
+				if (newLine == null) {
 					return null;
 				}
 				line += newLine;
-				openParenCounter = CountOpenParentheses(newLine, openParenCounter);
+				openParenCounter = CountOpenParentheses (newLine, openParenCounter);
 			}
 
-			line = line.Replace("(", " ( ");
-			line = line.Replace(")", " ) ");
+			line = line.Replace ("(", " ( ");
+			line = line.Replace (")", " ) ");
 
-			tokens = line.Split(seps, StringSplitOptions.RemoveEmptyEntries);
-			output = new List<string>();
+			tokens = line.Split (seps, StringSplitOptions.RemoveEmptyEntries);
+			output = new List<string> ();
 
 			var i = 0;
 			bool doneParsing = false;
 
-			while(!doneParsing)
-			{
-				switch (tokens[i])
-				{
-					case ")":
-					ParseEndOfExpression(ref i);
+			while (!doneParsing) {
+				switch (tokens [i]) {
+				case ")":
+					ParseEndOfExpression (ref i);
 					break;
 
-					case "define-fun":
-					output.Add(GetValue(i+1));
-					output.Add("->");
+				case "define-fun":
+					output.Add (GetValue (i + 1));
+					output.Add ("->");
 					i += 2;
 					break;
 
-					case "Array":
-					ParseArray(ref i);
+				case "Array":
+					ParseArray (ref i);
 					break;
 
-					case "ite":
-					ParseITE(ref i);
+				case "ite":
+					ParseITE (ref i);
 					break;
 
-					case "_ufmt_1":
-					case "x!1":
-					output.Add("{");
-					output.Add(" ");
+				case "_ufmt_1":
+				case "x!1":
+					output.Add ("{");
+					output.Add (" ");
 					i++;
 					break;
 
-					default:
+				default:
 					i++;
 					break;
 				}
@@ -408,290 +388,348 @@ namespace Microsoft.Boogie
 			return output;
 		}
 
-		internal override void Run()
+		List<string>[] TrySplitExpr (List<string> expr)
 		{
-			var selectFunctions = new Dictionary<int, Model.Func>();
-			var storeFunctions = new Dictionary<int, Model.Func>();
-			arrayNum = 0;
-
-			for (; ; )
-			{
-				var line = ReadLine();
-				if (line == null) break; // end of model, everything fine
-				if (line == "Counterexample:" || line == "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;
+			int splits = 1;
+			foreach (string tok in expr)
+				if (tok.Equals ("@SPLIT"))
+					splits++;
 
-				var words = GetParsedTokens(line);
-				/*
-				Console.WriteLine("");
-				for (int i = 0; i < words.Count; i++)
-				{
-					Console.Write(words[i] + " ");
-				}
-*/
-				if (words.Count == 0) continue;
-				var lastToken = words[words.Count - 1];
-				if (currModel == null)
-					BadModel("model begin marker not found");
+			List<string>[] newExpr = new List<string>[splits];
 
-				if (words.Count > 3 && words[1] == "->")
-				{
-					var funName = (string) words[0];
-					Model.Func fn = null;
-					int i = 4;
+			for (int s = 0; s < splits; s++)
+				newExpr [s] = new List<string> ();
 
-					if (words.Contains("@SPLIT"))
-					{
-						arrayNum++;
+			int i = 0;
+			foreach (string tok in expr) {
+				if (tok.Equals ("@SPLIT")) {
+					i++;
+					continue;
+				}
 
-						fn = currModel.MkFunc(funName, 0);
-						fn.SetConstant(GetElt(words[2]));
+				newExpr [i].Add (tok);
+			}
 
-						i = 8;
+			return newExpr;
+		}
 
-						funName = (string) words[4];
-						fn = null;
-					}
+		internal override void Run ()
+		{
+			var selectFunctions = new Dictionary<int, Model.Func> ();
+			var storeFunctions = new Dictionary<int, Model.Func> ();
+			arrayNum = 0;
 
-					if (words[2] != "{" && words[6] != "{")
-						BadModel("unidentified function definition 5");
+			for (; ;) {
+				var line = ReadLine ();
+				if (line == null)
+					break; // end of model, everything fine
+				if (line == "Counterexample:" || line == "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;
 
-					fn = currModel.TryGetFunc(funName);
+				var words = GetParsedTokens (line);
+				if (words.Count == 0)
+					continue;
+				var exprs = TrySplitExpr (words);
 
-					for (; ; )
-					{
-						if (words[i] == "}")
-						{
-							if (i == words.Count - 1)
-							{
-								if (fn == null)
-									fn = currModel.MkFunc(funName, 1);
-								break;
-							}
-							else
-							{
-								i++;
-								continue;
-							}
-						}
+				foreach (List<string> expr in exprs) {
+					/*Console.WriteLine ("");
+					for (int i = 0; i < expr.Count; i++) {
+						Console.Write (expr [i] + " ");
+					}*/
 
-						for (; ; )
-						{
-							if (words[i] == " ")
-							{
-								i++;
-								break;
-							}
+					var lastToken = expr [expr.Count - 1];
+					if (currModel == null)
+						BadModel ("model begin marker not found");
 
-							if ((i == 4 || i == 8)  && words[i - 1] == " " && words[i + 1] == " ") {
-								if (fn.Else == null)
-									fn.Else = GetElt(words[i]);
-								i++;
-								continue;
-							}
+					if (expr.Count > 3 && expr [1] == "->") {
+						var funName = (string)expr [0];
+						Model.Func fn = null;
+						int i = 4;
 
-							if (words[i] == "else")
-							{
-								if (words[i + 1] == "->")
-								{
-									i += 2;
+						if (expr [2] != "{" && expr [6] != "{")
+							BadModel ("unidentified function definition 5");
 
-									if (words[i] == "}")
-										BadModel("unidentified function definition 1");
+						fn = currModel.TryGetFunc (funName);
 
-									if (words[i] == "{")
-									{
-										i++;
-										continue;
-									}
-									else
-									{
-										if (fn != null && !(words[i] == "#unspecified") && fn.Else == null)
-											fn.Else = GetElt(words[i]);
-										i++;
-										continue;
-									}
+						for (; ;) {
+							if (expr [i] == "}") {
+								if (i == expr.Count - 1) {
+									if (fn == null)
+										fn = currModel.MkFunc (funName, 1);
+									break;
+								} else {
+									i++;
+									continue;
 								}
-								else
-									BadModel("unidentified function definition 2");
 							}
 
-							int arity = 0;
-							for (; ; )
-							{
-								arity++;
-								if (words[arity + i] == " ")
-								{
-									arity -= 2;
+							for (; ;) {
+								if (expr [i] == " ") {
+									i++;
 									break;
 								}
-							}
 
-							if (words[i + arity] == "->")
-							{
-								i += arity + 1;
+								if ((i == 4 || i == 8) && expr [i - 1] == " " && expr [i + 1] == " ") {
+									if (fn.Else == null)
+										fn.Else = GetElt (expr [i]);
+									i++;
+									continue;
+								}
 
-								if (words[i] == "}")
-									BadModel("unidentified function definition 3");
-							}
-							else
-								BadModel("unidentified function definition 4");
-
-							if (fn == null)
-							{
-								if (Regex.IsMatch(funName, "^MapType[0-9]*Select$"))
-								{
-									funName = string.Format("[{0}]", arity);
-
-									if (!selectFunctions.TryGetValue(arity, out fn))
-									{
-										fn = currModel.MkFunc(funName, arity);
-										selectFunctions.Add(arity, fn);
-									}
+								if (expr [i] == "else") {
+									if (expr [i + 1] == "->") {
+										i += 2;
+
+										if (expr [i] == "}")
+											BadModel ("unidentified function definition 1");
+
+										if (expr [i] == "{") {
+											i++;
+											continue;
+										} else {
+											if (fn != null && !(expr [i] == "#unspecified") && fn.Else == null)
+												fn.Else = GetElt (expr [i]);
+											i++;
+											continue;
+										}
+									} else
+										BadModel ("unidentified function definition 2");
 								}
-								else if (Regex.IsMatch(funName, "^MapType[0-9]*Store$"))
-								{
-									funName = string.Format("[{0}:=]", arity);
 
-									if (!storeFunctions.TryGetValue(arity, out fn)) {
-										fn = currModel.MkFunc(funName, arity);
-										storeFunctions.Add(arity, fn);
+								int arity = 0;
+								for (; ;) {
+									arity++;
+									if (expr [arity + i] == " ") {
+										arity -= 2;
+										break;
 									}
 								}
-								else
-								{
-									fn = currModel.MkFunc(funName, arity);
+
+								if (expr [i + arity] == "->") {
+									i += arity + 1;
+
+									if (expr [i] == "}")
+										BadModel ("unidentified function definition 3");
+								} else
+									BadModel ("unidentified function definition 4");
+
+								if (fn == null) {
+									if (Regex.IsMatch (funName, "^MapType[0-9]*Select$")) {
+										funName = string.Format ("[{0}]", arity);
+
+										if (!selectFunctions.TryGetValue (arity, out fn)) {
+											fn = currModel.MkFunc (funName, arity);
+											selectFunctions.Add (arity, fn);
+										}
+									} else if (Regex.IsMatch (funName, "^MapType[0-9]*Store$")) {
+										funName = string.Format ("[{0}:=]", arity);
+
+										if (!storeFunctions.TryGetValue (arity, out fn)) {
+											fn = currModel.MkFunc (funName, arity);
+											storeFunctions.Add (arity, fn);
+										}
+									} else {
+										fn = currModel.MkFunc (funName, arity);
+									}
 								}
-							}
 
-							var args = new Model.Element[fn.Arity];
+								var args = new Model.Element[fn.Arity];
 
-							for (var idx = 0; idx < fn.Arity; ++idx)
-								args[idx] = GetElt(words[idx + i - arity - 1]);
+								for (var idx = 0; idx < fn.Arity; ++idx)
+									args [idx] = GetElt (expr [idx + i - arity - 1]);
 
-							fn.AddApp(GetElt(words[i]), args);
+								fn.AddApp (GetElt (expr [i]), args);
 
-							i++;
-							break;
+								i++;
+								break;
+							}
 						}
-					}
+					} else if (expr.Count == 3 && expr [1] == "->") {
+						var funName = (string)expr [0];
+						Model.Func fn = null;
+
+						fn = currModel.MkFunc (funName, 0);
+						fn.SetConstant (GetElt (lastToken));
+					} else
+						BadModel ("unidentified line");
 				}
-				else if (words.Count == 3 && words[1] == "->")
-				{
-					var funName = (string) words[0];
-					Model.Func fn = null;
-
-					fn = currModel.MkFunc(funName, 0);
-					fn.SetConstant(GetElt(lastToken));
-				}
-				else
-					BadModel("unidentified line");
 			}
 		}
 	}
 
 	internal class ParserZ3_SMTLIB2 : ParserSMT
 	{
-		protected override void ParseArray(ref int i)
+		protected override void ParseArray (ref int i)
 		{
 			while (tokens[i] != "as-array")
 				i++;
 
-			output.Add("as-array[" + tokens[i + 1] + "]");
+			output.Add ("as-array[" + tokens [i + 1] + "]");
 		}
 
-		protected override void ParseITE(ref int i)
+		protected override void ParseITE (ref int i)
 		{
-			List<string> args = new List<string>();
-			List<string> results = new List<string>();
+			List<string> args = new List<string> ();
+			List<string> results = new List<string> ();
 
-			FindArity();
+			FindArity ();
 
-			for (; ; )
-			{
+			for (; ;) {
 				i++;
 
-				if (tokens[i] == "=")
-				{
-					if (tokens[i + 2] == "(" && tokens[i + 3] == "_")
-					{
-						args.Add(GetValue(i + 5));
+				if (tokens [i] == "=") {
+					if (tokens [i + 2] == "(" && tokens [i + 3] == "_") {
+						args.Add (GetValue (i + 5));
 						i += 6;
-					}
-					else if (tokens[i + 2] == "(" && tokens[i + 3] == "-")
-					{
-						args.Add(GetValue(i + 4));
+					} else if (tokens [i + 2] == "(" && tokens [i + 3] == "-") {
+						args.Add (GetValue (i + 4));
 						i += 5;
-					}
-					else
-					{
-						args.Add(GetValue(i + 2));
+					} else {
+						args.Add (GetValue (i + 2));
 						i += 3;
 					}
 				}
 
-				if (args.Count > 0 && args.Count % arity == 0)
-				{
-					if (tokens[i + 2] == "(" && tokens[i + 3] == "_")
-					{
-						results.Add(GetValue(i + 5));
+				if (args.Count > 0 && args.Count % arity == 0) {
+					if (tokens [i + 2] == "(" && tokens [i + 3] == "_") {
+						results.Add (GetValue (i + 5));
 						i += 6;
-					}
-					else if (tokens[i + 2] == "(" && tokens[i + 3] == "-")
-					{
-						results.Add(GetValue(i + 4));
+					} else if (tokens [i + 2] == "(" && tokens [i + 3] == "-") {
+						results.Add (GetValue (i + 4));
 						i += 5;
-					}
-					else
-					{
-						results.Add(GetValue(i + 2));
+					} else {
+						results.Add (GetValue (i + 2));
 						i += 3;
 					}
 
-					while (i < tokens.Length - 1 && tokens[i + 1] != "=")
-					{
+					while (i < tokens.Length - 1 && tokens[i + 1] != "=") {
 						i++;
 					}
 
-					if (i == tokens.Length - 1)
-					{
+					if (i == tokens.Length - 1) {
 						while (tokens[i] == ")")
 							i += -1;
-						results.Add(GetValue(i));
+						results.Add (GetValue (i));
 						break;
 					}
 				}
 			}
 
 			int idx = 0;
-			for (int j = 0; j < results.Count - 1; j++)
-			{
-				for (int r = 0; r < arity; r++)
-				{
-					output.Add(args[idx]);
+			for (int j = 0; j < results.Count - 1; j++) {
+				for (int r = 0; r < arity; r++) {
+					output.Add (args [idx]);
 					idx++;
 				}
 
-				output.Add("->");
-				output.Add(results[j]);
-				output.Add(" ");
+				output.Add ("->");
+				output.Add (results [j]);
+				output.Add (" ");
 			}
 
-			output.Add("else");
-			output.Add("->");
-			output.Add(results[results.Count - 1]);
+			output.Add ("else");
+			output.Add ("->");
+			output.Add (results [results.Count - 1]);
 		}
 	}
 
 	internal class ParserCVC4 : ParserSMT
 	{
+		void SplitArrayExpression ()
+		{
+			if (output.Contains ("@SPLIT")) {
+				output.Add (" ");
+				output.Add ("}");
+			}
+
+			output.Add ("@SPLIT");
+			output.Add ("k!" + arrayNum);
+			output.Add ("->");
+			output.Add ("{");
+			output.Add (" ");
+
+			arrayNum++;
+		}
+
+		protected override void ParseArray (ref int i)
+		{
+			output.Add ("as-array[k!" + arrayNum + "]");
+			SplitArrayExpression ();
+
+			while (tokens[i] != "store" && tokens[i] != "__array_store_all__")
+				i++;
+
+			if (tokens [i] == "store") {
+				List<string> args = new List<string> ();
+				int p_count = 1;
+				i += 4;
+
+				while (p_count > 0) {
+					if (tokens [i] == ")")
+						p_count--;
+					else if (tokens [i] == "(")
+						p_count++;
+					i++;
+				}
+
+				if (tokens [i] == "(" && tokens [i + 1] == "__array_store_all__") {
+					output.Add ("as-array[k!" + arrayNum + "]");
+					SplitArrayExpression ();
+				} else {
+					while (args.Count < 3) {
+						if (tokens [i] == ")")
+							i++;
+						else if (tokens [i] == "(" && tokens [i + 1] == "_") {
+							args.Add (GetValue (i + 3));
+							i += 5;
+						} else if (tokens [i + 1] == "(" && tokens [i + 1] == "-") {
+							args.Add (GetValue (i + 2));
+							i += 4;
+						} else {
+							args.Add (GetValue (i));
+							i++;
+						}
+					}
+
+					output.Add (args [1]);
+					output.Add ("->");
+					output.Add (args [2]);
+					output.Add (" ");
+					output.Add ("else");
+					output.Add ("->");
+					output.Add (args [0]);
+				}
+			} else if (tokens [i] == "__array_store_all__") {
+				int p_count = 1;
+				i += 2;
+
+				while (p_count > 0) {
+					if (tokens [i] == ")")
+						p_count--;
+					else if (tokens [i] == "(")
+						p_count++;
+					i++;
+				}
+
+				if (tokens [i] == "(" && tokens [i + 1] == "_") {
+					output.Add (GetValue (i + 3));
+					i += 5;
+				} else if (tokens [i] == "(" && tokens [i + 1] == "-") {
+					output.Add (GetValue (i + 2));
+					i += 4;
+				} else {
+					output.Add (GetValue (i));
+					i++;
+				}
+			}
+		}
+		/*
 		protected override void ParseArray(ref int i)
 		{
 			output.Add("as-array[k!" + arrayNum + "]");
@@ -779,73 +817,58 @@ namespace Microsoft.Boogie
 				}
 			}
 		}
-
-		protected override void ParseITE(ref int i)
+		*/
+		protected override void ParseITE (ref int i)
 		{
-			List<string> args = new List<string>();
-			List<string> results = new List<string>();
+			List<string> args = new List<string> ();
+			List<string> results = new List<string> ();
 
-			FindArity();
+			FindArity ();
 
 			int occurrences = 0;
 
-			foreach (string tok in tokens)
-			{
-				if (tok == "_ufmt_1") occurrences++;
+			foreach (string tok in tokens) {
+				if (tok == "_ufmt_1")
+					occurrences++;
 			}
 
-			for (; ; )
-			{
+			for (; ;) {
 				i++;
 
-				if (tokens[i] == "=")
-				{
-					if (tokens[i + 2] == "(" && tokens[i + 3] == "_")
-					{
-						args.Add(GetValue(i + 5));
+				if (tokens [i] == "=") {
+					if (tokens [i + 2] == "(" && tokens [i + 3] == "_") {
+						args.Add (GetValue (i + 5));
 						i += 6;
-					}
-					else if (tokens[i + 2] == "(" && tokens[i + 3] == "-")
-					{
-						args.Add(GetValue(i + 4));
+					} else if (tokens [i + 2] == "(" && tokens [i + 3] == "-") {
+						args.Add (GetValue (i + 4));
 						i += 5;
-					}
-					else
-					{
-						args.Add(GetValue(i + 2));
+					} else {
+						args.Add (GetValue (i + 2));
 						i += 2;
 					}
 				}
 
 				if ((args.Count > 0 && args.Count % arity == 0) ||
-				    (results.Count > 0 && occurrences <= 2))
-				{
-					if (tokens[i + 2] == "(" && tokens[i + 3] == "_")
-					{
-						results.Add(GetValue(i + 5));
+					(results.Count > 0 && occurrences <= 2)) {
+					if (tokens [i + 2] == "(" && tokens [i + 3] == "_") {
+						results.Add (GetValue (i + 5));
 						i += 6;
-					}
-					else if (tokens[i + 2] == "(" && tokens[i + 3] == "-")
-					{
-						results.Add(GetValue(i + 4));
+					} else if (tokens [i + 2] == "(" && tokens [i + 3] == "-") {
+						results.Add (GetValue (i + 4));
 						i += 5;
-					}
-					else
-					{
-						results.Add(GetValue(i + 2));
+					} else {
+						results.Add (GetValue (i + 2));
 						i += 2;
 					}
 
-					while (i < tokens.Length - 1 && tokens[i + 1] != "=")
-					{
+					while (i < tokens.Length - 1 && tokens[i + 1] != "=") {
 						i++;
 					}
 
-					if (i == tokens.Length - 1)
-					{
+					if (i == tokens.Length - 1) {
 						while (tokens[i] == ")")
 							i += -1;
-						results.Add(GetValue(i));
+						results.Add (GetValue (i));
 						break;
 					}
 				}
@@ -853,43 +876,34 @@ namespace Microsoft.Boogie
 
 			int idx = 0;
 
-			for (int j = 0; j < results.Count - 1; j++)
-			{
-				if (occurrences > 2)
-				{
-					for (int r = 0; r < arity; r++)
-					{
-						output.Add(args[idx]);
+			for (int j = 0; j < results.Count - 1; j++) {
+				if (occurrences > 2) {
+					for (int r = 0; r < arity; r++) {
+						output.Add (args [idx]);
 						idx++;
 					}
-				}
-				else
-				{
-					if (arity == 1)
-					{
-						output.Add(args[idx]);
+				} else {
+					if (arity == 1) {
+						output.Add (args [idx]);
 						idx++;
-					}
-					else
-					{
-						output.Add(args[0]);
+					} else {
+						output.Add (args [0]);
 
-						for (int r = 1; r < arity; r++)
-						{
+						for (int r = 1; r < arity; r++) {
 							idx++;
-							output.Add(args[idx]);
+							output.Add (args [idx]);
 						}
 					}
 				}
 
-				output.Add("->");
-				output.Add(results[j]);
-				output.Add(" ");
+				output.Add ("->");
+				output.Add (results [j]);
+				output.Add (" ");
 			}
 
-			output.Add("else");
-			output.Add("->");
-			output.Add(results[results.Count - 1]);
+			output.Add ("else");
+			output.Add ("->");
+			output.Add (results [results.Count - 1]);
 		}
 	}
 }