1 /********************* */
2 /*! \file ho_extension.h
4 ** Top contributors (to current version):
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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
12 ** \brief The higher-order extension of TheoryUF.
15 #include "cvc4_private.h"
17 #ifndef __CVC4__THEORY__UF__HO_EXTENSION_H
18 #define __CVC4__THEORY__UF__HO_EXTENSION_H
20 #include "context/cdhashmap.h"
21 #include "context/cdhashset.h"
22 #include "context/cdo.h"
23 #include "expr/node.h"
24 #include "theory/theory_model.h"
32 /** The higher-order extension of the theory of uninterpreted functions
34 * This extension is capable of handling UF constraints involving partial
35 * applications via the applicative encoding (kind HO_APPLY), and
36 * (dis)equalities involving function sorts. It uses a lazy applicative
37 * encoding and implements two axiom schemes, at a high level:
39 * (1) Extensionality, where disequalities between functions witnessed by
40 * arguments where the two functions differ,
42 * (2) App-Encode, where full applications of UF (kind APPLY_UF) are equated
43 * with curried applications (kind HO_APPLY).
45 * For more details, see "Extending SMT Solvers to Higher-Order", Barbosa et al.
49 typedef context::CDHashSet
<Node
, NodeHashFunction
> NodeSet
;
50 typedef context::CDHashMap
<Node
, Node
, NodeHashFunction
> NodeNodeMap
;
53 HoExtension(TheoryUF
& p
, context::Context
* c
, context::UserContext
* u
);
57 * This returns the expanded form of node.
59 * In particular, this function will convert applications of HO_APPLY
60 * to applications of APPLY_UF if they are fully applied, and introduce
61 * function variables for function heads that are not variables via the
62 * getApplyUfForHoApply method below.
64 Node
expandDefinition(Node node
);
66 /** check higher order
68 * This is called at full effort and infers facts and sends lemmas
69 * based on higher-order reasoning (specifically, extentionality and
70 * app completion). It returns the number of lemmas plus facts
71 * added to the equality engine.
75 /** applyExtensionality
77 * Given disequality deq f != g, if not already cached, this sends a lemma of
79 * f = g V (f k) != (g k) for fresh constant k on the output channel of the
80 * parent TheoryUF object. This is an "extensionality lemma".
81 * Return value is the number of lemmas of this form sent on the output
84 unsigned applyExtensionality(TNode deq
);
86 /** collect model info
88 * This method adds the necessary equalities to the model m such that
89 * model construction is possible if this method returns true. These
90 * equalities may include HO_APPLY versions of all APPLY_UF terms.
92 * The argument termSet is the set of relevant terms that the parent TheoryUF
93 * object has added to m that belong to TheoryUF.
95 * This method ensures that the function variables in termSet
96 * respect extensionality. If some pair does not, then this method adds an
97 * extensionality equality directly to the equality engine of m.
99 * In more detail, functions f and g do not respect extensionality if f and g
100 * are not equal in the model, and there is not a pair of unequal witness
101 * terms f(k), g(k). In this case, we add the disequality
103 * for fresh (tuple) of variables k' to the equality engine of m. Notice
104 * this is done only for functions whose type has infinite cardinality,
105 * since all functions with finite cardinality are ensured to respect
106 * extensionality by this point due to our extentionality inference schema.
108 * If this method returns true, then all pairs of functions that are in
109 * distinct equivalence classes will be guaranteed to be assigned different
110 * values in m. It returns false if any (dis)equality added to m led to
111 * an inconsistency in m.
113 bool collectModelInfoHo(std::set
<Node
>& termSet
, TheoryModel
* m
);
116 /** get apply uf for ho apply
118 * This returns the APPLY_UF equivalent for the HO_APPLY term node, where
119 * node has non-functional return type (that is, it corresponds to a fully
120 * applied function term).
121 * This call may introduce a skolem for the head operator and send out a lemma
122 * specifying the definition.
124 Node
getApplyUfForHoApply(Node node
);
126 /** get extensionality disequality
128 * Given disequality deq f != g, this returns the disequality:
129 * (f k) != (g k) for fresh constant(s) k.
131 * If isCached is true, then this returns the same k for all calls to this
132 * method with the same deq. If it is false, it creates fresh k and does not
135 Node
getExtensionalityDeq(TNode deq
, bool isCached
= true);
138 * Check whether extensionality should be applied for any pair of terms in the
141 * If we pass a null model m to this function, then we add extensionality
142 * lemmas to the output channel and return the total number of lemmas added.
143 * We only add lemmas for functions whose type is finite, since pairs of
144 * functions whose types are infinite can be made disequal in a model by
145 * witnessing a point they are disequal.
147 * If we pass a non-null model m to this function, then we add disequalities
148 * that correspond to the conclusion of extensionality lemmas to the model's
149 * equality engine. We return 0 if the equality engine of m is consistent
150 * after this call, and 1 otherwise. We only add disequalities for functions
151 * whose type is infinite, since our decision procedure guarantees that
152 * extensionality lemmas are added for all pairs of functions whose types are
155 unsigned checkExtensionality(TheoryModel
* m
= nullptr);
157 /** applyAppCompletion
158 * This infers a correspondence between APPLY_UF and HO_APPLY
159 * versions of terms for higher-order.
160 * Given APPLY_UF node e.g. (f a b c), this adds the equality to its
161 * HO_APPLY equivalent:
162 * (f a b c) == (@ (@ (@ f a) b) c)
163 * to equality engine, if not already equal.
164 * Return value is the number of equalities added.
166 unsigned applyAppCompletion(TNode n
);
168 /** check whether app-completion should be applied for any
169 * pair of terms in the equality engine.
171 unsigned checkAppCompletion();
172 /** collect model info for higher-order term
174 * This adds required constraints to m for term n. In particular, if n is
175 * an APPLY_UF term, we add its HO_APPLY equivalent in this call. We return
176 * true if the model m is consistent after this call.
178 bool collectModelInfoHoTerm(Node n
, TheoryModel
* m
);
181 /** common constants */
183 /** the parent of this extension */
185 /** extensionality has been applied to these disequalities */
186 NodeSet d_extensionality
;
188 /** cache of getExtensionalityDeq below */
189 std::map
<Node
, Node
> d_extensionality_deq
;
191 /** map from non-standard operators to their skolems */
192 NodeNodeMap d_uf_std_skolem
;
193 }; /* class TheoryUF */
196 } // namespace theory
199 #endif /* __CVC4__THEORY__UF__HO_EXTENSION_H */