Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/theory_inference_manager.cpp	Lines:	219	244	89.8 %
Date:	2021-11-06	Branches:	359	844	42.5 %


/******************************************************************************
 * 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_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(Env& env,
                                               Theory& t,
                                               TheoryState& state,
                                               const std::string& statsName,
                                               bool cacheLemmas)
    : EnvObj(env),
      d_theory(t),
      d_theoryState(state),
      d_out(t.getOutputChannel()),
      d_ee(nullptr),
      d_decManager(nullptr),
      d_pfee(nullptr),
      d_cacheLemmas(cacheLemmas),
      d_keep(context()),
      d_lemmasSent(userContext()),
      d_numConflicts(0),
      d_numCurrentLemmas(0),
      d_numCurrentFacts(0),
      d_conflictIdStats(statisticsRegistry().registerHistogram<InferenceId>(
          statsName + "inferencesConflict")),
      d_factIdStats(statisticsRegistry().registerHistogram<InferenceId>(
          statsName + "inferencesFact")),
      d_lemmaIdStats(statisticsRegistry().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 (isProofEnabled() && d_ee != nullptr)
  {
    d_pfee = d_ee->getProofEqualityEngine();
    if (d_pfee == nullptr)
    {
      d_pfeeAlloc = std::make_unique<eq::ProofEqEngine>(d_env, *d_ee);
      d_pfee = d_pfeeAlloc.get();
      d_ee->setProofEqualityEngine(d_pfee);
    }
  }
}

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

bool TheoryInferenceManager::isProofEnabled() const
{
  return d_env.isTheoryProofProducing();
}

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