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
135
136
137
138
139
140
141
142
143
144
145
|
/********************* */
/*! \file vts_term_cache.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 Virtual term substitution term cache.
**/
#include "cvc4_private.h"
#ifndef CVC4__THEORY__QUANTIFIERS__CEGQI__VTS_TERM_CACHE_H
#define CVC4__THEORY__QUANTIFIERS__CEGQI__VTS_TERM_CACHE_H
#include <map>
#include "expr/attribute.h"
#include "expr/node.h"
namespace cvc5 {
namespace theory {
/** Attribute to mark Skolems as virtual terms */
struct VirtualTermSkolemAttributeId
{
};
typedef expr::Attribute<VirtualTermSkolemAttributeId, bool>
VirtualTermSkolemAttribute;
namespace quantifiers {
class QuantifiersInferenceManager;
/** Virtual term substitution term cache
*
* This class stores skolems corresponding to virtual terms (e.g. delta and
* infinity) and has methods for performing virtual term substitution.
*
* In detail, there are three kinds of virtual terms:
* (1) delta, of Real type, representing a infinitesimally small real value,
* (2) infinity, of Real type, representing an infinitely large real value,
* (3) infinity, of Int type, representing an infinitely large integer value.
*
* For each of the above three virtual terms, we have 2 variants.
*
* The first variant we simply call "virtual terms". These terms are intended
* to never appear in assertions and are simply used by algorithms e.g. CEGQI
* for specifying instantiations. They are eliminated by the standard rules of
* virtual term substitution, e.g.:
* t < s + delta ---> t <=s
* t <= s + delta ---> t <= s
* t < s - delta ----> t < s
* t <= s - delta -----> t < s
* t <= s + inf ----> true
* t <= s - inf ----> false
*
* The second variant we call "free virtual terms". These terms are intended
* to appear in assertions and are constrained to have the semantics of the
* above virtual terms, e.g.:
* 0 < delta_free
* forall x. x < inf_free
* We use free virtual terms for some instantiation strategies, e.g. those
* that combine instantiating quantified formulas with nested quantifiers
* with terms containing virtual terms.
*/
class VtsTermCache
{
public:
VtsTermCache(QuantifiersInferenceManager& qim);
~VtsTermCache() {}
/**
* Get vts delta. The argument isFree indicates if we are getting the
* free variant of delta. If create is false, this method returns Node::null
* if the requested delta has not already been created.
*/
Node getVtsDelta(bool isFree = false, bool create = true);
/**
* Get vts infinity of type tn, where tn should be Int or Real.
* The argument isFree indicates if we are getting the free variant of
* infinity. If create is false, this method returns Node::null if the
* requested infinity has not already been created.
*/
Node getVtsInfinity(TypeNode tn, bool isFree = false, bool create = true);
/**
* Get all vts terms and add them to vector t.
* If the argument isFree is true, we return the free variant of all virtual
* terms. If create is false, we do not add virtual terms that have not
* already been created. If inc_delta is false, we do not include delta.
*/
void getVtsTerms(std::vector<Node>& t,
bool isFree = false,
bool create = true,
bool inc_delta = true);
/**
* Rewrite virtual terms in node n. This returns the rewritten form of n
* after virtual term substitution.
*
* This method ensures that the returned node is equivalent to n and does
* not contain free occurrences of the virtual terms.
*/
Node rewriteVtsSymbols(Node n);
/**
* This method returns true iff n contains a virtual term. If isFree is true,
* if returns true iff n contains a free virtual term.
*/
bool containsVtsTerm(Node n, bool isFree = false);
/**
* This method returns true iff any term in vector n contains a virtual term.
* If isFree is true, if returns true iff any term in vector n contains a
* free virtual term.
*/
bool containsVtsTerm(std::vector<Node>& n, bool isFree = false);
/**
* This method returns true iff n contains an occurence of the virtual term
* infinity. If isFree is true, if returns true iff n contains the free
* virtual term infinity.
*/
bool containsVtsInfinity(Node n, bool isFree = false);
private:
/** Reference to the quantifiers inference manager */
QuantifiersInferenceManager& d_qim;
/** constants */
Node d_zero;
/** The virtual term substitution delta */
Node d_vts_delta;
/** The virtual term substitution "free delta" */
Node d_vts_delta_free;
/** The virtual term substitution infinities for int/real types */
std::map<TypeNode, Node> d_vts_inf;
/** The virtual term substitution "free infinities" for int/real types */
std::map<TypeNode, Node> d_vts_inf_free;
/** substitute vts terms with their corresponding vts free terms */
Node substituteVtsFreeTerms(Node n);
}; /* class TermUtil */
} // namespace quantifiers
} // namespace theory
} // namespace cvc5
#endif /* CVC4__THEORY__QUANTIFIERS__CEGQI__VTS_TERM_CACHE_H */
|
