code cleanup and refactoring

3 files changed, 123 insertions, 198 deletions

diff --git a/Source/Model/Model.cs b/Source/Model/Model.cs
index 7668b370..b9a2dfcf 100644
--- a/Source/Model/Model.cs
+++ b/Source/Model/Model.cs
@@ -701,14 +701,11 @@ namespace Microsoft.Boogie
 		

 		switch (prover)

 		{

-			case "Z3_SMTLIB2":

-			p = new ParserZ3_SMTLIB2();

-			break;

-			case "CVC4":

-			p = new ParserCVC4();

+			case "SMTLIB2":

+				p = new ParserSMT();

 			break;

 			default:

-			p = new ParserZ3();

+				p = new ParserZ3();

 			break;

 		}

 

diff --git a/Source/Model/ModelParser.cs b/Source/Model/ModelParser.cs
index 0954a575..40fd3c9a 100644
--- a/Source/Model/ModelParser.cs
+++ b/Source/Model/ModelParser.cs
@@ -256,17 +256,15 @@ namespace Microsoft.Boogie
 		}
 	}
 
-	abstract class ParserSMT : ModelParser
+	class ParserSMT : ModelParser
 	{
-		protected string[] tokens;
-		protected List<string> output;
-		protected int arity;
-		protected int arrayNum;
-		protected int index;
+		string[] tokens;
+		List<string> output;
+		int arity;
+		int arrayNum;
+		int index;
 
-		abstract protected void ParseIteExpr ();
-
-		protected void FindArity ()
+		void FindArity ()
 		{
 			arity = 0;
 			int p_count = 1;
@@ -286,7 +284,7 @@ namespace Microsoft.Boogie
 			}
 		}
 
