GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/quantifiers_registry.h Lines: 1 1 100.0 %
Date: 2021-03-22 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file quantifiers_registry.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Morgan Deters, Mathias Preiner
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 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.\endverbatim
11
 **
12
 ** \brief The quantifiers registry
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H
18
#define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H
19
20
#include "expr/node.h"
21
#include "theory/quantifiers/quant_bound_inference.h"
22
#include "theory/quantifiers/quant_util.h"
23
#include "theory/quantifiers/quantifiers_attributes.h"
24
25
namespace CVC4 {
26
namespace theory {
27
28
class QuantifiersModule;
29
30
namespace quantifiers {
31
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();
45
8992
  ~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, std::vector<Node>& terms);
86
  /** substitute { instantiation constants of q -> terms } in n */
87
  Node substituteInstConstants(Node n, Node q, 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
  /**
94
   * Get quantifiers name, which returns a variable corresponding to the name of
95
   * quantified formula q if q has a name, or otherwise returns q itself.
96
   */
97
  Node getNameForQuant(Node q) const;
98
  /**
99
   * Get name for quantified formula. Returns true if q has a name or if req
100
   * is false. Sets name to the result of the above method.
101
   */
102
  bool getNameForQuant(Node q, Node& name, bool req = true) const;
103
104
 private:
105
  /**
106
   * Maps quantified formulas to the module that owns them, if any module has
107
   * specifically taken ownership of it.
108
   */
109
  std::map<Node, QuantifiersModule*> d_owner;
110
  /**
111
   * The priority value associated with the ownership of quantified formulas
112
   * in the domain of the above map, where higher values take higher
113
   * precendence.
114
   */
115
  std::map<Node, int32_t> d_owner_priority;
116
  /** map from universal quantifiers to the list of variables */
117
  std::map<Node, std::vector<Node> > d_vars;
118
  /** map from universal quantifiers to their inst constant body */
119
  std::map<Node, Node> d_inst_const_body;
120
  /** instantiation constants to universal quantifiers */
121
  std::map<Node, Node> d_inst_constants_map;
122
  /** map from universal quantifiers to the list of instantiation constants */
123
  std::map<Node, std::vector<Node> > d_inst_constants;
124
  /** The quantifiers attributes class */
125
  QuantAttributes d_quantAttr;
126
  /** The quantifiers bound inference class */
127
  QuantifiersBoundInference d_quantBoundInf;
128
};
129
130
}  // namespace quantifiers
131
}  // namespace theory
132
}  // namespace CVC4
133
134
#endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H */