more documentation for invalid names.
@@ -221,6 +221,24 @@ public interface FormulaManager {
/**
* Check whether the given String can be used as symbol/name for variables or undefined functions.
+ *
+ * <p>We explicitly state that with further development of SMT solvers and the SMTLib
+ * specification, the list of forbidden variable names may change in the future. Users should if
+ * possible not use logical or mathematical operators, or keywords strongly depending on SMTlib.
+ *
+ * <p>If a variable name is rejected, a possibility is escaping, e.g. either substituting the
+ * whole variable name or just every invalid character with an escaped form. We recommend to use
+ * an escape sequence based on the token "JAVASMT", because it might be unusual enough to appear
+ * when encoding a user's problem in SMT. Please not that you might also have to handle escaping
+ * the escape sequence. Examples:
+ *
+ * <ul>
+ * <li>the invalid variable name <code>"="</code> (logical operator for equality) can be
+ * replaced with a string <code>"JAVASMT_EQUALS"</code>.
+ * <li>the invalid SMTlib-escaped variable name <code>"|test|"</code> (the solver SMTInterpol
+ * does not allow the pipe symbol <code>"|"</code> in names) can be replaced with <code>
+ * "JAVASMT_PIPEtestJAVASMT_PIPE"</code>.
+ * </ul>
*/
boolean isValidName(String variableName);
}
