search

WatForm / fortress

Fortress: Finite Model Finder for Many-Sorted First-Order Logic
MIT License
5 stars 0 forks source link

Need Better message for file not found at fortress CLI than exception #103

Closed nancyday closed 4 months ago

nancyday commented 4 months ago

This should be easily fixed in the util.Errors

nancyday commented 4 months ago

Additionally put Fortress CLI have a verbose or not verbose mode with print statements in CLI

nancyday commented 4 months ago

make Fortress CLI by itself (with no args) produce the --help info

nancyday commented 4 months ago

@otzzila - as I'm cleaning up the Fortress CLI, I'm trying to figure out what stops a sort being given a scope multiple times in the cmd line and/or the file? Shouldn't we be flagging an error for this? They could also be specific with different exact/inexact/fixed attributes? I wonder if we could make what's in the file more consistent with what is expected at the CLI?

nancyday commented 4 months ago

@otzzila - I'm also confused because debug mode seems to run the compiler separately from the solver? But then compiling will be run again in modelFinder.checkSat()? Was that the intent? Perhaps instead we should give fortress an option to compileOnly?

nancyday commented 4 months ago
nancyday commented 4 months ago

https://github.com/WatForm/fortress/commit/eb7d67b2282472a4145b3190dee97ff707521687