Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/strings/inference_manager.cpp	Lines:	164	180	91.1 %
Date:	2021-05-21	Branches:	359	776	46.3 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Gereon Kremer, Mudathir Mohamed
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Implementation of the inference manager for the theory of strings.
 */

#include "theory/strings/inference_manager.h"

#include "options/strings_options.h"
#include "theory/ext_theory.h"
#include "theory/rewriter.h"
#include "theory/strings/theory_strings_utils.h"
#include "theory/strings/word.h"

using namespace std;
using namespace cvc5::context;
using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace strings {

InferenceManager::InferenceManager(Theory& t,
                                   SolverState& s,
                                   TermRegistry& tr,
                                   ExtTheory& e,
                                   SequencesStatistics& statistics,
                                   ProofNodeManager* pnm)
    : InferenceManagerBuffered(t, s, pnm, "theory::strings::", false),
      d_state(s),
      d_termReg(tr),
      d_extt(e),
      d_statistics(statistics),
      d_ipc(pnm ? new InferProofCons(d_state.getSatContext(), pnm, d_statistics)
                : nullptr)
{
  NodeManager* nm = NodeManager::currentNM();
  d_zero = nm->mkConst(Rational(0));
  d_one = nm->mkConst(Rational(1));
  d_true = nm->mkConst(true);
  d_false = nm->mkConst(false);
}

void InferenceManager::doPending()
{
  doPendingFacts();
  if (d_state.isInConflict())
  {
    // just clear the pending vectors, nothing else to do
    clearPendingLemmas();
    clearPendingPhaseRequirements();
    return;
  }
  doPendingLemmas();
  doPendingPhaseRequirements();
}

bool InferenceManager::sendInternalInference(std::vector<Node>& exp,
                                             Node conc,
                                             InferenceId infer)
{
  if (conc.getKind() == AND
      || (conc.getKind() == NOT && conc[0].getKind() == OR))
  {
    Node conj = conc.getKind() == AND ? conc : conc[0];
    bool pol = conc.getKind() == AND;
    bool ret = true;
    for (const Node& cc : conj)
    {
      bool retc = sendInternalInference(exp, pol ? cc : cc.negate(), infer);
      ret = ret && retc;
    }
    return ret;
  }
  bool pol = conc.getKind() != NOT;
  Node lit = pol ? conc : conc[0];
  if (lit.getKind() == EQUAL)
  {
    for (unsigned i = 0; i < 2; i++)
    {
      if (!lit[i].isConst() && !d_state.hasTerm(lit[i]))
      {
        // introduces a new non-constant term, do not infer
        return false;
      }
    }
    // does it already hold?
    if (pol ? d_state.areEqual(lit[0], lit[1])
            : d_state.areDisequal(lit[0], lit[1]))
    {
      return true;
    }
  }
  else if (lit.isConst())
  {
    if (lit.getConst<bool>())
    {
      Assert(pol);
      // trivially holds
      return true;
    }
  }
  else if (!d_state.hasTerm(lit))
  {
    // introduces a new non-constant term, do not infer
    return false;
  }
  else if (d_state.areEqual(lit, pol ? d_true : d_false))
  {
    // already holds
    return true;
  }
  sendInference(exp, conc, infer);
  return true;
}

bool InferenceManager::sendInference(const std::vector<Node>& exp,
                                     const std::vector<Node>& noExplain,
                                     Node eq,
                                     InferenceId infer,
                                     bool isRev,
                                     bool asLemma)
{
  if (eq.isNull())
  {
    eq = d_false;
  }
  else if (Rewriter::rewrite(eq) == d_true)
  {
    // if trivial, return
    return false;
  }
  // wrap in infer info and send below
  InferInfo ii(infer);
  ii.d_idRev = isRev;
  ii.d_conc = eq;
  ii.d_premises = exp;
  ii.d_noExplain = noExplain;
  sendInference(ii, asLemma);
  return true;
}

bool InferenceManager::sendInference(const std::vector<Node>& exp,
                                     Node eq,
                                     InferenceId infer,
                                     bool isRev,
                                     bool asLemma)
{
  std::vector<Node> noExplain;
  return sendInference(exp, noExplain, eq, infer, isRev, asLemma);
}

void InferenceManager::sendInference(InferInfo& ii, bool asLemma)
{
  Assert(!ii.isTrivial());
  // set that this inference manager will be processing this inference
  ii.d_sim = this;
  Trace("strings-infer-debug")
      << "sendInference: " << ii << ", asLemma = " << asLemma << std::endl;
  // check if we should send a conflict, lemma or a fact
  if (ii.isConflict())
  {
    Trace("strings-infer-debug") << "...as conflict" << std::endl;
    Trace("strings-lemma") << "Strings::Conflict: " << ii.d_premises << " by "
                           << ii.getId() << std::endl;
    Trace("strings-conflict") << "CONFLICT: inference conflict " << ii.d_premises << " by " << ii.getId() << std::endl;
    ++(d_statistics.d_conflictsInfer);
    // process the conflict immediately
    processConflict(ii);
    return;
  }
  else if (asLemma || options::stringInferAsLemmas() || !ii.isFact())
  {
    Trace("strings-infer-debug") << "...as lemma" << std::endl;
    addPendingLemma(std::unique_ptr<InferInfo>(new InferInfo(ii)));
    return;
  }
  if (options::stringInferSym())
  {
    std::vector<Node> unproc;
    for (const Node& ac : ii.d_premises)
    {
      d_termReg.removeProxyEqs(ac, unproc);
    }
    if (unproc.empty())
    {
      Node eqs = ii.d_conc;
      // keep the same id for now, since we are transforming the form of the
      // inference, not the root reason.
      InferInfo iiSubsLem(ii.getId());
      iiSubsLem.d_sim = this;
      iiSubsLem.d_conc = eqs;
      if (Trace.isOn("strings-lemma-debug"))
      {
        Trace("strings-lemma-debug")
            << "Strings::Infer " << iiSubsLem << std::endl;
        Trace("strings-lemma-debug")
            << "Strings::Infer Alternate : " << eqs << std::endl;
      }
      Trace("strings-infer-debug") << "...as symbolic lemma" << std::endl;
      addPendingLemma(std::unique_ptr<InferInfo>(new InferInfo(iiSubsLem)));
      return;
    }
    if (Trace.isOn("strings-lemma-debug"))
    {
      for (const Node& u : unproc)
      {
        Trace("strings-lemma-debug")
            << "  non-trivial explanation : " << u << std::endl;
      }
    }
  }
  Trace("strings-infer-debug") << "...as fact" << std::endl;
  // add to pending to be processed as a fact
  addPendingFact(std::unique_ptr<InferInfo>(new InferInfo(ii)));
}

bool InferenceManager::sendSplit(Node a, Node b, InferenceId infer, bool preq)
{
  Node eq = a.eqNode(b);
  eq = Rewriter::rewrite(eq);
  if (eq.isConst())
  {
    return false;
  }
  NodeManager* nm = NodeManager::currentNM();
  InferInfo iiSplit(infer);
  iiSplit.d_sim = this;
  iiSplit.d_conc = nm->mkNode(OR, eq, nm->mkNode(NOT, eq));
  eq = Rewriter::rewrite(eq);
  addPendingPhaseRequirement(eq, preq);
  addPendingLemma(std::unique_ptr<InferInfo>(new InferInfo(iiSplit)));
  return true;
}

void InferenceManager::addToExplanation(Node a,
                                        Node b,
                                        std::vector<Node>& exp) const
{
  if (a != b)
  {
    Debug("strings-explain")
        << "Add to explanation : " << a << " == " << b << std::endl;
    Assert(d_state.areEqual(a, b));
    exp.push_back(a.eqNode(b));
  }
}

void InferenceManager::addToExplanation(Node lit, std::vector<Node>& exp) const
{
  if (!lit.isNull())
  {
    Assert(!lit.isConst());
    exp.push_back(lit);
  }
}

bool InferenceManager::hasProcessed() const
{
  return d_state.isInConflict() || hasPending();
}

void InferenceManager::markReduced(Node n, ExtReducedId id, bool contextDepend)
{
  d_extt.markReduced(n, id, contextDepend);
}

void InferenceManager::processConflict(const InferInfo& ii)
{
  Assert(!d_state.isInConflict());
  // setup the fact to reproduce the proof in the call below
  if (d_ipc != nullptr)
  {
    d_ipc->notifyFact(ii);
  }
  // make the trust node
  TrustNode tconf = mkConflictExp(ii.d_premises, d_ipc.get());
  Assert(tconf.getKind() == TrustNodeKind::CONFLICT);
  Trace("strings-assert") << "(assert (not " << tconf.getNode()
                          << ")) ; conflict " << ii.getId() << std::endl;
  // send the trusted conflict
  trustedConflict(tconf, ii.getId());
}

void InferenceManager::processFact(InferInfo& ii, ProofGenerator*& pg)
{
  Trace("strings-assert") << "(assert (=> " << ii.getPremises() << " "
                          << ii.d_conc << ")) ; fact " << ii.getId() << std::endl;
  Trace("strings-lemma") << "Strings::Fact: " << ii.d_conc << " from "
                         << ii.getPremises() << " by " << ii.getId()
                         << std::endl;
  if (d_ipc != nullptr)
  {
    // ensure the proof generator is ready to explain this fact in the
    // current SAT context
    d_ipc->notifyFact(ii);
    pg = d_ipc.get();
  }
}

TrustNode InferenceManager::processLemma(InferInfo& ii, LemmaProperty& p)
{
  Assert(!ii.isTrivial());
  Assert(!ii.isConflict());
  // set up the explanation and no-explanation
  std::vector<Node> exp;
  for (const Node& ec : ii.d_premises)
  {
    utils::flattenOp(AND, ec, exp);
  }
  std::vector<Node> noExplain;
  if (!options::stringRExplainLemmas())
  {
    // if we aren't regressing the explanation, we add all literals to
    // noExplain and ignore ii.d_ant.
    noExplain.insert(noExplain.end(), exp.begin(), exp.end());
  }
  else
  {
    // otherwise, the no-explain literals are those provided
    for (const Node& ecn : ii.d_noExplain)
    {
      utils::flattenOp(AND, ecn, noExplain);
    }
  }
  // ensure that the proof generator is ready to explain the final conclusion
  // of the lemma (ii.d_conc).
  if (d_ipc != nullptr)
  {
    d_ipc->notifyFact(ii);
  }
  TrustNode tlem = mkLemmaExp(ii.d_conc, exp, noExplain, d_ipc.get());
  Trace("strings-pending") << "Process pending lemma : " << tlem.getNode()
                           << std::endl;

  // Process the side effects of the inference info.
  // Register the new skolems from this inference. We register them here
  // (lazily), since this is the moment when we have decided to process the
  // inference.
  for (const std::pair<const LengthStatus, std::vector<Node> >& sks :
       ii.d_skolems)
  {
    for (const Node& n : sks.second)
    {
      d_termReg.registerTermAtomic(n, sks.first);
    }
  }
  if (ii.getId() == InferenceId::STRINGS_REDUCTION)
  {
    p |= LemmaProperty::NEEDS_JUSTIFY;
  }
  Trace("strings-assert") << "(assert " << tlem.getNode() << ") ; lemma "
                          << ii.getId() << std::endl;
  Trace("strings-lemma") << "Strings::Lemma: " << tlem.getNode() << " by "
                         << ii.getId() << std::endl;
  return tlem;
}

}  // namespace strings
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Gereon Kremer, Mudathir Mohamed
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 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 the inference manager for the theory of strings.
14		*/
15
16		#include "theory/strings/inference_manager.h"
17
18		#include "options/strings_options.h"
19		#include "theory/ext_theory.h"
20		#include "theory/rewriter.h"
21		#include "theory/strings/theory_strings_utils.h"
22		#include "theory/strings/word.h"
23
24		using namespace std;
25		using namespace cvc5::context;
26		using namespace cvc5::kind;
27
28		namespace cvc5 {
29		namespace theory {
30		namespace strings {
31
32	8954	InferenceManager::InferenceManager(Theory& t,
33		SolverState& s,
34		TermRegistry& tr,
35		ExtTheory& e,
36		SequencesStatistics& statistics,
37	8954	ProofNodeManager* pnm)
38		: InferenceManagerBuffered(t, s, pnm, "theory::strings::", false),
39		d_state(s),
40		d_termReg(tr),
41		d_extt(e),
42		d_statistics(statistics),
43	1214	d_ipc(pnm ? new InferProofCons(d_state.getSatContext(), pnm, d_statistics)
44	10168	: nullptr)
45		{
46	8954	NodeManager* nm = NodeManager::currentNM();
47	8954	d_zero = nm->mkConst(Rational(0));
48	8954	d_one = nm->mkConst(Rational(1));
49	8954	d_true = nm->mkConst(true);
50	8954	d_false = nm->mkConst(false);
51	8954	}
52
53	24023	void InferenceManager::doPending()
54		{
55	24023	doPendingFacts();
56	24023	if (d_state.isInConflict())
57		{
58		// just clear the pending vectors, nothing else to do
59	1492	clearPendingLemmas();
60	1492	clearPendingPhaseRequirements();
61	1492	return;
62		}
63	22531	doPendingLemmas();
64	22531	doPendingPhaseRequirements();
65		}
66
67	16187	bool InferenceManager::sendInternalInference(std::vector<Node>& exp,
68		Node conc,
69		InferenceId infer)
70		{
71	32374	if (conc.getKind() == AND
72	32374	\|\| (conc.getKind() == NOT && conc[0].getKind() == OR))
73		{
74	3014	Node conj = conc.getKind() == AND ? conc : conc[0];
75	1507	bool pol = conc.getKind() == AND;
76	1507	bool ret = true;
77	5185	for (const Node& cc : conj)
78		{
79	3678	bool retc = sendInternalInference(exp, pol ? cc : cc.negate(), infer);
80	3678	ret = ret && retc;
81		}
82	1507	return ret;
83		}
84	14680	bool pol = conc.getKind() != NOT;
85	29360	Node lit = pol ? conc : conc[0];
86	14680	if (lit.getKind() == EQUAL)
87		{
88	9109	for (unsigned i = 0; i < 2; i++)
89		{
90	6166	if (!lit[i].isConst() && !d_state.hasTerm(lit[i]))
91		{
92		// introduces a new non-constant term, do not infer
93	140	return false;
94		}
95		}
96		// does it already hold?
97	10302	if (pol ? d_state.areEqual(lit[0], lit[1])
98	7359	: d_state.areDisequal(lit[0], lit[1]))
99		{
100	2683	return true;
101		}
102		}
103	11597	else if (lit.isConst())
104		{
105	4	if (lit.getConst<bool>())
106		{
107		Assert(pol);
108		// trivially holds
109		return true;
110		}
111		}
112	11593	else if (!d_state.hasTerm(lit))
113		{
114		// introduces a new non-constant term, do not infer
115	9459	return false;
116		}
117	2134	else if (d_state.areEqual(lit, pol ? d_true : d_false))
118		{
119		// already holds
120	2128	return true;
121		}
122	270	sendInference(exp, conc, infer);
123	270	return true;
124		}
125
126	25232	bool InferenceManager::sendInference(const std::vector<Node>& exp,
127		const std::vector<Node>& noExplain,
128		Node eq,
129		InferenceId infer,
130		bool isRev,
131		bool asLemma)
132		{
133	25232	if (eq.isNull())
134		{
135	76	eq = d_false;
136		}
137	25156	else if (Rewriter::rewrite(eq) == d_true)
138		{
139		// if trivial, return
140	2	return false;
141		}
142		// wrap in infer info and send below
143	50460	InferInfo ii(infer);
144	25230	ii.d_idRev = isRev;
145	25230	ii.d_conc = eq;
146	25230	ii.d_premises = exp;
147	25230	ii.d_noExplain = noExplain;
148	25230	sendInference(ii, asLemma);
149	25230	return true;
150		}
151
152	22978	bool InferenceManager::sendInference(const std::vector<Node>& exp,
153		Node eq,
154		InferenceId infer,
155		bool isRev,
156		bool asLemma)
157		{
158	45956	std::vector<Node> noExplain;
159	45956	return sendInference(exp, noExplain, eq, infer, isRev, asLemma);
160		}
161
162	27015	void InferenceManager::sendInference(InferInfo& ii, bool asLemma)
163		{
164	27015	Assert(!ii.isTrivial());
165		// set that this inference manager will be processing this inference
166	27015	ii.d_sim = this;
167	54030	Trace("strings-infer-debug")
168	27015	<< "sendInference: " << ii << ", asLemma = " << asLemma << std::endl;
169		// check if we should send a conflict, lemma or a fact
170	27015	if (ii.isConflict())
171		{
172	682	Trace("strings-infer-debug") << "...as conflict" << std::endl;
173	1364	Trace("strings-lemma") << "Strings::Conflict: " << ii.d_premises << " by "
174	682	<< ii.getId() << std::endl;
175	682	Trace("strings-conflict") << "CONFLICT: inference conflict " << ii.d_premises << " by " << ii.getId() << std::endl;
176	682	++(d_statistics.d_conflictsInfer);
177		// process the conflict immediately
178	682	processConflict(ii);
179	682	return;
180		}
181	40226	else if (asLemma \|\| options::stringInferAsLemmas() \|\| !ii.isFact())
182		{
183	13863	Trace("strings-infer-debug") << "...as lemma" << std::endl;
184	13863	addPendingLemma(std::unique_ptr<InferInfo>(new InferInfo(ii)));
185	13863	return;
186		}
187	12470	if (options::stringInferSym())
188		{
189	24512	std::vector<Node> unproc;
190	51281	for (const Node& ac : ii.d_premises)
191		{
192	38811	d_termReg.removeProxyEqs(ac, unproc);
193		}
194	12470	if (unproc.empty())
195		{
196	856	Node eqs = ii.d_conc;
197		// keep the same id for now, since we are transforming the form of the
198		// inference, not the root reason.
199	856	InferInfo iiSubsLem(ii.getId());
200	428	iiSubsLem.d_sim = this;
201	428	iiSubsLem.d_conc = eqs;
202	428	if (Trace.isOn("strings-lemma-debug"))
203		{
204		Trace("strings-lemma-debug")
205		<< "Strings::Infer " << iiSubsLem << std::endl;
206		Trace("strings-lemma-debug")
207		<< "Strings::Infer Alternate : " << eqs << std::endl;
208		}
209	428	Trace("strings-infer-debug") << "...as symbolic lemma" << std::endl;
210	428	addPendingLemma(std::unique_ptr<InferInfo>(new InferInfo(iiSubsLem)));
211	428	return;
212		}
213	12042	if (Trace.isOn("strings-lemma-debug"))
214		{
215		for (const Node& u : unproc)
216		{
217		Trace("strings-lemma-debug")
218		<< " non-trivial explanation : " << u << std::endl;
219		}
220		}
221		}
222	12042	Trace("strings-infer-debug") << "...as fact" << std::endl;
223		// add to pending to be processed as a fact
224	12042	addPendingFact(std::unique_ptr<InferInfo>(new InferInfo(ii)));
225		}
226
227	419	bool InferenceManager::sendSplit(Node a, Node b, InferenceId infer, bool preq)
228		{
229	838	Node eq = a.eqNode(b);
230	419	eq = Rewriter::rewrite(eq);
231	419	if (eq.isConst())
232		{
233		return false;
234		}
235	419	NodeManager* nm = NodeManager::currentNM();
236	838	InferInfo iiSplit(infer);
237	419	iiSplit.d_sim = this;
238	419	iiSplit.d_conc = nm->mkNode(OR, eq, nm->mkNode(NOT, eq));
239	419	eq = Rewriter::rewrite(eq);
240	419	addPendingPhaseRequirement(eq, preq);
241	419	addPendingLemma(std::unique_ptr<InferInfo>(new InferInfo(iiSplit)));
242	419	return true;
243		}
244
245	421890	void InferenceManager::addToExplanation(Node a,
246		Node b,
247		std::vector<Node>& exp) const
248		{
249	421890	if (a != b)
250		{
251	390146	Debug("strings-explain")
252	195073	<< "Add to explanation : " << a << " == " << b << std::endl;
253	195073	Assert(d_state.areEqual(a, b));
254	195073	exp.push_back(a.eqNode(b));
255		}
256	421890	}
257
258		void InferenceManager::addToExplanation(Node lit, std::vector<Node>& exp) const
259		{
260		if (!lit.isNull())
261		{
262		Assert(!lit.isConst());
263		exp.push_back(lit);
264		}
265		}
266
267	2072923	bool InferenceManager::hasProcessed() const
268		{
269	2072923	return d_state.isInConflict() \|\| hasPending();
270		}
271
272	94	void InferenceManager::markReduced(Node n, ExtReducedId id, bool contextDepend)
273		{
274	94	d_extt.markReduced(n, id, contextDepend);
275	94	}
276
277	874	void InferenceManager::processConflict(const InferInfo& ii)
278		{
279	874	Assert(!d_state.isInConflict());
280		// setup the fact to reproduce the proof in the call below
281	874	if (d_ipc != nullptr)
282		{
283	160	d_ipc->notifyFact(ii);
284		}
285		// make the trust node
286	1748	TrustNode tconf = mkConflictExp(ii.d_premises, d_ipc.get());
287	874	Assert(tconf.getKind() == TrustNodeKind::CONFLICT);
288	1748	Trace("strings-assert") << "(assert (not " << tconf.getNode()
289	874	<< ")) ; conflict " << ii.getId() << std::endl;
290		// send the trusted conflict
291	874	trustedConflict(tconf, ii.getId());
292	874	}
293
294	11701	void InferenceManager::processFact(InferInfo& ii, ProofGenerator*& pg)
295		{
296	23402	Trace("strings-assert") << "(assert (=> " << ii.getPremises() << " "
297	11701	<< ii.d_conc << ")) ; fact " << ii.getId() << std::endl;
298	23402	Trace("strings-lemma") << "Strings::Fact: " << ii.d_conc << " from "
299	23402	<< ii.getPremises() << " by " << ii.getId()
300	11701	<< std::endl;
301	11701	if (d_ipc != nullptr)
302		{
303		// ensure the proof generator is ready to explain this fact in the
304		// current SAT context
305	826	d_ipc->notifyFact(ii);
306	826	pg = d_ipc.get();
307		}
308	11701	}
309
310	14562	TrustNode InferenceManager::processLemma(InferInfo& ii, LemmaProperty& p)
311		{
312	14562	Assert(!ii.isTrivial());
313	14562	Assert(!ii.isConflict());
314		// set up the explanation and no-explanation
315	29124	std::vector<Node> exp;
316	42542	for (const Node& ec : ii.d_premises)
317		{
318	27980	utils::flattenOp(AND, ec, exp);
319		}
320	29124	std::vector<Node> noExplain;
321	29124	if (!options::stringRExplainLemmas())
322		{
323		// if we aren't regressing the explanation, we add all literals to
324		// noExplain and ignore ii.d_ant.
325		noExplain.insert(noExplain.end(), exp.begin(), exp.end());
326		}
327		else
328		{
329		// otherwise, the no-explain literals are those provided
330	17135	for (const Node& ecn : ii.d_noExplain)
331		{
332	2573	utils::flattenOp(AND, ecn, noExplain);
333		}
334		}
335		// ensure that the proof generator is ready to explain the final conclusion
336		// of the lemma (ii.d_conc).
337	14562	if (d_ipc != nullptr)
338		{
339	961	d_ipc->notifyFact(ii);
340		}
341	14562	TrustNode tlem = mkLemmaExp(ii.d_conc, exp, noExplain, d_ipc.get());
342	29124	Trace("strings-pending") << "Process pending lemma : " << tlem.getNode()
343	14562	<< std::endl;
344
345		// Process the side effects of the inference info.
346		// Register the new skolems from this inference. We register them here
347		// (lazily), since this is the moment when we have decided to process the
348		// inference.
349	822	for (const std::pair<const LengthStatus, std::vector<Node> >& sks :
350	14562	ii.d_skolems)
351		{
352	1644	for (const Node& n : sks.second)
353		{
354	822	d_termReg.registerTermAtomic(n, sks.first);
355		}
356		}
357	14562	if (ii.getId() == InferenceId::STRINGS_REDUCTION)
358		{
359	1392	p \|= LemmaProperty::NEEDS_JUSTIFY;
360		}
361	29124	Trace("strings-assert") << "(assert " << tlem.getNode() << ") ; lemma "
362	14562	<< ii.getId() << std::endl;
363	29124	Trace("strings-lemma") << "Strings::Lemma: " << tlem.getNode() << " by "
364	14562	<< ii.getId() << std::endl;
365	29124	return tlem;
366		}
367
368		} // namespace strings
369		} // namespace theory
370	27735	} // namespace cvc5