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) 20092021 by the authors listed in the file AUTHORS 
8 

** in the toplevel source directory and their institutional affiliations. 
9 

** All rights reserved. See the file COPYING in the toplevel source 
10 

** directory for licensing information.\endverbatim 
11 

** 
12 

** \brief The higherorder 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 higherorder 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) AppEncode, 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 HigherOrder", 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 higherorder 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 nonfunctional 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 nonnull 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 higherorder. 
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 appcompletion should be applied for any 
171 

* pair of terms in the equality engine. 
172 

*/ 
173 

unsigned checkAppCompletion(); 
174 

/** collect model info for higherorder 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 nonstandard 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 */ 