diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-09-11 19:58:10 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-09-11 19:58:10 -0500 |
commit | d44ef0e9af9230e1949b0d3d4b03f1fcd497ad6d (patch) | |
tree | 8de50a73a0730c9f9966b8605de4cd540a075001 /src/theory/quantifiers_engine.h | |
parent | dc3cee7cf3d49ad592139042a8e15e3905e55ee9 (diff) |
Refactoring finite bounds in Quantifiers Engine (#3261)
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 */ |