From e2a0f4614b14ca10d6813ed6ce3d84c077872770 Mon Sep 17 00:00:00 2001 From: pantazis Date: Thu, 13 Jun 2013 04:35:43 +0100 Subject: merged more CVC4 and Z3 SMTLIB2 parsing methods ... results into a more compact parser --- Source/Model/ModelParser.cs | 570 +++++++++++++++++++++----------------------- 1 file changed, 267 insertions(+), 303 deletions(-) (limited to 'Source/Model') diff --git a/Source/Model/ModelParser.cs b/Source/Model/ModelParser.cs index 49e403ff..617517ac 100644 --- a/Source/Model/ModelParser.cs +++ b/Source/Model/ModelParser.cs @@ -281,8 +281,34 @@ namespace Microsoft.Boogie { protected string[] tokens; protected List output; + protected int arity; protected int arrayNum; + abstract protected void ParseArray(ref int i); + abstract protected void ParseITE(ref int i); + + protected void FindArity() + { + arity = 0; + int p_count = 1; + int i = 4; + + while (p_count > 0) + { + if (i == tokens.Length - 1) + break; + else if (tokens[i] == ")") + p_count--; + else if (tokens[i] == "(" && tokens[i + 1] != "ite") + { + p_count++; + arity++; + } + + i++; + } + } + protected string GetValue(int idx) { string value = tokens[idx]; @@ -299,21 +325,7 @@ namespace Microsoft.Boogie return value; } - abstract protected void ParseITE(ref int i); - abstract protected void ParseArray(ref int i); - abstract protected void ParseTokens(); - - protected void ParseDefineFun(ref int i) - { - i++; - - output.Add(GetValue(i)); - output.Add("->"); - - i++; - } - - protected void ParseRightParenthesis(ref int i) + void ParseEndOfExpression(ref int i) { i++; @@ -365,7 +377,47 @@ namespace Microsoft.Boogie tokens = line.Split(seps, StringSplitOptions.RemoveEmptyEntries); output = new List(); - ParseTokens(); + + var i = 0; + bool doneParsing = false; + + while(!doneParsing) + { + switch (tokens[i]) + { + case ")": + ParseEndOfExpression(ref i); + break; + + case "define-fun": + output.Add(GetValue(i+1)); + output.Add("->"); + i += 2; + break; + + case "Array": + ParseArray(ref i); + break; + + case "ite": + ParseITE(ref i); + break; + + case "_ufmt_1": + case "x!1": + output.Add("{"); + output.Add(" "); + i++; + break; + + default: + i++; + break; + } + + if (i == tokens.Length) + doneParsing = true; + } return output; } @@ -391,13 +443,13 @@ namespace Microsoft.Boogie continue; 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) @@ -561,111 +613,6 @@ namespace Microsoft.Boogie internal class ParserZ3 : ParserSMT { - protected override void ParseITE(ref int i) - { - for (; ; ) - { - if (tokens[i] == "ite") - { - i++; - - for (; ; ) - { - if (tokens[i] == "(" && tokens[i + 1] == "and") - i += 2; - - if (tokens[i] == "(" && tokens[i + 1] == "=") - { - if (tokens[i + 3] == "(" && tokens[i + 4] == "-") - { - i += 7; - output.Add(GetValue(i - 2)); - } - else if (tokens[i + 3] == "(" && tokens[i + 4] == "_") - { - i += 8; - output.Add(GetValue(i - 2)); - } - else - { - i += 4; - output.Add(GetValue(i - 1)); - } - - i++; - continue; - } - - output.Add("->"); - - if (tokens[i] == ")") i++; - - if (tokens[i] == "(" && tokens[i + 1] == "-") - { - i += 3; - output.Add(GetValue(i - 1)); - } - else if (tokens[i] == "(" && tokens[i + 1] == "_") - { - i += 4; - output.Add(GetValue(i - 1)); - } - else - { - i++; - output.Add(GetValue(i - 1)); - } - - output.Add(" "); - break; - } - } - - if (tokens[i] == "(" && tokens[i + 1] == "-") - { - i += 2; - output.Add("else"); - output.Add("->"); - output.Add(GetValue(i)); - break; - } - else if (tokens[i] == "(" && tokens[i + 1] == "_") - { - i += 3; - output.Add("else"); - output.Add("->"); - output.Add(GetValue(i)); - break; - } - else if (tokens[i] == ")" && tokens[i - 2] == "-") - { - i++; - continue; - } - else if (tokens[i] == ")" && tokens[i - 3] == "_") - { - i++; - continue; - } - else if (tokens[i] != "(") - { - output.Add("else"); - output.Add("->"); - output.Add(GetValue(i)); - break; - } - else i++; - } - } - - void ParseArgument(ref int i) - { - output.Add("{"); - output.Add(" "); - - i++; - } - protected override void ParseArray(ref int i) { while (tokens[i] != "as-array") @@ -674,72 +621,6 @@ namespace Microsoft.Boogie output.Add("as-array[" + tokens[i + 1] + "]"); } - protected override void ParseTokens() - { - var i = 0; - bool doneParsing = false; - - while(!doneParsing) - { - switch (tokens[i]) - { - case ")": - ParseRightParenthesis(ref i); - break; - - case "define-fun": - ParseDefineFun(ref i); - break; - - case "Array": - ParseArray(ref i); - break; - - case "ite": - ParseITE(ref i); - break; - - case "x!1": - ParseArgument(ref i); - break; - - default: - i++; - break; - } - - if (i == tokens.Length) - doneParsing = true; - } - } - } - - internal class ParserCVC4 : ParserSMT - { - int arity; - - void FindArity() - { - arity = 0; - int p_count = 1; - int i = 4; - - while (p_count > 0) - { - if (i == tokens.Length - 1) - break; - else if (tokens[i] == ")") - p_count--; - else if (tokens[i] == "(" && tokens[i + 1] != "ite") - { - p_count++; - arity++; - } - - i++; - } - } - /* protected override void ParseITE(ref int i) { List args = new List(); @@ -747,120 +628,58 @@ namespace Microsoft.Boogie FindArity(); - output.Add("{"); - output.Add(" "); - for (; ; ) { - if (tokens[i] == ")") + i++; + + if (tokens[i] == "=") { - if ((tokens[i + 1] == ")" || tokens[i + 2] == ")") && - (tokens[i + 2] != "ite" || tokens[i + 3] != "ite") && - (tokens[i - 3] == "_" || tokens[i - 2] == "-")) + if (tokens[i + 2] == "(" && tokens[i + 3] == "_") { - results.Add(GetValue(i - 1)); - break; + args.Add(GetValue(i + 5)); + i += 6; } - else + else if (tokens[i + 2] == "(" && tokens[i + 3] == "-") { - args.Add(GetValue(i - 1)); - - if (tokens[i + 1] == "(" && tokens[i + 2] == "-") - { - results.Add(GetValue(i + 3)); - i += 5; - } - else if (tokens[i + 2] != "ite") - { - results.Add(GetValue(i + 1)); - i += 2; - } - else i++; + args.Add(GetValue(i + 4)); + i += 5; } - } - else i++; - } - - int idx = 0; - for (int j = 0; j < results.Count - 1; j++) - { - if (arity == 1) - { - output.Add(args[idx]); - idx++; - } - else - { - output.Add(args[0]); - - for (int r = 1; r < arity; r++) + else { - idx++; - output.Add(args[idx]); + args.Add(GetValue(i + 2)); + i += 3; } } - output.Add("->"); - output.Add(results[j]); - output.Add(" "); - } - - output.Add("else"); - output.Add("->"); - output.Add(results[results.Count - 1]); - } - */ - protected override void ParseITE(ref int i) - { - List args = new List(); - List results = new List(); - - FindArity(); - - output.Add("{"); - output.Add(" "); - - for (; ; ) - { - i++; - - if (tokens[i] == ")") + if (args.Count > 0 && args.Count % arity == 0) { - if (((tokens[i + 1] == ")" && tokens[i + 3] != "ite") || - (tokens[i + 2] == ")" && tokens[i + 4] != "ite")) && - args.Count % arity == 0) + if (tokens[i + 2] == "(" && tokens[i + 3] == "_") { - Console.WriteLine("Res(*): " + GetValue(i - 1)); - results.Add(GetValue(i - 1)); - break; + results.Add(GetValue(i + 5)); + i += 6; } - - if (tokens[i - 3] == "=" || tokens[i - 5] == "=" || tokens[i - 6] == "=") + else if (tokens[i + 2] == "(" && tokens[i + 3] == "-") { - Console.WriteLine("Arg: " + GetValue(i - 1)); - args.Add(GetValue(i - 1)); + results.Add(GetValue(i + 4)); + i += 5; } - - if (tokens [i + 1] == ")") i += 2; - else i++; - - if (tokens[i] == "(" && tokens[i + 1] == "-") + else { - Console.WriteLine("Res: " + GetValue(i + 2)); results.Add(GetValue(i + 2)); - i += 4; + i += 3; } - else if (tokens[i] == "(" && tokens[i + 1] == "_") + + while (i < tokens.Length - 1 && tokens[i + 1] != "=") { - Console.WriteLine("Res: " + GetValue(i + 3)); - results.Add(GetValue(i + 3)); - i += 5; + i++; } - else if (tokens[i] != "(") + + if (i == tokens.Length - 1) { - Console.WriteLine("Res: " + GetValue(i)); + while (tokens[i] == ")") + i += -1; results.Add(GetValue(i)); - i++; + break; } } } @@ -881,8 +700,12 @@ namespace Microsoft.Boogie output.Add("else"); output.Add("->"); + output.Add(results[results.Count - 1]); } + } + internal class ParserCVC4 : ParserSMT + { protected override void ParseArray(ref int i) { output.Add("as-array[k!" + arrayNum + "]"); @@ -915,8 +738,6 @@ namespace Microsoft.Boogie } else if (tokens[i] == ",") { - //i += 2; - //ParseBitVector(ref i); output.Add(GetValue(i + 4)); i += 5; break; @@ -924,38 +745,181 @@ namespace Microsoft.Boogie } } - protected override void ParseTokens() + protected override void ParseITE(ref int i) { - var i = 0; - bool doneParsing = false; + List args = new List(); + List results = new List(); - while(!doneParsing) + FindArity(); + + int occurrences = 0; + + foreach (string tok in tokens) { - switch (tokens[i]) + if (tok == "_ufmt_1") occurrences++; + } + + if (occurrences > 2) + { + for (; ; ) { - case ")": - ParseRightParenthesis(ref i); - break; + i++; - case "define-fun": - ParseDefineFun(ref i); - break; + 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)); + i += 5; + } + else + { + args.Add(GetValue(i + 2)); + i += 3; + } + } - case "Array": - ParseArray(ref i); - break; + 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)); + i += 5; + } + else + { + results.Add(GetValue(i + 2)); + i += 3; + } - case "ite": - ParseITE(ref i); - break; + while (i < tokens.Length - 1 && tokens[i + 1] != "=") + { + i++; + } - default: + if (i == tokens.Length - 1) + { + while (tokens[i] == ")") + i += -1; + 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]); + idx++; + } + + output.Add("->"); + output.Add(results[j]); + output.Add(" "); + } + + output.Add("else"); + output.Add("->"); + output.Add(results[results.Count - 1]); + } + else + { + for (; ; ) + { i++; - break; + + 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)); + i += 5; + } + else + { + args.Add(GetValue(i + 2)); + i += 2; + } + } + + if ((args.Count > 0 && args.Count % arity == 0) || results.Count > 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)); + i += 5; + } + else + { + results.Add(GetValue(i + 2)); + i += 2; + } + + while (i < tokens.Length - 1 && tokens[i + 1] != "=") + { + i++; + } + + if (i == tokens.Length - 1) + { + while (tokens[i] == ")") + i += -1; + results.Add(GetValue(i)); + break; + } + } } - if (i == tokens.Length) - doneParsing = true; + int idx = 0; + for (int j = 0; j < results.Count - 1; j++) + { + if (arity == 1) + { + output.Add(args[idx]); + idx++; + } + else + { + output.Add(args[0]); + + for (int r = 1; r < arity; r++) + { + idx++; + output.Add(args[idx]); + } + } + + output.Add("->"); + output.Add(results[j]); + output.Add(" "); + } + + output.Add("else"); + output.Add("->"); + output.Add(results[results.Count - 1]); } } } -- cgit v1.2.3