search

robertylewis / smtlib2polya

GNU General Public License v3.0
2 stars 2 forks source link

Option to use standard input and output? #1

Open gmalecha opened 8 years ago

gmalecha commented 8 years ago

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

robertylewis commented 8 years ago

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 commented 8 years ago

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 commented 8 years ago

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

On Fri, Mar 4, 2016, 11:32 AM Rob Lewis notifications@github.com 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 https://github.com/rlewis1988/smtlib2polya/issues/1#issuecomment-192430207 .

gmalecha commented 8 years ago

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 commented 8 years ago

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 commented 8 years ago

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 commented 8 years ago

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.