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

Line Exec Source
1
/*********************                                                        */
2
/*! \file ho_extension.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds
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 higher-order extension of TheoryUF.
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef __CVC4__THEORY__UF__HO_EXTENSION_H
18
#define __CVC4__THEORY__UF__HO_EXTENSION_H
19
20
#include "context/cdhashmap.h"
21
#include "context/cdhashset.h"
22
#include "context/cdo.h"
23
#include "expr/node.h"
24
#include "theory/theory_inference_manager.h"
25
#include "theory/theory_model.h"
26
#include "theory/theory_state.h"
27
28
namespace CVC4 {
29
namespace theory {
30
namespace uf {
31
32
class TheoryUF;
33
34
/** The higher-order extension of the theory of uninterpreted functions
35
 *
36
 * This extension is capable of handling UF constraints involving partial
37
 * applications via the applicative encoding (kind HO_APPLY), and
38
 * (dis)equalities involving function sorts. It uses a lazy applicative
39
 * encoding and implements two axiom schemes, at a high level:
40
 *
41
 * (1) Extensionality, where disequalities between functions witnessed by
42
 * arguments where the two functions differ,
43
 *
44
 * (2) App-Encode, where full applications of UF (kind APPLY_UF) are equated
45
 * with curried applications (kind HO_APPLY).
46
 *
47
 * For more details, see "Extending SMT Solvers to Higher-Order", Barbosa et al.
48
 */
49
214
class HoExtension
50
{
51
  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
52
  typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
53
54
 public:
55
  HoExtension(TheoryState& state, TheoryInferenceManager& im);
56
57
  /** ppRewrite
58
   *
59
   * This returns the expanded form of node.
60
   *
61
   * In particular, this function will convert applications of HO_APPLY
62
   * to applications of APPLY_UF if they are fully applied, and introduce
63
   * function variables for function heads that are not variables via the
64
   * getApplyUfForHoApply method below.
65
   */
66
  Node ppRewrite(Node node);
67
68
  /** check higher order
69
   *
70
   * This is called at full effort and infers facts and sends lemmas
71
   * based on higher-order reasoning (specifically, extentionality and
72
   * app completion). It returns the number of lemmas plus facts
73
   * added to the equality engine.
74
   */
75
  unsigned check();
76
77
  /** applyExtensionality
78
   *
79
   * Given disequality deq f != g, if not already cached, this sends a lemma of
80
   * the form:
81
   *   f = g V (f k) != (g k) for fresh constant k on the output channel of the
82
   * parent TheoryUF object. This is an "extensionality lemma".
83
   * Return value is the number of lemmas of this form sent on the output
84
   * channel.
85
   */
86
  unsigned applyExtensionality(TNode deq);
87
88
  /** collect model info
89
   *
90
   * This method adds the necessary equalities to the model m such that
91
   * model construction is possible if this method returns true. These
92
   * equalities may include HO_APPLY versions of all APPLY_UF terms.
93
   *
94
   * The argument termSet is the set of relevant terms that the parent TheoryUF
95
   * object has added to m that belong to TheoryUF.
96
   *
97
   * This method ensures that the function variables in termSet
98
   * respect extensionality. If some pair does not, then this method adds an
99
   * extensionality equality directly to the equality engine of m.
100
   *
101
   * In more detail, functions f and g do not respect extensionality if f and g
102
   * are not equal in the model, and there is not a pair of unequal witness
103
   * terms f(k), g(k). In this case, we add the disequality
104
   *    f(k') != g(k')
105
   * for fresh (tuple) of variables k' to the equality engine of m. Notice
106
   * this is done only for functions whose type has infinite cardinality,
107
   * since all functions with finite cardinality are ensured to respect
108
   * extensionality by this point due to our extentionality inference schema.
109
   *
110
   * If this method returns true, then all pairs of functions that are in
111
   * distinct equivalence classes will be guaranteed to be assigned different
112
   * values in m. It returns false if any (dis)equality added to m led to
113
   * an inconsistency in m.
114
   */
115
  bool collectModelInfoHo(TheoryModel* m, const std::set<Node>& termSet);
116
117
 protected:
118
  /** get apply uf for ho apply
119
   *
120
   * This returns the APPLY_UF equivalent for the HO_APPLY term node, where
121
   * node has non-functional return type (that is, it corresponds to a fully
122
   * applied function term).
123
   * This call may introduce a skolem for the head operator and send out a lemma
124
   * specifying the definition.
125
   */
126
  Node getApplyUfForHoApply(Node node);
127
128
  /** get extensionality disequality
129
   *
130
   * Given disequality deq f != g, this returns the disequality:
131
   *   (f k) != (g k) for fresh constant(s) k.
132
   *
133
   * If isCached is true, then this returns the same k for all calls to this
134
   * method with the same deq. If it is false, it creates fresh k and does not
135
   * cache the result.
136
   */
137
  Node getExtensionalityDeq(TNode deq, bool isCached = true);
138
139
  /**
140
   * Check whether extensionality should be applied for any pair of terms in the
141
   * equality engine.
142
   *
143
   * If we pass a null model m to this function, then we add extensionality
144
   * lemmas to the output channel and return the total number of lemmas added.
145
   * We only add lemmas for functions whose type is finite, since pairs of
146
   * functions whose types are infinite can be made disequal in a model by
147
   * witnessing a point they are disequal.
148
   *
149
   * If we pass a non-null model m to this function, then we add disequalities
150
   * that correspond to the conclusion of extensionality lemmas to the model's
151
   * equality engine. We return 0 if the equality engine of m is consistent
152
   * after this call, and 1 otherwise. We only add disequalities for functions
153
   * whose type is infinite, since our decision procedure guarantees that
154
   * extensionality lemmas are added for all pairs of functions whose types are
155
   * finite.
156
   */
157
  unsigned checkExtensionality(TheoryModel* m = nullptr);
158
159
  /** applyAppCompletion
160
   * This infers a correspondence between APPLY_UF and HO_APPLY
161
   * versions of terms for higher-order.
162
   * Given APPLY_UF node e.g. (f a b c), this adds the equality to its
163
   * HO_APPLY equivalent:
164
   *   (f a b c) == (@ (@ (@ f a) b) c)
165
   * to equality engine, if not already equal.
166
   * Return value is the number of equalities added.
167
   */
168
  unsigned applyAppCompletion(TNode n);
169
170
  /** check whether app-completion should be applied for any
171
   * pair of terms in the equality engine.
172
   */
173
  unsigned checkAppCompletion();
174
  /** collect model info for higher-order term
175
   *
176
   * This adds required constraints to m for term n. In particular, if n is
177
   * an APPLY_UF term, we add its HO_APPLY equivalent in this call. We return
178
   * true if the model m is consistent after this call.
179
   */
180
  bool collectModelInfoHoTerm(Node n, TheoryModel* m);
181
182
 private:
183
  /** common constants */
184
  Node d_true;
185
  /** Reference to the state object */
186
  TheoryState& d_state;
187
  /** Reference to the inference manager */
188
  TheoryInferenceManager& d_im;
189
  /** extensionality has been applied to these disequalities */
190
  NodeSet d_extensionality;
191
192
  /** cache of getExtensionalityDeq below */
193
  std::map<Node, Node> d_extensionality_deq;
194
195
  /** map from non-standard operators to their skolems */
196
  NodeNodeMap d_uf_std_skolem;
197
}; /* class TheoryUF */
198
199
}  // namespace uf
200
}  // namespace theory
201
}  // namespace CVC4
202
203
#endif /* __CVC4__THEORY__UF__HO_EXTENSION_H */