From 0c04738d73d4253135cc248a02dd7ac3d2d97d5a Mon Sep 17 00:00:00 2001 From: Pantazis Deligiannis Date: Thu, 11 Jul 2013 13:51:55 +0100 Subject: code cleanup and refactoring --- Source/Model/Model.cs | 9 +- Source/Model/ModelParser.cs | 301 ++++++++++++------------------- Source/Provers/SMTLib/ProverInterface.cs | 11 +- 3 files changed, 123 insertions(+), 198 deletions(-) (limited to 'Source') 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 output; - protected int arity; - protected int arrayNum; - protected int index; + string[] tokens; + List 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 args = new List (); @@ -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 args = new List (); + List results = new List (); + + 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 args = new List (); - List results = new List (); - - 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 args = new List (); - List results = new List (); - - 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); -- cgit v1.2.3