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
|
/********************* */
/*! \file quantifiers_registry.h
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds
** 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_util.h"
#include "theory/quantifiers/quantifiers_attributes.h"
namespace CVC4 {
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 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;
};
} // namespace quantifiers
} // namespace theory
} // namespace CVC4
#endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H */
|
