Remove logic request (#6089)

This removes use of the logic request utility.

It generally bad practice to change the logic dynamically, e.g. during preprocessing, since it makes it so that CVC4 does not properly initialize. We now insist that logic is changed upfront in set_defaults.

This is in preparation for the smt::Env class, which will change the ownership of logic.

9 files changed, 25 insertions, 127 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index b58e204c9..9124977ef 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -228,8 +228,6 @@ libcvc4_add_sources(
   smt/listeners.cpp
   smt/listeners.h
   smt/logic_exception.h
-  smt/logic_request.cpp
-  smt/logic_request.h
   smt/interpolation_solver.cpp
   smt/interpolation_solver.h
   smt/managed_ostreams.cpp
diff --git a/src/preprocessing/passes/bv_abstraction.cpp b/src/preprocessing/passes/bv_abstraction.cpp
index e9197754b..539cc3b36 100644
--- a/src/preprocessing/passes/bv_abstraction.cpp
+++ b/src/preprocessing/passes/bv_abstraction.cpp
@@ -49,17 +49,11 @@ PreprocessingPassResult BvAbstraction::applyInternal(
                                assertionsToPreprocess->end());
   TheoryEngine* te = d_preprocContext->getTheoryEngine();
   bv::TheoryBV* bv_theory = static_cast<bv::TheoryBV*>(te->theoryOf(THEORY_BV));
-  bool changed = bv_theory->applyAbstraction(assertions, new_assertions);
+  bv_theory->applyAbstraction(assertions, new_assertions);
   for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
   {
     assertionsToPreprocess->replace(i, Rewriter::rewrite(new_assertions[i]));
   }
-  // If we are using the lazy solver and the abstraction applies, then UF
-  // symbols were introduced.
-  if (options::bitblastMode() == options::BitblastMode::LAZY && changed)
-  {
-    d_preprocContext->widenLogic(theory::THEORY_UF);
-  }
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp
index 56a4448da..f6ae77bc2 100644
--- a/src/preprocessing/passes/miplib_trick.cpp
+++ b/src/preprocessing/passes/miplib_trick.cpp
@@ -555,7 +555,6 @@ PreprocessingPassResult MipLibTrick::applyInternal(
             {
               newVars.push_back(varRef);
             }
-            d_preprocContext->enableIntegers();
           }
           Node sum;
           if (pos.getKind() == kind::AND)
diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp
index ab807c97e..8cf885c27 100644
--- a/src/preprocessing/preprocessing_pass_context.cpp
+++ b/src/preprocessing/preprocessing_pass_context.cpp
@@ -17,7 +17,6 @@
 #include "preprocessing/preprocessing_pass_context.h"
 
 #include "expr/node_algorithm.h"
-#include "smt/logic_request.h"
 
 namespace CVC4 {
 namespace preprocessing {
@@ -35,24 +34,12 @@ PreprocessingPassContext::PreprocessingPassContext(
 {
 }
 
-void PreprocessingPassContext::widenLogic(theory::TheoryId id)
-{
-  LogicRequest req(*d_smt);
-  req.widenLogic(id);
-}
-
 theory::TrustSubstitutionMap&
 PreprocessingPassContext::getTopLevelSubstitutions()
 {
   return d_topLevelSubstitutions;
 }
 
-void PreprocessingPassContext::enableIntegers()
-{
-  LogicRequest req(*d_smt);
-  req.enableIntegers();
-}
-
 void PreprocessingPassContext::recordSymbolsInAssertions(
     const std::vector<Node>& assertions)
 {
diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h
index c8c665191..d210f6b60 100644
--- a/src/preprocessing/preprocessing_pass_context.h
+++ b/src/preprocessing/preprocessing_pass_context.h
@@ -69,15 +69,9 @@ class PreprocessingPassContext
   /** Get the current logic info of the SmtEngine */
   const LogicInfo& getLogicInfo() { return d_smt->getLogicInfo(); }
 
-  /* Widen the logic to include the given theory. */
-  void widenLogic(theory::TheoryId id);
-
   /** Gets a reference to the top-level substitution map */
   theory::TrustSubstitutionMap& getTopLevelSubstitutions();
 
-  /* Enable Integers. */
-  void enableIntegers();
-
   /** Record symbols in assertions
    *
    * This method is called when a set of assertions is finalized. It adds
diff --git a/src/smt/logic_request.cpp b/src/smt/logic_request.cpp
deleted file mode 100644
index 9937990f3..000000000
--- a/src/smt/logic_request.cpp
+++ /dev/null
@@ -1,43 +0,0 @@
-/*********************                                                        */
-/*! \file logic_request.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Mathias Preiner, Martin Brain, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "smt/logic_request.h"
-#include "smt/smt_engine.h"
-
-
-namespace CVC4 {
-
-/** Widen the logic to include the given theory. */
-void LogicRequest::widenLogic(theory::TheoryId id) {
-  d_smt.d_logic.getUnlockedCopy();
-  d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
-  d_smt.d_logic.enableTheory(id);
-  d_smt.d_logic.lock();
-}
-
-/** Enable Integers if not yet enabled. */
-void LogicRequest::enableIntegers()
-{
-  if (!d_smt.d_logic.areIntegersUsed())
-  {
-    d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
-    d_smt.d_logic.enableIntegers();
-    d_smt.d_logic.lock();
-  }
-}
-
-}/* CVC4 namespace */
diff --git a/src/smt/logic_request.h b/src/smt/logic_request.h
deleted file mode 100644
index 9639cb5c6..000000000
--- a/src/smt/logic_request.h
+++ /dev/null
@@ -1,52 +0,0 @@
-/*********************                                                        */
-/*! \file logic_request.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Martin Brain, Mathias Preiner, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief An object to request logic widening in the running SmtEngine
- **
- ** An object to request logic widening in the running SmtEngine.  This
- ** class exists as a proxy between theory code and the SmtEngine, allowing
- ** a theory to enable another theory in the SmtEngine after initialization
- ** (thus the usual, public setLogic() cannot be used).  This is mainly to
- ** support features like uninterpreted divide-by-zero (to support the
- ** partial function DIVISION), where during theory expansion, the theory
- ** of uninterpreted functions needs to be added to the logic to support
- ** partial functions.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef CVC4__LOGIC_REQUEST_H
-#define CVC4__LOGIC_REQUEST_H
-
-#include "theory/theory_id.h"
-
-namespace CVC4 {
-
-class SmtEngine;
-
-class LogicRequest {
-  /** The SmtEngine at play. */
-  SmtEngine& d_smt;
-
-public:
-  LogicRequest(SmtEngine& smt) : d_smt(smt) { }
-
-  /** Widen the logic to include the given theory. */
-  void widenLogic(theory::TheoryId id);
-
-  /** Enable Integers. */
-  void enableIntegers();
-
-};/* class LogicRequest */
-
-}/* CVC4 namespace */
-
-#endif /* CVC4__LOGIC_REQUEST_H */
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 91910da47..f37b406b4 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -583,6 +583,12 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     logic = log;
     logic.lock();
   }
+  if (options::bvAbstraction())
+  {
+    // bv abstraction may require UF
+    Notice() << "Enabling UF because bvAbstraction requires it." << std::endl;
+    needsUf = true;
+  }
   if (needsUf
       // Arrays, datatypes and sets permit Boolean terms and thus require UF
       || logic.isTheoryEnabled(THEORY_ARRAYS)
@@ -604,13 +610,29 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     if (!logic.isTheoryEnabled(THEORY_UF))
     {
       LogicInfo log(logic.getUnlockedCopy());
-      Notice() << "Enabling UF because " << logic << " requires it."
-               << std::endl;
+      if (!needsUf)
+      {
+        Notice() << "Enabling UF because " << logic << " requires it."
+                 << std::endl;
+      }
       log.enableTheory(THEORY_UF);
       logic = log;
       logic.lock();
     }
   }
+  if (options::arithMLTrick())
+  {
+    if (!logic.areIntegersUsed())
+    {
+      // enable integers
+      LogicInfo log(logic.getUnlockedCopy());
+      Notice() << "Enabling integers because arithMLTrick requires it."
+               << std::endl;
+      log.enableIntegers();
+      logic = log;
+      logic.lock();
+    }
+  }
   /////////////////////////////////////////////////////////////////////////////
 
   // Set the options for the theoryOf
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 4ce077547..c096a4896 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -40,7 +40,6 @@
 #include "options/smt_options.h"  // for incrementalSolving()
 #include "preprocessing/util/ite_utilities.h"
 #include "smt/logic_exception.h"
-#include "smt/logic_request.h"
 #include "smt/smt_statistics_registry.h"
 #include "smt_util/boolean_simplification.h"
 #include "theory/arith/approx_simplex.h"