Option to use standard input and output?

[gmalecha]

Is it possible to use standard in and standard out for the input and output instead of file names?

[robertylewis]

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 STDIN. Example:
cat file_name.smt2 | ./polya STDIN

[robertylewis]

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!

[gmalecha]

Neither is crucial. CVC4 doesn't seem to generate models either. What we
use them for are:

• sat model: display to user
• unsat core: clear all irrelevant hypotheses

On Fri, Mar 4, 2016, 11:32 AM Rob Lewis [email protected] wrote:

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!

—
Reply to this email directly or view it on GitHub
#1 (comment)
.

[gmalecha]

An alternative solution would be to pass a stream, e.g. open (filename, 'r') or sys.stdin to the constructor rather than the name of the file. It seems like the one place where this does not work is because you open the file a second time in get_pos. Is it possible to record the position information as you traverse the stream so that you do not need to re-open the file?

[robertylewis]

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.

[gmalecha]

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."

[robertylewis]

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.