diff options
Diffstat (limited to 'src/theory/quantifiers/quantifiers_registry.h')
-rw-r--r-- | src/theory/quantifiers/quantifiers_registry.h | 50 |
1 files changed, 47 insertions, 3 deletions
diff --git a/src/theory/quantifiers/quantifiers_registry.h b/src/theory/quantifiers/quantifiers_registry.h index 59db1dfe2..b89a2c01b 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_util.h" namespace CVC4 { namespace theory { @@ -26,15 +27,29 @@ class QuantifiersModule; namespace quantifiers { +class Instantiate; + /** * The quantifiers registry, which manages basic information about which - * quantifiers modules have ownership of quantified formulas. + * quantifiers modules have ownership of quantified formulas, and manages + * the allocation of instantiation constants per quantified formula. */ -class QuantifiersRegistry +class QuantifiersRegistry : public QuantifiersUtil { + friend class Instantiate; + public: QuantifiersRegistry() {} ~QuantifiersRegistry() {} + /** + * Register quantifier, which allocates the instantiation constants for q. + */ + void registerQuantifier(Node q) override; + /** reset */ + bool reset(Theory::Effort e) override; + /** identify */ + std::string identify() const override; + //----------------------------- ownership /** get the owner of quantified formula q */ QuantifiersModule* getOwner(Node q) const; /** @@ -47,7 +62,28 @@ class QuantifiersRegistry * Return true if module q has no owner registered or if its registered owner is m. */ bool hasOwnership(Node q, QuantifiersModule* m) const; - + //----------------------------- end ownership + //----------------------------- instantiation constants + /** get the i^th instantiation constant of q */ + Node getInstantiationConstant(Node q, size_t i) const; + /** get number of instantiation constants for q */ + size_t getNumInstantiationConstants(Node q) const; + /** get the ce body q[e/x] */ + Node getInstConstantBody(Node q); + /** returns node n with bound vars of q replaced by instantiation constants of + q node n : is the future pattern node q : is the quantifier containing + which bind the variable return a pattern where the variable are replaced by + variable for instantiation. + */ + Node substituteBoundVariablesToInstConstants(Node n, Node q); + /** substitute { instantiation constants of q -> bound variables of q } in n + */ + Node substituteInstConstantsToBoundVariables(Node n, Node q); + /** substitute { variables of q -> terms } in n */ + Node substituteBoundVariables(Node n, Node q, std::vector<Node>& terms); + /** substitute { instantiation constants of q -> terms } in n */ + Node substituteInstConstants(Node n, Node q, std::vector<Node>& terms); + //----------------------------- end instantiation constants private: /** * Maps quantified formulas to the module that owns them, if any module has @@ -60,6 +96,14 @@ class QuantifiersRegistry * precendence. */ std::map<Node, int32_t> d_owner_priority; + /** map from universal quantifiers to the list of variables */ + std::map<Node, std::vector<Node> > d_vars; + /** map from universal quantifiers to their inst constant body */ + std::map<Node, Node> d_inst_const_body; + /** instantiation constants to universal quantifiers */ + std::map<Node, Node> d_inst_constants_map; + /** map from universal quantifiers to the list of instantiation constants */ + std::map<Node, std::vector<Node> > d_inst_constants; }; } // namespace quantifiers |