Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * Implementation of utility for inferring whether a formula is in
11 : : * examples form (functions applied to concrete arguments only).
12 : : */
13 : : #include "theory/quantifiers/sygus/example_infer.h"
14 : :
15 : : #include "theory/quantifiers/quant_util.h"
16 : :
17 : : using namespace cvc5::internal;
18 : : using namespace cvc5::internal::kind;
19 : :
20 : : namespace cvc5::internal {
21 : : namespace theory {
22 : : namespace quantifiers {
23 : :
24 : 6233 : ExampleInfer::ExampleInfer(NodeManager* nm) : d_nm(nm) { d_isExamples = false; }
25 : :
26 : 6087 : ExampleInfer::~ExampleInfer() {}
27 : :
28 : 1379 : bool ExampleInfer::initialize(Node n, const std::vector<Node>& candidates)
29 : : {
30 [ + - ]: 1379 : Trace("ex-infer") << "Initialize example inference : " << n << std::endl;
31 : :
32 [ + + ]: 3093 : for (const Node& v : candidates)
33 : : {
34 : 1714 : d_examples[v].clear();
35 : 1714 : d_examplesOut[v].clear();
36 : 1714 : d_examplesTerm[v].clear();
37 : : }
38 : 1379 : std::map<std::pair<bool, bool>, std::unordered_set<Node>> visited;
39 : : // n is negated conjecture
40 [ + + ]: 1379 : if (!collectExamples(n, visited, true, false))
41 : : {
42 [ + - ]: 2 : Trace("ex-infer") << "...conflicting examples" << std::endl;
43 : 2 : return false;
44 : : }
45 : :
46 [ - + ]: 1377 : if (TraceIsOn("ex-infer"))
47 : : {
48 [ - - ]: 0 : for (unsigned i = 0; i < candidates.size(); i++)
49 : : {
50 : 0 : Node v = candidates[i];
51 [ - - ]: 0 : Trace("ex-infer") << " examples for " << v << " : ";
52 [ - - ]: 0 : if (d_examples_invalid.find(v) != d_examples_invalid.end())
53 : : {
54 [ - - ]: 0 : Trace("ex-infer") << "INVALID" << std::endl;
55 : : }
56 : : else
57 : : {
58 [ - - ]: 0 : Trace("ex-infer") << std::endl;
59 [ - - ]: 0 : for (unsigned j = 0; j < d_examples[v].size(); j++)
60 : : {
61 [ - - ]: 0 : Trace("ex-infer") << " ";
62 [ - - ]: 0 : for (unsigned k = 0; k < d_examples[v][j].size(); k++)
63 : : {
64 [ - - ]: 0 : Trace("ex-infer") << d_examples[v][j][k] << " ";
65 : : }
66 [ - - ]: 0 : if (!d_examplesOut[v][j].isNull())
67 : : {
68 [ - - ]: 0 : Trace("ex-infer") << " -> " << d_examplesOut[v][j];
69 : : }
70 [ - - ]: 0 : Trace("ex-infer") << std::endl;
71 : : }
72 : : }
73 [ - - ]: 0 : Trace("ex-infer") << "Initialize " << d_examples[v].size()
74 : 0 : << " example points for " << v << "..." << std::endl;
75 : 0 : }
76 : : }
77 : 1377 : return true;
78 : 1379 : }
79 : :
80 : 40231 : bool ExampleInfer::collectExamples(
81 : : Node n,
82 : : std::map<std::pair<bool, bool>, std::unordered_set<Node>>& visited,
83 : : bool hasPol,
84 : : bool pol)
85 : : {
86 : 40231 : std::pair<bool, bool> cacheIndex = std::pair<bool, bool>(hasPol, pol);
87 [ + + ]: 40231 : if (visited[cacheIndex].find(n) != visited[cacheIndex].end())
88 : : {
89 : : // already visited
90 : 14270 : return true;
91 : : }
92 : 25961 : visited[cacheIndex].insert(n);
93 : 25961 : Node neval;
94 : 25961 : Node n_output;
95 : 25961 : bool neval_is_evalapp = false;
96 [ + + ]: 25961 : if (n.getKind() == Kind::DT_SYGUS_EVAL)
97 : : {
98 : 2271 : neval = n;
99 [ + + ]: 2271 : if (hasPol)
100 : : {
101 : 212 : n_output = d_nm->mkConst(pol);
102 : : }
103 : 2271 : neval_is_evalapp = true;
104 : : }
105 [ + + ][ + + ]: 23690 : else if (n.getKind() == Kind::EQUAL && hasPol && pol)
[ + + ][ + + ]
106 : : {
107 [ + + ]: 1316 : for (unsigned r = 0; r < 2; r++)
108 : : {
109 [ + + ]: 1290 : if (n[r].getKind() == Kind::DT_SYGUS_EVAL)
110 : : {
111 : 690 : neval = n[r];
112 [ + + ]: 690 : if (n[1 - r].isConst())
113 : : {
114 : 670 : n_output = n[1 - r];
115 : : }
116 : 690 : neval_is_evalapp = true;
117 : 690 : break;
118 : : }
119 : : }
120 : : }
121 : : // is it an evaluation function?
122 [ + + ][ + - ]: 25961 : if (neval_is_evalapp && d_examples.find(neval[0]) != d_examples.end())
[ + + ][ + + ]
[ - - ]
123 : : {
124 [ + - ]: 5922 : Trace("ex-infer-debug")
125 : 2961 : << "Process head: " << n << " == " << n_output << std::endl;
126 : : // If n_output is null, then neval does not have a constant value
127 : : // If n_output is non-null, then neval is constrained to always be
128 : : // that value.
129 [ + + ]: 2961 : if (!n_output.isNull())
130 : : {
131 : 882 : std::map<Node, Node>::iterator itet = d_exampleTermMap.find(neval);
132 [ + + ]: 882 : if (itet == d_exampleTermMap.end())
133 : : {
134 : 880 : d_exampleTermMap[neval] = n_output;
135 : : }
136 [ + - ]: 2 : else if (itet->second != n_output)
137 : : {
138 : : // We have a conflicting pair f( c ) = d1 ^ f( c ) = d2 for d1 != d2,
139 : : // the conjecture is infeasible.
140 : 2 : return false;
141 : : }
142 : : }
143 : : // get the evaluation head
144 : 2959 : Node eh = neval[0];
145 : 2959 : std::map<Node, bool>::iterator itx = d_examples_invalid.find(eh);
146 [ + + ]: 2959 : if (itx == d_examples_invalid.end())
147 : : {
148 : : // have we already processed this as an example term?
149 : 2334 : if (std::find(d_examplesTerm[eh].begin(), d_examplesTerm[eh].end(), neval)
150 [ + + ]: 4668 : == d_examplesTerm[eh].end())
151 : : {
152 : : // collect example
153 : 2308 : bool success = true;
154 : 2308 : std::vector<Node> ex;
155 [ + + ]: 3680 : for (unsigned j = 1, nchild = neval.getNumChildren(); j < nchild; j++)
156 : : {
157 [ + + ]: 2626 : if (!neval[j].isConst())
158 : : {
159 : 1254 : success = false;
160 : 1254 : break;
161 : : }
162 : 1372 : ex.push_back(neval[j]);
163 : : }
164 [ + + ]: 2308 : if (success)
165 : : {
166 : 1054 : d_examples[eh].push_back(ex);
167 : 1054 : d_examplesOut[eh].push_back(n_output);
168 : 1054 : d_examplesTerm[eh].push_back(neval);
169 [ + + ]: 1054 : if (n_output.isNull())
170 : : {
171 : 196 : d_examplesOut_invalid[eh] = true;
172 : : }
173 : : else
174 : : {
175 [ - + ][ - + ]: 858 : Assert(n_output.isConst());
[ - - ]
176 : : // finished processing this node if it was an I/O pair
177 : 858 : return true;
178 : : }
179 : : }
180 : : else
181 : : {
182 : 1254 : d_examples_invalid[eh] = true;
183 : 1254 : d_examplesOut_invalid[eh] = true;
184 : : }
185 [ + + ]: 2308 : }
186 : : }
187 [ + + ]: 2959 : }
188 [ + + ]: 63949 : for (unsigned i = 0, nchild = n.getNumChildren(); i < nchild; i++)
189 : : {
190 : : bool newHasPol;
191 : : bool newPol;
192 : 38852 : QuantPhaseReq::getEntailPolarity(n, i, hasPol, pol, newHasPol, newPol);
193 [ + + ]: 38852 : if (!collectExamples(n[i], visited, newHasPol, newPol))
194 : : {
195 : 4 : return false;
196 : : }
197 : : }
198 : 25097 : return true;
199 : 25961 : }
200 : :
201 : 1799 : bool ExampleInfer::hasExamples(Node f) const
202 : : {
203 : 1799 : std::map<Node, bool>::const_iterator itx = d_examples_invalid.find(f);
204 [ + + ]: 1799 : if (itx == d_examples_invalid.end())
205 : : {
206 : 862 : return d_examples.find(f) != d_examples.end();
207 : : }
208 : 937 : return false;
209 : : }
210 : :
211 : 1433 : unsigned ExampleInfer::getNumExamples(Node f) const
212 : : {
213 : : std::map<Node, std::vector<std::vector<Node>>>::const_iterator it =
214 : 1433 : d_examples.find(f);
215 [ + - ]: 1433 : if (it != d_examples.end())
216 : : {
217 : 1433 : return it->second.size();
218 : : }
219 : 0 : return 0;
220 : : }
221 : :
222 : 1717 : void ExampleInfer::getExample(Node f, unsigned i, std::vector<Node>& ex) const
223 : : {
224 [ - + ][ - + ]: 1717 : Assert(!f.isNull());
[ - - ]
225 : : std::map<Node, std::vector<std::vector<Node>>>::const_iterator it =
226 : 1717 : d_examples.find(f);
227 [ + - ]: 1717 : if (it != d_examples.end())
228 : : {
229 [ - + ][ - + ]: 1717 : Assert(i < it->second.size());
[ - - ]
230 : 1717 : ex.insert(ex.end(), it->second[i].begin(), it->second[i].end());
231 : : }
232 : : else
233 : : {
234 : 0 : DebugUnhandled();
235 : : }
236 : 1717 : }
237 : :
238 : 2497 : void ExampleInfer::getExampleTerms(Node f, std::vector<Node>& exTerms) const
239 : : {
240 : : std::map<Node, std::vector<Node>>::const_iterator itt =
241 : 2497 : d_examplesTerm.find(f);
242 [ - + ]: 2497 : if (itt == d_examplesTerm.end())
243 : : {
244 : 0 : return;
245 : : }
246 : 2497 : exTerms.insert(exTerms.end(), itt->second.begin(), itt->second.end());
247 : : }
248 : :
249 : 637 : Node ExampleInfer::getExampleOut(Node f, unsigned i) const
250 : : {
251 [ - + ][ - + ]: 637 : Assert(!f.isNull());
[ - - ]
252 : 637 : std::map<Node, std::vector<Node>>::const_iterator it = d_examplesOut.find(f);
253 [ + - ]: 637 : if (it != d_examplesOut.end())
254 : : {
255 [ - + ][ - + ]: 637 : Assert(i < it->second.size());
[ - - ]
256 : 637 : return it->second[i];
257 : : }
258 : 0 : DebugUnhandled();
259 : : return Node::null();
260 : : }
261 : :
262 : 177 : bool ExampleInfer::hasExamplesOut(Node f) const
263 : : {
264 : 177 : return d_examplesOut_invalid.find(f) == d_examplesOut_invalid.end();
265 : : }
266 : :
267 : : } // namespace quantifiers
268 : : } // namespace theory
269 : : } // namespace cvc5::internal
|
