From d44ef0e9af9230e1949b0d3d4b03f1fcd497ad6d Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 11 Sep 2019 19:58:10 -0500 Subject: [PATCH] Refactoring finite bounds in Quantifiers Engine (#3261) --- src/CMakeLists.txt | 2 + src/theory/quantifiers/first_order_model.cpp | 77 ----------------- src/theory/quantifiers/first_order_model.h | 34 -------- .../quantifiers/fmf/bounded_integers.cpp | 55 +++++++++--- src/theory/quantifiers/fmf/bounded_integers.h | 80 +++++++++++------ .../quantifiers/fmf/full_model_check.cpp | 16 ++-- src/theory/quantifiers/fmf/model_builder.cpp | 1 + src/theory/quantifiers/fmf/model_engine.cpp | 1 + .../quantifiers/quant_rep_bound_ext.cpp | 85 +++++++++++++++++++ src/theory/quantifiers/quant_rep_bound_ext.h | 71 ++++++++++++++++ src/theory/quantifiers/quant_util.h | 18 ++++ src/theory/quantifiers_engine.cpp | 70 ++++++++++++--- src/theory/quantifiers_engine.h | 38 +++++++-- src/theory/rep_set.h | 30 ++++--- 14 files changed, 394 insertions(+), 184 deletions(-) create mode 100644 src/theory/quantifiers/quant_rep_bound_ext.cpp create mode 100644 src/theory/quantifiers/quant_rep_bound_ext.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index becc0be88..d6376fb8d 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -521,6 +521,8 @@ libcvc4_add_sources( theory/quantifiers/quant_epr.h theory/quantifiers/quant_relevance.cpp theory/quantifiers/quant_relevance.h + theory/quantifiers/quant_rep_bound_ext.cpp + theory/quantifiers/quant_rep_bound_ext.h theory/quantifiers/quant_split.cpp theory/quantifiers/quant_split.h theory/quantifiers/quant_util.cpp diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index b2b4c967b..4b8b65697 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -33,83 +33,6 @@ namespace CVC4 { namespace theory { namespace quantifiers { -RepSetIterator::RsiEnumType QRepBoundExt::setBound(Node owner, - unsigned i, - std::vector& elements) -{ - // builtin: check if it is bound by bounded integer module - if (owner.getKind() == FORALL && d_qe->getBoundedIntegers()) - { - if (d_qe->getBoundedIntegers()->isBoundVar(owner, owner[0][i])) - { - unsigned bvt = - d_qe->getBoundedIntegers()->getBoundVarType(owner, owner[0][i]); - if (bvt != BoundedIntegers::BOUND_FINITE) - { - d_bound_int[i] = true; - return RepSetIterator::ENUM_BOUND_INT; - } - else - { - // indicates the variable is finitely bound due to - // the (small) cardinality of its type, - // will treat in default way - } - } - } - return RepSetIterator::ENUM_INVALID; -} - -bool QRepBoundExt::resetIndex(RepSetIterator* rsi, - Node owner, - unsigned i, - bool initial, - std::vector& elements) -{ - if (d_bound_int.find(i) != d_bound_int.end()) - { - Assert(owner.getKind() == FORALL); - Assert(d_qe->getBoundedIntegers() != nullptr); - if (!d_qe->getBoundedIntegers()->getBoundElements( - rsi, initial, owner, owner[0][i], elements)) - { - return false; - } - } - return true; -} - -bool QRepBoundExt::initializeRepresentativesForType(TypeNode tn) -{ - return d_qe->getModel()->initializeRepresentativesForType(tn); -} - -bool QRepBoundExt::getVariableOrder(Node owner, std::vector& varOrder) -{ - // must set a variable index order based on bounded integers - if (owner.getKind() == FORALL && d_qe->getBoundedIntegers()) - { - Trace("bound-int-rsi") << "Calculating variable order..." << std::endl; - for (unsigned i = 0; i < d_qe->getBoundedIntegers()->getNumBoundVars(owner); - i++) - { - Node v = d_qe->getBoundedIntegers()->getBoundVar(owner, i); - Trace("bound-int-rsi") << " bound var #" << i << " is " << v - << std::endl; - varOrder.push_back(d_qe->getTermUtil()->getVariableNum(owner, v)); - } - for (unsigned i = 0; i < owner[0].getNumChildren(); i++) - { - if (!d_qe->getBoundedIntegers()->isBoundVar(owner, owner[0][i])) - { - varOrder.push_back(i); - } - } - return true; - } - return false; -} - FirstOrderModel::FirstOrderModel(QuantifiersEngine* qe, context::Context* c, std::string name) diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index 51b40f589..a113d1b1b 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -49,40 +49,6 @@ namespace fmcheck { struct IsStarAttributeId {}; typedef expr::Attribute IsStarAttribute; -/** Quantifiers representative bound - * - * This class is used for computing (finite) - * bounds for the domain of a quantifier - * in the context of a RepSetIterator - * (see theory/rep_set.h). - */ -class QRepBoundExt : public RepBoundExt -{ - public: - QRepBoundExt(QuantifiersEngine* qe) : d_qe(qe) {} - virtual ~QRepBoundExt() {} - /** set bound */ - RepSetIterator::RsiEnumType setBound(Node owner, - unsigned i, - std::vector& elements) override; - /** reset index */ - bool resetIndex(RepSetIterator* rsi, - Node owner, - unsigned i, - bool initial, - std::vector& elements) override; - /** initialize representative set for type */ - bool initializeRepresentativesForType(TypeNode tn) override; - /** get variable order */ - bool getVariableOrder(Node owner, std::vector& varOrder) override; - - private: - /** quantifiers engine associated with this bound */ - QuantifiersEngine* d_qe; - /** indices that are bound integer enumeration */ - std::map d_bound_int; -}; - // TODO (#1301) : document and refactor this class class FirstOrderModel : public TheoryModel { diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index 879771903..87f0b1ffe 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -94,10 +94,6 @@ void BoundedIntegers::presolve() { d_bnd_it.clear(); } -bool BoundedIntegers::isBound( Node f, Node v ) { - return std::find( d_set[f].begin(), d_set[f].end(), v )!=d_set[f].end(); -} - bool BoundedIntegers::hasNonBoundVar( Node f, Node b, std::map< Node, bool >& visited ) { if( visited.find( b )==visited.end() ){ visited[b] = true; @@ -300,11 +296,13 @@ void BoundedIntegers::check(Theory::Effort e, QEffort quant_e) } Trace("bint-engine") << " addedLemma = " << addedLemma << std::endl; } -void BoundedIntegers::setBoundedVar( Node q, Node v, unsigned bound_type ) { +void BoundedIntegers::setBoundedVar(Node q, Node v, BoundVarType bound_type) +{ d_bound_type[q][v] = bound_type; d_set_nums[q][v] = d_set[q].size(); d_set[q].push_back( v ); - Trace("bound-int-var") << "Bound variable #" << d_set_nums[q][v] << " : " << v << std::endl; + Trace("bound-int-var") << "Bound variable #" << d_set_nums[q][v] << " : " << v + << std::endl; } void BoundedIntegers::checkOwnership(Node f) @@ -506,12 +504,43 @@ void BoundedIntegers::checkOwnership(Node f) } } -unsigned BoundedIntegers::getBoundVarType( Node q, Node v ) { - std::map< Node, unsigned >::iterator it = d_bound_type[q].find( v ); - if( it==d_bound_type[q].end() ){ +bool BoundedIntegers::isBound(Node q, Node v) const +{ + std::map >::const_iterator its = d_set.find(q); + if (its == d_set.end()) + { + return false; + } + return std::find(its->second.begin(), its->second.end(), v) + != its->second.end(); +} + +BoundVarType BoundedIntegers::getBoundVarType(Node q, Node v) const +{ + std::map >::const_iterator itb = + d_bound_type.find(q); + if (itb == d_bound_type.end()) + { return BOUND_NONE; - }else{ - return it->second; + } + std::map::const_iterator it = itb->second.find(v); + if (it == itb->second.end()) + { + return BOUND_NONE; + } + return it->second; +} + +void BoundedIntegers::getBoundVarIndices(Node q, + std::vector& indices) const +{ + std::map >::const_iterator it = d_set.find(q); + if (it != d_set.end()) + { + for (const Node& v : it->second) + { + indices.push_back(d_quantEngine->getTermUtil()->getVariableNum(q, v)); + } } } @@ -547,7 +576,7 @@ void BoundedIntegers::getBoundValues( Node f, Node v, RepSetIterator * rsi, Node bool BoundedIntegers::isGroundRange(Node q, Node v) { - if (isBoundVar(q, v)) + if (isBound(q, v)) { if (d_bound_type[q][v] == BOUND_INT_RANGE) { @@ -728,7 +757,7 @@ Node BoundedIntegers::matchBoundVar( Node v, Node t, Node e ){ bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node q, Node v, std::vector< Node >& elements ) { if( initial || !isGroundRange( q, v ) ){ elements.clear(); - unsigned bvt = getBoundVarType( q, v ); + BoundVarType bvt = getBoundVarType(q, v); if( bvt==BOUND_INT_RANGE ){ Node l, u; getBoundValues( q, v, rsi, l, u ); diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h index 8e6738e9e..d668c6f02 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.h +++ b/src/theory/quantifiers/fmf/bounded_integers.h @@ -30,28 +30,23 @@ class RepSetIterator; namespace quantifiers { - class BoundedIntegers : public QuantifiersModule { typedef context::CDHashMap NodeBoolMap; typedef context::CDHashMap NodeIntMap; typedef context::CDHashMap NodeNodeMap; typedef context::CDHashMap IntBoolMap; -public: - enum { - BOUND_FINITE, - BOUND_INT_RANGE, - BOUND_SET_MEMBER, - BOUND_FIXED_SET, - BOUND_NONE - }; private: //for determining bounds - bool isBound( Node f, Node v ); bool hasNonBoundVar( Node f, Node b, std::map< Node, bool >& visited ); bool hasNonBoundVar( Node f, Node b ); - //bound type - std::map< Node, std::map< Node, unsigned > > d_bound_type; + /** The bound type for each quantified formula, variable pair */ + std::map> d_bound_type; + /** + * The ordered list of variables that are finitely bound, for each quantified + * formulas. Variables that occur later in this list may depend on having + * finite bounds for variables earlier in this list. + */ std::map< Node, std::vector< Node > > d_set; std::map< Node, std::map< Node, int > > d_set_nums; std::map< Node, std::map< Node, Node > > d_range; @@ -152,9 +147,6 @@ private: } }; std::map< Node, std::map< Node, BoundInstTrie > > d_bnd_it; -private: - - void setBoundedVar( Node f, Node v, unsigned bound_type ); public: BoundedIntegers( context::Context* c, QuantifiersEngine* qe ); virtual ~BoundedIntegers(); @@ -163,11 +155,54 @@ public: bool needsCheck(Theory::Effort e) override; void check(Theory::Effort e, QEffort quant_e) override; void checkOwnership(Node q) override; - bool isBoundVar( Node q, Node v ) { return std::find( d_set[q].begin(), d_set[q].end(), v )!=d_set[q].end(); } - unsigned getBoundVarType( Node q, Node v ); - unsigned getNumBoundVars( Node q ) { return d_set[q].size(); } - Node getBoundVar( Node q, int i ) { return d_set[q][i]; } -private: + /** + * Is v a variable of quantified formula q that this class has inferred to + * have a finite bound? + */ + bool isBound(Node q, Node v) const; + /** + * Get the type of bound that was inferred for variable v of quantified + * formula q, or BOUND_NONE if no bound was inferred. + */ + BoundVarType getBoundVarType(Node q, Node v) const; + /** + * Get the indices of bound variables, in the order they should be processed + * in a RepSetIterator. For example, for q: + * forall xyz. 0 <= x < 5 ^ 0 <= z <= x+7 => P(x,y,z) + * this would add {1,3} to the vector indices, indicating that x has a finite + * bound, z has a finite bound assuming x has a finite bound, and y does not + * have a finite bound. + */ + 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. + * + * This method determines the range of a variable depending on the current + * state of the iterator rsi and flag initial (which is true when rsi is + * being initialized). For example, if q is: + * forall xy. 0 <= x < 5 ^ 0 <= y <= x+7 => P(x,y) + * v is y, and rsi currently maps x to 4, then we add the elements 0...11 to + * the vector elements. + */ + bool getBoundElements(RepSetIterator* rsi, + bool initial, + Node q, + Node v, + std::vector& elements); + /** Identify this module */ + std::string identify() const override { return "BoundedIntegers"; } + + private: + /** + * Set that variable v of quantified formula q has a finite bound, where + * bound_type indicates how that bound was inferred. + */ + void setBoundedVar(Node f, Node v, BoundVarType bound_type); //for integer range Node getLowerBound( Node q, Node v ){ return d_bounds[0][q][v]; } Node getUpperBound( Node q, Node v ){ return d_bounds[1][q][v]; } @@ -180,11 +215,6 @@ private: Node matchBoundVar( Node v, Node t, Node e ); bool getRsiSubsitution( Node q, Node v, std::vector< Node >& vars, std::vector< Node >& subs, RepSetIterator * rsi ); -public: - bool getBoundElements( RepSetIterator * rsi, bool initial, Node q, Node v, std::vector< Node >& elements ); - - /** Identify this module */ - std::string identify() const override { return "BoundedIntegers"; } }; } diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index 0f06cef74..2306a0565 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -19,6 +19,7 @@ #include "options/uf_options.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/instantiate.h" +#include "theory/quantifiers/quant_rep_bound_ext.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" @@ -746,14 +747,15 @@ class RepBoundFmcEntry : public QRepBoundExt } ~RepBoundFmcEntry() {} /** set bound */ - virtual RepSetIterator::RsiEnumType setBound( - Node owner, unsigned i, std::vector& elements) override + virtual RsiEnumType setBound(Node owner, + unsigned i, + std::vector& elements) override { if (!d_fm->isStar(d_entry[i])) { // only need to consider the single point elements.push_back(d_entry[i]); - return RepSetIterator::ENUM_DEFAULT; + return ENUM_DEFAULT; } return QRepBoundExt::setBound(owner, i, elements); } @@ -820,8 +822,12 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No int index = riter.increment(); Trace("fmc-exh-debug") << "Incremented index " << index << std::endl; if( !riter.isFinished() ){ - if (index>=0 && riter.d_index[index]>0 && addedLemmas>0 && riter.d_enum_type[index]==RepSetIterator::ENUM_BOUND_INT ) { - Trace("fmc-exh-debug") << "Since this is a range enumeration, skip to the next..." << std::endl; + if (index >= 0 && riter.d_index[index] > 0 && addedLemmas > 0 + && riter.d_enum_type[index] == ENUM_CUSTOM) + { + Trace("fmc-exh-debug") + << "Since this is a custom enumeration, skip to the next..." + << std::endl; riter.incrementAtIndex(index - 1); } } diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp index cdbc5e391..63f004448 100644 --- a/src/theory/quantifiers/fmf/model_builder.cpp +++ b/src/theory/quantifiers/fmf/model_builder.cpp @@ -19,6 +19,7 @@ #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/fmf/model_engine.h" #include "theory/quantifiers/instantiate.h" +#include "theory/quantifiers/quant_rep_bound_ext.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp index f34dc1b85..35d1f82fd 100644 --- a/src/theory/quantifiers/fmf/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -18,6 +18,7 @@ #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/fmf/full_model_check.h" #include "theory/quantifiers/instantiate.h" +#include "theory/quantifiers/quant_rep_bound_ext.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" diff --git a/src/theory/quantifiers/quant_rep_bound_ext.cpp b/src/theory/quantifiers/quant_rep_bound_ext.cpp new file mode 100644 index 000000000..8b3aaf589 --- /dev/null +++ b/src/theory/quantifiers/quant_rep_bound_ext.cpp @@ -0,0 +1,85 @@ +/********************* */ +/*! \file quant_rep_bound_ext.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 representative bound utility + **/ + +#include "theory/quantifiers/quant_rep_bound_ext.h" + +#include "theory/quantifiers_engine.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +QRepBoundExt::QRepBoundExt(QuantifiersEngine* qe) : d_qe(qe) {} + +RsiEnumType QRepBoundExt::setBound(Node owner, + unsigned i, + std::vector& elements) +{ + // builtin: check if it is bound by bounded integer module + if (owner.getKind() == FORALL) + { + BoundVarType bvt = d_qe->getBoundVarType(owner, owner[0][i]); + if (bvt != BOUND_FINITE) + { + d_bound_int[i] = true; + return ENUM_CUSTOM; + } + // indicates the variable is finitely bound due to + // the (small) cardinality of its type, + // will treat in default way + } + return ENUM_INVALID; +} + +bool QRepBoundExt::resetIndex(RepSetIterator* rsi, + Node owner, + unsigned i, + bool initial, + std::vector& elements) +{ + if (d_bound_int.find(i) == d_bound_int.end()) + { + // not bound + return true; + } + Assert(owner.getKind() == FORALL); + if (!d_qe->getBoundElements(rsi, initial, owner, owner[0][i], elements)) + { + return false; + } + return true; +} + +bool QRepBoundExt::initializeRepresentativesForType(TypeNode tn) +{ + return d_qe->getModel()->initializeRepresentativesForType(tn); +} + +bool QRepBoundExt::getVariableOrder(Node owner, std::vector& varOrder) +{ + // must set a variable index order based on bounded integers + if (owner.getKind() != FORALL) + { + return false; + } + Trace("bound-int-rsi") << "Calculating variable order..." << std::endl; + d_qe->getBoundVarIndices(owner, varOrder); + return true; +} + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/quant_rep_bound_ext.h b/src/theory/quantifiers/quant_rep_bound_ext.h new file mode 100644 index 000000000..1e54786a3 --- /dev/null +++ b/src/theory/quantifiers/quant_rep_bound_ext.h @@ -0,0 +1,71 @@ +/********************* */ +/*! \file quant_rep_bound_ext.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 representative bound utility + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__QUANTIFIERS__QUANT_REP_BOUND_EXT_H +#define CVC4__THEORY__QUANTIFIERS__QUANT_REP_BOUND_EXT_H + +#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 { + +/** Quantifiers representative bound + * + * This class is used for computing (finite) bounds for the domain of a + * quantifier in the context of a RepSetIterator (see theory/rep_set.h) + * based on modules from the quantifiers engine. + */ +class QRepBoundExt : public RepBoundExt +{ + public: + QRepBoundExt(QuantifiersEngine* qe); + virtual ~QRepBoundExt() {} + /** set bound */ + RsiEnumType setBound(Node owner, + unsigned i, + std::vector& elements) override; + /** reset index */ + bool resetIndex(RepSetIterator* rsi, + Node owner, + unsigned i, + bool initial, + std::vector& elements) override; + /** initialize representative set for type */ + bool initializeRepresentativesForType(TypeNode tn) override; + /** get variable order */ + bool getVariableOrder(Node owner, std::vector& varOrder) override; + + private: + /** Quantifiers engine associated with this bound */ + QuantifiersEngine* d_qe; + /** indices that are bound integer enumeration */ + std::map d_bound_int; +}; + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__FIRST_ORDER_MODEL_H */ diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 43861d6e9..640a62780 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -234,6 +234,24 @@ public: virtual TNode getCongruentTerm( Node f, std::vector< TNode >& args ) = 0; };/* class EqualityQuery */ +/** 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_engine.cpp b/src/theory/quantifiers_engine.cpp index def1f969c..a03596060 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -21,6 +21,7 @@ #include "theory/quantifiers/anti_skolem.h" #include "theory/quantifiers/conjecture_generator.h" #include "theory/quantifiers/ematching/instantiation_engine.h" +#include "theory/quantifiers/fmf/bounded_integers.h" #include "theory/quantifiers/fmf/full_model_check.h" #include "theory/quantifiers/fmf/model_engine.h" #include "theory/quantifiers/inst_propagator.h" @@ -384,10 +385,6 @@ inst::TriggerTrie* QuantifiersEngine::getTriggerDatabase() const return d_tr_trie.get(); } -quantifiers::BoundedIntegers* QuantifiersEngine::getBoundedIntegers() const -{ - return d_private->d_bint.get(); -} quantifiers::SynthEngine* QuantifiersEngine::getSynthEngine() const { return d_private->d_synth_e.get(); @@ -445,19 +442,66 @@ bool QuantifiersEngine::hasOwnership( Node q, QuantifiersModule * m ) { return mo==m || mo==NULL; } -bool QuantifiersEngine::isFiniteBound( Node q, Node v ) { - if( getBoundedIntegers() && getBoundedIntegers()->isBoundVar( q, v ) ){ +bool QuantifiersEngine::isFiniteBound(Node q, Node v) const +{ + quantifiers::BoundedIntegers* bi = d_private->d_bint.get(); + if (bi && bi->isBound(q, v)) + { return true; - }else{ - TypeNode tn = v.getType(); - if( tn.isSort() && options::finiteModelFind() ){ - return true; - } - else if (d_term_enum->mayComplete(tn)) + } + TypeNode tn = v.getType(); + if (tn.isSort() && options::finiteModelFind()) + { + return true; + } + else if (d_term_enum->mayComplete(tn)) + { + return true; + } + return false; +} + +BoundVarType QuantifiersEngine::getBoundVarType(Node q, Node v) const +{ + quantifiers::BoundedIntegers* bi = d_private->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_private->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()) { - return true; + indices.push_back(i); } } +} + +bool QuantifiersEngine::getBoundElements(RepSetIterator* rsi, + bool initial, + Node q, + Node v, + std::vector& elements) const +{ + quantifiers::BoundedIntegers* bi = d_private->d_bint.get(); + if (bi) + { + return bi->getBoundElements(rsi, initial, q, v, elements); + } return false; } diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 458ba07bc..36b58fd60 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -28,7 +28,6 @@ #include "theory/quantifiers/equality_infer.h" #include "theory/quantifiers/equality_query.h" #include "theory/quantifiers/first_order_model.h" -#include "theory/quantifiers/fmf/bounded_integers.h" #include "theory/quantifiers/fmf/model_builder.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quant_epr.h" @@ -114,8 +113,6 @@ public: quantifiers::RelevantDomain* getRelevantDomain() const; //---------------------- end utilities //---------------------- modules (TODO remove these #1163) - /** get bounded integers utility */ - quantifiers::BoundedIntegers* getBoundedIntegers() const; /** ceg instantiation */ quantifiers::SynthEngine* getSynthEngine() const; //---------------------- end modules @@ -144,9 +141,38 @@ public: void setOwner(Node q, quantifiers::QAttributes& qa); /** considers */ bool hasOwnership( Node q, QuantifiersModule * m = NULL ); - /** is finite bound */ - bool isFiniteBound( Node q, Node v ); -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 */ void presolve(); /** notify preprocessed assertion */ diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h index d972a7a84..2ae5e1c4b 100644 --- a/src/theory/rep_set.h +++ b/src/theory/rep_set.h @@ -121,6 +121,22 @@ typedef std::vector< int > RepDomain; class RepBoundExt; +/** + * Representative set iterator enumeration type, which indicates how the + * bound on a variable was determined. + */ +enum RsiEnumType +{ + // the bound on the variable is invalid + ENUM_INVALID = 0, + // the bound on the variable was determined in the default way, i.e. based + // on an enumeration of terms in the model. + ENUM_DEFAULT, + // The bound on the variable was determined in a custom way, i.e. via a + // quantifiers module like the BoundedIntegers module. + ENUM_CUSTOM, +}; + /** Rep set iterator. * * This class is used for iterating over (tuples of) terms @@ -139,14 +155,6 @@ class RepBoundExt; * TODO (#1199): this class needs further documentation. */ class RepSetIterator { -public: - enum RsiEnumType - { - ENUM_INVALID = 0, - ENUM_DEFAULT, - ENUM_BOUND_INT, - }; - public: RepSetIterator(const RepSet* rs, RepBoundExt* rext = nullptr); ~RepSetIterator() {} @@ -264,9 +272,9 @@ class RepBoundExt * iterating over domain elements of the type * of its i^th bound variable. */ - virtual RepSetIterator::RsiEnumType setBound(Node owner, - unsigned i, - std::vector& elements) = 0; + virtual RsiEnumType setBound(Node owner, + unsigned i, + std::vector& elements) = 0; /** reset index * * This method initializes iteration for the i^th -- 2.30.2