Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Mathias Preiner, Haniel Barbosa
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 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.
11 : : * ****************************************************************************
12 : : *
13 : : * Implementation of utility for inferring whether a formula is in
14 : : * examples form (functions applied to concrete arguments only).
15 : : */
16 : : #include "theory/quantifiers/sygus/example_infer.h"
17 : :
18 : : #include "theory/quantifiers/quant_util.h"
19 : :
20 : : using namespace cvc5::internal;
21 : : using namespace cvc5::internal::kind;
22 : :
23 : : namespace cvc5::internal {
24 : : namespace theory {
25 : : namespace quantifiers {
26 : :
27 : 7270 : ExampleInfer::ExampleInfer(NodeManager* nm, TermDbSygus* tds)
28 : 7270 : : d_nm(nm), d_tds(tds)
29 : : {
30 : 7270 : d_isExamples = false;
31 : 7270 : }
32 : :
33 : 7163 : ExampleInfer::~ExampleInfer() {}
34 : :
35 : 1758 : bool ExampleInfer::initialize(Node n, const std::vector<Node>& candidates)
36 : : {
37 [ + - ]: 1758 : Trace("ex-infer") << "Initialize example inference : " << n << std::endl;
38 : :
39 [ + + ]: 3850 : for (const Node& v : candidates)
40 : : {
41 : 2092 : d_examples[v].clear();
42 : 2092 : d_examplesOut[v].clear();
43 : 2092 : d_examplesTerm[v].clear();
44 : : }
45 : 3516 : std::map<std::pair<bool, bool>, std::unordered_set<Node>> visited;
46 : : // n is negated conjecture
47 [ + + ]: 1758 : if (!collectExamples(n, visited, true, false))
48 : : {
49 [ + - ]: 2 : Trace("ex-infer") << "...conflicting examples" << std::endl;
50 : 2 : return false;
51 : : }
52 : :
53 [ - + ]: 1756 : if (TraceIsOn("ex-infer"))
54 : : {
55 [ - - ]: 0 : for (unsigned i = 0; i < candidates.size(); i++)
56 : : {
57 : 0 : Node v = candidates[i];
58 [ - - ]: 0 : Trace("ex-infer") << " examples for " << v << " : ";
59 [ - - ]: 0 : if (d_examples_invalid.find(v) != d_examples_invalid.end())
60 : : {
61 [ - - ]: 0 : Trace("ex-infer") << "INVALID" << std::endl;
62 : : }
63 : : else
64 : : {
65 [ - - ]: 0 : Trace("ex-infer") << std::endl;
66 [ - - ]: 0 : for (unsigned j = 0; j < d_examples[v].size(); j++)
67 : : {
68 [ - - ]: 0 : Trace("ex-infer") << " ";
69 [ - - ]: 0 : for (unsigned k = 0; k < d_examples[v][j].size(); k++)
70 : : {
71 [ - - ]: 0 : Trace("ex-infer") << d_examples[v][j][k] << " ";
72 : : }
73 [ - - ]: 0 : if (!d_examplesOut[v][j].isNull())
74 : : {
75 [ - - ]: 0 : Trace("ex-infer") << " -> " << d_examplesOut[v][j];
76 : : }
77 [ - - ]: 0 : Trace("ex-infer") << std::endl;
78 : : }
79 : : }
80 [ - - ]: 0 : Trace("ex-infer") << "Initialize " << d_examples[v].size()
81 : 0 : << " example points for " << v << "..." << std::endl;
82 : : }
83 : : }
84 : 1756 : return true;
85 : : }
86 : :
87 : 45009 : bool ExampleInfer::collectExamples(
88 : : Node n,
89 : : std::map<std::pair<bool, bool>, std::unordered_set<Node>>& visited,
90 : : bool hasPol,
91 : : bool pol)
92 : : {
93 : 45009 : std::pair<bool, bool> cacheIndex = std::pair<bool, bool>(hasPol, pol);
94 [ + + ]: 45009 : if (visited[cacheIndex].find(n) != visited[cacheIndex].end())
95 : : {
96 : : // already visited
97 : 15916 : return true;
98 : : }
99 : 29093 : visited[cacheIndex].insert(n);
100 : 58186 : Node neval;
101 : 58186 : Node n_output;
102 : 29093 : bool neval_is_evalapp = false;
103 [ + + ]: 29093 : if (n.getKind() == Kind::DT_SYGUS_EVAL)
104 : : {
105 : 2754 : neval = n;
106 [ + + ]: 2754 : if (hasPol)
107 : : {
108 : 446 : n_output = d_nm->mkConst(pol);
109 : : }
110 : 2754 : neval_is_evalapp = true;
111 : : }
112 [ + + ][ + + ]: 26339 : else if (n.getKind() == Kind::EQUAL && hasPol && pol)
[ + + ][ + + ]
113 : : {
114 [ + + ]: 1316 : for (unsigned r = 0; r < 2; r++)
115 : : {
116 [ + + ]: 1290 : if (n[r].getKind() == Kind::DT_SYGUS_EVAL)
117 : : {
118 : 690 : neval = n[r];
119 [ + + ]: 690 : if (n[1 - r].isConst())
120 : : {
121 : 668 : n_output = n[1 - r];
122 : : }
123 : 690 : neval_is_evalapp = true;
124 : 690 : break;
125 : : }
126 : : }
127 : : }
128 : : // is it an evaluation function?
129 [ + + ][ + - ]: 29093 : if (neval_is_evalapp && d_examples.find(neval[0]) != d_examples.end())
[ + + ][ + + ]
[ - - ]
130 : : {
131 [ + - ]: 6888 : Trace("ex-infer-debug")
132 : 3444 : << "Process head: " << n << " == " << n_output << std::endl;
133 : : // If n_output is null, then neval does not have a constant value
134 : : // If n_output is non-null, then neval is constrained to always be
135 : : // that value.
136 [ + + ]: 3444 : if (!n_output.isNull())
137 : : {
138 : 1114 : std::map<Node, Node>::iterator itet = d_exampleTermMap.find(neval);
139 [ + + ]: 1114 : if (itet == d_exampleTermMap.end())
140 : : {
141 : 1112 : d_exampleTermMap[neval] = n_output;
142 : : }
143 [ + - ]: 2 : else if (itet->second != n_output)
144 : : {
145 : : // We have a conflicting pair f( c ) = d1 ^ f( c ) = d2 for d1 != d2,
146 : : // the conjecture is infeasible.
147 : 2 : return false;
148 : : }
149 : : }
150 : : // get the evaluation head
151 : 3442 : Node eh = neval[0];
152 : 3442 : std::map<Node, bool>::iterator itx = d_examples_invalid.find(eh);
153 [ + + ]: 3442 : if (itx == d_examples_invalid.end())
154 : : {
155 : : // have we already processed this as an example term?
156 : 2714 : if (std::find(d_examplesTerm[eh].begin(), d_examplesTerm[eh].end(), neval)
157 [ + + ]: 5428 : == d_examplesTerm[eh].end())
158 : : {
159 : : // collect example
160 : 2686 : bool success = true;
161 : 2686 : std::vector<Node> ex;
162 [ + + ]: 4058 : for (unsigned j = 1, nchild = neval.getNumChildren(); j < nchild; j++)
163 : : {
164 [ + + ]: 2767 : if (!neval[j].isConst())
165 : : {
166 : 1395 : success = false;
167 : 1395 : break;
168 : : }
169 : 1372 : ex.push_back(neval[j]);
170 : : }
171 [ + + ]: 2686 : if (success)
172 : : {
173 : 1291 : d_examples[eh].push_back(ex);
174 : 1291 : d_examplesOut[eh].push_back(n_output);
175 : 1291 : d_examplesTerm[eh].push_back(neval);
176 [ + + ]: 1291 : if (n_output.isNull())
177 : : {
178 : 199 : d_examplesOut_invalid[eh] = true;
179 : : }
180 : : else
181 : : {
182 [ - + ][ - + ]: 1092 : Assert(n_output.isConst());
[ - - ]
183 : : // finished processing this node if it was an I/O pair
184 : 1092 : return true;
185 : : }
186 : : }
187 : : else
188 : : {
189 : 1395 : d_examples_invalid[eh] = true;
190 : 1395 : d_examplesOut_invalid[eh] = true;
191 : : }
192 : : }
193 : : }
194 : : }
195 [ + + ]: 71246 : for (unsigned i = 0, nchild = n.getNumChildren(); i < nchild; i++)
196 : : {
197 : : bool newHasPol;
198 : : bool newPol;
199 : 43251 : QuantPhaseReq::getEntailPolarity(n, i, hasPol, pol, newHasPol, newPol);
200 [ + + ]: 43251 : if (!collectExamples(n[i], visited, newHasPol, newPol))
201 : : {
202 : 4 : return false;
203 : : }
204 : : }
205 : 27995 : return true;
206 : : }
207 : :
208 : 2169 : bool ExampleInfer::hasExamples(Node f) const
209 : : {
210 : 2169 : std::map<Node, bool>::const_iterator itx = d_examples_invalid.find(f);
211 [ + + ]: 2169 : if (itx == d_examples_invalid.end())
212 : : {
213 : 1090 : return d_examples.find(f) != d_examples.end();
214 : : }
215 : 1079 : return false;
216 : : }
217 : :
218 : 1873 : unsigned ExampleInfer::getNumExamples(Node f) const
219 : : {
220 : : std::map<Node, std::vector<std::vector<Node>>>::const_iterator it =
221 : 1873 : d_examples.find(f);
222 [ + - ]: 1873 : if (it != d_examples.end())
223 : : {
224 : 1873 : return it->second.size();
225 : : }
226 : 0 : return 0;
227 : : }
228 : :
229 : 1952 : void ExampleInfer::getExample(Node f, unsigned i, std::vector<Node>& ex) const
230 : : {
231 [ - + ][ - + ]: 1952 : Assert(!f.isNull());
[ - - ]
232 : : std::map<Node, std::vector<std::vector<Node>>>::const_iterator it =
233 : 1952 : d_examples.find(f);
234 [ + - ]: 1952 : if (it != d_examples.end())
235 : : {
236 [ - + ][ - + ]: 1952 : Assert(i < it->second.size());
[ - - ]
237 : 1952 : ex.insert(ex.end(), it->second[i].begin(), it->second[i].end());
238 : : }
239 : : else
240 : : {
241 : 0 : Assert(false);
242 : : }
243 : 1952 : }
244 : :
245 : 2497 : void ExampleInfer::getExampleTerms(Node f, std::vector<Node>& exTerms) const
246 : : {
247 : : std::map<Node, std::vector<Node>>::const_iterator itt =
248 : 2497 : d_examplesTerm.find(f);
249 [ - + ]: 2497 : if (itt == d_examplesTerm.end())
250 : : {
251 : 0 : return;
252 : : }
253 : 2497 : exTerms.insert(exTerms.end(), itt->second.begin(), itt->second.end());
254 : : }
255 : :
256 : 636 : Node ExampleInfer::getExampleOut(Node f, unsigned i) const
257 : : {
258 [ - + ][ - + ]: 636 : Assert(!f.isNull());
[ - - ]
259 : 636 : std::map<Node, std::vector<Node>>::const_iterator it = d_examplesOut.find(f);
260 [ + - ]: 636 : if (it != d_examplesOut.end())
261 : : {
262 [ - + ][ - + ]: 636 : Assert(i < it->second.size());
[ - - ]
263 : 636 : return it->second[i];
264 : : }
265 : 0 : Assert(false);
266 : : return Node::null();
267 : : }
268 : :
269 : 175 : bool ExampleInfer::hasExamplesOut(Node f) const
270 : : {
271 : 175 : return d_examplesOut_invalid.find(f) == d_examplesOut_invalid.end();
272 : : }
273 : :
274 : : } // namespace quantifiers
275 : : } // namespace theory
276 : : } // namespace cvc5::internal
|
