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
|
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", "*", "/", "-", "+", "<", "<=", ">", ">=",
// SMT v1 stuff
"flet", "implies", "!=", "if_then_else",
// Z3 extensions
"lblneg", "lblpos", "lbl-lit",
"if", "&&", "||", "equals", "equiv", "bool",
};
static Dictionary<string, bool> reservedSmtWords;
static bool[] validIdChar;
static bool symbolListsInitilized;
static void InitSymbolLists()
{
if (symbolListsInitilized)
return;
lock (reservedSmtWordsList) {
if (symbolListsInitilized)
return;
reservedSmtWords = new Dictionary<string, bool>();
foreach (var w in reservedSmtWordsList)
reservedSmtWords.Add(w, true);
validIdChar = new bool[255];
for (int i = 0; i < validIdChar.Length; ++i)
validIdChar[i] = char.IsLetterOrDigit((char)i) || idCharacters.IndexOf((char)i) >= 0;
System.Threading.Thread.MemoryBarrier(); // c.f. http://en.wikipedia.org/wiki/Double-checked_locking
symbolListsInitilized = true;
}
}
static string AddQuotes(string s)
{
InitSymbolLists();
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)
{
InitSymbolLists();
if (reservedSmtWords.ContainsKey(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 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 = "@@";
}
}
}
|
