-
Notifications
You must be signed in to change notification settings - Fork 2
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
Option to use standard input and output? #1
Comments
I've added support for this. It's a bit of a hack -- the input just gets written to a temp file. There are a lot of things I want to change about the parser, and when I have a chance to make improvements I'll handle this option more cleanly. To use this, call the executable with file name |
By the way, looking at your z3 interface, it seems like you're making use of z3's unsat core/model generation features? Unfortunately Polya supports neither of those at the moment. In principle, it can find an unsat core, but I don't have it implemented yet. Model generation is out of scope. We're considering how to do it by using other systems (e.g., Polya + z3 may be able to find a model more efficiently than z3 alone), but have no clear plan for this yet. I don't know if these features are vital for your purposes, just wanted to point it out! |
Neither is crucial. CVC4 doesn't seem to generate models either. What we
On Fri, Mar 4, 2016, 11:32 AM Rob Lewis [email protected] wrote:
|
An alternative solution would be to pass a stream, e.g. |
Thanks for the suggestion! Yes, I'm suspect that's possible. This is based off of a parser written by someone else, and I've tried to mess with their code as little as possible. There are a lot of hacks that I need to clean up now that this project has become a bit more public :) I'm traveling at the moment, but revisiting the parser is on my to-do list for later this week. |
An option that I had considered that would be easy (maybe I could hack it up) is to just have get_pos return (0,0) when the input is a stream instead of a file and printing a message that says "error reporting is not currently supported when using streams." |
I just implemented the easy solution, and when I have a chance to revise the rest of the parser, I'll figure out how to track the position on the first pass through. |
Is it possible to use standard in and standard out for the input and output instead of file names?
The text was updated successfully, but these errors were encountered: