diff options
Diffstat (limited to 'src/theory/quantifiers_engine.h')
-rw-r--r-- | src/theory/quantifiers_engine.h | 38 |
1 files changed, 32 insertions, 6 deletions
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<unsigned>& 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<Node>& elements) const; + + public: /** presolve */ void presolve(); /** notify preprocessed assertion */ |