|
The `--force-logic` command line argument can be used to override a
logic specified in an input file or to set a logic when none is given.
Before this commit, both the `SmtEngine` and the parser were aware of
that argument. However, there were two issues if an input file didn't
specify a logic but `--force-logic` was used:
- Upon parsing `--force-logic`, the `SmtEngine` was informed about it
and set the logic to the forced logic. Then, the parser detected that
there was no `set-logic` command, so it set the logic to `ALL` and
emitted a corresponding warning. Finally, `SmtEngine::setDefaults()`
detected that `forceLogic` was set by the user and changed the logic
back to the forced logic. The warning was confusing and setting the
logic multiple times was not elegant.
- For eager bit-blasting, the logic was checked before resetting the
logic to the forced logic, so it would emit an error that eager
bit-blasting couldn't be used with the logic (which was `ALL` at that
point of the execution). This was a problem in the competition because
our runscript parses the `set-logic` command to decide on the
appropriate arguments to use and passes the logic to CVC4 via
`--force-logic`.
This commit moves the handling of `--force-logic` entirely into the
parser. The rationale for that is that this is not an API-level issue
(if you use the API you simply set the logic you want, forcing a
different logic in addition doesn't make sense) and simplifies the
handling of the option (no listeners need to be installed and the logic
is set only once). This commit also removes the option to set the logic
via `(set-option :cvc4-logic ...)` because it complicates matters (e.g.
which method of setting the logic takes precedence?). For the CVC and
the TPTP languages the commit creates a command to set the logic in
`SmtEngine` when the logic is forced in the parser instead of relying on
`SmtEngine` to figure it out itself.
|
