From f42ed22928bdc1bc68e2269ac0a738238f9e0cd7 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 3 Jun 2021 17:49:32 -0500
Subject: Simplify automatic set-logic in smt2 parser (#6678)

This simplifies the smt2 parser so that automatically setting the logic is done directly instead of being buffered as a command.

This prevents spurious errors for features that require (A) checking the logic is set and (B) fully intialize the underlying SMT engine.  `declare-pool` is an example of an smt2 command where the user will get an error (instead of a warning) when set-logic is not used due to setting the logic, after fully initing SMT engine and then executing the buffered set-logic command.

Note this should also make dump=raw-benchmark more accurate (no set-logic is included when dumping benchmarks with no set-logic command).
---
 src/parser/smt2/smt2.cpp | 21 ++++++++++++++-------
 src/parser/smt2/smt2.h   |  3 ++-
 2 files changed, 16 insertions(+), 8 deletions(-)

(limited to 'src')

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 4f5440944..5961de587 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -690,9 +690,17 @@ Command* Smt2::setLogic(std::string name, bool fromCommand)
     addSepOperators();
   }
 
-  Command* cmd =
-      new SetBenchmarkLogicCommand(sygus() ? d_logic.getLogicString() : name);
-  cmd->setMuted(!fromCommand);
+  std::string logic = sygus() ? d_logic.getLogicString() : name;
+  if (!fromCommand)
+  {
+    // If not from a command, just set the logic directly. Notice this is
+    // important since we do not want to enqueue a set-logic command and
+    // fully initialize the underlying SmtEngine in the meantime before the
+    // command has a chance to execute, which would lead to an error.
+    d_solver->setLogic(logic);
+    return nullptr;
+  }
+  Command* cmd = new SetBenchmarkLogicCommand(logic);
   return cmd;
 } /* Smt2::setLogic() */
 
@@ -725,10 +733,10 @@ void Smt2::checkThatLogicIsSet()
     }
     else
     {
-      Command* cmd = nullptr;
+      // the calls to setLogic below set the logic on the solver directly
       if (logicIsForced())
       {
-        cmd = setLogic(getForcedLogic(), false);
+        setLogic(getForcedLogic(), false);
       }
       else
       {
@@ -739,9 +747,8 @@ void Smt2::checkThatLogicIsSet()
             "performance.");
         warning("To suppress this warning in the future use (set-logic ALL).");
 
-        cmd = setLogic("ALL", false);
+        setLogic("ALL", false);
       }
-      preemptCommand(cmd);
     }
   }
 }
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 2dd4bf663..c70a60e99 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -205,7 +205,8 @@ class Smt2 : public Parser
    * @param name the name of the logic (e.g., QF_UF, AUFLIA)
    * @param fromCommand should be set to true if the request originates from a
    *                    set-logic command and false otherwise
-   * @return the command corresponding to setting the logic
+   * @return the command corresponding to setting the logic (if fromCommand
+   * is true), and nullptr otherwise.
    */
   Command* setLogic(std::string name, bool fromCommand = true);
 
-- 
cgit v1.2.3