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, 10 insertions, 42 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 2b81b3835..5cf690147 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -285,18 +285,6 @@ class HardResourceOutListener : public Listener {
   SmtEngine* d_smt;
 }; /* class HardResourceOutListener */
 
-class SetLogicListener : public Listener {
- public:
-  SetLogicListener(SmtEngine& smt) : d_smt(&smt) {}
-  void notify() override
-  {
-    LogicInfo inOptions(options::forceLogicString());
-    d_smt->setLogic(inOptions);
-  }
- private:
-  SmtEngine* d_smt;
-}; /* class SetLogicListener */
-
 class BeforeSearchListener : public Listener {
  public:
   BeforeSearchListener(SmtEngine& smt) : d_smt(&smt) {}
@@ -452,7 +440,6 @@ class SmtEnginePrivate : public NodeManagerListener {
    * This list contains:
    *  softResourceOut
    *  hardResourceOut
-   *  setForceLogic
    *  beforeSearchListener
    *  UseTheoryListListener
    *
@@ -600,9 +587,6 @@ class SmtEnginePrivate : public NodeManagerListener {
     try
     {
       Options& nodeManagerOptions = NodeManager::currentNM()->getOptions();
-      d_listenerRegistrations->add(
-          nodeManagerOptions.registerForceLogicListener(
-              new SetLogicListener(d_smt), true));
 
       // Multiple options reuse BeforeSearchListener so registration requires an
       // extra bit of care.
@@ -1209,9 +1193,8 @@ void SmtEngine::setDefaults() {
     }
   }
 
-  if(options::forceLogicString.wasSetByUser()) {
-    d_logic = LogicInfo(options::forceLogicString());
-  }else if (options::solveIntAsBV() > 0) {
+  if (options::solveIntAsBV() > 0)
+  {
     if (!(d_logic <= LogicInfo("QF_NIA")))
     {
       throw OptionException(
@@ -1219,11 +1202,15 @@ void SmtEngine::setDefaults() {
           "QF_LIA, QF_IDL)");
     }
     d_logic = LogicInfo("QF_BV");
-  }else if (d_logic.getLogicString() == "QF_NRA" && options::solveRealAsInt()) {
+  }
+  else if (d_logic.getLogicString() == "QF_NRA" && options::solveRealAsInt())
+  {
     d_logic = LogicInfo("QF_NIA");
-  } else if ((d_logic.getLogicString() == "QF_UFBV" ||
-              d_logic.getLogicString() == "QF_ABV") &&
-             options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
+  }
+  else if ((d_logic.getLogicString() == "QF_UFBV"
+            || d_logic.getLogicString() == "QF_ABV")
+           && options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER)
+  {
     d_logic = LogicInfo("QF_BV");
   }
 
@@ -2346,25 +2333,6 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
     }
   }
 
-  // Check for CVC4-specific info keys (prefixed with "cvc4-" or "cvc4_")
-  if(key.length() > 5) {
-    string prefix = key.substr(0, 5);
-    if(prefix == "cvc4-" || prefix == "cvc4_") {
-      string cvc4key = key.substr(5);
-      if(cvc4key == "logic") {
-        if(! value.isAtom()) {
-          throw OptionException("argument to (set-info :cvc4-logic ..) must be a string");
-        }
-        SmtScope smts(this);
-        d_logic = value.getValue();
-        setLogicInternal();
-        return;
-      } else {
-        throw UnrecognizedOptionException();
-      }
-    }
-  }
-
   // Check for standard info keys (SMT-LIB v1, SMT-LIB v2, ...)
   if (key == "source" || key == "category" || key == "difficulty"
       || key == "notes" || key == "name" || key == "license")