diff options
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 70 |
1 files changed, 57 insertions, 13 deletions
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<unsigned>& 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<Node>& elements) const +{ + quantifiers::BoundedIntegers* bi = d_private->d_bint.get(); + if (bi) + { + return bi->getBoundElements(rsi, initial, q, v, elements); + } return false; } |