1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
|
/********************* */
/*! \file quantifiers_registry.h
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds, Morgan Deters, Mathias Preiner
** This file is part of the CVC4 project.
** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
** in the top-level source directory and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
** \brief The quantifiers registry
**/
#include "cvc4_private.h"
#ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H
#define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H
#include "expr/node.h"
#include "theory/quantifiers/quant_bound_inference.h"
#include "theory/quantifiers/quant_util.h"
#include "theory/quantifiers/quantifiers_attributes.h"
namespace CVC5 {
namespace theory {
class QuantifiersModule;
namespace quantifiers {
class Instantiate;
/**
* The quantifiers registry, which manages basic information about which
* quantifiers modules have ownership of quantified formulas, and manages
* the allocation of instantiation constants per quantified formula.
*/
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;
/**
* Set owner of quantified formula q to module m with given priority. If
* the quantified formula has previously been assigned an owner with
* lower priority, that owner is overwritten.
*/
void setOwner(Node q, QuantifiersModule* m, int32_t priority = 0);
/**
* 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
/** Get quantifiers attributes utility class */
QuantAttributes& getQuantAttributes();
/** Get quantifiers bound inference utility */
QuantifiersBoundInference& getQuantifiersBoundInference();
/**
* Get quantifiers name, which returns a variable corresponding to the name of
* quantified formula q if q has a name, or otherwise returns q itself.
*/
Node getNameForQuant(Node q) const;
/**
* Get name for quantified formula. Returns true if q has a name or if req
* is false. Sets name to the result of the above method.
*/
bool getNameForQuant(Node q, Node& name, bool req = true) const;
private:
/**
* Maps quantified formulas to the module that owns them, if any module has
* specifically taken ownership of it.
*/
std::map<Node, QuantifiersModule*> d_owner;
/**
* The priority value associated with the ownership of quantified formulas
* in the domain of the above map, where higher values take higher
* 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;
/** The quantifiers attributes class */
QuantAttributes d_quantAttr;
/** The quantifiers bound inference class */
QuantifiersBoundInference d_quantBoundInf;
};
} // namespace quantifiers
} // namespace theory
} // namespace CVC5
#endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H */
|
