Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/inference_manager_buffered.cpp	Lines:	77	83	92.8 %
Date:	2021-05-24	Branches:	55	154	35.7 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Gereon Kremer, Aina Niemetz
 *
 * 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.
 * ****************************************************************************
 *
 * A buffered inference manager.
 */

#include "theory/inference_manager_buffered.h"

#include "theory/rewriter.h"
#include "theory/theory.h"
#include "theory/theory_state.h"

using namespace cvc5::kind;

namespace cvc5 {
namespace theory {

InferenceManagerBuffered::InferenceManagerBuffered(Theory& t,
                                                   TheoryState& state,
                                                   ProofNodeManager* pnm,
                                                   const std::string& statsName,
                                                   bool cacheLemmas)
    : TheoryInferenceManager(t, state, pnm, statsName, cacheLemmas),
      d_processingPendingLemmas(false)
{
}

bool InferenceManagerBuffered::hasPending() const
{
  return hasPendingFact() || hasPendingLemma();
}

bool InferenceManagerBuffered::hasPendingFact() const
{
  return !d_pendingFact.empty();
}

bool InferenceManagerBuffered::hasPendingLemma() const
{
  return !d_pendingLem.empty();
}

bool InferenceManagerBuffered::addPendingLemma(Node lem,
                                               InferenceId id,
                                               LemmaProperty p,
                                               ProofGenerator* pg,
                                               bool checkCache)
{
  if (checkCache)
  {
    // check if it is unique up to rewriting
    Node lemr = Rewriter::rewrite(lem);
    if (hasCachedLemma(lemr, p))
    {
      return false;
    }
  }
  // make the simple theory lemma
  d_pendingLem.emplace_back(new SimpleTheoryLemma(id, lem, p, pg));
  return true;
}

void InferenceManagerBuffered::addPendingLemma(
    std::unique_ptr<TheoryInference> lemma)
{
  d_pendingLem.emplace_back(std::move(lemma));
}

void InferenceManagerBuffered::addPendingFact(Node conc,
                                              InferenceId id,
                                              Node exp,
                                              ProofGenerator* pg)
{
  // make a simple theory internal fact
  Assert(conc.getKind() != AND && conc.getKind() != OR);
  d_pendingFact.emplace_back(new SimpleTheoryInternalFact(id, conc, exp, pg));
}

void InferenceManagerBuffered::addPendingFact(
    std::unique_ptr<TheoryInference> fact)
{
  d_pendingFact.emplace_back(std::move(fact));
}

void InferenceManagerBuffered::addPendingPhaseRequirement(Node lit, bool pol)
{
  // it is the responsibility of the caller to ensure lit is rewritten
  d_pendingReqPhase[lit] = pol;
}

void InferenceManagerBuffered::doPendingFacts()
{
  size_t i = 0;
  while (!d_theoryState.isInConflict() && i < d_pendingFact.size())
  {
    // assert the internal fact, which notice may enqueue more pending facts in
    // this loop, or result in a conflict.
    assertInternalFactTheoryInference(d_pendingFact[i].get());
    i++;
  }
  d_pendingFact.clear();
}

void InferenceManagerBuffered::doPendingLemmas()
{
  if (d_processingPendingLemmas)
  {
    // already processing
    return;
  }
  d_processingPendingLemmas = true;
  size_t i = 0;
  while (i < d_pendingLem.size())
  {
    // process this lemma, which notice may enqueue more pending lemmas in this
    // loop, or clear the lemmas.
    lemmaTheoryInference(d_pendingLem[i].get());
    i++;
  }
  d_pendingLem.clear();
  d_processingPendingLemmas = false;
}

void InferenceManagerBuffered::doPendingPhaseRequirements()
{
  // process the pending require phase calls
  for (const std::pair<const Node, bool>& prp : d_pendingReqPhase)
  {
    requirePhase(prp.first, prp.second);
  }
  d_pendingReqPhase.clear();
}
void InferenceManagerBuffered::clearPending()
{
  d_pendingFact.clear();
  d_pendingLem.clear();
  d_pendingReqPhase.clear();
}
void InferenceManagerBuffered::clearPendingFacts() { d_pendingFact.clear(); }
void InferenceManagerBuffered::clearPendingLemmas() { d_pendingLem.clear(); }
void InferenceManagerBuffered::clearPendingPhaseRequirements()
{
  d_pendingReqPhase.clear();
}

std::size_t InferenceManagerBuffered::numPendingLemmas() const
{
  return d_pendingLem.size();
}
std::size_t InferenceManagerBuffered::numPendingFacts() const
{
  return d_pendingFact.size();
}

void InferenceManagerBuffered::lemmaTheoryInference(TheoryInference* lem)
{
  // process this lemma
  LemmaProperty p = LemmaProperty::NONE;
  TrustNode tlem = lem->processLemma(p);
  Assert(!tlem.isNull());
  // send the lemma
  trustedLemma(tlem, lem->getId(), p);
}

void InferenceManagerBuffered::assertInternalFactTheoryInference(
    TheoryInference* fact)
{
  // process this fact
  std::vector<Node> exp;
  ProofGenerator* pg = nullptr;
  Node lit = fact->processFact(exp, pg);
  Assert(!lit.isNull());
  bool pol = lit.getKind() != NOT;
  TNode atom = pol ? lit : lit[0];
  // no double negation or conjunctive conclusions
  Assert(atom.getKind() != NOT && atom.getKind() != AND);
  // assert the internal fact
  assertInternalFact(atom, pol, fact->getId(), exp, pg);
}

}  // 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, Aina Niemetz
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		* A buffered inference manager.
14		*/
15
16		#include "theory/inference_manager_buffered.h"
17
18		#include "theory/rewriter.h"
19		#include "theory/theory.h"
20		#include "theory/theory_state.h"
21
22		using namespace cvc5::kind;
23
24		namespace cvc5 {
25		namespace theory {
26
27	66213	InferenceManagerBuffered::InferenceManagerBuffered(Theory& t,
28		TheoryState& state,
29		ProofNodeManager* pnm,
30		const std::string& statsName,
31	66213	bool cacheLemmas)
32		: TheoryInferenceManager(t, state, pnm, statsName, cacheLemmas),
33	66213	d_processingPendingLemmas(false)
34		{
35	66213	}
36
37	2114363	bool InferenceManagerBuffered::hasPending() const
38		{
39	2114363	return hasPendingFact() \|\| hasPendingLemma();
40		}
41
42	2532966	bool InferenceManagerBuffered::hasPendingFact() const
43		{
44	2532966	return !d_pendingFact.empty();
45		}
46
47	2657075	bool InferenceManagerBuffered::hasPendingLemma() const
48		{
49	2657075	return !d_pendingLem.empty();
50		}
51
52	111335	bool InferenceManagerBuffered::addPendingLemma(Node lem,
53		InferenceId id,
54		LemmaProperty p,
55		ProofGenerator* pg,
56		bool checkCache)
57		{
58	111335	if (checkCache)
59		{
60		// check if it is unique up to rewriting
61	187462	Node lemr = Rewriter::rewrite(lem);
62	111335	if (hasCachedLemma(lemr, p))
63		{
64	35208	return false;
65		}
66		}
67		// make the simple theory lemma
68	76127	d_pendingLem.emplace_back(new SimpleTheoryLemma(id, lem, p, pg));
69	76127	return true;
70		}
71
72	14739	void InferenceManagerBuffered::addPendingLemma(
73		std::unique_ptr<TheoryInference> lemma)
74		{
75	14739	d_pendingLem.emplace_back(std::move(lemma));
76	14739	}
77
78		void InferenceManagerBuffered::addPendingFact(Node conc,
79		InferenceId id,
80		Node exp,
81		ProofGenerator* pg)
82		{
83		// make a simple theory internal fact
84		Assert(conc.getKind() != AND && conc.getKind() != OR);
85		d_pendingFact.emplace_back(new SimpleTheoryInternalFact(id, conc, exp, pg));
86		}
87
88	12076	void InferenceManagerBuffered::addPendingFact(
89		std::unique_ptr<TheoryInference> fact)
90		{
91	12076	d_pendingFact.emplace_back(std::move(fact));
92	12076	}
93
94	3664	void InferenceManagerBuffered::addPendingPhaseRequirement(Node lit, bool pol)
95		{
96		// it is the responsibility of the caller to ensure lit is rewritten
97	3664	d_pendingReqPhase[lit] = pol;
98	3664	}
99
100	2656971	void InferenceManagerBuffered::doPendingFacts()
101		{
102	2656971	size_t i = 0;
103	3263129	while (!d_theoryState.isInConflict() && i < d_pendingFact.size())
104		{
105		// assert the internal fact, which notice may enqueue more pending facts in
106		// this loop, or result in a conflict.
107	303079	assertInternalFactTheoryInference(d_pendingFact[i].get());
108	303079	i++;
109		}
110	2656971	d_pendingFact.clear();
111	2656971	}
112
113	2696141	void InferenceManagerBuffered::doPendingLemmas()
114		{
115	2696141	if (d_processingPendingLemmas)
116		{
117		// already processing
118	10773	return;
119		}
120	2685368	d_processingPendingLemmas = true;
121	2685368	size_t i = 0;
122	2926242	while (i < d_pendingLem.size())
123		{
124		// process this lemma, which notice may enqueue more pending lemmas in this
125		// loop, or clear the lemmas.
126	120438	lemmaTheoryInference(d_pendingLem[i].get());
127	120437	i++;
128		}
129	2685367	d_pendingLem.clear();
130	2685367	d_processingPendingLemmas = false;
131		}
132
133	191844	void InferenceManagerBuffered::doPendingPhaseRequirements()
134		{
135		// process the pending require phase calls
136	195507	for (const std::pair<const Node, bool>& prp : d_pendingReqPhase)
137		{
138	3663	requirePhase(prp.first, prp.second);
139		}
140	191844	d_pendingReqPhase.clear();
141	191844	}
142	496015	void InferenceManagerBuffered::clearPending()
143		{
144	496015	d_pendingFact.clear();
145	496015	d_pendingLem.clear();
146	496015	d_pendingReqPhase.clear();
147	496015	}
148	1166	void InferenceManagerBuffered::clearPendingFacts() { d_pendingFact.clear(); }
149	18412	void InferenceManagerBuffered::clearPendingLemmas() { d_pendingLem.clear(); }
150	1492	void InferenceManagerBuffered::clearPendingPhaseRequirements()
151		{
152	1492	d_pendingReqPhase.clear();
153	1492	}
154
155	211356	std::size_t InferenceManagerBuffered::numPendingLemmas() const
156		{
157	211356	return d_pendingLem.size();
158		}
159		std::size_t InferenceManagerBuffered::numPendingFacts() const
160		{
161		return d_pendingFact.size();
162		}
163
164	123059	void InferenceManagerBuffered::lemmaTheoryInference(TheoryInference* lem)
165		{
166		// process this lemma
167	123059	LemmaProperty p = LemmaProperty::NONE;
168	246118	TrustNode tlem = lem->processLemma(p);
169	123059	Assert(!tlem.isNull());
170		// send the lemma
171	123059	trustedLemma(tlem, lem->getId(), p);
172	123058	}
173
174	303079	void InferenceManagerBuffered::assertInternalFactTheoryInference(
175		TheoryInference* fact)
176		{
177		// process this fact
178	606158	std::vector<Node> exp;
179	303079	ProofGenerator* pg = nullptr;
180	606158	Node lit = fact->processFact(exp, pg);
181	303079	Assert(!lit.isNull());
182	303079	bool pol = lit.getKind() != NOT;
183	606158	TNode atom = pol ? lit : lit[0];
184		// no double negation or conjunctive conclusions
185	303079	Assert(atom.getKind() != NOT && atom.getKind() != AND);
186		// assert the internal fact
187	303079	assertInternalFact(atom, pol, fact->getId(), exp, pg);
188	303079	}
189
190		} // namespace theory
191	28191	} // namespace cvc5