From 7e9a4a35084c4e9dcb047a4593dcdf256244bf9b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 17 Mar 2021 13:43:39 -0500 Subject: [PATCH] Move utilities for inferred bounds on quantifers to own class (#6159) This also moves some methods from TermEnumeration to QuantifiersBoundInference. This is required for breaking several cyclic dependencies within quantifiers. --- src/CMakeLists.txt | 2 + src/theory/quantifiers/first_order_model.cpp | 2 +- .../quantifiers/fmf/bounded_integers.cpp | 2 +- .../quantifiers/fmf/full_model_check.cpp | 20 ++- src/theory/quantifiers/fmf/full_model_check.h | 4 +- src/theory/quantifiers/fmf/model_builder.cpp | 12 +- src/theory/quantifiers/fmf/model_builder.h | 7 +- src/theory/quantifiers/fmf/model_engine.cpp | 8 +- .../quantifiers/quant_bound_inference.cpp | 130 ++++++++++++++++++ .../quantifiers/quant_bound_inference.h | 127 +++++++++++++++++ .../quantifiers/quant_rep_bound_ext.cpp | 16 ++- src/theory/quantifiers/quant_rep_bound_ext.h | 15 +- src/theory/quantifiers/quant_split.cpp | 3 +- src/theory/quantifiers/quant_util.h | 18 --- .../quantifiers/quantifiers_registry.cpp | 14 +- src/theory/quantifiers/quantifiers_registry.h | 5 + src/theory/quantifiers/term_enumeration.cpp | 42 +----- src/theory/quantifiers/term_enumeration.h | 29 ++-- src/theory/quantifiers_engine.cpp | 78 ++--------- src/theory/quantifiers_engine.h | 31 ----- 20 files changed, 360 insertions(+), 205 deletions(-) create mode 100644 src/theory/quantifiers/quant_bound_inference.cpp create mode 100644 src/theory/quantifiers/quant_bound_inference.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index e8dd5d0aa..5ceb44615 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -735,6 +735,8 @@ libcvc4_add_sources( theory/quantifiers/lazy_trie.h theory/quantifiers/proof_checker.cpp theory/quantifiers/proof_checker.h + theory/quantifiers/quant_bound_inference.cpp + theory/quantifiers/quant_bound_inference.h theory/quantifiers/quant_conflict_find.cpp theory/quantifiers/quant_conflict_find.h theory/quantifiers/quant_relevance.cpp diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 98f440894..44c42b305 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -129,7 +129,7 @@ bool FirstOrderModel::initializeRepresentativesForType(TypeNode tn) else { // can we complete it? - if (d_qe->getTermEnumeration()->mayComplete(tn)) + if (d_qreg.getQuantifiersBoundInference().mayComplete(tn)) { Trace("fm-debug") << " do complete, since cardinality is small (" << tn.getCardinality() << ")..." << std::endl; diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index 99aca6408..0a035a691 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -416,7 +416,7 @@ void BoundedIntegers::checkOwnership(Node f) if( d_bound_type[f].find( f[0][i] )==d_bound_type[f].end() ){ TypeNode tn = f[0][i].getType(); if ((tn.isSort() && tn.isInterpretedFinite()) - || d_quantEngine->getTermEnumeration()->mayComplete(tn)) + || d_qreg.getQuantifiersBoundInference().mayComplete(tn)) { success = true; setBoundedVar( f, f[0][i], BOUND_FINITE ); diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index 46c27df3d..abcd5a794 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -18,8 +18,11 @@ #include "options/theory_options.h" #include "options/uf_options.h" #include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/fmf/bounded_integers.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quant_rep_bound_ext.h" +#include "theory/quantifiers/quantifiers_registry.h" +#include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" @@ -281,8 +284,10 @@ void Def::debugPrint(const char * tr, Node op, FullModelChecker * m) { } } -FullModelChecker::FullModelChecker(QuantifiersEngine* qe, QuantifiersState& qs) - : QModelBuilder(qe, qs) +FullModelChecker::FullModelChecker(QuantifiersEngine* qe, + QuantifiersState& qs, + QuantifiersRegistry& qr) + : QModelBuilder(qe, qs, qr) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); @@ -785,8 +790,10 @@ int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i class RepBoundFmcEntry : public QRepBoundExt { public: - RepBoundFmcEntry(QuantifiersEngine* qe, Node e, FirstOrderModelFmc* f) - : QRepBoundExt(qe), d_entry(e), d_fm(f) + RepBoundFmcEntry(QuantifiersBoundInference& qbi, + Node e, + FirstOrderModelFmc* f) + : QRepBoundExt(qbi, f), d_entry(e), d_fm(f) { } ~RepBoundFmcEntry() {} @@ -818,8 +825,9 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc* fm, Trace("fmc-exh") << "----Exhaustive instantiate based on " << c << " "; debugPrintCond("fmc-exh", c, true); Trace("fmc-exh")<< std::endl; - RepBoundFmcEntry rbfe(d_qe, c, fm); - RepSetIterator riter(d_qe->getModel()->getRepSet(), &rbfe); + QuantifiersBoundInference& qbi = d_qreg.getQuantifiersBoundInference(); + RepBoundFmcEntry rbfe(qbi, c, fm); + RepSetIterator riter(fm->getRepSet(), &rbfe); Trace("fmc-exh-debug") << "Set quantifier..." << std::endl; //initialize if (riter.setQuantifier(f)) diff --git a/src/theory/quantifiers/fmf/full_model_check.h b/src/theory/quantifiers/fmf/full_model_check.h index 6cad3fff5..b3c55ee7a 100644 --- a/src/theory/quantifiers/fmf/full_model_check.h +++ b/src/theory/quantifiers/fmf/full_model_check.h @@ -154,7 +154,9 @@ protected: Node getSomeDomainElement( FirstOrderModelFmc * fm, TypeNode tn ); public: - FullModelChecker(QuantifiersEngine* qe, QuantifiersState& qs); + FullModelChecker(QuantifiersEngine* qe, + QuantifiersState& qs, + QuantifiersRegistry& qr); void debugPrintCond(const char * tr, Node n, bool dispStar = false); void debugPrint(const char * tr, Node n, bool dispStar = false); diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp index 878b4ddd3..89e4fa29d 100644 --- a/src/theory/quantifiers/fmf/model_builder.cpp +++ b/src/theory/quantifiers/fmf/model_builder.cpp @@ -30,12 +30,15 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; -QModelBuilder::QModelBuilder(QuantifiersEngine* qe, QuantifiersState& qs) +QModelBuilder::QModelBuilder(QuantifiersEngine* qe, + QuantifiersState& qs, + QuantifiersRegistry& qr) : TheoryEngineModelBuilder(), d_qe(qe), d_addedLemmas(0), d_triedLemmas(0), - d_qstate(qs) + d_qstate(qs), + d_qreg(qr) { } @@ -94,14 +97,15 @@ void QModelBuilder::debugModel( TheoryModel* m ){ Trace("quant-check-model") << "Testing quantifier instantiations..." << std::endl; int tests = 0; int bad = 0; + QuantifiersBoundInference& qbi = d_qreg.getQuantifiersBoundInference(); for( unsigned i=0; igetNumAssertedQuantifiers(); i++ ){ Node f = fm->getAssertedQuantifier( i ); std::vector< Node > vars; for( unsigned j=0; jgetModel()->getRepSet(), &qrbe); + QRepBoundExt qrbe(qbi, fm); + RepSetIterator riter(fm->getRepSet(), &qrbe); if( riter.setQuantifier( f ) ){ while( !riter.isFinished() ){ tests++; diff --git a/src/theory/quantifiers/fmf/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h index 578554d79..534226a7c 100644 --- a/src/theory/quantifiers/fmf/model_builder.h +++ b/src/theory/quantifiers/fmf/model_builder.h @@ -27,6 +27,7 @@ namespace quantifiers { class FirstOrderModel; class QuantifiersState; +class QuantifiersRegistry; class QModelBuilder : public TheoryEngineModelBuilder { @@ -41,7 +42,9 @@ class QModelBuilder : public TheoryEngineModelBuilder unsigned d_triedLemmas; public: - QModelBuilder(QuantifiersEngine* qe, QuantifiersState& qs); + QModelBuilder(QuantifiersEngine* qe, + QuantifiersState& qs, + QuantifiersRegistry& qr); //do exhaustive instantiation // 0 : failed, but resorting to true exhaustive instantiation may work @@ -61,6 +64,8 @@ class QModelBuilder : public TheoryEngineModelBuilder protected: /** The quantifiers state object */ QuantifiersState& d_qstate; + /** Reference to the quantifiers registry */ + QuantifiersRegistry& d_qreg; }; }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp index 6cfb31c53..257926737 100644 --- a/src/theory/quantifiers/fmf/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -251,7 +251,8 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ quantifiers::QModelBuilder * mb = d_quantEngine->getModelBuilder(); unsigned prev_alem = mb->getNumAddedLemmas(); unsigned prev_tlem = mb->getNumTriedLemmas(); - int retEi = mb->doExhaustiveInstantiation( d_quantEngine->getModel(), f, effort ); + FirstOrderModel* fm = d_quantEngine->getModel(); + int retEi = mb->doExhaustiveInstantiation(fm, f, effort); if( retEi!=0 ){ if( retEi<0 ){ Trace("fmf-exh-inst") << "-> Builder determined complete instantiation was impossible." << std::endl; @@ -270,9 +271,10 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ } Trace("fmf-exh-inst-debug") << std::endl; } + QuantifiersBoundInference& qbi = d_qreg.getQuantifiersBoundInference(); //create a rep set iterator and iterate over the (relevant) domain of the quantifier - QRepBoundExt qrbe(d_quantEngine); - RepSetIterator riter(d_quantEngine->getModel()->getRepSet(), &qrbe); + QRepBoundExt qrbe(qbi, fm); + RepSetIterator riter(fm->getRepSet(), &qrbe); if( riter.setQuantifier( f ) ){ Trace("fmf-exh-inst") << "...exhaustive instantiation set, incomplete=" << riter.isIncomplete() << "..." << std::endl; if( !riter.isIncomplete() ){ diff --git a/src/theory/quantifiers/quant_bound_inference.cpp b/src/theory/quantifiers/quant_bound_inference.cpp new file mode 100644 index 000000000..45c2b5e42 --- /dev/null +++ b/src/theory/quantifiers/quant_bound_inference.cpp @@ -0,0 +1,130 @@ +/********************* */ +/*! \file quant_bound_inference.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Tim King, Morgan Deters + ** 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 Implementation of quantifiers bound inference + **/ + +#include "theory/quantifiers/quant_bound_inference.h" + +#include "theory/quantifiers/fmf/bounded_integers.h" +#include "theory/rewriter.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +QuantifiersBoundInference::QuantifiersBoundInference(unsigned cardMax, + bool isFmf) + : d_cardMax(cardMax), d_isFmf(isFmf), d_bint(nullptr) +{ +} + +void QuantifiersBoundInference::finishInit(BoundedIntegers* b) { d_bint = b; } + +bool QuantifiersBoundInference::mayComplete(TypeNode tn) +{ + std::unordered_map::iterator it = + d_may_complete.find(tn); + if (it == d_may_complete.end()) + { + // cache + bool mc = mayComplete(tn, d_cardMax); + d_may_complete[tn] = mc; + return mc; + } + return it->second; +} + +bool QuantifiersBoundInference::mayComplete(TypeNode tn, unsigned maxCard) +{ + bool mc = false; + if (tn.isClosedEnumerable() && tn.isInterpretedFinite()) + { + Cardinality c = tn.getCardinality(); + if (!c.isLargeFinite()) + { + NodeManager* nm = NodeManager::currentNM(); + Node card = nm->mkConst(Rational(c.getFiniteCardinality())); + // check if less than fixed upper bound + Node oth = nm->mkConst(Rational(maxCard)); + Node eq = nm->mkNode(LEQ, card, oth); + eq = Rewriter::rewrite(eq); + mc = eq.isConst() && eq.getConst(); + } + } + return mc; +} + +bool QuantifiersBoundInference::isFiniteBound(Node q, Node v) +{ + if (d_bint && d_bint->isBound(q, v)) + { + return true; + } + TypeNode tn = v.getType(); + if (tn.isSort() && d_isFmf) + { + return true; + } + else if (mayComplete(tn)) + { + return true; + } + return false; +} + +BoundVarType QuantifiersBoundInference::getBoundVarType(Node q, Node v) +{ + if (d_bint) + { + return d_bint->getBoundVarType(q, v); + } + return isFiniteBound(q, v) ? BOUND_FINITE : BOUND_NONE; +} + +void QuantifiersBoundInference::getBoundVarIndices( + Node q, std::vector& indices) const +{ + Assert(indices.empty()); + // we take the bounded variables first + if (d_bint) + { + d_bint->getBoundVarIndices(q, indices); + } + // then get the remaining ones + for (size_t i = 0, nvars = q[0].getNumChildren(); i < nvars; i++) + { + if (std::find(indices.begin(), indices.end(), i) == indices.end()) + { + indices.push_back(i); + } + } +} + +bool QuantifiersBoundInference::getBoundElements( + RepSetIterator* rsi, + bool initial, + Node q, + Node v, + std::vector& elements) const +{ + if (d_bint) + { + return d_bint->getBoundElements(rsi, initial, q, v, elements); + } + return false; +} + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/quant_bound_inference.h b/src/theory/quantifiers/quant_bound_inference.h new file mode 100644 index 000000000..58b4e3db9 --- /dev/null +++ b/src/theory/quantifiers/quant_bound_inference.h @@ -0,0 +1,127 @@ +/********************* */ +/*! \file quant_bound_inference.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** 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 Quantifiers bound inference + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__QUANTIFIERS__QUANT_BOUND_INFERENCE_H +#define CVC4__THEORY__QUANTIFIERS__QUANT_BOUND_INFERENCE_H + +#include +#include "expr/node.h" + +namespace CVC4 { +namespace theory { + +class RepSetIterator; + +namespace quantifiers { + +class BoundedIntegers; + +/** Types of bounds that can be inferred for quantified formulas */ +enum BoundVarType +{ + // a variable has a finite bound because it has finite cardinality + BOUND_FINITE, + // a variable has a finite bound because it is in an integer range, e.g. + // forall x. u <= x <= l => P(x) + BOUND_INT_RANGE, + // a variable has a finite bound because it is a member of a set, e.g. + // forall x. x in S => P(x) + BOUND_SET_MEMBER, + // a variable has a finite bound because only a fixed set of terms are + // relevant for it in the domain of the quantified formula, e.g. + // forall x. ( x = t1 OR ... OR x = tn ) => P(x) + BOUND_FIXED_SET, + // a bound has not been inferred for the variable + BOUND_NONE +}; + +/** + * This class is the central utility for determining if the domain of a + * quantified formula is finite, or whether its domain can be restricted to + * a finite subdomain based on one of the above types. + */ +class QuantifiersBoundInference +{ + public: + /** + * @param cardMax The maximum cardinality we consider to be small enough + * to "complete" below. + * @param isFmf Whether finite model finding (for uninterpreted sorts) is + * enabled. + */ + QuantifiersBoundInference(unsigned cardMax, bool isFmf = false); + /** finish initialize */ + void finishInit(BoundedIntegers* b); + /** may complete type + * + * Returns true if the type tn is closed enumerable, is interpreted as a + * finite type, and has cardinality less than some reasonable value + * (currently < 1000). This method caches the results of whether each type + * may be completed. + */ + bool mayComplete(TypeNode tn); + /** + * Static version of the above method where maximum cardinality is + * configurable. + */ + static bool mayComplete(TypeNode tn, unsigned cardMax); + /** does variable v of quantified formula q have a finite bound? */ + bool isFiniteBound(Node q, Node v); + /** get bound var type + * + * This returns the type of bound that was inferred for variable v of + * quantified formula q. + */ + BoundVarType getBoundVarType(Node q, Node v); + /** + * Get the indices of bound variables, in the order they should be processed + * in a RepSetIterator. + * + * For details, see BoundedIntegers::getBoundVarIndices. + */ + void getBoundVarIndices(Node q, std::vector& indices) const; + /** + * Get bound elements + * + * This gets the (finite) enumeration of the range of variable v of quantified + * formula q and adds it into the vector elements in the context of the + * iteration being performed by rsi. It returns true if it could successfully + * determine this range. + * + * For details, see BoundedIntegers::getBoundElements. + */ + bool getBoundElements(RepSetIterator* rsi, + bool initial, + Node q, + Node v, + std::vector& elements) const; + + private: + /** The maximum cardinality for which we complete */ + unsigned d_cardMax; + /** Whether finite model finding is enabled */ + bool d_isFmf; + /** may complete */ + std::unordered_map d_may_complete; + /** The bounded integers module, which may help infer bounds */ + BoundedIntegers* d_bint; +}; + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__QUANTIFIERS__QUANT_BOUND_INFERENCE_H */ diff --git a/src/theory/quantifiers/quant_rep_bound_ext.cpp b/src/theory/quantifiers/quant_rep_bound_ext.cpp index 70ac2ddfa..b26a5bfa2 100644 --- a/src/theory/quantifiers/quant_rep_bound_ext.cpp +++ b/src/theory/quantifiers/quant_rep_bound_ext.cpp @@ -14,8 +14,9 @@ #include "theory/quantifiers/quant_rep_bound_ext.h" -#include "theory/quantifiers_engine.h" #include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/quant_bound_inference.h" +#include "theory/quantifiers_engine.h" using namespace CVC4::kind; @@ -23,7 +24,10 @@ namespace CVC4 { namespace theory { namespace quantifiers { -QRepBoundExt::QRepBoundExt(QuantifiersEngine* qe) : d_qe(qe) {} +QRepBoundExt::QRepBoundExt(QuantifiersBoundInference& qbi, FirstOrderModel* m) + : d_qbi(qbi), d_model(m) +{ +} RsiEnumType QRepBoundExt::setBound(Node owner, unsigned i, @@ -32,7 +36,7 @@ RsiEnumType QRepBoundExt::setBound(Node owner, // builtin: check if it is bound by bounded integer module if (owner.getKind() == FORALL) { - BoundVarType bvt = d_qe->getBoundVarType(owner, owner[0][i]); + BoundVarType bvt = d_qbi.getBoundVarType(owner, owner[0][i]); if (bvt != BOUND_FINITE) { d_bound_int[i] = true; @@ -57,7 +61,7 @@ bool QRepBoundExt::resetIndex(RepSetIterator* rsi, return true; } Assert(owner.getKind() == FORALL); - if (!d_qe->getBoundElements(rsi, initial, owner, owner[0][i], elements)) + if (!d_qbi.getBoundElements(rsi, initial, owner, owner[0][i], elements)) { return false; } @@ -66,7 +70,7 @@ bool QRepBoundExt::resetIndex(RepSetIterator* rsi, bool QRepBoundExt::initializeRepresentativesForType(TypeNode tn) { - return d_qe->getModel()->initializeRepresentativesForType(tn); + return d_model->initializeRepresentativesForType(tn); } bool QRepBoundExt::getVariableOrder(Node owner, std::vector& varOrder) @@ -77,7 +81,7 @@ bool QRepBoundExt::getVariableOrder(Node owner, std::vector& varOrder) return false; } Trace("bound-int-rsi") << "Calculating variable order..." << std::endl; - d_qe->getBoundVarIndices(owner, varOrder); + d_qbi.getBoundVarIndices(owner, varOrder); return true; } diff --git a/src/theory/quantifiers/quant_rep_bound_ext.h b/src/theory/quantifiers/quant_rep_bound_ext.h index ed636c1b2..30dbd520b 100644 --- a/src/theory/quantifiers/quant_rep_bound_ext.h +++ b/src/theory/quantifiers/quant_rep_bound_ext.h @@ -20,17 +20,16 @@ #include #include "expr/node.h" -#include "theory/quantifiers/fmf/bounded_integers.h" #include "theory/rep_set.h" #include "theory/theory_model.h" namespace CVC4 { namespace theory { - -class QuantifiersEngine; - namespace quantifiers { +class QuantifiersBoundInference; +class FirstOrderModel; + /** Quantifiers representative bound * * This class is used for computing (finite) bounds for the domain of a @@ -40,7 +39,7 @@ namespace quantifiers { class QRepBoundExt : public RepBoundExt { public: - QRepBoundExt(QuantifiersEngine* qe); + QRepBoundExt(QuantifiersBoundInference& qbi, FirstOrderModel* m); virtual ~QRepBoundExt() {} /** set bound */ RsiEnumType setBound(Node owner, @@ -58,8 +57,10 @@ class QRepBoundExt : public RepBoundExt bool getVariableOrder(Node owner, std::vector& varOrder) override; private: - /** Quantifiers engine associated with this bound */ - QuantifiersEngine* d_qe; + /** Reference to the quantifiers bound inference */ + QuantifiersBoundInference& d_qbi; + /** Pointer to the quantifiers model */ + FirstOrderModel* d_model; /** indices that are bound integer enumeration */ std::map d_bound_int; }; diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp index 269a51625..55f3469d2 100644 --- a/src/theory/quantifiers/quant_split.cpp +++ b/src/theory/quantifiers/quant_split.cpp @@ -48,6 +48,7 @@ void QuantDSplit::checkOwnership(Node q) } bool takeOwnership = false; bool doSplit = false; + QuantifiersBoundInference& qbi = d_qreg.getQuantifiersBoundInference(); Trace("quant-dsplit-debug") << "Check split quantified formula : " << q << std::endl; for( unsigned i=0; iisFiniteBound(q, q[0][i])) + if (!qbi.isFiniteBound(q, q[0][i])) { if (dt.isInterpretedFinite(tn)) { diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 714a0f467..d536fa84d 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -77,24 +77,6 @@ public: static void getEntailPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol ); }; -/** Types of bounds that can be inferred for quantified formulas */ -enum BoundVarType -{ - // a variable has a finite bound because it has finite cardinality - BOUND_FINITE, - // a variable has a finite bound because it is in an integer range, e.g. - // forall x. u <= x <= l => P(x) - BOUND_INT_RANGE, - // a variable has a finite bound because it is a member of a set, e.g. - // forall x. x in S => P(x) - BOUND_SET_MEMBER, - // a variable has a finite bound because only a fixed set of terms are - // relevant for it in the domain of the quantified formula, e.g. - // forall x. ( x = t1 OR ... OR x = tn ) => P(x) - BOUND_FIXED_SET, - // a bound has not been inferred for the variable - BOUND_NONE -}; } } diff --git a/src/theory/quantifiers/quantifiers_registry.cpp b/src/theory/quantifiers/quantifiers_registry.cpp index 76e2b3078..daaaea0ad 100644 --- a/src/theory/quantifiers/quantifiers_registry.cpp +++ b/src/theory/quantifiers/quantifiers_registry.cpp @@ -14,6 +14,7 @@ #include "theory/quantifiers/quantifiers_registry.h" +#include "options/quantifiers_options.h" #include "theory/quantifiers/quant_module.h" #include "theory/quantifiers/term_util.h" @@ -21,7 +22,12 @@ namespace CVC4 { namespace theory { namespace quantifiers { -QuantifiersRegistry::QuantifiersRegistry() : d_quantAttr() {} +QuantifiersRegistry::QuantifiersRegistry() + : d_quantAttr(), + d_quantBoundInf(options::fmfTypeCompletionThresh(), + options::finiteModelFind()) +{ +} void QuantifiersRegistry::registerQuantifier(Node q) { @@ -177,6 +183,12 @@ QuantAttributes& QuantifiersRegistry::getQuantAttributes() { return d_quantAttr; } + +QuantifiersBoundInference& QuantifiersRegistry::getQuantifiersBoundInference() +{ + return d_quantBoundInf; +} + Node QuantifiersRegistry::getNameForQuant(Node q) const { Node name = d_quantAttr.getQuantName(q); diff --git a/src/theory/quantifiers/quantifiers_registry.h b/src/theory/quantifiers/quantifiers_registry.h index fb1643765..f2d3f085e 100644 --- a/src/theory/quantifiers/quantifiers_registry.h +++ b/src/theory/quantifiers/quantifiers_registry.h @@ -18,6 +18,7 @@ #define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H #include "expr/node.h" +#include "theory/quantifiers/quant_bound_inference.h" #include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/quantifiers_attributes.h" @@ -87,6 +88,8 @@ class QuantifiersRegistry : public QuantifiersUtil //----------------------------- end instantiation constants /** Get quantifiers attributes utility class */ QuantAttributes& getQuantAttributes(); + /** Get quantifiers bound inference utility */ + QuantifiersBoundInference& getQuantifiersBoundInference(); /** * Get quantifiers name, which returns a variable corresponding to the name of * quantified formula q if q has a name, or otherwise returns q itself. @@ -120,6 +123,8 @@ class QuantifiersRegistry : public QuantifiersUtil std::map > d_inst_constants; /** The quantifiers attributes class */ QuantAttributes d_quantAttr; + /** The quantifiers bound inference class */ + QuantifiersBoundInference d_quantBoundInf; }; } // namespace quantifiers diff --git a/src/theory/quantifiers/term_enumeration.cpp b/src/theory/quantifiers/term_enumeration.cpp index 1a066a886..0b1b1cdae 100644 --- a/src/theory/quantifiers/term_enumeration.cpp +++ b/src/theory/quantifiers/term_enumeration.cpp @@ -14,9 +14,7 @@ #include "theory/quantifiers/term_enumeration.h" -#include "options/quantifiers_options.h" -#include "theory/quantifiers/term_util.h" -#include "theory/rewriter.h" +#include "theory/quantifiers/quant_bound_inference.h" using namespace CVC4::kind; @@ -24,6 +22,8 @@ namespace CVC4 { namespace theory { namespace quantifiers { +TermEnumeration::TermEnumeration(QuantifiersBoundInference* qbi) : d_qbi(qbi) {} + Node TermEnumeration::getEnumerateTerm(TypeNode tn, unsigned index) { Trace("term-db-enum") << "Get enumerate term " << tn << " " << index @@ -53,43 +53,9 @@ Node TermEnumeration::getEnumerateTerm(TypeNode tn, unsigned index) return d_enum_terms[tn][index]; } -bool TermEnumeration::mayComplete(TypeNode tn) -{ - std::unordered_map::iterator it = - d_may_complete.find(tn); - if (it == d_may_complete.end()) - { - // cache - bool mc = mayComplete(tn, options::fmfTypeCompletionThresh()); - d_may_complete[tn] = mc; - return mc; - } - return it->second; -} - -bool TermEnumeration::mayComplete(TypeNode tn, unsigned maxCard) -{ - bool mc = false; - if (tn.isClosedEnumerable() && tn.isInterpretedFinite()) - { - Cardinality c = tn.getCardinality(); - if (!c.isLargeFinite()) - { - NodeManager* nm = NodeManager::currentNM(); - Node card = nm->mkConst(Rational(c.getFiniteCardinality())); - // check if less than fixed upper bound - Node oth = nm->mkConst(Rational(maxCard)); - Node eq = nm->mkNode(LEQ, card, oth); - eq = Rewriter::rewrite(eq); - mc = eq.isConst() && eq.getConst(); - } - } - return mc; -} - bool TermEnumeration::getDomain(TypeNode tn, std::vector& dom) { - if (!mayComplete(tn)) + if (!d_qbi || !d_qbi->mayComplete(tn)) { return false; } diff --git a/src/theory/quantifiers/term_enumeration.h b/src/theory/quantifiers/term_enumeration.h index fcad50f05..9cd57bfd0 100644 --- a/src/theory/quantifiers/term_enumeration.h +++ b/src/theory/quantifiers/term_enumeration.h @@ -28,6 +28,8 @@ namespace CVC4 { namespace theory { namespace quantifiers { +class QuantifiersBoundInference; + /** Term enumeration * * This class has utilities for enumerating terms. It stores @@ -38,33 +40,26 @@ namespace quantifiers { class TermEnumeration { public: - TermEnumeration() {} + TermEnumeration(QuantifiersBoundInference* qbi = nullptr); ~TermEnumeration() {} /** get i^th term for type tn */ Node getEnumerateTerm(TypeNode tn, unsigned i); - /** may complete type - * - * Returns true if the type tn is closed enumerable, is interpreted as a - * finite type, and has cardinality less than some reasonable value - * (currently < 1000). This method caches the results of whether each type - * may be completed. - */ - bool mayComplete(TypeNode tn); - /** - * Static version of the above method where maximum cardinality is - * configurable. - */ - static bool mayComplete(TypeNode tn, unsigned cardMax); /** get domain * - * If tn is a type such that mayComplete(tn) returns true, this method + * If tn is a type such that d_qbi.mayComplete(tn) returns true, this method * adds all domain elements of tn to dom and returns true. Otherwise, this * method returns false. */ bool getDomain(TypeNode tn, std::vector& dom); private: + /** + * Reference to quantifiers bound inference, which determines when it is + * possible to enumerate the entire domain of a type. If this is not provided, + * getDomain above always returns false. + */ + QuantifiersBoundInference* d_qbi; /** ground terms enumerated for types */ std::unordered_map, TypeNodeHashFunction> d_enum_terms; @@ -72,10 +67,6 @@ class TermEnumeration std::unordered_map d_typ_enum_map; /** type enumerators */ std::vector d_typ_enum; - /** closed enumerable type cache */ - std::unordered_map d_typ_closed_enum; - /** may complete */ - std::unordered_map d_may_complete; }; } /* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index c41fa36e6..1784b976e 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -93,13 +93,14 @@ QuantifiersEngine::QuantifiersEngine( { Trace("quant-engine-debug") << "...make fmc builder." << std::endl; d_model.reset(new quantifiers::fmcheck::FirstOrderModelFmc( - this, qstate, d_qreg, "FirstOrderModelFmc")); - d_builder.reset(new quantifiers::fmcheck::FullModelChecker(this, qstate)); + this, qstate, qr, "FirstOrderModelFmc")); + d_builder.reset( + new quantifiers::fmcheck::FullModelChecker(this, qstate, qr)); }else{ Trace("quant-engine-debug") << "...make default model builder." << std::endl; d_model.reset(new quantifiers::FirstOrderModel( - this, qstate, d_qreg, "FirstOrderModel")); - d_builder.reset(new quantifiers::QModelBuilder(this, qstate)); + this, qstate, qr, "FirstOrderModel")); + d_builder.reset(new quantifiers::QModelBuilder(this, qstate, qr)); } }else{ d_model.reset(new quantifiers::FirstOrderModel( @@ -123,6 +124,12 @@ void QuantifiersEngine::finishInit(TheoryEngine* te, DecisionManager* dm) { d_util.push_back(d_qmodules->d_rel_dom.get()); } + + // handle any circular dependencies + + // quantifiers bound inference needs to be informed of the bounded integers + // module, which has information about which quantifiers have finite bounds + d_qreg.getQuantifiersBoundInference().finishInit(d_qmodules->d_bint.get()); } DecisionManager* QuantifiersEngine::getDecisionManager() @@ -178,69 +185,6 @@ inst::TriggerTrie* QuantifiersEngine::getTriggerDatabase() const return d_tr_trie.get(); } -bool QuantifiersEngine::isFiniteBound(Node q, Node v) const -{ - quantifiers::BoundedIntegers* bi = d_qmodules->d_bint.get(); - if (bi && bi->isBound(q, v)) - { - return true; - } - TypeNode tn = v.getType(); - if (tn.isSort() && options::finiteModelFind()) - { - return true; - } - else if (d_treg.getTermEnumeration()->mayComplete(tn)) - { - return true; - } - return false; -} - -BoundVarType QuantifiersEngine::getBoundVarType(Node q, Node v) const -{ - quantifiers::BoundedIntegers* bi = d_qmodules->d_bint.get(); - if (bi) - { - return bi->getBoundVarType(q, v); - } - return isFiniteBound(q, v) ? BOUND_FINITE : BOUND_NONE; -} - -void QuantifiersEngine::getBoundVarIndices(Node q, - std::vector& indices) const -{ - Assert(indices.empty()); - // we take the bounded variables first - quantifiers::BoundedIntegers* bi = d_qmodules->d_bint.get(); - if (bi) - { - bi->getBoundVarIndices(q, indices); - } - // then get the remaining ones - for (unsigned i = 0, nvars = q[0].getNumChildren(); i < nvars; i++) - { - if (std::find(indices.begin(), indices.end(), i) == indices.end()) - { - indices.push_back(i); - } - } -} - -bool QuantifiersEngine::getBoundElements(RepSetIterator* rsi, - bool initial, - Node q, - Node v, - std::vector& elements) const -{ - quantifiers::BoundedIntegers* bi = d_qmodules->d_bint.get(); - if (bi) - { - return bi->getBoundElements(rsi, initial, q, v, elements); - } - return false; -} - void QuantifiersEngine::presolve() { Trace("quant-engine-proc") << "QuantifiersEngine : presolve " << std::endl; d_qim.clearPending(); diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index c7c716105..92b90c375 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -111,37 +111,6 @@ class QuantifiersEngine { */ void finishInit(TheoryEngine* te, DecisionManager* dm); //---------------------- end private initialization - public: - /** does variable v of quantified formula q have a finite bound? */ - bool isFiniteBound(Node q, Node v) const; - /** get bound var type - * - * This returns the type of bound that was inferred for variable v of - * quantified formula q. - */ - BoundVarType getBoundVarType(Node q, Node v) const; - /** - * Get the indices of bound variables, in the order they should be processed - * in a RepSetIterator. - * - * For details, see BoundedIntegers::getBoundVarIndices. - */ - void getBoundVarIndices(Node q, std::vector& indices) const; - /** - * Get bound elements - * - * This gets the (finite) enumeration of the range of variable v of quantified - * formula q and adds it into the vector elements in the context of the - * iteration being performed by rsi. It returns true if it could successfully - * determine this range. - * - * For details, see BoundedIntegers::getBoundElements. - */ - bool getBoundElements(RepSetIterator* rsi, - bool initial, - Node q, - Node v, - std::vector& elements) const; public: /** presolve */ -- 2.30.2