From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:14:18 -0600 Subject: Merging complete. Everything looks good *crosses fingers* --- Source/Provers/SMTLib/SMTLibNamer.cs | 289 ++++++++++++++++++----------------- 1 file changed, 147 insertions(+), 142 deletions(-) (limited to 'Source/Provers/SMTLib/SMTLibNamer.cs') diff --git a/Source/Provers/SMTLib/SMTLibNamer.cs b/Source/Provers/SMTLib/SMTLibNamer.cs index 3ef2039b..f1179159 100644 --- a/Source/Provers/SMTLib/SMTLibNamer.cs +++ b/Source/Provers/SMTLib/SMTLibNamer.cs @@ -1,142 +1,147 @@ -using System; -using System.Collections.Generic; -using System.Linq; -using System.Text; -using Microsoft.Boogie.VCExprAST; - -namespace Microsoft.Boogie.SMTLib -{ - public class SMTLibNamer : UniqueNamer - { - // The following Boogie ID characters are not SMT ID characters: `'\# - const string idCharacters = "~!@$%^&*_-+=<>.?/"; - - - static string[] reservedSmtWordsList = - { // Basic symbols: - "", "!", "_", "as", "DECIMAL", "exists", "forall", "let", "NUMERAL", "par", "STRING", - // Commands: - "assert", "check-sat", "declare-sort", "declare-fun", "define-sort,", "define-fun", "exit", - "get-assertions", "get-assignment", "get-info", "get-option,", "get-proof", "get-unsat-core", - "get-value", "pop", "push", "set-logic", "set-info", "set-option", - // Core theory: - "and", "or", "not", "iff", "true", "false", "xor", "distinct", "ite", "=", "Bool", - "=>", // implies (sic!) - // Integers and reals - "Int", "Real", "*", "/", "-", "~", "+", "<", "<=", ">", ">=", "div", "mod", "rem", - "^", "sin", "cos", "tan", "asin", "acos", "atan", "sinh", "cosh", "tanh", "asinh", "acosh", "atanh", "pi", "euler", - "to_real", "to_int", "is_int", - // Bitvectors - "extract", "concat", - "bvnot", "bvneg", "bvand", "bvor", "bvadd", "bvmul", "bvudiv", "bvurem", "bvshl", "bvlshr", "bvult", - // arrays - "store", "select", "const", "default", "map", "union", "intersect", "difference", "complement", - "subset", "array-ext", "as-array", "Array", - // Z3 (and not only?) extensions to bitvectors - "bit1", "bit0", "bvsub", "bvsdiv", "bvsrem", "bvsmod", "bvsdiv0", "bvudiv0", "bvsrem0", "bvurem0", - "bvsmod0", "bvsdiv_i", "bvudiv_i", "bvsrem_i", "bvurem_i", "bvumod_i", "bvule", "bvsle", "bvuge", - "bvsge", "bvslt", "bvugt", "bvsgt", "bvxor", "bvnand", "bvnor", "bvxnor", "sign_extend", "zero_extend", - "repeat", "bvredor", "bvredand", "bvcomp", "bvumul_noovfl", "bvsmul_noovfl", "bvsmul_noudfl", "bvashr", - "rotate_left", "rotate_right", "ext_rotate_left", "ext_rotate_right", "int2bv", "bv2int", "mkbv", - // floating point (FIXME: Legacy, remove this) - "plusInfinity", "minusInfinity", - "+", "-", "/", "*", "==", "<", ">", "<=", ">=", - "abs", "remainder", "fusedMA", "squareRoot", "roundToIntegral", - "isZero", "isNZero", "isPZero", "isSignMinus", "min", "max", "asFloat", - // SMT v1 stuff (FIXME: Legacy, remove this) - "flet", "implies", "!=", "if_then_else", - // Z3 extensions - "lblneg", "lblpos", "lbl-lit", - "if", "&&", "||", "equals", "equiv", "bool", - // Boogie-defined - "real_pow", "UOrdering2", "UOrdering3", - // Floating point (final draft SMTLIB-v2.5) - "NaN", - "roundNearestTiesToEven", "roundNearestTiesToAway", "roundTowardPositive", "roundTowardNegative", "roundTowardZero", - "RNE", "RNA", "RTP", "RTN", "RTZ", - "fp.abs", "fp.neg", "fp.add", "fp.sub", "fp.mul", "fp.div", "fp.fma", "fp.sqrt", "fp.rem", "fp.roundToIntegral", - "fp.min", "fp.max", "fp.leq", "fp.lt", "fp.geq", "fp.gt", "fp.eq", - "fp.isNormal", "fp.isSubnormal", "fp.isZero", "fp.isInfinite", "fp.isNaN", "fp.isNegative", "fp.isPositive", - "fp", "fp.to_ubv", "fp.to_sbv", "to_fp", - }; - - static HashSet reservedSmtWords; - static bool[] validIdChar; - static bool symbolListsInitilized; - - static void InitSymbolLists() - { - lock (reservedSmtWordsList) { - // don't move out, c.f. http://en.wikipedia.org/wiki/Double-checked_locking - if (symbolListsInitilized) - return; - reservedSmtWords = new HashSet(); - foreach (var w in reservedSmtWordsList) - reservedSmtWords.Add(w); - validIdChar = new bool[255]; - for (int i = 0; i < validIdChar.Length; ++i) - validIdChar[i] = char.IsLetterOrDigit((char)i) || idCharacters.IndexOf((char)i) >= 0; - symbolListsInitilized = true; - } - } - - static string AddQuotes(string s) - { - var allGood = true; - - foreach (char ch in s) { - var c = (int)ch; - if (c >= validIdChar.Length || !validIdChar[c]) { - allGood = false; - break; - } - } - - if (allGood) - return s; - - return "|" + s + "|"; - } - - static string NonKeyword(string s) - { - if (reservedSmtWords.Contains(s) || char.IsDigit(s[0])) - s = "q@" + s; - - // | and \ are illegal even in quoted identifiers - if (s.IndexOf('|') >= 0) - s = s.Replace("|", "_"); - - if (s.IndexOf('\\') >= 0) - s = s.Replace("\\", "_"); - - return s; - } - - public static string LabelVar(string s) - { - return "%lbl%" + s; - } - - public static string QuoteId(string s) - { - return AddQuotes(NonKeyword(s)); - } - - public override string GetQuotedLocalName(object thingie, string inherentName) - { - return AddQuotes(base.GetLocalName(thingie, NonKeyword(inherentName))); - } - - public override string GetQuotedName(object thingie, string inherentName) - { - return AddQuotes(base.GetName(thingie, NonKeyword(inherentName))); - } - - public SMTLibNamer() - { - this.Spacer = "@@"; - InitSymbolLists(); - } - } -} +using System; +using System.Collections.Generic; +using System.Linq; +using System.Text; +using Microsoft.Boogie.VCExprAST; + +namespace Microsoft.Boogie.SMTLib +{ + public class SMTLibNamer : UniqueNamer + { + // The following Boogie ID characters are not SMT ID characters: `'\# + const string idCharacters = "~!@$%^&*_-+=<>.?/"; + + + static string[] reservedSmtWordsList = + { // Basic symbols: + "", "!", "_", "as", "DECIMAL", "exists", "forall", "let", "NUMERAL", "par", "STRING", + // Commands: + "assert", "check-sat", "declare-sort", "declare-fun", "define-sort,", "define-fun", "exit", + "get-assertions", "get-assignment", "get-info", "get-option,", "get-proof", "get-unsat-core", + "get-value", "pop", "push", "set-logic", "set-info", "set-option", + // Core theory: + "and", "or", "not", "iff", "true", "false", "xor", "distinct", "ite", "=", "Bool", + "=>", // implies (sic!) + // Integers and reals + "Int", "Real", "*", "/", "-", "~", "+", "<", "<=", ">", ">=", "div", "mod", "rem", + "^", "sin", "cos", "tan", "asin", "acos", "atan", "sinh", "cosh", "tanh", "asinh", "acosh", "atanh", "pi", "euler", + "to_real", "to_int", "is_int", + // Bitvectors + "extract", "concat", + "bvnot", "bvneg", "bvand", "bvor", "bvadd", "bvmul", "bvudiv", "bvurem", "bvshl", "bvlshr", "bvult", + // arrays + "store", "select", "const", "default", "map", "union", "intersect", "difference", "complement", + "subset", "array-ext", "as-array", "Array", + // Z3 (and not only?) extensions to bitvectors + "bit1", "bit0", "bvsub", "bvsdiv", "bvsrem", "bvsmod", "bvsdiv0", "bvudiv0", "bvsrem0", "bvurem0", + "bvsmod0", "bvsdiv_i", "bvudiv_i", "bvsrem_i", "bvurem_i", "bvumod_i", "bvule", "bvsle", "bvuge", + "bvsge", "bvslt", "bvugt", "bvsgt", "bvxor", "bvnand", "bvnor", "bvxnor", "sign_extend", "zero_extend", + "repeat", "bvredor", "bvredand", "bvcomp", "bvumul_noovfl", "bvsmul_noovfl", "bvsmul_noudfl", "bvashr", + "rotate_left", "rotate_right", "ext_rotate_left", "ext_rotate_right", "int2bv", "bv2int", "mkbv", + // floating point (FIXME: Legacy, remove this) + "plusInfinity", "minusInfinity", + "+", "-", "/", "*", "==", "<", ">", "<=", ">=", + "abs", "remainder", "fusedMA", "squareRoot", "roundToIntegral", + "isZero", "isNZero", "isPZero", "isSignMinus", "min", "max", "asFloat", + // SMT v1 stuff (FIXME: Legacy, remove this) + "flet", "implies", "!=", "if_then_else", + // Z3 extensions + "lblneg", "lblpos", "lbl-lit", + "if", "&&", "||", "equals", "equiv", "bool", "minimize", "maximize", + // Boogie-defined + "real_pow", "UOrdering2", "UOrdering3", + // Floating point (final draft SMTLIB-v2.5) + "NaN", + "roundNearestTiesToEven", "roundNearestTiesToAway", "roundTowardPositive", "roundTowardNegative", "roundTowardZero", + "RNE", "RNA", "RTP", "RTN", "RTZ", + "fp.abs", "fp.neg", "fp.add", "fp.sub", "fp.mul", "fp.div", "fp.fma", "fp.sqrt", "fp.rem", "fp.roundToIntegral", + "fp.min", "fp.max", "fp.leq", "fp.lt", "fp.geq", "fp.gt", "fp.eq", + "fp.isNormal", "fp.isSubnormal", "fp.isZero", "fp.isInfinite", "fp.isNaN", "fp.isNegative", "fp.isPositive", + "fp", "fp.to_ubv", "fp.to_sbv", "to_fp", + }; + + static HashSet reservedSmtWords; + static bool[] validIdChar; + static bool symbolListsInitilized; + + static void InitSymbolLists() + { + lock (reservedSmtWordsList) { + // don't move out, c.f. http://en.wikipedia.org/wiki/Double-checked_locking + if (symbolListsInitilized) + return; + reservedSmtWords = new HashSet(); + foreach (var w in reservedSmtWordsList) + reservedSmtWords.Add(w); + validIdChar = new bool[255]; + for (int i = 0; i < validIdChar.Length; ++i) + validIdChar[i] = char.IsLetterOrDigit((char)i) || idCharacters.IndexOf((char)i) >= 0; + symbolListsInitilized = true; + } + } + + static string AddQuotes(string s) + { + var allGood = true; + + foreach (char ch in s) { + var c = (int)ch; + if (c >= validIdChar.Length || !validIdChar[c]) { + allGood = false; + break; + } + } + + if (allGood) + return s; + + return "|" + s + "|"; + } + + static string FilterReserved(string s) + { + // Note symbols starting with ``.`` and ``@`` are reserved for internal + // solver use in SMT-LIBv2 however if we check for the first character + // being ``@`` then Boogie's tests fail spectacularly because they are + // used for labels so we don't check for it here. It hopefully won't matter + // in practice because ``@`` cannot be legally used in Boogie identifiers. + if (reservedSmtWords.Contains(s) || char.IsDigit(s[0]) || s[0] == '.') + s = "q@" + s; + + // | and \ are illegal even in quoted identifiers + if (s.IndexOf('|') >= 0) + s = s.Replace("|", "_"); + + if (s.IndexOf('\\') >= 0) + s = s.Replace("\\", "_"); + + return s; + } + + public static string LabelVar(string s) + { + return "%lbl%" + s; + } + + public static string QuoteId(string s) + { + return AddQuotes(FilterReserved(s)); + } + + public override string GetQuotedLocalName(object thingie, string inherentName) + { + return AddQuotes(base.GetLocalName(thingie, FilterReserved(inherentName))); + } + + public override string GetQuotedName(object thingie, string inherentName) + { + return AddQuotes(base.GetName(thingie, FilterReserved(inherentName))); + } + + public SMTLibNamer() + { + this.Spacer = "@@"; + InitSymbolLists(); + } + } +} -- cgit v1.2.3