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
|
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<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 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();
}
}
}
|
