Hello,
we would like to use yices_term_to_string() to generate short SMTLIB scripts from yices terms. Unfortunately the function does not seem to escape illegal variable names, which can lead to broken output strings.
Here is an example:
#include <yices.h>
int main() {
yices_init();
type_t int_type = yices_int_type();
term_t x = yices_new_uninterpreted_term(int_type);
term_t y = yices_new_uninterpreted_term(int_type);
yices_set_term_name(x, "x");
yices_set_term_name(y, ")");
term_t formula = yices_arith_eq_atom(x, y);
char* output = yices_term_to_string(formula, 1000, 1, 0);
printf("%s\n", output);
yices_exit();
return 0;
}
Running this program will print (= x )) to the console. This is not a valid formula and trying to read it back in with yices_parse_term will result in a segmentation fault. In the SMTLIB format the problem is solved by quoting such variable names with |s. The output then becomes (= x |)|) for our example. (Other than parentheses there are some more restrictions on what may be included as part of a variable name. A full definition can be found on page 23 of the SMTLIB standard (link) under "Symbols".)
Would it be possible to add SMTLIB quoting to yices?
Hello, we would like to use
yices_term_to_string()to generate short SMTLIB scripts from yices terms. Unfortunately the function does not seem to escape illegal variable names, which can lead to broken output strings.Here is an example:
Running this program will print
(= x ))to the console. This is not a valid formula and trying to read it back in withyices_parse_termwill result in a segmentation fault. In the SMTLIB format the problem is solved by quoting such variable names with|s. The output then becomes(= x |)|)for our example. (Other than parentheses there are some more restrictions on what may be included as part of a variable name. A full definition can be found on page 23 of the SMTLIB standard (link) under "Symbols".)Would it be possible to add SMTLIB quoting to yices?