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 : : * Learner for literals asserted at level zero.
11 : : */
12 : : #include "prop/zero_level_learner.h"
13 : :
14 : : #include "context/context.h"
15 : : #include "expr/node_algorithm.h"
16 : : #include "expr/skolem_manager.h"
17 : : #include "options/base_options.h"
18 : : #include "options/prop_options.h"
19 : : #include "options/smt_options.h"
20 : : #include "smt/env.h"
21 : : #include "theory/theory_engine.h"
22 : : #include "theory/trust_substitutions.h"
23 : :
24 : : namespace cvc5::internal {
25 : : namespace prop {
26 : :
27 : 33 : ZeroLevelLearner::ZeroLevelLearner(Env& env, TheoryEngine* theoryEngine)
28 : : : EnvObj(env),
29 : 33 : d_theoryEngine(theoryEngine),
30 : 33 : d_levelZeroAsserts(userContext()),
31 : 33 : d_ldb(userContext()),
32 : 33 : d_nonZeroAssert(context(), false),
33 : 33 : d_ppnAtoms(userContext()),
34 : 33 : d_ppnTerms(userContext()),
35 : 33 : d_ppnSyms(userContext()),
36 : 33 : d_assertNoLearnCount(0),
37 : 66 : d_tsmap(env, userContext(), "ZllSimplificationMap")
38 : : {
39 : : // get the learned types
40 : 33 : options::DeepRestartMode lmode = options().smt.deepRestartMode;
41 [ + + ]: 33 : if (lmode != options::DeepRestartMode::NONE)
42 : : {
43 : 15 : d_learnedTypes.insert(modes::LearnedLitType::INPUT);
44 [ - + ]: 15 : if (lmode == options::DeepRestartMode::ALL)
45 : : {
46 : 0 : d_learnedTypes.insert(modes::LearnedLitType::INTERNAL);
47 : 0 : d_learnedTypes.insert(modes::LearnedLitType::SOLVABLE);
48 : 0 : d_learnedTypes.insert(modes::LearnedLitType::CONSTANT_PROP);
49 : : }
50 [ - + ]: 15 : else if (lmode == options::DeepRestartMode::INPUT_AND_SOLVABLE)
51 : : {
52 : 0 : d_learnedTypes.insert(modes::LearnedLitType::SOLVABLE);
53 : : }
54 [ + + ]: 15 : else if (lmode == options::DeepRestartMode::INPUT_AND_PROP)
55 : : {
56 : 2 : d_learnedTypes.insert(modes::LearnedLitType::SOLVABLE);
57 : 2 : d_learnedTypes.insert(modes::LearnedLitType::CONSTANT_PROP);
58 : : }
59 : : }
60 : 33 : d_trackSimplifications = true;
61 : 33 : }
62 : :
63 : 66 : ZeroLevelLearner::~ZeroLevelLearner() {}
64 : :
65 : 131 : void ZeroLevelLearner::getAtoms(TNode a,
66 : : std::unordered_set<TNode>& visited,
67 : : std::unordered_set<Node>& atoms)
68 : : {
69 : 131 : std::vector<TNode> visit;
70 : 131 : TNode cur;
71 : 131 : visit.push_back(a);
72 : : do
73 : : {
74 : 289 : cur = visit.back();
75 : 289 : visit.pop_back();
76 [ + + ]: 289 : if (visited.find(cur) == visited.end())
77 : : {
78 : 187 : visited.insert(cur);
79 [ + + ]: 187 : if (expr::isBooleanConnective(cur))
80 : : {
81 : 82 : visit.insert(visit.end(), cur.begin(), cur.end());
82 : 82 : continue;
83 : : }
84 : 105 : atoms.insert(cur);
85 : : }
86 [ + + ]: 289 : } while (!visit.empty());
87 : 131 : }
88 : :
89 : 6 : void ZeroLevelLearner::notifyTopLevelSubstitution(const Node& lhs,
90 : : const Node& rhs)
91 : : {
92 : : // process as a preprocess solved learned literal.
93 : 6 : Node eq = lhs.eqNode(rhs);
94 : 6 : processLearnedLiteral(eq, modes::LearnedLitType::PREPROCESS_SOLVED);
95 : 6 : }
96 : :
97 : 32 : void ZeroLevelLearner::notifyInputFormulas(const std::vector<Node>& assertions)
98 : : {
99 : 32 : std::unordered_set<TNode> visited;
100 : 32 : std::unordered_set<TNode> visitedWithinAtom;
101 : 32 : std::unordered_set<Node> inputSymbols;
102 : : // We consider top level literals of assertions, including those occurring
103 : : // as children of AND to be the preprocessed learned literals only, and not
104 : : // the literals tracked by the preprocessor
105 : : // (Preprocessor::getLearnedLiterals). This means that a learned literal from
106 : : // e.g. circuit propagation that is not trivially a top level assertion will
107 : : // be considered an ordinary learned literal.
108 : : // Note that d_pplAtoms and d_ppnAtoms are disjoint
109 : 32 : std::vector<Node> toProcess = assertions;
110 : 32 : size_t index = 0;
111 [ + + ]: 163 : while (index < toProcess.size())
112 : : {
113 : 131 : TNode lit = toProcess[index];
114 : 131 : index++;
115 [ - + ]: 131 : if (lit.getKind() == Kind::AND)
116 : : {
117 : 0 : toProcess.insert(toProcess.end(), lit.begin(), lit.end());
118 : 0 : continue;
119 : : }
120 [ + + ]: 131 : TNode atom = lit.getKind() == Kind::NOT ? lit[0] : lit;
121 [ + + ]: 131 : if (expr::isBooleanConnective(atom))
122 : : {
123 : 46 : continue;
124 : : }
125 : : // we mark that we visited this
126 : 85 : visited.insert(atom);
127 : : // ignore the true node
128 [ + + ][ + + ]: 85 : if (!lit.isConst() || !lit.getConst<bool>())
[ + + ]
129 : : {
130 : : // output learned literals from preprocessing
131 [ + - ]: 44 : if (d_trackSimplifications)
132 : : {
133 : 44 : computeLearnedLiteralType(lit);
134 : : }
135 : 44 : processLearnedLiteral(lit, modes::LearnedLitType::PREPROCESS);
136 : : // also get its symbols
137 : 44 : expr::getSymbols(atom, inputSymbols, visitedWithinAtom);
138 : : }
139 : : // remember we've seen it
140 : 85 : d_levelZeroAsserts.insert(lit);
141 [ + + ][ + + ]: 177 : }
142 : : // Compute the set of literals in the preprocessed assertions
143 : 32 : std::unordered_set<Node> inputAtoms;
144 [ + + ]: 163 : for (const Node& a : assertions)
145 : : {
146 : 131 : getAtoms(a, visited, inputAtoms);
147 : : }
148 [ + + ]: 137 : for (const Node& a : inputAtoms)
149 : : {
150 : 105 : d_ppnAtoms.insert(a);
151 : : // also get its symbols
152 : 105 : expr::getSymbols(a, inputSymbols, visitedWithinAtom);
153 : : }
154 [ + + ]: 504 : for (const TNode& t : visitedWithinAtom)
155 : : {
156 : 472 : d_ppnTerms.insert(t);
157 : : }
158 [ + + ]: 132 : for (const Node& s : inputSymbols)
159 : : {
160 : 100 : d_ppnSyms.insert(s);
161 : : }
162 : :
163 [ + - ]: 32 : Trace("level-zero") << "Preprocess status:" << std::endl;
164 [ + - ]: 64 : Trace("level-zero") << "#Non-learned lits = " << d_ppnAtoms.size()
165 : 32 : << std::endl;
166 [ + - ]: 32 : Trace("level-zero") << "#Symbols = " << d_ppnSyms.size() << std::endl;
167 [ + - ]: 32 : Trace("level-zero") << "#Subterms = " << d_ppnTerms.size() << std::endl;
168 [ + - ]: 64 : Trace("level-zero") << "#Current top level subs = "
169 : 32 : << d_env.getTopLevelSubstitutions().get().size()
170 : 32 : << std::endl;
171 [ + - ][ - + ]: 32 : Trace("level-zero") << d_ldb.toStringDebug();
[ - - ]
172 : : // the threshold is by default d_ppnAtoms.size()*3.0, which means we restart
173 : : // if we have learned any literals, and the number of assertions since the
174 : : // last learned literal is equal to the total number of literals in the
175 : : // input problem times 3, i.e. each literal has been asserted on average 3
176 : : // times.
177 : 32 : d_deepRestartThreshold = static_cast<size_t>(
178 : 32 : static_cast<double>(d_ppnAtoms.size()) * options().smt.deepRestartFactor);
179 [ + - ]: 64 : Trace("level-zero") << "Restart threshold is " << d_deepRestartThreshold
180 : 32 : << std::endl;
181 : 32 : }
182 : :
183 : 404 : bool ZeroLevelLearner::notifyAsserted(TNode assertion, int32_t alevel)
184 : : {
185 : : // check if at level zero
186 [ + + ]: 404 : if (d_nonZeroAssert.get())
187 : : {
188 : : // already not at level zero, skip
189 : 224 : d_assertNoLearnCount++;
190 : : }
191 [ + + ]: 180 : else if (alevel != 0)
192 : : {
193 [ + - ]: 28 : Trace("level-zero-dec") << "First non-zero: " << assertion << std::endl;
194 : 28 : d_nonZeroAssert = true;
195 : 28 : d_assertNoLearnCount++;
196 : : }
197 [ + + ]: 152 : else if (d_levelZeroAsserts.find(assertion) == d_levelZeroAsserts.end())
198 : : {
199 : : // remember we've processed this
200 : 117 : d_levelZeroAsserts.insert(assertion);
201 : : // process what we should do with the learned literal
202 : 117 : modes::LearnedLitType ltype = computeLearnedLiteralType(assertion);
203 : 117 : processLearnedLiteral(assertion, ltype);
204 : 117 : return true;
205 : : }
206 : : // request a deep restart?
207 [ + + ]: 287 : if (options().smt.deepRestartMode != options::DeepRestartMode::NONE)
208 : : {
209 [ + + ]: 193 : if (hasLearnedLiteralForRestart() > 0)
210 : : {
211 : : // if non-empty and non-learned atoms have been asserted beyond the
212 : : // threshold
213 [ + + ]: 128 : if (d_assertNoLearnCount > d_deepRestartThreshold)
214 : : {
215 [ + - ]: 14 : Trace("level-zero") << "DEEP RESTART after " << d_assertNoLearnCount
216 : 7 : << " asserts." << std::endl;
217 : 7 : return false;
218 : : }
219 : : }
220 : : }
221 [ - + ]: 280 : if (TraceIsOn("level-zero-debug"))
222 : : {
223 [ - - ][ - - ]: 0 : if (d_assertNoLearnCount > 0 && d_deepRestartThreshold > 0
224 [ - - ]: 0 : && d_assertNoLearnCount % d_deepRestartThreshold == 0)
225 : : {
226 [ - - ]: 0 : Trace("level-zero-debug")
227 : 0 : << "#asserts without learning = " << d_assertNoLearnCount << " ("
228 : 0 : << (d_assertNoLearnCount / d_deepRestartThreshold) << "x)"
229 : 0 : << std::endl;
230 : : }
231 : : }
232 : 280 : return true;
233 : : }
234 : :
235 : 161 : modes::LearnedLitType ZeroLevelLearner::computeLearnedLiteralType(
236 : : const Node& input)
237 : : {
238 : : // literal was learned, determine its type
239 : : // compute whether internal prior to substitution
240 [ + + ]: 161 : TNode aatom = input.getKind() == Kind::NOT ? input[0] : input;
241 : 161 : bool internal = d_ppnAtoms.find(aatom) == d_ppnAtoms.end();
242 : : // apply substitutions now
243 : 161 : Node lit = d_tsmap.apply(input, d_env.getRewriter());
244 : 161 : modes::LearnedLitType ltype =
245 [ + + ]: 161 : internal ? modes::LearnedLitType::INTERNAL : modes::LearnedLitType::INPUT;
246 : : // we don't try to solve for literals that simplify to constants
247 [ + + ][ + - ]: 161 : if ((internal || d_trackSimplifications) && !lit.isConst())
[ + + ][ + + ]
248 : : {
249 : 133 : Subs ss;
250 : 133 : bool processed = false;
251 [ + + ]: 133 : if (getSolved(lit, ss))
252 : : {
253 : : // if we solved for any variable from input, we are SOLVABLE.
254 [ + + ]: 86 : for (size_t i = 0, nvars = ss.d_vars.size(); i < nvars; i++)
255 : : {
256 : 43 : Node v = ss.d_vars[i];
257 [ + + ]: 43 : if (d_ppnSyms.find(v) != d_ppnSyms.end())
258 : : {
259 [ + - ]: 31 : Trace("level-zero-assert") << "...solvable due to " << v << std::endl;
260 [ + + ]: 31 : if (ltype == modes::LearnedLitType::INTERNAL)
261 : : {
262 : 1 : ltype = modes::LearnedLitType::SOLVABLE;
263 : : }
264 : : }
265 [ + - ]: 43 : if (d_trackSimplifications)
266 : : {
267 : 43 : bool addSubs = true;
268 [ + - ]: 43 : switch (options().theory.lemmaInprocessSubsMode)
269 : : {
270 : 43 : case options::LemmaInprocessSubsMode::SIMPLE:
271 : 43 : addSubs = ss.d_subs[i].getNumChildren() == 0;
272 : 43 : break;
273 : 0 : default: break;
274 : : }
275 [ + + ]: 43 : if (addSubs)
276 : : {
277 : 23 : processed = true;
278 [ + - ]: 46 : Trace("lemma-inprocess-subs")
279 : 23 : << "Add subs: " << v << " -> " << ss.d_subs[i] << std::endl;
280 : 23 : addSimplification(v, ss.d_subs[i]);
281 : : }
282 : : }
283 : 43 : }
284 : : }
285 [ + - ][ + + ]: 133 : if ((d_trackSimplifications && !processed)
286 [ + - ]: 23 : || ltype != modes::LearnedLitType::SOLVABLE)
287 : : {
288 : : // maybe a constant prop?
289 [ + + ]: 133 : if (lit.getKind() == Kind::EQUAL)
290 : : {
291 [ + + ]: 115 : for (size_t i = 0; i < 2; i++)
292 : : {
293 : : // Only consider substitutions whose RHS are constants.
294 : : // A more general policy could consider lit[i].getNumChildren()==0.
295 [ + + ]: 88 : if (lit[i].isConst())
296 : : {
297 : 60 : if (ltype == modes::LearnedLitType::INTERNAL
298 [ + + ][ + + ]: 30 : && d_ppnTerms.find(lit[1 - i]) != d_ppnTerms.end())
[ + + ][ + + ]
[ - - ]
299 : : {
300 : 2 : ltype = modes::LearnedLitType::CONSTANT_PROP;
301 : : }
302 [ + - ][ + + ]: 30 : if (d_trackSimplifications && !processed)
303 : : {
304 [ + - ]: 30 : Trace("lemma-inprocess-subs")
305 : 15 : << "Add cp: " << lit[1 - i] << " -> " << lit[i] << std::endl;
306 : 15 : addSimplification(lit[1 - i], lit[i]);
307 : 15 : processed = true;
308 : : }
309 : 30 : break;
310 : : }
311 [ + + ]: 58 : else if ((d_trackSimplifications && !processed)
312 : 116 : && expr::hasSubterm(lit[1 - i], lit[i]))
313 : : {
314 : 0 : Trace("lemma-inprocess-subs") << "Add cp subterm: " << lit[1 - i]
315 : 0 : << " -> " << lit[i] << std::endl;
316 : 0 : addSimplification(lit[1 - i], lit[i]);
317 : 0 : processed = true;
318 : 0 : break;
319 : : }
320 : : }
321 : : }
322 [ + + ]: 133 : if (!processed)
323 : : {
324 [ + - ]: 190 : Trace("lemma-inprocess-subs-n")
325 : 95 : << "Unused unit learned: " << lit << std::endl;
326 : : }
327 : : }
328 : 133 : }
329 [ + - ]: 322 : Trace("level-zero-assert")
330 : 161 : << "Level zero assert: " << lit << ", type=" << ltype << std::endl;
331 : 161 : return ltype;
332 : 161 : }
333 : :
334 : 5 : theory::TrustSubstitutionMap& ZeroLevelLearner::getSimplifications()
335 : : {
336 [ - + ][ - + ]: 5 : Assert(d_trackSimplifications);
[ - - ]
337 : 5 : return d_tsmap;
338 : : }
339 : :
340 : 38 : void ZeroLevelLearner::addSimplification(const Node& t, const Node& s)
341 : : {
342 : : // in rare cases we may already have a substitution for v, e.g.
343 : : // if x -> 0, (f y) ---> a, and we learn (f (+ x y)) = b, we
344 : : // would substitute+rewrite to get (f y) --> b despite already
345 : : // having a substitution for (f y). We could avoid this by applying
346 : : // substitution+rewriting until fixed point at the beginning of
347 : : // computeLearnedLiteralType, but this may be expensive.
348 [ + + ]: 38 : if (!d_tsmap.get().hasSubstitution(t))
349 : : {
350 : 36 : d_tsmap.addSubstitution(t, s);
351 : : }
352 : 38 : }
353 : :
354 : 167 : void ZeroLevelLearner::processLearnedLiteral(const Node& lit,
355 : : modes::LearnedLitType ltype)
356 : : {
357 : : // add to the database
358 : 167 : d_ldb.addLearnedLiteral(lit, ltype);
359 : : // reset the counter for deep restart if the literal was learnable
360 [ + + ]: 167 : if (isLearnable(ltype))
361 : : {
362 : 25 : d_assertNoLearnCount = 0;
363 : : }
364 : : // print to stream
365 [ + + ]: 167 : if (isOutputOn(OutputTag::LEARNED_LITS))
366 : : {
367 : : // get the original form so that internally generated variables
368 : : // are mapped back to their original form
369 : 6 : output(OutputTag::LEARNED_LITS)
370 : 6 : << "(learned-lit " << SkolemManager::getOriginalForm(lit);
371 : 6 : std::stringstream tss;
372 : 6 : tss << ltype;
373 : 6 : std::string ltstr = tss.str();
374 : 6 : std::transform(
375 : 40 : ltstr.begin(), ltstr.end(), ltstr.begin(), [](unsigned char c) {
376 : 40 : return std::tolower(c);
377 : : });
378 : 6 : output(OutputTag::LEARNED_LITS) << " :" << ltstr;
379 : 6 : output(OutputTag::LEARNED_LITS) << ")" << std::endl;
380 : 6 : }
381 : 167 : }
382 : :
383 : 29 : std::vector<Node> ZeroLevelLearner::getLearnedZeroLevelLiterals(
384 : : modes::LearnedLitType ltype) const
385 : : {
386 : 29 : std::vector<Node> ret = d_ldb.getLearnedLiterals(ltype);
387 [ - + ]: 29 : if (TraceIsOn("level-zero"))
388 : : {
389 [ - - ]: 0 : if (!ret.empty())
390 : : {
391 [ - - ]: 0 : Trace("level-zero") << "...learned #literals (" << ltype
392 : 0 : << ") = " << ret.size() << std::endl;
393 : : }
394 : : }
395 : 29 : return ret;
396 : 0 : }
397 : :
398 : 7 : std::vector<Node> ZeroLevelLearner::getLearnedZeroLevelLiteralsForRestart()
399 : : const
400 : : {
401 : 7 : std::vector<Node> ret;
402 [ + + ]: 16 : for (modes::LearnedLitType ltype : d_learnedTypes)
403 : : {
404 : 9 : std::vector<Node> rett = getLearnedZeroLevelLiterals(ltype);
405 : 9 : ret.insert(ret.end(), rett.begin(), rett.end());
406 : 9 : }
407 : 7 : return ret;
408 : 0 : }
409 : :
410 : 193 : bool ZeroLevelLearner::hasLearnedLiteralForRestart() const
411 : : {
412 [ + + ]: 269 : for (modes::LearnedLitType ltype : d_learnedTypes)
413 : : {
414 [ + + ]: 204 : if (d_ldb.getNumLearnedLiterals(ltype) > 0)
415 : : {
416 : 128 : return true;
417 : : }
418 : : }
419 : 65 : return false;
420 : : }
421 : :
422 : 167 : bool ZeroLevelLearner::isLearnable(modes::LearnedLitType ltype) const
423 : : {
424 : 167 : return d_learnedTypes.find(ltype) != d_learnedTypes.end();
425 : : }
426 : :
427 : 133 : bool ZeroLevelLearner::getSolved(const Node& lit, Subs& subs)
428 : : {
429 : 133 : context::Context dummyContext;
430 : 266 : theory::TrustSubstitutionMap subsOut(d_env, &dummyContext);
431 : 133 : TrustNode tlit = TrustNode::mkTrustLemma(lit);
432 : 133 : bool status = d_theoryEngine->solve(tlit, subsOut);
433 [ + + ]: 133 : if (status)
434 : : {
435 [ + - ]: 43 : Trace("level-zero-debug") << lit << " is solvable" << std::endl;
436 : : // extract the substitution
437 : 43 : std::unordered_map<Node, Node> ss = subsOut.get().getSubstitutions();
438 [ + + ]: 86 : for (const std::pair<const Node, Node>& s : ss)
439 : : {
440 : 43 : subs.add(s.first, s.second);
441 [ + - ]: 86 : Trace("level-zero-debug")
442 : 43 : << " subs: " << s.first << " -> " << s.second << std::endl;
443 : : }
444 : 43 : return true;
445 : 43 : }
446 [ + - ]: 90 : Trace("level-zero-debug") << lit << " is not solvable" << std::endl;
447 : 90 : return false;
448 : 133 : }
449 : :
450 : : } // namespace prop
451 : : } // namespace cvc5::internal
|
