Yices2 produces invalid SMTLIB output when dumping formulas

[daniel-raffler]

Hello everyone, yices2 does not apply correct quotes while dumping SMTLIB formulas. An example for this can be seen in VariableNamesTest.testBoolVariableDump() where the formula for a (boolean) variable named "(" produces the following output:

(declare-fun |(| () Bool)
(assert ()

The correct output should use quotes for the "(" in the assertion:

(declare-fun |(| () Bool)
(assert |(|)

Without the quotes the SMTLIB string is invalid and will cause an exception during post-processing. (Which is why the test was temporarily disabled for yices2)

The problem is with the yices2 function yices_term_to_string(), which fails to apply the quotes while printing the formula. We should report this to the yices2 developers and wait for a fix. If this is not an option we may want to handle quoting on our end by overloading `Yices2FormulaManager.makeVariable.

[kfriedberger]

Does this issue only affect simple formulas like |(| or also complex ones like and |(| x |)|?

[daniel-raffler]

Does this issue only affect simple formulas like |(| or also complex ones like and |(| x |)|?

It seems to be for all formulas. Take for instance:

BooleanFormula var1 = bmgr.makeVariable(")");
BooleanFormula var2 = bmgr.makeVariable("var2");
BooleanFormula formula = bmgr.and(var1, var2);
String dump = mgr.dumpFormula(formula).toString()

Here Yices2FormulaManager.dumpFormulaImpl will give us:

(declare-fun var2 () Bool)
(declare-fun |)| () Bool)
(assert (and ) var2))"

Which does not quote the ")" in the assert.

(Note that the ")" in declare-fun is in fact quoted. This is because we added the declaration ourselves before the term is printed. For this job there already is a function quote in Yices2FormulaManager. Applying it to an entire term, however, would require us to use a visitor that rewrites the variable names.)

[kfriedberger]

Please report this issue to Yices. If they provide a fix, we can update the library in JavaSMT quite easily.

Also, using a formula visitor to print a formula (and escape symbols) could be a good exercise for new developers and could be added as example. A plain String representation can be exponentially large, so one would introduce let-terms for some parts. 🐞 Maybe someone wants toplay around here.

[daniel-raffler]

I've now opened an issue for Yices: https://github.com/SRI-CSL/yices2/issues/534

[daniel-raffler]

I've now opened an issue for Yices: SRI-CSL/yices2#534

This issue has now been fixed in Yices2. We should check if it's now working with the latest version