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.

1 files changed, 0 insertions, 6 deletions

diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index 289fc26f0..33ee51007 100644
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -881,8 +881,6 @@ void SolverBlack::testDefineFunsRec()
 
 void SolverBlack::testSetInfo()
 {
-  TS_ASSERT_THROWS_NOTHING(d_solver->setInfo("cvc4-logic", "QF_BV"));
-  TS_ASSERT_THROWS_NOTHING(d_solver->setInfo("cvc4_logic", "QF_BV"));
   TS_ASSERT_THROWS(d_solver->setInfo("cvc4-lagic", "QF_BV"), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->setInfo("cvc2-logic", "QF_BV"), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->setInfo("cvc4-logic", "asdf"), CVC4ApiException&);
@@ -907,10 +905,6 @@ void SolverBlack::testSetInfo()
   TS_ASSERT_THROWS_NOTHING(d_solver->setInfo("status", "unsat"));
   TS_ASSERT_THROWS_NOTHING(d_solver->setInfo("status", "unknown"));
   TS_ASSERT_THROWS(d_solver->setInfo("status", "asdf"), CVC4ApiException&);
-
-  d_solver->assertFormula(d_solver->mkTrue());
-  TS_ASSERT_THROWS(d_solver->setInfo("cvc4-logic", "QF_BV"), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->setInfo("cvc4_logic", "QF_BV"), CVC4ApiException&);
 }
 
 void SolverBlack::testSetLogic()