-		protected string GetValue (int idx)
+		string GetValue (int idx)
 		{
 			string value = tokens [idx];
 
@@ -301,6 +299,8 @@ namespace Microsoft.Boogie
 
 		void SplitArrayExpression ()
 		{
+			output.Add ("as-array[k!" + arrayNum + "]");
+
 			if (output.Contains ("@SPLIT")) {
 				output.Add (" ");
 				output.Add ("}");
@@ -321,7 +321,6 @@ namespace Microsoft.Boogie
 				index++;
 
 			if (tokens [index] == "store") {
-				output.Add ("as-array[k!" + arrayNum + "]");
 				SplitArrayExpression ();
 
 				List<string> args = new List<string> ();
@@ -336,26 +335,22 @@ namespace Microsoft.Boogie
 					index++;
 				}
 
-				if (tokens [index] == "(" && tokens [index + 1] == "__array_store_all__") {
-					output.Add ("as-array[k!" + arrayNum + "]");
-					SplitArrayExpression ();
-				} else if (tokens [index] == "(" && tokens [index + 1] == "store") {
-					output.Add ("as-array[k!" + arrayNum + "]");
+				if ((tokens [index] == "(" && tokens [index + 1] == "__array_store_all__") ||
+				    (tokens [index] == "(" && tokens [index + 1] == "store")) {
 					SplitArrayExpression ();
 				} else {
 					while (args.Count < 3) {
 						if (tokens [index] == ")")
 							index++;
-						else if (tokens [index] == "(" && tokens [index + 1] == "_") {
-							args.Add (GetValue (index + 3));
-							index += 5;
-						} else if (tokens [index + 1] == "(" && tokens [index + 1] == "-") {
-							args.Add (GetValue (index + 2));
-							index += 4;
+						else if (tokens [index] == "(") {
+							while (tokens [index] != ")")
+								index++;
+							args.Add (GetValue (index - 1));
 						} else {
 							args.Add (GetValue (index));
-							index++;
 						}
+
+						index++;
 					}
 
 					output.Add (args [1]);
@@ -367,7 +362,6 @@ namespace Microsoft.Boogie
 					output.Add (args [0]);
 				}
 			} else if (tokens [index] == "__array_store_all__") {
-				output.Add ("as-array[k!" + arrayNum + "]");
 				SplitArrayExpression ();
 
 				while (tokens[index] == "__array_store_all__") {
@@ -383,20 +377,20 @@ namespace Microsoft.Boogie
 					}
 
 					if (tokens [index] == "(" && tokens [index + 1] == "__array_store_all__") {
-						output.Add ("as-array[k!" + arrayNum + "]");
 						SplitArrayExpression ();
 						index++;
 					} else {
-						if (tokens [index] == "(" && tokens [index + 1] == "_") {
-							output.Add (GetValue (index + 3));
-							index += 5;
-						} else if (tokens [index] == "(" && tokens [index + 1] == "-") {
-							output.Add (GetValue (index + 2));
-							index += 4;
+						if (tokens [index] == ")")
+							index++;
+						else if (tokens [index] == "(") {
+							while (tokens [index] != ")")
+								index++;
+							output.Add (GetValue (index - 1));
 						} else {
 							output.Add (GetValue (index));
-							index++;
 						}
+
+						index++;
 					}
 				}
 			} else if (tokens [index] == "as-array") {
@@ -404,6 +398,96 @@ namespace Microsoft.Boogie
 			}
 		}
 
+		void ParseIteExpr ()
+		{
+			List<string> args = new List<string> ();
+			List<string> results = new List<string> ();
+
+			FindArity ();
+
+			int occurrences = 0;
+
+			foreach (string tok in tokens) {
+				if (tok == "_ufmt_1")
+					occurrences++;
+			}
+
+			for (; ;) {
+				index++;
+
+				if (tokens [index] == "=") {
+					index += 2;
+
+					if (tokens [index] == "(") {
+						while (tokens [index] != ")")
+							index++;
+						args.Add (GetValue (index - 1));
+					} else {
+						args.Add (GetValue (index));
+					}
+				}
+
+				if ((args.Count > 0 && args.Count % arity == 0) ||
+				    (results.Count > 0 && occurrences <= 2 && occurrences > 0)) {
+					index += 2;
+
+					if (tokens [index] == "(") {
+						while (tokens [index] != ")")
+							index++;
+						results.Add (GetValue (index - 1));
+					} else {
+						results.Add (GetValue (index));
+					}
+
+					while (index < tokens.Length - 1 && tokens[index + 1] != "=")
+						index++;
+
+					if (index == tokens.Length - 1) {
+						while (tokens[index] == ")")
+							index += -1;
+						results.Add (GetValue (index));
+						break;
+					}
+				}
+			}
+
+			int i = 0;
+
+			for (int j = 0; j < results.Count - 1; j++) {
+				if (occurrences > 2) {
+					for (int r = 0; r < arity; r++) {
+						output.Add (args [i]);
+						i++;
+					}
+				} else if (occurrences > 0) {
+					if (arity == 1) {
+						output.Add (args [i]);
+						i++;
+					} else {
+						output.Add (args [0]);
+
+						for (int r = 1; r < arity; r++) {
+							i++;
+							output.Add (args [i]);
+						}
+					}
+				} else {
+					for (int r = 0; r < arity; r++) {
+						output.Add (args [i]);
+						i++;
+					}
+				}
+
+				output.Add ("->");
+				output.Add (results [j]);
+				output.Add (" ");
+			}
+
+			output.Add ("else");
+			output.Add ("->");
+			output.Add (results [results.Count - 1]);
+		}
+
 		void ParseEndOfExpr ()
 		{
 			index++;
@@ -668,157 +752,4 @@ namespace Microsoft.Boogie
 			}
 		}
 	}
-
-	internal class ParserZ3_SMTLIB2 : ParserSMT
-	{
-		protected override void ParseIteExpr ()
-		{
-			List<string> args = new List<string> ();
-			List<string> results = new List<string> ();
-
-			FindArity ();
-
-			for (; ;) {
-				index++;
-
-				if (tokens [index] == "=") {
-					index += 2;
-
-					if (tokens [index] == "(") {
-						while (tokens [index] != ")")
-							index++;
-						args.Add (GetValue (index - 1));
-					} else {
-						args.Add (GetValue (index));
-					}
-				}
-
-				if (args.Count > 0 && args.Count % arity == 0) {
-					index += 2;
-
-					if (tokens [index] == "(") {
-						while (tokens [index] != ")")
-							index++;
-						results.Add (GetValue (index - 1));
-					} else {
-						results.Add (GetValue (index));
-					}
-
-					while (index < tokens.Length - 1 && tokens[index + 1] != "=")
-						index++;
-
-					if (index == tokens.Length - 1) {
-						while (tokens[index] == ")")
-							index += -1;
-						results.Add (GetValue (index));
-						break;
-					}
-				}
-			}
-
-			int idx = 0;
-			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 ("else");
-			output.Add ("->");
-			output.Add (results [results.Count - 1]);
-		}
-	}
-
-	internal class ParserCVC4 : ParserSMT
-	{
-		protected override void ParseIteExpr ()
-		{
-			List<string> args = new List<string> ();
-			List<string> results = new List<string> ();
-
-			FindArity ();
-
-			int occurrences = 0;
-
-			foreach (string tok in tokens) {
-				if (tok == "_ufmt_1")
-					occurrences++;
-			}
-
-			for (; ;) {
-				index++;
-
-				if (tokens [index] == "=") {
-					index += 2;
-
-					if (tokens [index] == "(") {
-						while (tokens [index] != ")")
-							index++;
-						args.Add (GetValue (index - 1));
-					} else {
-						args.Add (GetValue (index));
-					}
-				}
-
-				if ((args.Count > 0 && args.Count % arity == 0) ||
-				    (results.Count > 0 && occurrences <= 2)) {
-					index += 2;
-
-					if (tokens [index] == "(") {
-						while (tokens [index] != ")")
-							index++;
-						results.Add (GetValue (index - 1));
-					} else {
-						results.Add (GetValue (index));
-					}
-
-					while (index < tokens.Length - 1 && tokens[index + 1] != "=")
-						index++;
-
-					if (index == tokens.Length - 1) {
-						while (tokens[index] == ")")
-							index += -1;
-						results.Add (GetValue (index));
-						break;
-					}
-				}
-			}
-
-			int i = 0;
-
-			for (int j = 0; j < results.Count - 1; j++) {
-				if (occurrences > 2) {
-					for (int r = 0; r < arity; r++) {
-						output.Add (args [i]);
-						i++;
-					}
-				} else {
-					if (arity == 1) {
-						output.Add (args [i]);
-						i++;
-					} else {
-						output.Add (args [0]);
-
-						for (int r = 1; r < arity; r++) {
-							i++;
-							output.Add (args [i]);
-						}
-					}
-				}
-
-				output.Add ("->");
-				output.Add (results [j]);
-				output.Add (" ");
-			}
-
-			output.Add ("else");
-			output.Add ("->");
-			output.Add (results [results.Count - 1]);
-		}
-	}
 }
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 09696c40..7c42df01 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -929,17 +929,14 @@ namespace Microsoft.Boogie.SMTLib
 				try {

 					switch (options.Solver) {

 					case SolverKind.Z3:

-						if (options.SMTLib2Model)

-						{

-							models = Model.ParseModels(new StringReader("Error model: \n" + modelStr), "Z3_SMTLIB2");

-						}

-						else

-						{

+						if (options.SMTLib2Model) {

+							models = Model.ParseModels(new StringReader("Error model: \n" + modelStr), "SMTLIB2");

+						} else {

 							models = Model.ParseModels(new StringReader("Error model: \n" + modelStr), "");

 						}

 						break;

 					case SolverKind.CVC4:

-						models = Model.ParseModels(new StringReader("Error model: \n" + modelStr), "CVC4");

+						models = Model.ParseModels(new StringReader("Error model: \n" + modelStr), "SMTLIB2");

 						break;

 					default:

 						Debug.Assert(false);