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.
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
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;
}
{
newVars.push_back(varRef);
}
- d_preprocContext->enableIntegers();
}
Node sum;
if (pos.getKind() == kind::AND)
#include "preprocessing/preprocessing_pass_context.h"
#include "expr/node_algorithm.h"
-#include "smt/logic_request.h"
namespace CVC4 {
namespace preprocessing {
{
}
-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)
{
/** 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
+++ /dev/null
-/********************* */
-/*! \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 */
+++ /dev/null
-/********************* */
-/*! \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 */
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)
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
#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"
projects / cvc5.git / commitdiff