uuverifiers / eldarica

The Eldarica model checker
Other
81 stars 23 forks source link

Add support for reading from stdin #53

Closed sankalpgambhir closed 9 months ago

sankalpgambhir commented 9 months ago

As title says, modified the main file and some associated parser calls to use InputStream instead.

Factorized creation of the input stream from the file name into a function to have a uniform process and error.

Added CLI option -in (like z3) to allow reading files from standard input. This defaults to SMT Horn input format if no other has been given yet. (Since the format cannot be determined from file name).

As with most other options, if you later provide a file name in the argument list, it will override -in.

I needed this while trying to interface with Eldarica via scala-smtlib (to reuse some solver interfaces instead of using the Eldarica Scala API).

I think it is a good thing to have, in any case.

As to why the PR is draft, I tested the stdin input in three ways:

  1. Providing a file, e.g. ./eld -in < file --- this works well as expected
  2. Typing manually (less interesting, but still), e.g. ./eld -in and simply typing the query. I had to press Ctrl-D multiples times before my EOF was accepted and the query processed.
  3. Using run -in from within sbt. This did not work at all. Eldarica immediately outputs sat corresponding to the empty input stream.

I will try to investigate situations 2 and 3 before un-marking the PR as draft. That, and more testing.

Till then, happy to take any feedback, especially as it is my first PR for this project.

pruemmer commented 9 months ago

Thanks!

In other tools, in the interactive mode I'm reading from Console.in, not from System.in. The latter might be problematic due to buffering getting in the way.

(Also, I rather want to avoid "sys.exit(...)" in the code, there might be other threads still working.)

sankalpgambhir commented 9 months ago

I can change to Console.in, that makes sense. The sys.exit part was lifted from how the NTSWrapper used to read files internally and moved to the main class to make it uniform.

Would it instead be preferable to raise a warning that the file was not found and continue processing the CLI options?

pruemmer commented 9 months ago

It would make sense to test whether changing to Console.in will solve the problems (situations 2 and 3) you were observing.

For the error handling, just throwing an exception is the best option in my opinion!

sankalpgambhir commented 9 months ago

:heavy_check_mark: Fixed to throw an exception on not finding a file :heavy_check_mark: Changed to read from Console.In

Does not solve the issue regarding situations 2 and 3 above :/

pruemmer commented 9 months ago

Situation 2 seems to work now; I believe we encountered the same problem a while ago in a different context, and developed a work-around then. Situation 3, I have no idea what is happening here, but this might be an sbt issue?