Fix and simplify handling of --force-logic (#3062)
authorAndres Noetzli <andres.noetzli@gmail.com>
Fri, 21 Jun 2019 18:58:25 +0000 (11:58 -0700)
committerGitHub <noreply@github.com>
Fri, 21 Jun 2019 18:58:25 +0000 (11:58 -0700)
commitbe33ac9656bf7feafa3715d6623749f6afd962b5
tree63fe6f537e6b2df5791c02f0183706a8e7f5ead2
parentcf9dfb9be23b4f802989fecd18756ed62aecc8e4
Fix and simplify handling of --force-logic (#3062)

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.
22 files changed:
src/api/cvc4cpp.cpp
src/options/options.h
src/options/options_handler.cpp
src/options/options_handler.h
src/options/options_template.cpp
src/options/parser_options.toml
src/options/smt_options.toml
src/parser/CMakeLists.txt
src/parser/cvc/cvc.cpp [new file with mode: 0644]
src/parser/cvc/cvc.h [new file with mode: 0644]
src/parser/parser.h
src/parser/parser_builder.cpp
src/parser/smt2/Smt2.g
src/parser/smt2/smt2.cpp
src/parser/smt2/smt2.h
src/parser/tptp/tptp.cpp
src/parser/tptp/tptp.h
src/smt/smt_engine.cpp
test/regress/CMakeLists.txt
test/regress/regress0/bv/eager-force-logic.smt2 [new file with mode: 0644]
test/regress/regress0/parser/force_logic_set_logic.smt2 [new file with mode: 0644]
test/unit/api/solver_black.h