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
|
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
"Int", "*", "/", "-", "+", "<", "<=", ">", ">=",
// Bitvectors
"extract", "concat",
"bvnot", "bvneg", "bvand", "bvor", "bvadd", "bvmul", "bvudiv", "bvurem", "bvshl", "bvlshr", "bvult",
// 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",
// SMT v1 stuff
"flet", "implies", "!=", "if_then_else",
// Z3 extensions
"lblneg", "lblpos", "lbl-lit",
"if", "&&", "||", "equals", "equiv", "bool",
// Boogie-defined
"int_mod", "int_div", "UOrdering2", "UOrdering3",
};
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();
}
}
}
|
