diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-02-17 13:34:54 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-02-17 13:34:54 -0600 |
commit | 0f03dbb1378354adcfef635a93f8b13987c2d983 (patch) | |
tree | 6c6dcc0e806b0867d19d01cb045a5a50764bf0e0 /src/theory/quantifiers/quant_module.cpp | |
parent | d107bf9b8b4dd206580681e601a033742029ec79 (diff) |
Move methods from term util to quantifiers registry (#5916)
Towards eliminating dependencies on quantifiers engine, and eliminating the TermUtil class.
Note that QuantifiersModule had to be moved to its own file to avoid circular include dependencies.
Diffstat (limited to 'src/theory/quantifiers/quant_module.cpp')
-rw-r--r-- | src/theory/quantifiers/quant_module.cpp | 92 |
1 files changed, 92 insertions, 0 deletions
diff --git a/src/theory/quantifiers/quant_module.cpp b/src/theory/quantifiers/quant_module.cpp new file mode 100644 index 000000000..1d2da7e79 --- /dev/null +++ b/src/theory/quantifiers/quant_module.cpp @@ -0,0 +1,92 @@ +/********************* */ +/*! \file quant_module.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Morgan Deters + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 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 Implementation of quantifier module + **/ + +#include "theory/quantifiers/quant_module.h" +#include "theory/quantifiers/inst_match.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" +#include "theory/quantifiers_engine.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { + +QuantifiersModule::QuantifiersModule( + quantifiers::QuantifiersState& qs, + quantifiers::QuantifiersInferenceManager& qim, + quantifiers::QuantifiersRegistry& qr, + QuantifiersEngine* qe) + : d_quantEngine(qe), d_qstate(qs), d_qim(qim), d_qreg(qr) +{ +} + +QuantifiersModule::QEffort QuantifiersModule::needsModel(Theory::Effort e) +{ + return QEFFORT_NONE; +} + +eq::EqualityEngine* QuantifiersModule::getEqualityEngine() const +{ + return d_qstate.getEqualityEngine(); +} + +bool QuantifiersModule::areEqual(TNode n1, TNode n2) const +{ + return d_qstate.areEqual(n1, n2); +} + +bool QuantifiersModule::areDisequal(TNode n1, TNode n2) const +{ + return d_qstate.areDisequal(n1, n2); +} + +TNode QuantifiersModule::getRepresentative(TNode n) const +{ + return d_qstate.getRepresentative(n); +} + +QuantifiersEngine* QuantifiersModule::getQuantifiersEngine() const +{ + return d_quantEngine; +} + +quantifiers::TermDb* QuantifiersModule::getTermDatabase() const +{ + return d_quantEngine->getTermDatabase(); +} + +quantifiers::TermUtil* QuantifiersModule::getTermUtil() const +{ + return d_quantEngine->getTermUtil(); +} + +quantifiers::QuantifiersState& QuantifiersModule::getState() +{ + return d_qstate; +} + +quantifiers::QuantifiersInferenceManager& +QuantifiersModule::getInferenceManager() +{ + return d_qim; +} + +quantifiers::QuantifiersRegistry& QuantifiersModule::getQuantifiersRegistry() +{ + return d_qreg; +} + +} // namespace theory +} /* namespace CVC4 */ |