Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/inference_manager_buffered.cpp	Lines:	81	87	93.1 %
Date:	2021-09-10	Branches:	55	152	36.2 %


/******************************************************************************
 * 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(Env& env,
                                                   Theory& t,
                                                   TheoryState& state,
                                                   ProofNodeManager* pnm,
                                                   const std::string& statsName,
                                                   bool cacheLemmas)
    : TheoryInferenceManager(env, 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);
}

void InferenceManagerBuffered::notifyInConflict()
{
  d_theoryState.notifyInConflict();
  // also clear the pending facts, which will be stale after backtracking
  clearPending();
}

}  // 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	69391	InferenceManagerBuffered::InferenceManagerBuffered(Env& env,
28		Theory& t,
29		TheoryState& state,
30		ProofNodeManager* pnm,
31		const std::string& statsName,
32	69391	bool cacheLemmas)
33		: TheoryInferenceManager(env, t, state, pnm, statsName, cacheLemmas),
34	69391	d_processingPendingLemmas(false)
35		{
36	69391	}
37
38	3900757	bool InferenceManagerBuffered::hasPending() const
39		{
40	3900757	return hasPendingFact() \|\| hasPendingLemma();
41		}
42
43	4691951	bool InferenceManagerBuffered::hasPendingFact() const
44		{
45	4691951	return !d_pendingFact.empty();
46		}
47
48	4798439	bool InferenceManagerBuffered::hasPendingLemma() const
49		{
50	4798439	return !d_pendingLem.empty();
51		}
52
53	111667	bool InferenceManagerBuffered::addPendingLemma(Node lem,
54		InferenceId id,
55		LemmaProperty p,
56		ProofGenerator* pg,
57		bool checkCache)
58		{
59	111667	if (checkCache)
60		{
61		// check if it is unique up to rewriting
62	188650	Node lemr = Rewriter::rewrite(lem);
63	111667	if (hasCachedLemma(lemr, p))
64		{
65	34684	return false;
66		}
67		}
68		// make the simple theory lemma
69	76983	d_pendingLem.emplace_back(new SimpleTheoryLemma(id, lem, p, pg));
70	76983	return true;
71		}
72
73	25576	void InferenceManagerBuffered::addPendingLemma(
74		std::unique_ptr<TheoryInference> lemma)
75		{
76	25576	d_pendingLem.emplace_back(std::move(lemma));
77	25576	}
78
79		void InferenceManagerBuffered::addPendingFact(Node conc,
80		InferenceId id,
81		Node exp,
82		ProofGenerator* pg)
83		{
84		// make a simple theory internal fact
85		Assert(conc.getKind() != AND && conc.getKind() != OR);
86		d_pendingFact.emplace_back(new SimpleTheoryInternalFact(id, conc, exp, pg));
87		}
88
89	38599	void InferenceManagerBuffered::addPendingFact(
90		std::unique_ptr<TheoryInference> fact)
91		{
92	38599	d_pendingFact.emplace_back(std::move(fact));
93	38599	}
94
95	4532	void InferenceManagerBuffered::addPendingPhaseRequirement(Node lit, bool pol)
96		{
97		// it is the responsibility of the caller to ensure lit is rewritten
98	4532	d_pendingReqPhase[lit] = pol;
99	4532	}
100
101	3907788	void InferenceManagerBuffered::doPendingFacts()
102		{
103	3907788	size_t i = 0;
104	4634228	while (!d_theoryState.isInConflict() && i < d_pendingFact.size())
105		{
106		// assert the internal fact, which notice may enqueue more pending facts in
107		// this loop, or result in a conflict.
108	363220	assertInternalFactTheoryInference(d_pendingFact[i].get());
109	363220	i++;
110		}
111	3907788	d_pendingFact.clear();
112	3907788	}
113
114	3709094	void InferenceManagerBuffered::doPendingLemmas()
115		{
116	3709094	if (d_processingPendingLemmas)
117		{
118		// already processing
119	11859	return;
120		}
121	3697235	d_processingPendingLemmas = true;
122	3697235	size_t i = 0;
123	3956075	while (i < d_pendingLem.size())
124		{
125		// process this lemma, which notice may enqueue more pending lemmas in this
126		// loop, or clear the lemmas.
127	129421	lemmaTheoryInference(d_pendingLem[i].get());
128	129420	i++;
129		}
130	3697234	d_pendingLem.clear();
131	3697234	d_processingPendingLemmas = false;
132		}
133
134	231523	void InferenceManagerBuffered::doPendingPhaseRequirements()
135		{
136		// process the pending require phase calls
137	236053	for (const std::pair<const Node, bool>& prp : d_pendingReqPhase)
138		{
139	4530	requirePhase(prp.first, prp.second);
140		}
141	231523	d_pendingReqPhase.clear();
142	231523	}
143	1433187	void InferenceManagerBuffered::clearPending()
144		{
145	1433187	d_pendingFact.clear();
146	1433187	d_pendingLem.clear();
147	1433187	d_pendingReqPhase.clear();
148	1433187	}
149	1290	void InferenceManagerBuffered::clearPendingFacts() { d_pendingFact.clear(); }
150	23463	void InferenceManagerBuffered::clearPendingLemmas() { d_pendingLem.clear(); }
151	2906	void InferenceManagerBuffered::clearPendingPhaseRequirements()
152		{
153	2906	d_pendingReqPhase.clear();
154	2906	}
155
156	289026	std::size_t InferenceManagerBuffered::numPendingLemmas() const
157		{
158	289026	return d_pendingLem.size();
159		}
160		std::size_t InferenceManagerBuffered::numPendingFacts() const
161		{
162		return d_pendingFact.size();
163		}
164
165	132304	void InferenceManagerBuffered::lemmaTheoryInference(TheoryInference* lem)
166		{
167		// process this lemma
168	132304	LemmaProperty p = LemmaProperty::NONE;
169	264608	TrustNode tlem = lem->processLemma(p);
170	132304	Assert(!tlem.isNull());
171		// send the lemma
172	132304	trustedLemma(tlem, lem->getId(), p);
173	132303	}
174
175	363220	void InferenceManagerBuffered::assertInternalFactTheoryInference(
176		TheoryInference* fact)
177		{
178		// process this fact
179	726440	std::vector<Node> exp;
180	363220	ProofGenerator* pg = nullptr;
181	726440	Node lit = fact->processFact(exp, pg);
182	363220	Assert(!lit.isNull());
183	363220	bool pol = lit.getKind() != NOT;
184	726440	TNode atom = pol ? lit : lit[0];
185		// no double negation or conjunctive conclusions
186	363220	Assert(atom.getKind() != NOT && atom.getKind() != AND);
187		// assert the internal fact
188	363220	assertInternalFact(atom, pol, fact->getId(), exp, pg);
189	363220	}
190
191	1410584	void InferenceManagerBuffered::notifyInConflict()
192		{
193	1410584	d_theoryState.notifyInConflict();
194		// also clear the pending facts, which will be stale after backtracking
195	1410584	clearPending();
196	1410584	}
197
198		} // namespace theory
199	29502	} // namespace cvc5