Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/theory_inference_manager.cpp	Lines:	178	215	82.8 %
Date:	2021-05-24	Branches:	217	518	41.9 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Gereon Kremer, Mathias Preiner
 *
 * 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.
 * ****************************************************************************
 *
 * An inference manager for Theory.
 */

#include "theory/theory_inference_manager.h"

#include "smt/smt_engine_scope.h"
#include "smt/smt_statistics_registry.h"
#include "theory/output_channel.h"
#include "theory/rewriter.h"
#include "theory/theory.h"
#include "theory/theory_state.h"
#include "theory/uf/equality_engine.h"
#include "theory/uf/proof_equality_engine.h"

using namespace cvc5::kind;

namespace cvc5 {
namespace theory {

TheoryInferenceManager::TheoryInferenceManager(Theory& t,
                                               TheoryState& state,
                                               ProofNodeManager* pnm,
                                               const std::string& statsName,
                                               bool cacheLemmas)
    : d_theory(t),
      d_theoryState(state),
      d_out(t.getOutputChannel()),
      d_ee(nullptr),
      d_decManager(nullptr),
      d_pnm(pnm),
      d_cacheLemmas(cacheLemmas),
      d_keep(t.getSatContext()),
      d_lemmasSent(t.getUserContext()),
      d_numConflicts(0),
      d_numCurrentLemmas(0),
      d_numCurrentFacts(0),
      d_conflictIdStats(smtStatisticsRegistry().registerHistogram<InferenceId>(
          statsName + "inferencesConflict")),
      d_factIdStats(smtStatisticsRegistry().registerHistogram<InferenceId>(
          statsName + "inferencesFact")),
      d_lemmaIdStats(smtStatisticsRegistry().registerHistogram<InferenceId>(
          statsName + "inferencesLemma"))
{
  // don't add true lemma
  Node truen = NodeManager::currentNM()->mkConst(true);
  d_lemmasSent.insert(truen);
}

TheoryInferenceManager::~TheoryInferenceManager()
{
}

void TheoryInferenceManager::setEqualityEngine(eq::EqualityEngine* ee)
{
  d_ee = ee;
  // if proofs are enabled, also make a proof equality engine to wrap ee
  // if it is non-null
  if (d_pnm != nullptr && d_ee != nullptr)
  {
    d_pfee.reset(new eq::ProofEqEngine(d_theoryState.getSatContext(),
                                       d_theoryState.getUserContext(),
                                       *d_ee,
                                       d_pnm));
  }
}

void TheoryInferenceManager::setDecisionManager(DecisionManager* dm)
{
  d_decManager = dm;
}

bool TheoryInferenceManager::isProofEnabled() const { return d_pnm != nullptr; }

void TheoryInferenceManager::reset()
{
  d_numConflicts = 0;
  d_numCurrentLemmas = 0;
  d_numCurrentFacts = 0;
}

bool TheoryInferenceManager::hasSent() const
{
  return d_theoryState.isInConflict() || d_numCurrentLemmas > 0
         || d_numCurrentFacts > 0;
}

eq::ProofEqEngine* TheoryInferenceManager::getProofEqEngine()
{
  return d_pfee.get();
}

void TheoryInferenceManager::conflictEqConstantMerge(TNode a, TNode b)
{
  if (!d_theoryState.isInConflict())
  {
    TrustNode tconf = explainConflictEqConstantMerge(a, b);
    trustedConflict(tconf, InferenceId::EQ_CONSTANT_MERGE);
  }
}

void TheoryInferenceManager::conflict(TNode conf, InferenceId id)
{
  TrustNode tconf = TrustNode::mkTrustConflict(conf, nullptr);
  return trustedConflict(tconf, id);
}

void TheoryInferenceManager::trustedConflict(TrustNode tconf, InferenceId id)
{
  d_conflictIdStats << id;
  smt::currentResourceManager()->spendResource(id);
  Trace("im") << "(conflict " << id << " " << tconf.getProven() << ")"
              << std::endl;
  d_theoryState.notifyInConflict();
  d_out.trustedConflict(tconf);
  ++d_numConflicts;
}

void TheoryInferenceManager::conflictExp(InferenceId id,
                                         PfRule pfr,
                                         const std::vector<Node>& exp,
                                         const std::vector<Node>& args)
{
  if (!d_theoryState.isInConflict())
  {
    // make the trust node
    TrustNode tconf = mkConflictExp(pfr, exp, args);
    // send it on the output channel
    trustedConflict(tconf, id);
  }
}

TrustNode TheoryInferenceManager::mkConflictExp(PfRule id,
                                                const std::vector<Node>& exp,
                                                const std::vector<Node>& args)
{
  if (d_pfee != nullptr)
  {
    // use proof equality engine to construct the trust node
    return d_pfee->assertConflict(id, exp, args);
  }
  // version without proofs
  Node conf = mkExplainPartial(exp, {});
  return TrustNode::mkTrustConflict(conf, nullptr);
}

void TheoryInferenceManager::conflictExp(InferenceId id,
                                         const std::vector<Node>& exp,
                                         ProofGenerator* pg)
{
  if (!d_theoryState.isInConflict())
  {
    // make the trust node
    TrustNode tconf = mkConflictExp(exp, pg);
    // send it on the output channel
    trustedConflict(tconf, id);
  }
}

TrustNode TheoryInferenceManager::mkConflictExp(const std::vector<Node>& exp,
                                                ProofGenerator* pg)
{
  if (d_pfee != nullptr)
  {
    Assert(pg != nullptr);
    // use proof equality engine to construct the trust node
    return d_pfee->assertConflict(exp, pg);
  }
  // version without proofs
  Node conf = mkExplainPartial(exp, {});
  return TrustNode::mkTrustConflict(conf, nullptr);
}

bool TheoryInferenceManager::propagateLit(TNode lit)
{
  // If already in conflict, no more propagation
  if (d_theoryState.isInConflict())
  {
    return false;
  }
  // Propagate out
  bool ok = d_out.propagate(lit);
  if (!ok)
  {
    d_theoryState.notifyInConflict();
  }
  return ok;
}

TrustNode TheoryInferenceManager::explainLit(TNode lit)
{
  if (d_pfee != nullptr)
  {
    return d_pfee->explain(lit);
  }
  if (d_ee != nullptr)
  {
    Node exp = d_ee->mkExplainLit(lit);
    return TrustNode::mkTrustPropExp(lit, exp, nullptr);
  }
  Unimplemented() << "Inference manager for " << d_theory.getId()
                  << " was asked to explain a propagation but doesn't have an "
                     "equality engine or implement the "
                     "TheoryInferenceManager::explainLit interface!";
}

TrustNode TheoryInferenceManager::explainConflictEqConstantMerge(TNode a,
                                                                 TNode b)
{
  Node lit = a.eqNode(b);
  if (d_pfee != nullptr)
  {
    return d_pfee->assertConflict(lit);
  }
  if (d_ee != nullptr)
  {
    Node conf = d_ee->mkExplainLit(lit);
    return TrustNode::mkTrustConflict(conf, nullptr);
  }
  Unimplemented() << "Inference manager for " << d_theory.getId()
                  << " mkTrustedConflictEqConstantMerge";
}

bool TheoryInferenceManager::lemma(TNode lem, InferenceId id, LemmaProperty p)
{
  TrustNode tlem = TrustNode::mkTrustLemma(lem, nullptr);
  return trustedLemma(tlem, id, p);
}

bool TheoryInferenceManager::trustedLemma(const TrustNode& tlem,
                                          InferenceId id,
                                          LemmaProperty p)
{
  // if the policy says to cache lemmas, check the cache and return false if
  // we are a duplicate
  if (d_cacheLemmas)
  {
    if (!cacheLemma(tlem.getNode(), p))
    {
      return false;
    }
  }
  d_lemmaIdStats << id;
  smt::currentResourceManager()->spendResource(id);
  Trace("im") << "(lemma " << id << " " << tlem.getProven() << ")" << std::endl;
  d_numCurrentLemmas++;
  d_out.trustedLemma(tlem, p);
  return true;
}

bool TheoryInferenceManager::lemmaExp(Node conc,
                                      InferenceId id,
                                      PfRule pfr,
                                      const std::vector<Node>& exp,
                                      const std::vector<Node>& noExplain,
                                      const std::vector<Node>& args,
                                      LemmaProperty p)
{
  // make the trust node
  TrustNode trn = mkLemmaExp(conc, pfr, exp, noExplain, args);
  // send it on the output channel
  return trustedLemma(trn, id, p);
}

TrustNode TheoryInferenceManager::mkLemmaExp(Node conc,
                                             PfRule id,
                                             const std::vector<Node>& exp,
                                             const std::vector<Node>& noExplain,
                                             const std::vector<Node>& args)
{
  if (d_pfee != nullptr)
  {
    // make the trust node from the proof equality engine
    return d_pfee->assertLemma(conc, id, exp, noExplain, args);
  }
  // otherwise, not using proofs, explain and make trust node
  Node ant = mkExplainPartial(exp, noExplain);
  Node lem = NodeManager::currentNM()->mkNode(kind::IMPLIES, ant, conc);
  return TrustNode::mkTrustLemma(lem, nullptr);
}

bool TheoryInferenceManager::lemmaExp(Node conc,
                                      InferenceId id,
                                      const std::vector<Node>& exp,
                                      const std::vector<Node>& noExplain,
                                      ProofGenerator* pg,
                                      LemmaProperty p)
{
  // make the trust node
  TrustNode trn = mkLemmaExp(conc, exp, noExplain, pg);
  // send it on the output channel
  return trustedLemma(trn, id, p);
}

TrustNode TheoryInferenceManager::mkLemmaExp(Node conc,
                                             const std::vector<Node>& exp,
                                             const std::vector<Node>& noExplain,
                                             ProofGenerator* pg)
{
  if (d_pfee != nullptr)
  {
    // make the trust node from the proof equality engine
    return d_pfee->assertLemma(conc, exp, noExplain, pg);
  }
  // otherwise, not using proofs, explain and make trust node
  Node ant = mkExplainPartial(exp, noExplain);
  Node lem = NodeManager::currentNM()->mkNode(kind::IMPLIES, ant, conc);
  return TrustNode::mkTrustLemma(lem, nullptr);
}

bool TheoryInferenceManager::hasCachedLemma(TNode lem, LemmaProperty p)
{
  Node rewritten = Rewriter::rewrite(lem);
  return d_lemmasSent.find(rewritten) != d_lemmasSent.end();
}

uint32_t TheoryInferenceManager::numSentLemmas() const
{
  return d_numCurrentLemmas;
}

bool TheoryInferenceManager::hasSentLemma() const
{
  return d_numCurrentLemmas != 0;
}

bool TheoryInferenceManager::assertInternalFact(TNode atom,
                                                bool pol,
                                                InferenceId id,
                                                TNode exp)
{
  return processInternalFact(
      atom, pol, id, PfRule::UNKNOWN, {exp}, {}, nullptr);
}

bool TheoryInferenceManager::assertInternalFact(TNode atom,
                                                bool pol,
                                                InferenceId id,
                                                PfRule pfr,
                                                const std::vector<Node>& exp,
                                                const std::vector<Node>& args)
{
  Assert(pfr != PfRule::UNKNOWN);
  return processInternalFact(atom, pol, id, pfr, exp, args, nullptr);
}

bool TheoryInferenceManager::assertInternalFact(TNode atom,
                                                bool pol,
                                                InferenceId id,
                                                const std::vector<Node>& exp,
                                                ProofGenerator* pg)
{
  return processInternalFact(atom, pol, id, PfRule::ASSUME, exp, {}, pg);
}

bool TheoryInferenceManager::processInternalFact(TNode atom,
                                                 bool pol,
                                                 InferenceId iid,
                                                 PfRule id,
                                                 const std::vector<Node>& exp,
                                                 const std::vector<Node>& args,
                                                 ProofGenerator* pg)
{
  d_factIdStats << iid;
  smt::currentResourceManager()->spendResource(iid);
  Trace("im") << "(fact " << iid << " " << (pol ? Node(atom) : atom.notNode())
              << ")" << std::endl;
  // make the node corresponding to the explanation
  Node expn = NodeManager::currentNM()->mkAnd(exp);
  // call the pre-notify fact method with preReg = false, isInternal = true
  if (d_theory.preNotifyFact(atom, pol, expn, false, true))
  {
    // Handled in a theory-specific way that doesn't require equality engine,
    // notice we return true, indicating that the fact was processed.
    return true;
  }
  Assert(d_ee != nullptr);
  Trace("infer-manager") << "TheoryInferenceManager::assertInternalFact: "
                         << expn << std::endl;
  d_numCurrentFacts++;
  // Now, assert the fact. How to do so depends on whether proofs are enabled.
  // If no proof production, or no proof rule was given
  bool ret = false;
  if (d_pfee == nullptr || id == PfRule::UNKNOWN)
  {
    if (atom.getKind() == kind::EQUAL)
    {
      ret = d_ee->assertEquality(atom, pol, expn);
    }
    else
    {
      ret = d_ee->assertPredicate(atom, pol, expn);
    }
    // Must reference count the equality and its explanation, which is not done
    // by the equality engine. Notice that we do *not* need to do this for
    // external assertions, which enter as facts in theory check. This is also
    // not done if we are asserting to the proof equality engine, which does
    // this caching itself within ProofEqEngine::assertFact.
    d_keep.insert(atom);
    d_keep.insert(expn);
  }
  else
  {
    // Note that we reconstruct the original literal lit here, since both the
    // original literal is needed for bookkeeping proofs. It is possible to
    // optimize this so that a few less nodes are created, but at the cost
    // of a more verbose interface to proof equality engine.
    Node lit = pol ? Node(atom) : atom.notNode();
    if (pg != nullptr)
    {
      // use the proof generator interface
      ret = d_pfee->assertFact(lit, expn, pg);
    }
    else
    {
      // use the explict proof step interface
      ret = d_pfee->assertFact(lit, id, expn, args);
    }
  }
  // call the notify fact method with isInternal = true
  d_theory.notifyFact(atom, pol, expn, true);
  Trace("infer-manager")
      << "TheoryInferenceManager::finished assertInternalFact" << std::endl;
  return ret;
}

void TheoryInferenceManager::explain(TNode n, std::vector<TNode>& assumptions)
{
  if (n.getKind() == kind::AND)
  {
    for (const Node& nc : n)
    {
      d_ee->explainLit(nc, assumptions);
    }
  }
  else
  {
    d_ee->explainLit(n, assumptions);
  }
}

Node TheoryInferenceManager::mkExplain(TNode n)
{
  std::vector<TNode> assumptions;
  explain(n, assumptions);
  return NodeManager::currentNM()->mkAnd(assumptions);
}

Node TheoryInferenceManager::mkExplainPartial(
    const std::vector<Node>& exp, const std::vector<Node>& noExplain)
{
  std::vector<TNode> assumps;
  for (const Node& e : exp)
  {
    if (std::find(noExplain.begin(), noExplain.end(), e) != noExplain.end())
    {
      if (std::find(assumps.begin(), assumps.end(), e) == assumps.end())
      {
        // a non-explained literal
        assumps.push_back(e);
      }
      continue;
    }
    // otherwise, explain it
    explain(e, assumps);
  }
  return NodeManager::currentNM()->mkAnd(assumps);
}

uint32_t TheoryInferenceManager::numSentFacts() const
{
  return d_numCurrentFacts;
}

bool TheoryInferenceManager::hasSentFact() const
{
  return d_numCurrentFacts != 0;
}

bool TheoryInferenceManager::cacheLemma(TNode lem, LemmaProperty p)
{
  Node rewritten = Rewriter::rewrite(lem);
  if (d_lemmasSent.find(rewritten) != d_lemmasSent.end())
  {
    return false;
  }
  d_lemmasSent.insert(rewritten);
  return true;
}

DecisionManager* TheoryInferenceManager::getDecisionManager()
{
  return d_decManager;
}

void TheoryInferenceManager::requirePhase(TNode n, bool pol)
{
  return d_out.requirePhase(n, pol);
}

void TheoryInferenceManager::spendResource(Resource r)
{
  d_out.spendResource(r);
}

void TheoryInferenceManager::safePoint(Resource r)
{
  d_out.safePoint(r);
}

void TheoryInferenceManager::setIncomplete(IncompleteId id)
{
  d_out.setIncomplete(id);
}

}  // 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, Mathias Preiner
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		* An inference manager for Theory.
14		*/
15
16		#include "theory/theory_inference_manager.h"
17
18		#include "smt/smt_engine_scope.h"
19		#include "smt/smt_statistics_registry.h"
20		#include "theory/output_channel.h"
21		#include "theory/rewriter.h"
22		#include "theory/theory.h"
23		#include "theory/theory_state.h"
24		#include "theory/uf/equality_engine.h"
25		#include "theory/uf/proof_equality_engine.h"
26
27		using namespace cvc5::kind;
28
29		namespace cvc5 {
30		namespace theory {
31
32	104049	TheoryInferenceManager::TheoryInferenceManager(Theory& t,
33		TheoryState& state,
34		ProofNodeManager* pnm,
35		const std::string& statsName,
36	104049	bool cacheLemmas)
37		: d_theory(t),
38		d_theoryState(state),
39	104049	d_out(t.getOutputChannel()),
40		d_ee(nullptr),
41		d_decManager(nullptr),
42		d_pnm(pnm),
43		d_cacheLemmas(cacheLemmas),
44		d_keep(t.getSatContext()),
45	104049	d_lemmasSent(t.getUserContext()),
46		d_numConflicts(0),
47		d_numCurrentLemmas(0),
48		d_numCurrentFacts(0),
49	104049	d_conflictIdStats(smtStatisticsRegistry().registerHistogram<InferenceId>(
50	208098	statsName + "inferencesConflict")),
51	104049	d_factIdStats(smtStatisticsRegistry().registerHistogram<InferenceId>(
52	208098	statsName + "inferencesFact")),
53	104049	d_lemmaIdStats(smtStatisticsRegistry().registerHistogram<InferenceId>(
54	624294	statsName + "inferencesLemma"))
55		{
56		// don't add true lemma
57	208098	Node truen = NodeManager::currentNM()->mkConst(true);
58	104049	d_lemmasSent.insert(truen);
59	104049	}
60
61	104049	TheoryInferenceManager::~TheoryInferenceManager()
62		{
63	104049	}
64
65	104049	void TheoryInferenceManager::setEqualityEngine(eq::EqualityEngine* ee)
66		{
67	104049	d_ee = ee;
68		// if proofs are enabled, also make a proof equality engine to wrap ee
69		// if it is non-null
70	104049	if (d_pnm != nullptr && d_ee != nullptr)
71		{
72	15714	d_pfee.reset(new eq::ProofEqEngine(d_theoryState.getSatContext(),
73	7857	d_theoryState.getUserContext(),
74	7857	*d_ee,
75	15714	d_pnm));
76		}
77	104049	}
78
79	104049	void TheoryInferenceManager::setDecisionManager(DecisionManager* dm)
80		{
81	104049	d_decManager = dm;
82	104049	}
83
84	19097	bool TheoryInferenceManager::isProofEnabled() const { return d_pnm != nullptr; }
85
86	733071	void TheoryInferenceManager::reset()
87		{
88	733071	d_numConflicts = 0;
89	733071	d_numCurrentLemmas = 0;
90	733071	d_numCurrentFacts = 0;
91	733071	}
92
93	191034	bool TheoryInferenceManager::hasSent() const
94		{
95	382068	return d_theoryState.isInConflict() \|\| d_numCurrentLemmas > 0
96	372854	\|\| d_numCurrentFacts > 0;
97		}
98
99	9459	eq::ProofEqEngine* TheoryInferenceManager::getProofEqEngine()
100		{
101	9459	return d_pfee.get();
102		}
103
104	11305	void TheoryInferenceManager::conflictEqConstantMerge(TNode a, TNode b)
105		{
106	11305	if (!d_theoryState.isInConflict())
107		{
108	22420	TrustNode tconf = explainConflictEqConstantMerge(a, b);
109	11210	trustedConflict(tconf, InferenceId::EQ_CONSTANT_MERGE);
110		}
111	11305	}
112
113	74435	void TheoryInferenceManager::conflict(TNode conf, InferenceId id)
114		{
115	148870	TrustNode tconf = TrustNode::mkTrustConflict(conf, nullptr);
116	148870	return trustedConflict(tconf, id);
117		}
118
119	102410	void TheoryInferenceManager::trustedConflict(TrustNode tconf, InferenceId id)
120		{
121	102410	d_conflictIdStats << id;
122	102410	smt::currentResourceManager()->spendResource(id);
123	204820	Trace("im") << "(conflict " << id << " " << tconf.getProven() << ")"
124	102410	<< std::endl;
125	102410	d_theoryState.notifyInConflict();
126	102410	d_out.trustedConflict(tconf);
127	102410	++d_numConflicts;
128	102410	}
129
130		void TheoryInferenceManager::conflictExp(InferenceId id,
131		PfRule pfr,
132		const std::vector<Node>& exp,
133		const std::vector<Node>& args)
134		{
135		if (!d_theoryState.isInConflict())
136		{
137		// make the trust node
138		TrustNode tconf = mkConflictExp(pfr, exp, args);
139		// send it on the output channel
140		trustedConflict(tconf, id);
141		}
142		}
143
144		TrustNode TheoryInferenceManager::mkConflictExp(PfRule id,
145		const std::vector<Node>& exp,
146		const std::vector<Node>& args)
147		{
148		if (d_pfee != nullptr)
149		{
150		// use proof equality engine to construct the trust node
151		return d_pfee->assertConflict(id, exp, args);
152		}
153		// version without proofs
154		Node conf = mkExplainPartial(exp, {});
155		return TrustNode::mkTrustConflict(conf, nullptr);
156		}
157
158	4520	void TheoryInferenceManager::conflictExp(InferenceId id,
159		const std::vector<Node>& exp,
160		ProofGenerator* pg)
161		{
162	4520	if (!d_theoryState.isInConflict())
163		{
164		// make the trust node
165	8856	TrustNode tconf = mkConflictExp(exp, pg);
166		// send it on the output channel
167	4428	trustedConflict(tconf, id);
168		}
169	4520	}
170
171	5300	TrustNode TheoryInferenceManager::mkConflictExp(const std::vector<Node>& exp,
172		ProofGenerator* pg)
173		{
174	5300	if (d_pfee != nullptr)
175		{
176	929	Assert(pg != nullptr);
177		// use proof equality engine to construct the trust node
178	929	return d_pfee->assertConflict(exp, pg);
179		}
180		// version without proofs
181	8742	Node conf = mkExplainPartial(exp, {});
182	4371	return TrustNode::mkTrustConflict(conf, nullptr);
183		}
184
185	8423016	bool TheoryInferenceManager::propagateLit(TNode lit)
186		{
187		// If already in conflict, no more propagation
188	8423016	if (d_theoryState.isInConflict())
189		{
190	2980	return false;
191		}
192		// Propagate out
193	8420036	bool ok = d_out.propagate(lit);
194	8420036	if (!ok)
195		{
196	59919	d_theoryState.notifyInConflict();
197		}
198	8420036	return ok;
199		}
200
201	219888	TrustNode TheoryInferenceManager::explainLit(TNode lit)
202		{
203	219888	if (d_pfee != nullptr)
204		{
205	41673	return d_pfee->explain(lit);
206		}
207	178215	if (d_ee != nullptr)
208		{
209	356430	Node exp = d_ee->mkExplainLit(lit);
210	178215	return TrustNode::mkTrustPropExp(lit, exp, nullptr);
211		}
212		Unimplemented() << "Inference manager for " << d_theory.getId()
213		<< " was asked to explain a propagation but doesn't have an "
214		"equality engine or implement the "
215		"TheoryInferenceManager::explainLit interface!";
216		}
217
218	11210	TrustNode TheoryInferenceManager::explainConflictEqConstantMerge(TNode a,
219		TNode b)
220		{
221	22420	Node lit = a.eqNode(b);
222	11210	if (d_pfee != nullptr)
223		{
224	1586	return d_pfee->assertConflict(lit);
225		}
226	9624	if (d_ee != nullptr)
227		{
228	19248	Node conf = d_ee->mkExplainLit(lit);
229	9624	return TrustNode::mkTrustConflict(conf, nullptr);
230		}
231		Unimplemented() << "Inference manager for " << d_theory.getId()
232		<< " mkTrustedConflictEqConstantMerge";
233		}
234
235	449158	bool TheoryInferenceManager::lemma(TNode lem, InferenceId id, LemmaProperty p)
236		{
237	898315	TrustNode tlem = TrustNode::mkTrustLemma(lem, nullptr);
238	898315	return trustedLemma(tlem, id, p);
239		}
240
241	662020	bool TheoryInferenceManager::trustedLemma(const TrustNode& tlem,
242		InferenceId id,
243		LemmaProperty p)
244		{
245		// if the policy says to cache lemmas, check the cache and return false if
246		// we are a duplicate
247	662020	if (d_cacheLemmas)
248		{
249	619122	if (!cacheLemma(tlem.getNode(), p))
250		{
251	393254	return false;
252		}
253		}
254	268766	d_lemmaIdStats << id;
255	268766	smt::currentResourceManager()->spendResource(id);
256	268766	Trace("im") << "(lemma " << id << " " << tlem.getProven() << ")" << std::endl;
257	268766	d_numCurrentLemmas++;
258	268768	d_out.trustedLemma(tlem, p);
259	268764	return true;
260		}
261
262		bool TheoryInferenceManager::lemmaExp(Node conc,
263		InferenceId id,
264		PfRule pfr,
265		const std::vector<Node>& exp,
266		const std::vector<Node>& noExplain,
267		const std::vector<Node>& args,
268		LemmaProperty p)
269		{
270		// make the trust node
271		TrustNode trn = mkLemmaExp(conc, pfr, exp, noExplain, args);
272		// send it on the output channel
273		return trustedLemma(trn, id, p);
274		}
275
276		TrustNode TheoryInferenceManager::mkLemmaExp(Node conc,
277		PfRule id,
278		const std::vector<Node>& exp,
279		const std::vector<Node>& noExplain,
280		const std::vector<Node>& args)
281		{
282		if (d_pfee != nullptr)
283		{
284		// make the trust node from the proof equality engine
285		return d_pfee->assertLemma(conc, id, exp, noExplain, args);
286		}
287		// otherwise, not using proofs, explain and make trust node
288		Node ant = mkExplainPartial(exp, noExplain);
289		Node lem = NodeManager::currentNM()->mkNode(kind::IMPLIES, ant, conc);
290		return TrustNode::mkTrustLemma(lem, nullptr);
291		}
292
293		bool TheoryInferenceManager::lemmaExp(Node conc,
294		InferenceId id,
295		const std::vector<Node>& exp,
296		const std::vector<Node>& noExplain,
297		ProofGenerator* pg,
298		LemmaProperty p)
299		{
300		// make the trust node
301		TrustNode trn = mkLemmaExp(conc, exp, noExplain, pg);
302		// send it on the output channel
303		return trustedLemma(trn, id, p);
304		}
305
306	14969	TrustNode TheoryInferenceManager::mkLemmaExp(Node conc,
307		const std::vector<Node>& exp,
308		const std::vector<Node>& noExplain,
309		ProofGenerator* pg)
310		{
311	14969	if (d_pfee != nullptr)
312		{
313		// make the trust node from the proof equality engine
314	947	return d_pfee->assertLemma(conc, exp, noExplain, pg);
315		}
316		// otherwise, not using proofs, explain and make trust node
317	28044	Node ant = mkExplainPartial(exp, noExplain);
318	28044	Node lem = NodeManager::currentNM()->mkNode(kind::IMPLIES, ant, conc);
319	14022	return TrustNode::mkTrustLemma(lem, nullptr);
320		}
321
322	120458	bool TheoryInferenceManager::hasCachedLemma(TNode lem, LemmaProperty p)
323		{
324	240916	Node rewritten = Rewriter::rewrite(lem);
325	240916	return d_lemmasSent.find(rewritten) != d_lemmasSent.end();
326		}
327
328		uint32_t TheoryInferenceManager::numSentLemmas() const
329		{
330		return d_numCurrentLemmas;
331		}
332
333	458439	bool TheoryInferenceManager::hasSentLemma() const
334		{
335	458439	return d_numCurrentLemmas != 0;
336		}
337
338	23608	bool TheoryInferenceManager::assertInternalFact(TNode atom,
339		bool pol,
340		InferenceId id,
341		TNode exp)
342		{
343	70824	return processInternalFact(
344	70824	atom, pol, id, PfRule::UNKNOWN, {exp}, {}, nullptr);
345		}
346
347	2404	bool TheoryInferenceManager::assertInternalFact(TNode atom,
348		bool pol,
349		InferenceId id,
350		PfRule pfr,
351		const std::vector<Node>& exp,
352		const std::vector<Node>& args)
353		{
354	2404	Assert(pfr != PfRule::UNKNOWN);
355	2404	return processInternalFact(atom, pol, id, pfr, exp, args, nullptr);
356		}
357
358	303079	bool TheoryInferenceManager::assertInternalFact(TNode atom,
359		bool pol,
360		InferenceId id,
361		const std::vector<Node>& exp,
362		ProofGenerator* pg)
363		{
364	303079	return processInternalFact(atom, pol, id, PfRule::ASSUME, exp, {}, pg);
365		}
366
367	329091	bool TheoryInferenceManager::processInternalFact(TNode atom,
368		bool pol,
369		InferenceId iid,
370		PfRule id,
371		const std::vector<Node>& exp,
372		const std::vector<Node>& args,
373		ProofGenerator* pg)
374		{
375	329091	d_factIdStats << iid;
376	329091	smt::currentResourceManager()->spendResource(iid);
377	658182	Trace("im") << "(fact " << iid << " " << (pol ? Node(atom) : atom.notNode())
378	329091	<< ")" << std::endl;
379		// make the node corresponding to the explanation
380	658182	Node expn = NodeManager::currentNM()->mkAnd(exp);
381		// call the pre-notify fact method with preReg = false, isInternal = true
382	329091	if (d_theory.preNotifyFact(atom, pol, expn, false, true))
383		{
384		// Handled in a theory-specific way that doesn't require equality engine,
385		// notice we return true, indicating that the fact was processed.
386		return true;
387		}
388	329091	Assert(d_ee != nullptr);
389	658182	Trace("infer-manager") << "TheoryInferenceManager::assertInternalFact: "
390	329091	<< expn << std::endl;
391	329091	d_numCurrentFacts++;
392		// Now, assert the fact. How to do so depends on whether proofs are enabled.
393		// If no proof production, or no proof rule was given
394	329091	bool ret = false;
395	329091	if (d_pfee == nullptr \|\| id == PfRule::UNKNOWN)
396		{
397	316363	if (atom.getKind() == kind::EQUAL)
398		{
399	265920	ret = d_ee->assertEquality(atom, pol, expn);
400		}
401		else
402		{
403	50443	ret = d_ee->assertPredicate(atom, pol, expn);
404		}
405		// Must reference count the equality and its explanation, which is not done
406		// by the equality engine. Notice that we do not need to do this for
407		// external assertions, which enter as facts in theory check. This is also
408		// not done if we are asserting to the proof equality engine, which does
409		// this caching itself within ProofEqEngine::assertFact.
410	316363	d_keep.insert(atom);
411	316363	d_keep.insert(expn);
412		}
413		else
414		{
415		// Note that we reconstruct the original literal lit here, since both the
416		// original literal is needed for bookkeeping proofs. It is possible to
417		// optimize this so that a few less nodes are created, but at the cost
418		// of a more verbose interface to proof equality engine.
419	25456	Node lit = pol ? Node(atom) : atom.notNode();
420	12728	if (pg != nullptr)
421		{
422		// use the proof generator interface
423	11330	ret = d_pfee->assertFact(lit, expn, pg);
424		}
425		else
426		{
427		// use the explict proof step interface
428	1398	ret = d_pfee->assertFact(lit, id, expn, args);
429		}
430		}
431		// call the notify fact method with isInternal = true
432	329091	d_theory.notifyFact(atom, pol, expn, true);
433	658182	Trace("infer-manager")
434	329091	<< "TheoryInferenceManager::finished assertInternalFact" << std::endl;
435	329091	return ret;
436		}
437
438	33103	void TheoryInferenceManager::explain(TNode n, std::vector<TNode>& assumptions)
439		{
440	33103	if (n.getKind() == kind::AND)
441		{
442		for (const Node& nc : n)
443		{
444		d_ee->explainLit(nc, assumptions);
445		}
446		}
447		else
448		{
449	33103	d_ee->explainLit(n, assumptions);
450		}
451	33103	}
452
453		Node TheoryInferenceManager::mkExplain(TNode n)
454		{
455		std::vector<TNode> assumptions;
456		explain(n, assumptions);
457		return NodeManager::currentNM()->mkAnd(assumptions);
458		}
459
460	18393	Node TheoryInferenceManager::mkExplainPartial(
461		const std::vector<Node>& exp, const std::vector<Node>& noExplain)
462		{
463	36786	std::vector<TNode> assumps;
464	53922	for (const Node& e : exp)
465		{
466	37955	if (std::find(noExplain.begin(), noExplain.end(), e) != noExplain.end())
467		{
468	2426	if (std::find(assumps.begin(), assumps.end(), e) == assumps.end())
469		{
470		// a non-explained literal
471	2426	assumps.push_back(e);
472		}
473	2426	continue;
474		}
475		// otherwise, explain it
476	33103	explain(e, assumps);
477		}
478	36786	return NodeManager::currentNM()->mkAnd(assumps);
479		}
480
481		uint32_t TheoryInferenceManager::numSentFacts() const
482		{
483		return d_numCurrentFacts;
484		}
485
486	57194	bool TheoryInferenceManager::hasSentFact() const
487		{
488	57194	return d_numCurrentFacts != 0;
489		}
490
491	619122	bool TheoryInferenceManager::cacheLemma(TNode lem, LemmaProperty p)
492		{
493	1238244	Node rewritten = Rewriter::rewrite(lem);
494	619122	if (d_lemmasSent.find(rewritten) != d_lemmasSent.end())
495		{
496	393254	return false;
497		}
498	225868	d_lemmasSent.insert(rewritten);
499	225868	return true;
500		}
501
502	13300	DecisionManager* TheoryInferenceManager::getDecisionManager()
503		{
504	13300	return d_decManager;
505		}
506
507	23856	void TheoryInferenceManager::requirePhase(TNode n, bool pol)
508		{
509	23856	return d_out.requirePhase(n, pol);
510		}
511
512	728065	void TheoryInferenceManager::spendResource(Resource r)
513		{
514	728065	d_out.spendResource(r);
515	728065	}
516
517	22244200	void TheoryInferenceManager::safePoint(Resource r)
518		{
519	22244200	d_out.safePoint(r);
520	22244200	}
521
522	2091	void TheoryInferenceManager::setIncomplete(IncompleteId id)
523		{
524	2091	d_out.setIncomplete(id);
525	2091	}
526
527		} // namespace theory
528	28191	} // namespace cvc5