Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/theory_inference_manager.cpp	Lines:	224	246	91.1 %
Date:	2021-08-06	Branches:	356	842	42.3 %


/******************************************************************************
 * 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_pfee(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 its proof equality engine has already been assigned,
  // use it. This is to ensure that all theories use the same proof equality
  // engine when in ee-mode=central.
  if (d_pnm != nullptr && d_ee != nullptr)
  {
    d_pfee = d_ee->getProofEqualityEngine();
    if (d_pfee == nullptr)
    {
      d_pfeeAlloc.reset(new eq::ProofEqEngine(d_theoryState.getSatContext(),
                                              d_theoryState.getUserContext(),
                                              *d_ee,
                                              d_pnm));
      d_pfee = d_pfeeAlloc.get();
      d_ee->setProofEqualityEngine(d_pfee);
    }
  }
}

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; }

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_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;
  // shouldn't send trivially true or false lemmas
  Assert(!Rewriter::rewrite(tlem.getProven()).isConst());
  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);
  // make the node corresponding to the explanation
  Node expn = NodeManager::currentNM()->mkAnd(exp);
  Trace("im") << "(fact " << iid << " " << (pol ? Node(atom) : atom.notNode())
              << " " << expn << ")" << std::endl;
  // 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: "
                         << (pol ? Node(atom) : atom.notNode()) << " from "
                         << expn << " / " << iid << " " << id << std::endl;
  if (Configuration::isAssertionBuild())
  {
    // check that all facts hold in the equality engine, to ensure that we
    // aren't processing a stale fact
    std::vector<Node> expc = exp;
    for (size_t i = 0; i < expc.size(); i++)
    {
      Node e = expc[i];
      bool epol = e.getKind() != NOT;
      Node eatom = epol ? e : e[0];
      Trace("infer-manager")
          << "...check " << eatom << " " << epol << std::endl;
      if (eatom.getKind() == AND)
      {
        Assert(epol);
        for (const Node& ea : eatom)
        {
          expc.push_back(ea);
        }
        continue;
      }
      else if (eatom.getKind() == EQUAL)
      {
        Assert(d_ee->hasTerm(eatom[0]));
        Assert(d_ee->hasTerm(eatom[1]));
        Assert(!epol || d_ee->areEqual(eatom[0], eatom[1]));
        Assert(epol || d_ee->areDisequal(eatom[0], eatom[1], false));
      }
      else
      {
        Assert(d_ee->hasTerm(eatom));
        Assert(d_ee->areEqual(eatom, NodeManager::currentNM()->mkConst(epol)));
      }
    }
  }
  d_numCurrentFacts++;
  // Now, assert the fact. How to do so depends on whether proofs are enabled.
  bool ret = false;
  if (d_pfee == nullptr)
  {
    Trace("infer-manager") << "...assert without proofs..." << std::endl;
    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
  {
    Assert(id != PfRule::UNKNOWN);
    Trace("infer-manager") << "...assert with proofs..." << std::endl;
    // 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, ret=" << ret
      << 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);
}

void TheoryInferenceManager::notifyInConflict()
{
  d_theoryState.notifyInConflict();
}

}  // 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	118236	TheoryInferenceManager::TheoryInferenceManager(Theory& t,
33		TheoryState& state,
34		ProofNodeManager* pnm,
35		const std::string& statsName,
36	118236	bool cacheLemmas)
37		: d_theory(t),
38		d_theoryState(state),
39	118236	d_out(t.getOutputChannel()),
40		d_ee(nullptr),
41		d_decManager(nullptr),
42		d_pfee(nullptr),
43		d_pnm(pnm),
44		d_cacheLemmas(cacheLemmas),
45		d_keep(t.getSatContext()),
46	118236	d_lemmasSent(t.getUserContext()),
47		d_numConflicts(0),
48		d_numCurrentLemmas(0),
49		d_numCurrentFacts(0),
50	118236	d_conflictIdStats(smtStatisticsRegistry().registerHistogram<InferenceId>(
51	236472	statsName + "inferencesConflict")),
52	118236	d_factIdStats(smtStatisticsRegistry().registerHistogram<InferenceId>(
53	236472	statsName + "inferencesFact")),
54	118236	d_lemmaIdStats(smtStatisticsRegistry().registerHistogram<InferenceId>(
55	709416	statsName + "inferencesLemma"))
56		{
57		// don't add true lemma
58	236472	Node truen = NodeManager::currentNM()->mkConst(true);
59	118236	d_lemmasSent.insert(truen);
60	118236	}
61
62	118236	TheoryInferenceManager::~TheoryInferenceManager()
63		{
64	118236	}
65
66	118236	void TheoryInferenceManager::setEqualityEngine(eq::EqualityEngine* ee)
67		{
68	118236	d_ee = ee;
69		// if proofs are enabled, also make a proof equality engine to wrap ee
70		// if it is non-null. If its proof equality engine has already been assigned,
71		// use it. This is to ensure that all theories use the same proof equality
72		// engine when in ee-mode=central.
73	118236	if (d_pnm != nullptr && d_ee != nullptr)
74		{
75	11959	d_pfee = d_ee->getProofEqualityEngine();
76	11959	if (d_pfee == nullptr)
77		{
78	23792	d_pfeeAlloc.reset(new eq::ProofEqEngine(d_theoryState.getSatContext(),
79	11896	d_theoryState.getUserContext(),
80	11896	*d_ee,
81	23792	d_pnm));
82	11896	d_pfee = d_pfeeAlloc.get();
83	11896	d_ee->setProofEqualityEngine(d_pfee);
84		}
85		}
86	118236	}
87
88	118236	void TheoryInferenceManager::setDecisionManager(DecisionManager* dm)
89		{
90	118236	d_decManager = dm;
91	118236	}
92
93	21469	bool TheoryInferenceManager::isProofEnabled() const { return d_pnm != nullptr; }
94
95	787814	void TheoryInferenceManager::reset()
96		{
97	787814	d_numConflicts = 0;
98	787814	d_numCurrentLemmas = 0;
99	787814	d_numCurrentFacts = 0;
100	787814	}
101
102	217614	bool TheoryInferenceManager::hasSent() const
103		{
104	435228	return d_theoryState.isInConflict() \|\| d_numCurrentLemmas > 0
105	425658	\|\| d_numCurrentFacts > 0;
106		}
107
108		eq::ProofEqEngine* TheoryInferenceManager::getProofEqEngine() { return d_pfee; }
109
110	12926	void TheoryInferenceManager::conflictEqConstantMerge(TNode a, TNode b)
111		{
112	12926	if (!d_theoryState.isInConflict())
113		{
114	25690	TrustNode tconf = explainConflictEqConstantMerge(a, b);
115	12845	trustedConflict(tconf, InferenceId::EQ_CONSTANT_MERGE);
116		}
117	12926	}
118
119	78961	void TheoryInferenceManager::conflict(TNode conf, InferenceId id)
120		{
121	157922	TrustNode tconf = TrustNode::mkTrustConflict(conf, nullptr);
122	157922	return trustedConflict(tconf, id);
123		}
124
125	107863	void TheoryInferenceManager::trustedConflict(TrustNode tconf, InferenceId id)
126		{
127	107863	d_conflictIdStats << id;
128	107863	smt::currentResourceManager()->spendResource(id);
129	215726	Trace("im") << "(conflict " << id << " " << tconf.getProven() << ")"
130	107863	<< std::endl;
131	107863	d_out.trustedConflict(tconf);
132	107863	++d_numConflicts;
133	107863	}
134
135	8	void TheoryInferenceManager::conflictExp(InferenceId id,
136		PfRule pfr,
137		const std::vector<Node>& exp,
138		const std::vector<Node>& args)
139		{
140	8	if (!d_theoryState.isInConflict())
141		{
142		// make the trust node
143	16	TrustNode tconf = mkConflictExp(pfr, exp, args);
144		// send it on the output channel
145	8	trustedConflict(tconf, id);
146		}
147	8	}
148
149	8	TrustNode TheoryInferenceManager::mkConflictExp(PfRule id,
150		const std::vector<Node>& exp,
151		const std::vector<Node>& args)
152		{
153	8	if (d_pfee != nullptr)
154		{
155		// use proof equality engine to construct the trust node
156	2	return d_pfee->assertConflict(id, exp, args);
157		}
158		// version without proofs
159	12	Node conf = mkExplainPartial(exp, {});
160	6	return TrustNode::mkTrustConflict(conf, nullptr);
161		}
162
163	2497	void TheoryInferenceManager::conflictExp(InferenceId id,
164		const std::vector<Node>& exp,
165		ProofGenerator* pg)
166		{
167	2497	if (!d_theoryState.isInConflict())
168		{
169		// make the trust node
170	4768	TrustNode tconf = mkConflictExp(exp, pg);
171		// send it on the output channel
172	2384	trustedConflict(tconf, id);
173		}
174	2497	}
175
176	4002	TrustNode TheoryInferenceManager::mkConflictExp(const std::vector<Node>& exp,
177		ProofGenerator* pg)
178		{
179	4002	if (d_pfee != nullptr)
180		{
181	436	Assert(pg != nullptr);
182		// use proof equality engine to construct the trust node
183	436	return d_pfee->assertConflict(exp, pg);
184		}
185		// version without proofs
186	7132	Node conf = mkExplainPartial(exp, {});
187	3566	return TrustNode::mkTrustConflict(conf, nullptr);
188		}
189
190	9565754	bool TheoryInferenceManager::propagateLit(TNode lit)
191		{
192		// If already in conflict, no more propagation
193	9565754	if (d_theoryState.isInConflict())
194		{
195	1475	return false;
196		}
197		// Propagate out
198	9564279	bool ok = d_out.propagate(lit);
199	9564279	if (!ok)
200		{
201	62325	d_theoryState.notifyInConflict();
202		}
203	9564279	return ok;
204		}
205
206	211085	TrustNode TheoryInferenceManager::explainLit(TNode lit)
207		{
208	211085	if (d_pfee != nullptr)
209		{
210	33287	return d_pfee->explain(lit);
211		}
212	177798	if (d_ee != nullptr)
213		{
214	355596	Node exp = d_ee->mkExplainLit(lit);
215	177798	return TrustNode::mkTrustPropExp(lit, exp, nullptr);
216		}
217		Unimplemented() << "Inference manager for " << d_theory.getId()
218		<< " was asked to explain a propagation but doesn't have an "
219		"equality engine or implement the "
220		"TheoryInferenceManager::explainLit interface!";
221		}
222
223	12845	TrustNode TheoryInferenceManager::explainConflictEqConstantMerge(TNode a,
224		TNode b)
225		{
226	25690	Node lit = a.eqNode(b);
227	12845	if (d_pfee != nullptr)
228		{
229	1540	return d_pfee->assertConflict(lit);
230		}
231	11305	if (d_ee != nullptr)
232		{
233	22610	Node conf = d_ee->mkExplainLit(lit);
234	11305	return TrustNode::mkTrustConflict(conf, nullptr);
235		}
236		Unimplemented() << "Inference manager for " << d_theory.getId()
237		<< " mkTrustedConflictEqConstantMerge";
238		}
239
240	1218327	bool TheoryInferenceManager::lemma(TNode lem, InferenceId id, LemmaProperty p)
241		{
242	2436653	TrustNode tlem = TrustNode::mkTrustLemma(lem, nullptr);
243	2436653	return trustedLemma(tlem, id, p);
244		}
245
246	1588514	bool TheoryInferenceManager::trustedLemma(const TrustNode& tlem,
247		InferenceId id,
248		LemmaProperty p)
249		{
250		// if the policy says to cache lemmas, check the cache and return false if
251		// we are a duplicate
252	1588514	if (d_cacheLemmas)
253		{
254	1533256	if (!cacheLemma(tlem.getNode(), p))
255		{
256	1280344	return false;
257		}
258		}
259	308170	d_lemmaIdStats << id;
260	308170	smt::currentResourceManager()->spendResource(id);
261	308170	Trace("im") << "(lemma " << id << " " << tlem.getProven() << ")" << std::endl;
262		// shouldn't send trivially true or false lemmas
263	308170	Assert(!Rewriter::rewrite(tlem.getProven()).isConst());
264	308170	d_numCurrentLemmas++;
265	308172	d_out.trustedLemma(tlem, p);
266	308168	return true;
267		}
268
269		bool TheoryInferenceManager::lemmaExp(Node conc,
270		InferenceId id,
271		PfRule pfr,
272		const std::vector<Node>& exp,
273		const std::vector<Node>& noExplain,
274		const std::vector<Node>& args,
275		LemmaProperty p)
276		{
277		// make the trust node
278		TrustNode trn = mkLemmaExp(conc, pfr, exp, noExplain, args);
279		// send it on the output channel
280		return trustedLemma(trn, id, p);
281		}
282
283	386	TrustNode TheoryInferenceManager::mkLemmaExp(Node conc,
284		PfRule id,
285		const std::vector<Node>& exp,
286		const std::vector<Node>& noExplain,
287		const std::vector<Node>& args)
288		{
289	386	if (d_pfee != nullptr)
290		{
291		// make the trust node from the proof equality engine
292	51	return d_pfee->assertLemma(conc, id, exp, noExplain, args);
293		}
294		// otherwise, not using proofs, explain and make trust node
295	670	Node ant = mkExplainPartial(exp, noExplain);
296	670	Node lem = NodeManager::currentNM()->mkNode(kind::IMPLIES, ant, conc);
297	335	return TrustNode::mkTrustLemma(lem, nullptr);
298		}
299
300		bool TheoryInferenceManager::lemmaExp(Node conc,
301		InferenceId id,
302		const std::vector<Node>& exp,
303		const std::vector<Node>& noExplain,
304		ProofGenerator* pg,
305		LemmaProperty p)
306		{
307		// make the trust node
308		TrustNode trn = mkLemmaExp(conc, exp, noExplain, pg);
309		// send it on the output channel
310		return trustedLemma(trn, id, p);
311		}
312
313	21422	TrustNode TheoryInferenceManager::mkLemmaExp(Node conc,
314		const std::vector<Node>& exp,
315		const std::vector<Node>& noExplain,
316		ProofGenerator* pg)
317		{
318	21422	if (d_pfee != nullptr)
319		{
320		// make the trust node from the proof equality engine
321	2069	return d_pfee->assertLemma(conc, exp, noExplain, pg);
322		}
323		// otherwise, not using proofs, explain and make trust node
324	38706	Node ant = mkExplainPartial(exp, noExplain);
325	38706	Node lem = NodeManager::currentNM()->mkNode(kind::IMPLIES, ant, conc);
326	19353	return TrustNode::mkTrustLemma(lem, nullptr);
327		}
328
329	121395	bool TheoryInferenceManager::hasCachedLemma(TNode lem, LemmaProperty p)
330		{
331	242790	Node rewritten = Rewriter::rewrite(lem);
332	242790	return d_lemmasSent.find(rewritten) != d_lemmasSent.end();
333		}
334
335		uint32_t TheoryInferenceManager::numSentLemmas() const
336		{
337		return d_numCurrentLemmas;
338		}
339
340	550935	bool TheoryInferenceManager::hasSentLemma() const
341		{
342	550935	return d_numCurrentLemmas != 0;
343		}
344
345	14619	bool TheoryInferenceManager::assertInternalFact(TNode atom,
346		bool pol,
347		InferenceId id,
348		TNode exp)
349		{
350	43857	return processInternalFact(
351	43857	atom, pol, id, PfRule::UNKNOWN, {exp}, {}, nullptr);
352		}
353
354	27959	bool TheoryInferenceManager::assertInternalFact(TNode atom,
355		bool pol,
356		InferenceId id,
357		PfRule pfr,
358		const std::vector<Node>& exp,
359		const std::vector<Node>& args)
360		{
361	27959	Assert(pfr != PfRule::UNKNOWN);
362	27959	return processInternalFact(atom, pol, id, pfr, exp, args, nullptr);
363		}
364
365	318943	bool TheoryInferenceManager::assertInternalFact(TNode atom,
366		bool pol,
367		InferenceId id,
368		const std::vector<Node>& exp,
369		ProofGenerator* pg)
370		{
371	318943	return processInternalFact(atom, pol, id, PfRule::ASSUME, exp, {}, pg);
372		}
373
374	361521	bool TheoryInferenceManager::processInternalFact(TNode atom,
375		bool pol,
376		InferenceId iid,
377		PfRule id,
378		const std::vector<Node>& exp,
379		const std::vector<Node>& args,
380		ProofGenerator* pg)
381		{
382	361521	d_factIdStats << iid;
383	361521	smt::currentResourceManager()->spendResource(iid);
384		// make the node corresponding to the explanation
385	723042	Node expn = NodeManager::currentNM()->mkAnd(exp);
386	723042	Trace("im") << "(fact " << iid << " " << (pol ? Node(atom) : atom.notNode())
387	361521	<< " " << expn << ")" << std::endl;
388		// call the pre-notify fact method with preReg = false, isInternal = true
389	361521	if (d_theory.preNotifyFact(atom, pol, expn, false, true))
390		{
391		// Handled in a theory-specific way that doesn't require equality engine,
392		// notice we return true, indicating that the fact was processed.
393		return true;
394		}
395	361521	Assert(d_ee != nullptr);
396	723042	Trace("infer-manager") << "TheoryInferenceManager::assertInternalFact: "
397	723042	<< (pol ? Node(atom) : atom.notNode()) << " from "
398	361521	<< expn << " / " << iid << " " << id << std::endl;
399	361521	if (Configuration::isAssertionBuild())
400		{
401		// check that all facts hold in the equality engine, to ensure that we
402		// aren't processing a stale fact
403	723042	std::vector<Node> expc = exp;
404	900998	for (size_t i = 0; i < expc.size(); i++)
405		{
406	1046511	Node e = expc[i];
407	539477	bool epol = e.getKind() != NOT;
408	1046511	Node eatom = epol ? e : e[0];
409	1078954	Trace("infer-manager")
410	539477	<< "...check " << eatom << " " << epol << std::endl;
411	539477	if (eatom.getKind() == AND)
412		{
413	32443	Assert(epol);
414	219334	for (const Node& ea : eatom)
415		{
416	186891	expc.push_back(ea);
417		}
418	32443	continue;
419		}
420	507034	else if (eatom.getKind() == EQUAL)
421		{
422	214434	Assert(d_ee->hasTerm(eatom[0]));
423	214434	Assert(d_ee->hasTerm(eatom[1]));
424	214434	Assert(!epol \|\| d_ee->areEqual(eatom[0], eatom[1]));
425	214434	Assert(epol \|\| d_ee->areDisequal(eatom[0], eatom[1], false));
426		}
427		else
428		{
429	292600	Assert(d_ee->hasTerm(eatom));
430	292600	Assert(d_ee->areEqual(eatom, NodeManager::currentNM()->mkConst(epol)));
431		}
432		}
433		}
434	361521	d_numCurrentFacts++;
435		// Now, assert the fact. How to do so depends on whether proofs are enabled.
436	361521	bool ret = false;
437	361521	if (d_pfee == nullptr)
438		{
439	344719	Trace("infer-manager") << "...assert without proofs..." << std::endl;
440	344719	if (atom.getKind() == kind::EQUAL)
441		{
442	290546	ret = d_ee->assertEquality(atom, pol, expn);
443		}
444		else
445		{
446	54173	ret = d_ee->assertPredicate(atom, pol, expn);
447		}
448		// Must reference count the equality and its explanation, which is not done
449		// by the equality engine. Notice that we do not need to do this for
450		// external assertions, which enter as facts in theory check. This is also
451		// not done if we are asserting to the proof equality engine, which does
452		// this caching itself within ProofEqEngine::assertFact.
453	344719	d_keep.insert(atom);
454	344719	d_keep.insert(expn);
455		}
456		else
457		{
458	16802	Assert(id != PfRule::UNKNOWN);
459	16802	Trace("infer-manager") << "...assert with proofs..." << std::endl;
460		// Note that we reconstruct the original literal lit here, since both the
461		// original literal is needed for bookkeeping proofs. It is possible to
462		// optimize this so that a few less nodes are created, but at the cost
463		// of a more verbose interface to proof equality engine.
464	33604	Node lit = pol ? Node(atom) : atom.notNode();
465	16802	if (pg != nullptr)
466		{
467		// use the proof generator interface
468	15183	ret = d_pfee->assertFact(lit, expn, pg);
469		}
470		else
471		{
472		// use the explict proof step interface
473	1619	ret = d_pfee->assertFact(lit, id, expn, args);
474		}
475		}
476		// call the notify fact method with isInternal = true
477	361521	d_theory.notifyFact(atom, pol, expn, true);
478	723042	Trace("infer-manager")
479	361521	<< "TheoryInferenceManager::finished assertInternalFact, ret=" << ret
480	361521	<< std::endl;
481	361521	return ret;
482		}
483
484	43505	void TheoryInferenceManager::explain(TNode n, std::vector<TNode>& assumptions)
485		{
486	43505	if (n.getKind() == kind::AND)
487		{
488		for (const Node& nc : n)
489		{
490		d_ee->explainLit(nc, assumptions);
491		}
492		}
493		else
494		{
495	43505	d_ee->explainLit(n, assumptions);
496		}
497	43505	}
498
499		Node TheoryInferenceManager::mkExplain(TNode n)
500		{
501		std::vector<TNode> assumptions;
502		explain(n, assumptions);
503		return NodeManager::currentNM()->mkAnd(assumptions);
504		}
505
506	23260	Node TheoryInferenceManager::mkExplainPartial(
507		const std::vector<Node>& exp, const std::vector<Node>& noExplain)
508		{
509	46520	std::vector<TNode> assumps;
510	71084	for (const Node& e : exp)
511		{
512	52143	if (std::find(noExplain.begin(), noExplain.end(), e) != noExplain.end())
513		{
514	4319	if (std::find(assumps.begin(), assumps.end(), e) == assumps.end())
515		{
516		// a non-explained literal
517	4319	assumps.push_back(e);
518		}
519	4319	continue;
520		}
521		// otherwise, explain it
522	43505	explain(e, assumps);
523		}
524	46520	return NodeManager::currentNM()->mkAnd(assumps);
525		}
526
527		uint32_t TheoryInferenceManager::numSentFacts() const
528		{
529		return d_numCurrentFacts;
530		}
531
532	69813	bool TheoryInferenceManager::hasSentFact() const
533		{
534	69813	return d_numCurrentFacts != 0;
535		}
536
537	1533256	bool TheoryInferenceManager::cacheLemma(TNode lem, LemmaProperty p)
538		{
539	3066512	Node rewritten = Rewriter::rewrite(lem);
540	1533256	if (d_lemmasSent.find(rewritten) != d_lemmasSent.end())
541		{
542	1280344	return false;
543		}
544	252912	d_lemmasSent.insert(rewritten);
545	252912	return true;
546		}
547
548	13904	DecisionManager* TheoryInferenceManager::getDecisionManager()
549		{
550	13904	return d_decManager;
551		}
552
553	31532	void TheoryInferenceManager::requirePhase(TNode n, bool pol)
554		{
555	31532	return d_out.requirePhase(n, pol);
556		}
557
558	12	void TheoryInferenceManager::spendResource(Resource r)
559		{
560	12	d_out.spendResource(r);
561	12	}
562
563	159598	void TheoryInferenceManager::safePoint(Resource r)
564		{
565	159598	d_out.safePoint(r);
566	159598	}
567
568	2174	void TheoryInferenceManager::setIncomplete(IncompleteId id)
569		{
570	2174	d_out.setIncomplete(id);
571	2174	}
572
573	961260	void TheoryInferenceManager::notifyInConflict()
574		{
575	961260	d_theoryState.notifyInConflict();
576	961260	}
577
578		} // namespace theory
579	29322	} // namespace cvc5