Skip to content

Commit 9044e9a

Browse files
committed
remove dependency of Yices2 component to SMTInterpol.
1 parent 5038195 commit 9044e9a

File tree

1 file changed

+16
-1
lines changed

1 file changed

+16
-1
lines changed

Diff for: src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaManager.java

+16-1
Original file line numberDiff line numberDiff line change
@@ -88,7 +88,7 @@ public void appendTo(Appendable out) throws IOException {
8888
}
8989
if (types.length > 0) {
9090
out.append("(declare-fun ");
91-
out.append(PrintTerm.quoteIdentifier(entry.getKey()));
91+
out.append(quoteIdentifier(entry.getKey()));
9292
out.append(" (");
9393
for (int i = 0; i < types.length - 1; i++) {
9494
out.append(getTypeRepr(types[i]));
@@ -111,4 +111,19 @@ private String getTypeRepr(int type) {
111111
}
112112
};
113113
}
114+
115+
/** copied from {@link PrintTerm#quoteIdentifier(String)} */
116+
private static String quoteIdentifier(String id) {
117+
assert id.indexOf('|') < 0 && id.indexOf('\\') < 0;
118+
for (int idx = 0; idx < id.length(); idx++) {
119+
final char c = id.charAt(idx);
120+
if (!(c >= 'A' && c <= 'Z')
121+
&& !(c >= 'a' && c <= 'z')
122+
&& !(c >= '0' && c <= '9' && idx > 0)
123+
&& "~!@$%^&*_+-=<>.?/".indexOf(c) < 0) {
124+
return "|" + id + "|";
125+
}
126+
}
127+
return id;
128+
}
114129
}

0 commit comments

Comments
 (0)