Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/strings/inference_manager.cpp	Lines:	159	183	86.9 %
Date:	2021-11-05	Branches:	352	788	44.7 %


/******************************************************************************
 * 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"
#include "util/rational.h"

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

namespace cvc5 {
namespace theory {
namespace strings {

InferenceManager::InferenceManager(Env& env,
                                   Theory& t,
                                   SolverState& s,
                                   TermRegistry& tr,
                                   ExtTheory& e,
                                   SequencesStatistics& statistics)
    : InferenceManagerBuffered(env, t, s, "theory::strings::", false),
      d_state(s),
      d_termReg(tr),
      d_extt(e),
      d_statistics(statistics),
      d_ipc(isProofEnabled()
                ? new InferProofCons(
                      context(), env.getProofNodeManager(), d_statistics)
                : nullptr),
      d_ipcl(isProofEnabled()
                 ? new InferProofCons(
                       context(), env.getProofNodeManager(), 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_ipcl != nullptr)
  {
    d_ipcl->notifyLemma(ii);
  }
  // make the trust node
  TrustNode tconf = mkConflictExp(ii.d_premises, d_ipcl.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_ipcl != nullptr)
  {
    d_ipcl->notifyLemma(ii);
  }
  TrustNode tlem = mkLemmaExp(ii.d_conc, exp, noExplain, d_ipcl.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		#include "util/rational.h"
24
25		using namespace std;
26		using namespace cvc5::context;
27		using namespace cvc5::kind;
28
29		namespace cvc5 {
30		namespace theory {
31		namespace strings {
32
33	15271	InferenceManager::InferenceManager(Env& env,
34		Theory& t,
35		SolverState& s,
36		TermRegistry& tr,
37		ExtTheory& e,
38	15271	SequencesStatistics& statistics)
39		: InferenceManagerBuffered(env, t, s, "theory::strings::", false),
40		d_state(s),
41		d_termReg(tr),
42		d_extt(e),
43		d_statistics(statistics),
44	15271	d_ipc(isProofEnabled()
45		? new InferProofCons(
46	5372	context(), env.getProofNodeManager(), d_statistics)
47		: nullptr),
48	15271	d_ipcl(isProofEnabled()
49		? new InferProofCons(
50	5372	context(), env.getProofNodeManager(), d_statistics)
51	56557	: nullptr)
52		{
53	15271	NodeManager* nm = NodeManager::currentNM();
54	15271	d_zero = nm->mkConst(Rational(0));
55	15271	d_one = nm->mkConst(Rational(1));
56	15271	d_true = nm->mkConst(true);
57	15271	d_false = nm->mkConst(false);
58	15271	}
59
60	44213	void InferenceManager::doPending()
61		{
62	44213	doPendingFacts();
63	44213	if (d_state.isInConflict())
64		{
65		// just clear the pending vectors, nothing else to do
66	2824	clearPendingLemmas();
67	2824	clearPendingPhaseRequirements();
68	2824	return;
69		}
70	41389	doPendingLemmas();
71	41389	doPendingPhaseRequirements();
72		}
73
74	38662	bool InferenceManager::sendInternalInference(std::vector<Node>& exp,
75		Node conc,
76		InferenceId infer)
77		{
78	77324	if (conc.getKind() == AND
79	77324	\|\| (conc.getKind() == NOT && conc[0].getKind() == OR))
80		{
81	5456	Node conj = conc.getKind() == AND ? conc : conc[0];
82	2728	bool pol = conc.getKind() == AND;
83	2728	bool ret = true;
84	10058	for (const Node& cc : conj)
85		{
86	7330	bool retc = sendInternalInference(exp, pol ? cc : cc.negate(), infer);
87	7330	ret = ret && retc;
88		}
89	2728	return ret;
90		}
91	35934	bool pol = conc.getKind() != NOT;
92	71868	Node lit = pol ? conc : conc[0];
93	35934	if (lit.getKind() == EQUAL)
94		{
95	16022	for (unsigned i = 0; i < 2; i++)
96		{
97	10780	if (!lit[i].isConst() && !d_state.hasTerm(lit[i]))
98		{
99		// introduces a new non-constant term, do not infer
100	148	return false;
101		}
102		}
103		// does it already hold?
104	18228	if (pol ? d_state.areEqual(lit[0], lit[1])
105	12986	: d_state.areDisequal(lit[0], lit[1]))
106		{
107	4754	return true;
108		}
109		}
110	30544	else if (lit.isConst())
111		{
112	142	if (lit.getConst<bool>())
113		{
114		Assert(pol);
115		// trivially holds
116		return true;
117		}
118		}
119	30402	else if (!d_state.hasTerm(lit))
120		{
121		// introduces a new non-constant term, do not infer
122	27730	return false;
123		}
124	2672	else if (d_state.areEqual(lit, pol ? d_true : d_false))
125		{
126		// already holds
127	2628	return true;
128		}
129	674	sendInference(exp, conc, infer);
130	674	return true;
131		}
132
133	61969	bool InferenceManager::sendInference(const std::vector<Node>& exp,
134		const std::vector<Node>& noExplain,
135		Node eq,
136		InferenceId infer,
137		bool isRev,
138		bool asLemma)
139		{
140	61969	if (eq.isNull())
141		{
142	86	eq = d_false;
143		}
144	61883	else if (Rewriter::rewrite(eq) == d_true)
145		{
146		// if trivial, return
147	6	return false;
148		}
149		// wrap in infer info and send below
150	123926	InferInfo ii(infer);
151	61963	ii.d_idRev = isRev;
152	61963	ii.d_conc = eq;
153	61963	ii.d_premises = exp;
154	61963	ii.d_noExplain = noExplain;
155	61963	sendInference(ii, asLemma);
156	61963	return true;
157		}
158
159	57210	bool InferenceManager::sendInference(const std::vector<Node>& exp,
160		Node eq,
161		InferenceId infer,
162		bool isRev,
163		bool asLemma)
164		{
165	114420	std::vector<Node> noExplain;
166	114420	return sendInference(exp, noExplain, eq, infer, isRev, asLemma);
167		}
168
169	65028	void InferenceManager::sendInference(InferInfo& ii, bool asLemma)
170		{
171	65028	Assert(!ii.isTrivial());
172		// set that this inference manager will be processing this inference
173	65028	ii.d_sim = this;
174	130056	Trace("strings-infer-debug")
175	65028	<< "sendInference: " << ii << ", asLemma = " << asLemma << std::endl;
176		// check if we should send a conflict, lemma or a fact
177	65028	if (ii.isConflict())
178		{
179	1335	Trace("strings-infer-debug") << "...as conflict" << std::endl;
180	2670	Trace("strings-lemma") << "Strings::Conflict: " << ii.d_premises << " by "
181	1335	<< ii.getId() << std::endl;
182	1335	Trace("strings-conflict") << "CONFLICT: inference conflict " << ii.d_premises << " by " << ii.getId() << std::endl;
183	1335	++(d_statistics.d_conflictsInfer);
184		// process the conflict immediately
185	1335	processConflict(ii);
186	1335	return;
187		}
188	63693	else if (asLemma \|\| options::stringInferAsLemmas() \|\| !ii.isFact())
189		{
190	25388	Trace("strings-infer-debug") << "...as lemma" << std::endl;
191	25388	addPendingLemma(std::unique_ptr<InferInfo>(new InferInfo(ii)));
192	25388	return;
193		}
194	38305	if (options::stringInferSym())
195		{
196	76610	std::vector<Node> unproc;
197	125938	for (const Node& ac : ii.d_premises)
198		{
199	87633	d_termReg.removeProxyEqs(ac, unproc);
200		}
201	38305	if (unproc.empty())
202		{
203		Node eqs = ii.d_conc;
204		// keep the same id for now, since we are transforming the form of the
205		// inference, not the root reason.
206		InferInfo iiSubsLem(ii.getId());
207		iiSubsLem.d_sim = this;
208		iiSubsLem.d_conc = eqs;
209		if (Trace.isOn("strings-lemma-debug"))
210		{
211		Trace("strings-lemma-debug")
212		<< "Strings::Infer " << iiSubsLem << std::endl;
213		Trace("strings-lemma-debug")
214		<< "Strings::Infer Alternate : " << eqs << std::endl;
215		}
216		Trace("strings-infer-debug") << "...as symbolic lemma" << std::endl;
217		addPendingLemma(std::unique_ptr<InferInfo>(new InferInfo(iiSubsLem)));
218		return;
219		}
220	38305	if (Trace.isOn("strings-lemma-debug"))
221		{
222		for (const Node& u : unproc)
223		{
224		Trace("strings-lemma-debug")
225		<< " non-trivial explanation : " << u << std::endl;
226		}
227		}
228		}
229	38305	Trace("strings-infer-debug") << "...as fact" << std::endl;
230		// add to pending to be processed as a fact
231	38305	addPendingFact(std::unique_ptr<InferInfo>(new InferInfo(ii)));
232		}
233
234	591	bool InferenceManager::sendSplit(Node a, Node b, InferenceId infer, bool preq)
235		{
236	1182	Node eq = a.eqNode(b);
237	591	eq = Rewriter::rewrite(eq);
238	591	if (eq.isConst())
239		{
240		return false;
241		}
242	591	NodeManager* nm = NodeManager::currentNM();
243	1182	InferInfo iiSplit(infer);
244	591	iiSplit.d_sim = this;
245	591	iiSplit.d_conc = nm->mkNode(OR, eq, nm->mkNode(NOT, eq));
246	591	eq = Rewriter::rewrite(eq);
247	591	addPendingPhaseRequirement(eq, preq);
248	591	addPendingLemma(std::unique_ptr<InferInfo>(new InferInfo(iiSplit)));
249	591	return true;
250		}
251
252	936666	void InferenceManager::addToExplanation(Node a,
253		Node b,
254		std::vector<Node>& exp) const
255		{
256	936666	if (a != b)
257		{
258	939774	Debug("strings-explain")
259	469887	<< "Add to explanation : " << a << " == " << b << std::endl;
260	469887	Assert(d_state.areEqual(a, b));
261	469887	exp.push_back(a.eqNode(b));
262		}
263	936666	}
264
265		void InferenceManager::addToExplanation(Node lit, std::vector<Node>& exp) const
266		{
267		if (!lit.isNull())
268		{
269		Assert(!lit.isConst());
270		exp.push_back(lit);
271		}
272		}
273
274	3915610	bool InferenceManager::hasProcessed() const
275		{
276	3915610	return d_state.isInConflict() \|\| hasPending();
277		}
278
279	197	void InferenceManager::markReduced(Node n, ExtReducedId id, bool contextDepend)
280		{
281	197	d_extt.markReduced(n, id, contextDepend);
282	197	}
283
284	1952	void InferenceManager::processConflict(const InferInfo& ii)
285		{
286	1952	Assert(!d_state.isInConflict());
287		// setup the fact to reproduce the proof in the call below
288	1952	if (d_ipcl != nullptr)
289		{
290	288	d_ipcl->notifyLemma(ii);
291		}
292		// make the trust node
293	3904	TrustNode tconf = mkConflictExp(ii.d_premises, d_ipcl.get());
294	1952	Assert(tconf.getKind() == TrustNodeKind::CONFLICT);
295	3904	Trace("strings-assert") << "(assert (not " << tconf.getNode()
296	1952	<< ")) ; conflict " << ii.getId() << std::endl;
297		// send the trusted conflict
298	1952	trustedConflict(tconf, ii.getId());
299	1952	}
300
301	37411	void InferenceManager::processFact(InferInfo& ii, ProofGenerator*& pg)
302		{
303	74822	Trace("strings-assert") << "(assert (=> " << ii.getPremises() << " "
304	37411	<< ii.d_conc << ")) ; fact " << ii.getId() << std::endl;
305	74822	Trace("strings-lemma") << "Strings::Fact: " << ii.d_conc << " from "
306	74822	<< ii.getPremises() << " by " << ii.getId()
307	37411	<< std::endl;
308	37411	if (d_ipc != nullptr)
309		{
310		// ensure the proof generator is ready to explain this fact in the
311		// current SAT context
312	9245	d_ipc->notifyFact(ii);
313	9245	pg = d_ipc.get();
314		}
315	37411	}
316
317	25693	TrustNode InferenceManager::processLemma(InferInfo& ii, LemmaProperty& p)
318		{
319	25693	Assert(!ii.isTrivial());
320	25693	Assert(!ii.isConflict());
321		// set up the explanation and no-explanation
322	51386	std::vector<Node> exp;
323	82533	for (const Node& ec : ii.d_premises)
324		{
325	56840	utils::flattenOp(AND, ec, exp);
326		}
327	51386	std::vector<Node> noExplain;
328	25693	if (!options::stringRExplainLemmas())
329		{
330		// if we aren't regressing the explanation, we add all literals to
331		// noExplain and ignore ii.d_ant.
332		noExplain.insert(noExplain.end(), exp.begin(), exp.end());
333		}
334		else
335		{
336		// otherwise, the no-explain literals are those provided
337	31422	for (const Node& ecn : ii.d_noExplain)
338		{
339	5729	utils::flattenOp(AND, ecn, noExplain);
340		}
341		}
342		// ensure that the proof generator is ready to explain the final conclusion
343		// of the lemma (ii.d_conc).
344	25693	if (d_ipcl != nullptr)
345		{
346	5168	d_ipcl->notifyLemma(ii);
347		}
348	25693	TrustNode tlem = mkLemmaExp(ii.d_conc, exp, noExplain, d_ipcl.get());
349	51386	Trace("strings-pending") << "Process pending lemma : " << tlem.getNode()
350	25693	<< std::endl;
351
352		// Process the side effects of the inference info.
353		// Register the new skolems from this inference. We register them here
354		// (lazily), since this is the moment when we have decided to process the
355		// inference.
356	1409	for (const std::pair<const LengthStatus, std::vector<Node> >& sks :
357	25693	ii.d_skolems)
358		{
359	2818	for (const Node& n : sks.second)
360		{
361	1409	d_termReg.registerTermAtomic(n, sks.first);
362		}
363		}
364	25693	if (ii.getId() == InferenceId::STRINGS_REDUCTION)
365		{
366	2167	p \|= LemmaProperty::NEEDS_JUSTIFY;
367		}
368	51386	Trace("strings-assert") << "(assert " << tlem.getNode() << ") ; lemma "
369	25693	<< ii.getId() << std::endl;
370	51386	Trace("strings-lemma") << "Strings::Lemma: " << tlem.getNode() << " by "
371	25693	<< ii.getId() << std::endl;
372	51386	return tlem;
373		}
374
375		} // namespace strings
376		} // namespace theory
377	31125	} // namespace cvc5