1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
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", "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<string> 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<string>();
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();
}
}
}
|
