Skip to content

Commit f96547b

Browse files
daniel-rafflerdaniel-raffler
committed
Add more reserved keywords to the list of forbidden variable/UF names in AbstractFormulaManager
1 parent 61acda9 commit f96547b

File tree

3 files changed

+133
-45
lines changed

3 files changed

+133
-45
lines changed

‎src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java‎

Lines changed: 131 additions & 42 deletions
Original file line numberDiff line numberDiff line change
@@ -15,8 +15,8 @@
1515
import com.google.common.base.CharMatcher;
1616
import com.google.common.base.Preconditions;
1717
import com.google.common.collect.ImmutableBiMap;
18+
import com.google.common.collect.ImmutableList;
1819
import com.google.common.collect.ImmutableMap;
19-
import com.google.common.collect.ImmutableSet;
2020
import com.google.common.collect.Iterables;
2121
import java.io.IOException;
2222
import java.util.Arrays;
@@ -58,29 +58,135 @@
5858
public abstract class AbstractFormulaManager<TFormulaInfo, TType, TEnv, TFuncDecl>
5959
implements FormulaManager {
6060

61-
/**
62-
* Avoid using basic mathematical or logical operators of SMT-LIB2 as names for symbols.
63-
*
64-
* <p>We do not accept some names as identifiers for variables or UFs, because they easily
65-
* misguide the user. Most solvers even would allow such identifiers directly, currently only
66-
* SMTInterpol has problems with some of them. For consistency, we disallow those names for all
67-
* solvers.
68-
*/
6961
@VisibleForTesting
70-
public static final ImmutableSet<String> BASIC_OPERATORS =
71-
ImmutableSet.of("!", "+", "-", "*", "/", "%", "=", "<", ">", "<=", ">=");
62+
public static final ImmutableList<String> RESERVED =
63+
ImmutableList.of(
64+
// Keywords
65+
"_",
66+
"!",
67+
"as",
68+
"let",
69+
"exists",
70+
"forall",
71+
"match",
72+
"par",
73+
74+
// Commands
75+
"assert",
76+
"check-sat",
77+
"check-sat-assuming",
78+
"declare-const",
79+
"declare-datatype",
80+
"declare-datatypes",
81+
"declare-fun",
82+
"declare-sort",
83+
"define-fun",
84+
"define-fun-rec",
85+
"define-funs-rec",
86+
"define-sort",
87+
"echo",
88+
"exit",
89+
"get-assertions",
90+
"get-assignment",
91+
"get-info",
92+
"get-model",
93+
"get-option",
94+
"get-proof",
95+
"get-unsat-assumptions",
96+
"get-unsat-core",
97+
"get-value",
98+
"pop",
99+
"push",
100+
"reset",
101+
"reset-assertions",
102+
"set-info",
103+
"set-logic",
104+
"set-option",
105+
106+
// Predefined symbols
107+
// Arrays
108+
"select",
109+
"store",
110+
"const",
111+
112+
// Bitvectors
113+
"concat",
114+
"extract",
115+
// + any symbol starting with "bv"
116+
"bvneg",
117+
118+
// Core
119+
"true",
120+
"false",
121+
"not",
122+
"=>",
123+
"and",
124+
"or",
125+
"xor",
126+
"=",
127+
"distinct",
128+
"ite",
129+
130+
// Floats
131+
"roundNearestTiesToEven RoundingMode",
132+
"roundNearestTiesToAway",
133+
"roundTowardPositive",
134+
"roundTowardNegative",
135+
"roundTowardZero",
136+
"RNE",
137+
"RNA",
138+
"RTP",
139+
"RTN",
140+
"RTZ",
141+
"fp",
142+
"+oo",
143+
"-oo",
144+
"+zero",
145+
"-zero",
146+
"NaN",
147+
"to_fp",
148+
"to_fp_unsigned",
149+
// + any symbol starting with "fp."
150+
"fp.neg",
151+
152+
// Integers and Reals
153+
"-",
154+
"+",
155+
"*",
156+
"div",
157+
"mod",
158+
"/",
159+
"abs",
160+
"<=",
161+
"<",
162+
">=",
163+
">",
164+
"divisible",
165+
"to_real",
166+
"to_int",
167+
"is_int",
168+
169+
// Strings
170+
// + any symbol starting with "str."
171+
"str.concat",
172+
// + any symbol starting with "re."
173+
"re.opt");
72174

73175
/**
74-
* Avoid using basic keywords of SMT-LIB2 as names for symbols.
176+
* Checks if the symbol name is a reserved keyword in SMTLIB2.
75177
*
76178
* <p>We do not accept some names as identifiers for variables or UFs, because they easily
77179
* misguide the user. Most solvers even would allow such identifiers directly, currently only
78180
* SMTInterpol has problems with some of them. For consistency, we disallow those names for all
79181
* solvers.
80182
*/
81-
@VisibleForTesting
82-
public static final ImmutableSet<String> SMTLIB2_KEYWORDS =
83-
ImmutableSet.of("true", "false", "and", "or", "select", "store", "xor", "distinct", "let");
183+
public static boolean isReserved(String pVar) {
184+
return pVar.startsWith("bv")
185+
|| pVar.startsWith("fp.*")
186+
|| pVar.startsWith("str.")
187+
|| pVar.startsWith("re.")
188+
|| RESERVED.contains(pVar);
189+
}
84190

85191
/**
86192
* Avoid using escape characters of SMT-LIB2 as part of names for symbols.
@@ -587,19 +693,7 @@ private Formula replace(Formula f) {
587693
*/
588694
@Override
589695
public final boolean isValidName(String pVar) {
590-
if (pVar.isEmpty()) {
591-
return false;
592-
}
593-
if (BASIC_OPERATORS.contains(pVar)) {
594-
return false;
595-
}
596-
if (SMTLIB2_KEYWORDS.contains(pVar)) {
597-
return false;
598-
}
599-
if (DISALLOWED_CHARACTERS.matchesAnyOf(pVar)) {
600-
return false;
601-
}
602-
return true;
696+
return !pVar.isEmpty() && !DISALLOWED_CHARACTERS.matchesAnyOf(pVar) && !isReserved(pVar);
603697
}
604698

605699
/**
@@ -613,32 +707,27 @@ public final boolean isValidName(String pVar) {
613707
public static void checkVariableName(final String variableName) {
614708
final String help = "Use FormulaManager#isValidName to check your identifier before using it.";
615709
Preconditions.checkArgument(
616-
!variableName.isEmpty(), "Identifier for variable should not be empty.");
617-
Preconditions.checkArgument(
618-
!BASIC_OPERATORS.contains(variableName),
619-
"Identifier '%s' can not be used, because it is a simple operator. %s",
620-
variableName,
621-
help);
622-
Preconditions.checkArgument(
623-
!SMTLIB2_KEYWORDS.contains(variableName),
624-
"Identifier '%s' can not be used, because it is a keyword of SMT-LIB2. %s",
625-
variableName,
626-
help);
710+
!variableName.isEmpty(), "Identifier for variable must not be empty.");
627711
Preconditions.checkArgument(
628712
DISALLOWED_CHARACTERS.matchesNoneOf(variableName),
629713
"Identifier '%s' can not be used, "
630-
+ "because it should not contain an escape character %s of SMT-LIB2. %s",
714+
+ "because it contains an escape character %s of SMT-LIB2. %s",
631715
variableName,
632716
DISALLOWED_CHARACTER_REPLACEMENT
633717
.keySet(), // toString prints UTF8-encoded escape sequence, better than nothing.
634718
help);
719+
Preconditions.checkArgument(
720+
!isReserved(variableName),
721+
"Identifier '%s' can not be used, because it is a reserved symbol in SMT-LIB2. " + "%s",
722+
variableName,
723+
help);
635724
}
636725

637726
/* This escaping works for simple escape sequences only, i.e., keywords are unique enough. */
638727
@Override
639728
public final String escape(String pVar) {
640729
// as long as keywords stay simple, this simple escaping is sufficient
641-
if (pVar.isEmpty() || BASIC_OPERATORS.contains(pVar) || SMTLIB2_KEYWORDS.contains(pVar)) {
730+
if (pVar.isEmpty() || isReserved(pVar)) {
642731
return ESCAPE + pVar;
643732
}
644733
if (pVar.indexOf(ESCAPE) != -1) {
@@ -660,7 +749,7 @@ public final String unescape(String pVar) {
660749
// unescape BASIC_OPERATORS and SMTLIB2_KEYWORDS
661750
if (idx == 0) {
662751
String tmp = pVar.substring(1);
663-
if (tmp.isEmpty() || BASIC_OPERATORS.contains(tmp) || SMTLIB2_KEYWORDS.contains(tmp)) {
752+
if (tmp.isEmpty() || isReserved(tmp)) {
664753
return tmp;
665754
}
666755
}

‎src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaManager.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -133,7 +133,7 @@ assert getFormulaCreator().getFormulaType(formula) == FormulaType.BooleanType
133133
private static String quote(String str) {
134134
Preconditions.checkArgument(!Strings.isNullOrEmpty(str));
135135
Preconditions.checkArgument(CharMatcher.anyOf("|\\").matchesNoneOf(str));
136-
Preconditions.checkArgument(!SMTLIB2_KEYWORDS.contains(str));
136+
Preconditions.checkArgument(!isReserved(str));
137137

138138
if (VALID_CHARS.matchesAllOf(str) && !DIGITS.matches(str.charAt(0))) {
139139
// simple symbol

‎src/org/sosy_lab/java_smt/test/VariableNamesTest.java‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -162,8 +162,7 @@ public class VariableNamesTest extends SolverBasedTest0.ParameterizedSolverBased
162162
protected List<String> getAllNames() {
163163
return ImmutableList.<String>builder()
164164
.addAll(NAMES)
165-
.addAll(AbstractFormulaManager.BASIC_OPERATORS)
166-
.addAll(AbstractFormulaManager.SMTLIB2_KEYWORDS)
165+
.addAll(AbstractFormulaManager.RESERVED)
167166
.addAll(AbstractFormulaManager.DISALLOWED_CHARACTER_REPLACEMENT.values())
168167
.addAll(FURTHER_SMTLIB2_KEYWORDS)
169168
.addAll(UNSUPPORTED_NAMES)

0 commit comments

Comments
 (0)