Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Andrew Reynolds, Morgan Deters, Aina Niemetz
       4                 :            :  *
       5                 :            :  * This file is part of the cvc5 project.
       6                 :            :  *
       7                 :            :  * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
       8                 :            :  * in the top-level source directory and their institutional affiliations.
       9                 :            :  * All rights reserved.  See the file COPYING in the top-level source
      10                 :            :  * directory for licensing information.
      11                 :            :  * ****************************************************************************
      12                 :            :  *
      13                 :            :  * The quantifiers registry.
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "cvc5_private.h"
      17                 :            : 
      18                 :            : #ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H
      19                 :            : #define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H
      20                 :            : 
      21                 :            : #include "expr/node.h"
      22                 :            : #include "theory/quantifiers/quant_bound_inference.h"
      23                 :            : #include "theory/quantifiers/quant_util.h"
      24                 :            : #include "theory/quantifiers/quantifiers_attributes.h"
      25                 :            : #include "theory/quantifiers/quantifiers_preprocess.h"
      26                 :            : 
      27                 :            : namespace cvc5::internal {
      28                 :            : namespace theory {
      29                 :            : namespace quantifiers {
      30                 :            : 
      31                 :            : class QuantifiersModule;
      32                 :            : class Instantiate;
      33                 :            : 
      34                 :            : /**
      35                 :            :  * The quantifiers registry, which manages basic information about which
      36                 :            :  * quantifiers modules have ownership of quantified formulas, and manages
      37                 :            :  * the allocation of instantiation constants per quantified formula.
      38                 :            :  */
      39                 :            : class QuantifiersRegistry : public QuantifiersUtil
      40                 :            : {
      41                 :            :   friend class Instantiate;
      42                 :            : 
      43                 :            :  public:
      44                 :            :   QuantifiersRegistry(Env& env);
      45                 :      48952 :   ~QuantifiersRegistry() {}
      46                 :            :   /**
      47                 :            :    * Register quantifier, which allocates the instantiation constants for q.
      48                 :            :    */
      49                 :            :   void registerQuantifier(Node q) override;
      50                 :            :   /** reset */
      51                 :            :   bool reset(Theory::Effort e) override;
      52                 :            :   /** identify */
      53                 :            :   std::string identify() const override;
      54                 :            :   //----------------------------- ownership
      55                 :            :   /** get the owner of quantified formula q */
      56                 :            :   QuantifiersModule* getOwner(Node q) const;
      57                 :            :   /**
      58                 :            :    * Set owner of quantified formula q to module m with given priority. If
      59                 :            :    * the quantified formula has previously been assigned an owner with
      60                 :            :    * lower priority, that owner is overwritten.
      61                 :            :    */
      62                 :            :   void setOwner(Node q, QuantifiersModule* m, int32_t priority = 0);
      63                 :            :   /**
      64                 :            :    * Return true if module q has no owner registered or if its registered owner is m.
      65                 :            :    */
      66                 :            :   bool hasOwnership(Node q, QuantifiersModule* m) const;
      67                 :            :   //----------------------------- end ownership
      68                 :            :   //----------------------------- instantiation constants
      69                 :            :   /** get the i^th instantiation constant of q */
      70                 :            :   Node getInstantiationConstant(Node q, size_t i) const;
      71                 :            :   /** get number of instantiation constants for q */
      72                 :            :   size_t getNumInstantiationConstants(Node q) const;
      73                 :            :   /** get the ce body q[e/x] */
      74                 :            :   Node getInstConstantBody(Node q);
      75                 :            :   /** returns node n with bound vars of q replaced by instantiation constants of
      76                 :            :      q node n : is the future pattern node q : is the quantifier containing
      77                 :            :      which bind the variable return a pattern where the variable are replaced by
      78                 :            :      variable for instantiation.
      79                 :            :    */
      80                 :            :   Node substituteBoundVariablesToInstConstants(Node n, Node q);
      81                 :            :   /** substitute { instantiation constants of q -> bound variables of q } in n
      82                 :            :    */
      83                 :            :   Node substituteInstConstantsToBoundVariables(Node n, Node q);
      84                 :            :   /** substitute { variables of q -> terms } in n */
      85                 :            :   Node substituteBoundVariables(Node n, Node q, const std::vector<Node>& terms);
      86                 :            :   /** substitute { instantiation constants of q -> terms } in n */
      87                 :            :   Node substituteInstConstants(Node n, Node q, const std::vector<Node>& terms);
      88                 :            :   //----------------------------- end instantiation constants
      89                 :            :   /** Get quantifiers attributes utility class */
      90                 :            :   QuantAttributes& getQuantAttributes();
      91                 :            :   /** Get quantifiers bound inference utility */
      92                 :            :   QuantifiersBoundInference& getQuantifiersBoundInference();
      93                 :            :   /** Get the preprocess utility */
      94                 :            :   QuantifiersPreprocess& getPreprocess();
      95                 :            :   /**
      96                 :            :    * Get quantifiers name, which returns a variable corresponding to the name of
      97                 :            :    * quantified formula q if q has a name, or otherwise returns q itself.
      98                 :            :    */
      99                 :            :   Node getNameForQuant(Node q) const;
     100                 :            :   /**
     101                 :            :    * Get name for quantified formula. Returns true if q has a name or if req
     102                 :            :    * is false. Sets name to the result of the above method.
     103                 :            :    */
     104                 :            :   bool getNameForQuant(Node q, Node& name, bool req = true) const;
     105                 :            : 
     106                 :            :  private:
     107                 :            :   /**
     108                 :            :    * Maps quantified formulas to the module that owns them, if any module has
     109                 :            :    * specifically taken ownership of it.
     110                 :            :    */
     111                 :            :   std::map<Node, QuantifiersModule*> d_owner;
     112                 :            :   /**
     113                 :            :    * The priority value associated with the ownership of quantified formulas
     114                 :            :    * in the domain of the above map, where higher values take higher
     115                 :            :    * precendence.
     116                 :            :    */
     117                 :            :   std::map<Node, int32_t> d_owner_priority;
     118                 :            :   /** map from universal quantifiers to the list of variables */
     119                 :            :   std::map<Node, std::vector<Node> > d_vars;
     120                 :            :   /** map from universal quantifiers to their inst constant body */
     121                 :            :   std::map<Node, Node> d_inst_const_body;
     122                 :            :   /** instantiation constants to universal quantifiers */
     123                 :            :   std::map<Node, Node> d_inst_constants_map;
     124                 :            :   /** map from universal quantifiers to the list of instantiation constants */
     125                 :            :   std::map<Node, std::vector<Node> > d_inst_constants;
     126                 :            :   /** The quantifiers attributes class */
     127                 :            :   QuantAttributes d_quantAttr;
     128                 :            :   /** The quantifiers bound inference class */
     129                 :            :   QuantifiersBoundInference d_quantBoundInf;
     130                 :            :   /** The quantifiers preprocessor utility */
     131                 :            :   QuantifiersPreprocess d_quantPreproc;
     132                 :            : };
     133                 :            : 
     134                 :            : }  // namespace quantifiers
     135                 :            : }  // namespace theory
     136                 :            : }  // namespace cvc5::internal
     137                 :            : 
     138                 :            : #endif /* CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H */