From 6808152d40b0b4293816c18a8ddf83df2afc39f7 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 9 Mar 2021 16:07:30 -0600 Subject: [PATCH] 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. --- src/CMakeLists.txt | 2 - src/preprocessing/passes/bv_abstraction.cpp | 8 +-- src/preprocessing/passes/miplib_trick.cpp | 1 - .../preprocessing_pass_context.cpp | 13 ----- .../preprocessing_pass_context.h | 6 --- src/smt/logic_request.cpp | 43 --------------- src/smt/logic_request.h | 52 ------------------- src/smt/set_defaults.cpp | 26 +++++++++- src/theory/arith/theory_arith_private.cpp | 1 - 9 files changed, 25 insertions(+), 127 deletions(-) delete mode 100644 src/smt/logic_request.cpp delete mode 100644 src/smt/logic_request.h 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(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& 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" -- 2.30.2