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
|
/******************************************************************************
* Top contributors (to current version):
* Yoni Zohar, Andrew Reynolds, Mathias Preiner
*
* This file is part of the cvc5 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.
* ****************************************************************************
*
* Utility for detecting quantifier macro definitions.
*/
#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_MACROS_H
#define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_MACROS_H
#include <map>
#include <vector>
#include "expr/node.h"
namespace cvc5 {
namespace theory {
namespace quantifiers {
class QuantifiersRegistry;
/**
* A utility for inferring macros from quantified formulas. This can be seen as
* a method for putting quantified formulas in solved form, e.g.
* forall x. P(x) ---> P = (lambda x. true)
*/
class QuantifiersMacros
{
public:
QuantifiersMacros(QuantifiersRegistry& qr);
~QuantifiersMacros() {}
/**
* Called on quantified formulas lit of the form
* forall x1 ... xn. n = ndef
* where n is of the form U(x1...xn). Returns an equality of the form
* U = lambda x1 ... xn. ndef
* if this is a legal macro definition for U, and the null node otherwise.
*
* @param lit The body of the quantified formula
* @param reqGround Whether we require the macro definition to be ground,
* i.e. does not contain quantified formulas as subterms.
* @return If a macro can be inferred, an equality of the form
* (op = lambda x1 ... xn. def)), or the null node otherwise.
*/
Node solve(Node lit, bool reqGround = false);
private:
/**
* Return true n is an APPLY_UF with pairwise unique BOUND_VARIABLE as
* children.
*/
bool isBoundVarApplyUf(Node n);
/**
* Returns true if n contains op, or if n contains a quantified formula
* as a subterm and reqGround is true.
*/
bool containsBadOp(Node n, Node op, bool reqGround);
/**
* Return true if n preserves trigger variables in quantified formula q, that
* is, triggers can be inferred containing all variables in q in term n.
*/
bool preservesTriggerVariables(Node q, Node n);
/**
* From n, get a list of possible subterms of n that could be the head of a
* macro definition.
*/
void getMacroCandidates(Node n,
std::vector<Node>& candidates,
std::map<Node, bool>& visited);
/**
* Solve n in literal lit, return n' such that n = n' is equivalent to lit
* if possible, or null otherwise.
*/
Node solveInEquality(Node n, Node lit);
/**
* Called when we have inferred a quantified formula is of the form
* forall x1 ... xn. n = ndef
* where n is of the form U(x1...xn).
*/
Node solveEq(Node n, Node ndef);
/**
* Returns the macro fdef, which originated from lit. This method is for
* debugging.
*/
Node returnMacro(Node fdef, Node lit) const;
/** Reference to the quantifiers registry */
QuantifiersRegistry& d_qreg;
};
} // namespace quantifiers
} // namespace theory
} // namespace cvc5
#endif /*CVC5__THEORY__QUANTIFIERS__QUANTIFIER_MACROS_H */
|
