Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Function names quoted with ' instead of | when seraializing to smt2 #584

Closed
ekiwi opened this issue May 23, 2019 · 3 comments

Comments

Projects
None yet
2 participants
@ekiwi
Copy link

commented May 23, 2019

A short example:

from pysmt.shortcuts import *
f_t = FunctionType(BOOL, [BOOL])
f0 = Symbol('f 0', f_t)
f0_of_false = Function(f0, [Bool(False)])
to_smtlib(f0_of_false, False)

The last expression results in the string: "('f 0' false)"
The expected result would be: '(|f 0| false)'

I can get the expected result by changing pysmt/smtlib/printers.py#L94 to:

return self.walk_nary(formula, quote(formula.function_name().symbol_name()))

However, I am not sure if that is a valid fix.

@mikand

This comment has been minimized.

Copy link
Contributor

commented May 23, 2019

@ekiwi Thanks for reporting this. Indeed you are right and pysmt/smtlib/printers.py#L94 should be changed as you suggest. I'll do it right away.

@mikand mikand self-assigned this May 23, 2019

@mikand mikand added the bug label May 23, 2019

mikand added a commit that referenced this issue May 23, 2019

Fixed Issue #584
Fixed printing as suggested by @ekiwi

@mikand mikand referenced this issue May 23, 2019

Merged

Fixed Issue #584 #585

mikand added a commit that referenced this issue May 23, 2019

@mikand

This comment has been minimized.

Copy link
Contributor

commented May 23, 2019

This is now fixed in master. If you are using pysmt using pip you can installa pre-release package with
pip install --upgrade --pre pysmt

@mikand mikand closed this May 23, 2019

@ekiwi

This comment has been minimized.

Copy link
Author

commented May 23, 2019

That was quick.
Thanks a lot!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.