Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/inference_manager_buffered.h	Lines:	1	1	100.0 %
Date:	2021-09-16	Branches:	0	0	0.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Gereon Kremer
 *
 * 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 "cvc5_private.h"

#ifndef CVC5__THEORY__INFERENCE_MANAGER_BUFFERED_H
#define CVC5__THEORY__INFERENCE_MANAGER_BUFFERED_H

#include "expr/node.h"
#include "theory/theory_inference.h"
#include "theory/theory_inference_manager.h"

namespace cvc5 {
namespace theory {

/**
 * The buffered inference manager.  This class implements standard methods
 * for buffering facts, lemmas and phase requirements.
 */
class InferenceManagerBuffered : public TheoryInferenceManager
{
 public:
  InferenceManagerBuffered(Env& env,
                           Theory& t,
                           TheoryState& state,
                           ProofNodeManager* pnm,
                           const std::string& statsName,
                           bool cacheLemmas = true);
  virtual ~InferenceManagerBuffered() {}
  /**
   * Do we have a pending fact or lemma?
   */
  bool hasPending() const;
  /**
   * Do we have a pending fact to add as an internal fact to the equality
   * engine?
   */
  bool hasPendingFact() const;
  /** Do we have a pending lemma to send on the output channel? */
  bool hasPendingLemma() const;
  /**
   * Add pending lemma lem with property p, with proof generator pg. If
   * non-null, pg must be able to provide a proof for lem for the remainder
   * of the user context. Pending lemmas are sent to the output channel using
   * doPendingLemmas.
   *
   * @param lem The lemma to send
   * @param id The identifier of the inference
   * @param p The property of the lemma
   * @param pg The proof generator which can provide a proof for lem
   * @param checkCache Whether we want to check that the lemma is already in
   * the cache.
   * @return true if the lemma was added to the list of pending lemmas and
   * false if the lemma is already cached.
   */
  bool addPendingLemma(Node lem,
                       InferenceId id,
                       LemmaProperty p = LemmaProperty::NONE,
                       ProofGenerator* pg = nullptr,
                       bool checkCache = true);
  /**
   * Add pending lemma, where lemma can be a (derived) class of the
   * theory inference base class.
   */
  void addPendingLemma(std::unique_ptr<TheoryInference> lemma);
  /**
   * Add pending fact, which adds a fact on the pending fact queue. It must
   * be the case that:
   * (1) exp => conc is valid,
   * (2) exp is a literal (or conjunction of literals) that holds in the
   * equality engine of the theory.
   *
   * Pending facts are sent to the equality engine of this class using
   * doPendingFacts.
   * @param conc The conclustion
   * @param id The identifier of the inference
   * @param exp The explanation in the equality engine of the theory
   * @param pg The proof generator which can provide a proof for conc
   */
  void addPendingFact(Node conc, InferenceId id, Node exp, ProofGenerator* pg = nullptr);
  /**
   * Add pending fact, where fact can be a (derived) class of the
   * theory inference base class.
   */
  void addPendingFact(std::unique_ptr<TheoryInference> fact);
  /** Add pending phase requirement
   *
   * This method is called to indicate this class should send a phase
   * requirement request to the output channel for literal lit to be
   * decided with polarity pol. The literal lit should be a SAT literal
   * by the time that doPendingPhaseRequirements is called. Typically,
   * lit is a literal that is a subformula of a pending lemma that is processed
   * prior to sending the phase requirement.
   */
  void addPendingPhaseRequirement(Node lit, bool pol);
  /** Do pending facts
   *
   * This method asserts pending facts (d_pendingFact) with explanations
   * to the equality engine of the theory via calls
   * to assertInternalFact.
   *
   * It terminates early if a conflict is encountered, for instance, by
   * equality reasoning within the equality engine.
   *
   * Regardless of whether a conflict is encountered, the vector d_pendingFact
   * is cleared after this call.
   */
  void doPendingFacts();
  /** Do pending lemmas
   *
   * This method send all pending lemmas (d_pendingLem) on the output
   * channel of the theory.
   *
   * Unlike doPendingFacts, this function will not terminate early if a conflict
   * has already been encountered by the theory. The vector d_pendingLem is
   * cleared after this call.
   */
  void doPendingLemmas();
  /**
   * Do pending phase requirements. Calls the output channel for all pending
   * phase requirements and clears d_pendingReqPhase.
   */
  void doPendingPhaseRequirements();
  /** Clear pending facts, lemmas, and phase requirements without processing */
  void clearPending();
  /** Clear pending facts, without processing */
  void clearPendingFacts();
  /** Clear pending lemmas, without processing */
  void clearPendingLemmas();
  /** Clear pending phase requirements, without processing */
  void clearPendingPhaseRequirements();

  /** Returns the number of pending lemmas. */
  std::size_t numPendingLemmas() const;
  /** Returns the number of pending facts. */
  std::size_t numPendingFacts() const;

  /**
   * Send the given theory inference as a lemma on the output channel of this
   * inference manager. This calls TheoryInferenceManager::trustedLemma based
   * on the provided theory inference.
   */
  void lemmaTheoryInference(TheoryInference* lem);
  /**
   * Add the given theory inference as an internal fact. This calls
   * TheoryInferenceManager::assertInternalFact based on the provided theory
   * inference.
   */
  void assertInternalFactTheoryInference(TheoryInference* fact);

  /**
   * Notify this inference manager that a conflict was sent in this SAT context.
   * This method is called via TheoryEngine when a conflict is sent. This
   * method will clear all pending facts, lemmas, and phase requirements, as
   * these will be stale after the solver backtracks.
   */
  void notifyInConflict() override;

 protected:
  /** A set of pending inferences to be processed as lemmas */
  std::vector<std::unique_ptr<TheoryInference>> d_pendingLem;
  /** A set of pending inferences to be processed as facts */
  std::vector<std::unique_ptr<TheoryInference>> d_pendingFact;
  /** A map from literals to their pending phase requirement */
  std::map<Node, bool> d_pendingReqPhase;
  /**
   * Whether we are currently processing pending lemmas. This flag ensures
   * that we do not call pending lemmas recursively, which may lead to
   * segfaults.
   */
  bool d_processingPendingLemmas;
};

}  // namespace theory
}  // namespace cvc5

#endif


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Gereon Kremer
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 "cvc5_private.h"
17
18		#ifndef CVC5__THEORY__INFERENCE_MANAGER_BUFFERED_H
19		#define CVC5__THEORY__INFERENCE_MANAGER_BUFFERED_H
20
21		#include "expr/node.h"
22		#include "theory/theory_inference.h"
23		#include "theory/theory_inference_manager.h"
24
25		namespace cvc5 {
26		namespace theory {
27
28		/**
29		* The buffered inference manager. This class implements standard methods
30		* for buffering facts, lemmas and phase requirements.
31		*/
32		class InferenceManagerBuffered : public TheoryInferenceManager
33		{
34		public:
35		InferenceManagerBuffered(Env& env,
36		Theory& t,
37		TheoryState& state,
38		ProofNodeManager* pnm,
39		const std::string& statsName,
40		bool cacheLemmas = true);
41	69573	virtual ~InferenceManagerBuffered() {}
42		/**
43		* Do we have a pending fact or lemma?
44		*/
45		bool hasPending() const;
46		/**
47		* Do we have a pending fact to add as an internal fact to the equality
48		* engine?
49		*/
50		bool hasPendingFact() const;
51		/** Do we have a pending lemma to send on the output channel? */
52		bool hasPendingLemma() const;
53		/**
54		* Add pending lemma lem with property p, with proof generator pg. If
55		* non-null, pg must be able to provide a proof for lem for the remainder
56		* of the user context. Pending lemmas are sent to the output channel using
57		* doPendingLemmas.
58		*
59		* @param lem The lemma to send
60		* @param id The identifier of the inference
61		* @param p The property of the lemma
62		* @param pg The proof generator which can provide a proof for lem
63		* @param checkCache Whether we want to check that the lemma is already in
64		* the cache.
65		* @return true if the lemma was added to the list of pending lemmas and
66		* false if the lemma is already cached.
67		*/
68		bool addPendingLemma(Node lem,
69		InferenceId id,
70		LemmaProperty p = LemmaProperty::NONE,
71		ProofGenerator* pg = nullptr,
72		bool checkCache = true);
73		/**
74		* Add pending lemma, where lemma can be a (derived) class of the
75		* theory inference base class.
76		*/
77		void addPendingLemma(std::unique_ptr<TheoryInference> lemma);
78		/**
79		* Add pending fact, which adds a fact on the pending fact queue. It must
80		* be the case that:
81		* (1) exp => conc is valid,
82		* (2) exp is a literal (or conjunction of literals) that holds in the
83		* equality engine of the theory.
84		*
85		* Pending facts are sent to the equality engine of this class using
86		* doPendingFacts.
87		* @param conc The conclustion
88		* @param id The identifier of the inference
89		* @param exp The explanation in the equality engine of the theory
90		* @param pg The proof generator which can provide a proof for conc
91		*/
92		void addPendingFact(Node conc, InferenceId id, Node exp, ProofGenerator* pg = nullptr);
93		/**
94		* Add pending fact, where fact can be a (derived) class of the
95		* theory inference base class.
96		*/
97		void addPendingFact(std::unique_ptr<TheoryInference> fact);
98		/** Add pending phase requirement
99		*
100		* This method is called to indicate this class should send a phase
101		* requirement request to the output channel for literal lit to be
102		* decided with polarity pol. The literal lit should be a SAT literal
103		* by the time that doPendingPhaseRequirements is called. Typically,
104		* lit is a literal that is a subformula of a pending lemma that is processed
105		* prior to sending the phase requirement.
106		*/
107		void addPendingPhaseRequirement(Node lit, bool pol);
108		/** Do pending facts
109		*
110		* This method asserts pending facts (d_pendingFact) with explanations
111		* to the equality engine of the theory via calls
112		* to assertInternalFact.
113		*
114		* It terminates early if a conflict is encountered, for instance, by
115		* equality reasoning within the equality engine.
116		*
117		* Regardless of whether a conflict is encountered, the vector d_pendingFact
118		* is cleared after this call.
119		*/
120		void doPendingFacts();
121		/** Do pending lemmas
122		*
123		* This method send all pending lemmas (d_pendingLem) on the output
124		* channel of the theory.
125		*
126		* Unlike doPendingFacts, this function will not terminate early if a conflict
127		* has already been encountered by the theory. The vector d_pendingLem is
128		* cleared after this call.
129		*/
130		void doPendingLemmas();
131		/**
132		* Do pending phase requirements. Calls the output channel for all pending
133		* phase requirements and clears d_pendingReqPhase.
134		*/
135		void doPendingPhaseRequirements();
136		/** Clear pending facts, lemmas, and phase requirements without processing */
137		void clearPending();
138		/** Clear pending facts, without processing */
139		void clearPendingFacts();
140		/** Clear pending lemmas, without processing */
141		void clearPendingLemmas();
142		/** Clear pending phase requirements, without processing */
143		void clearPendingPhaseRequirements();
144
145		/** Returns the number of pending lemmas. */
146		std::size_t numPendingLemmas() const;
147		/** Returns the number of pending facts. */
148		std::size_t numPendingFacts() const;
149
150		/**
151		* Send the given theory inference as a lemma on the output channel of this
152		* inference manager. This calls TheoryInferenceManager::trustedLemma based
153		* on the provided theory inference.
154		*/
155		void lemmaTheoryInference(TheoryInference* lem);
156		/**
157		* Add the given theory inference as an internal fact. This calls
158		* TheoryInferenceManager::assertInternalFact based on the provided theory
159		* inference.
160		*/
161		void assertInternalFactTheoryInference(TheoryInference* fact);
162
163		/**
164		* Notify this inference manager that a conflict was sent in this SAT context.
165		* This method is called via TheoryEngine when a conflict is sent. This
166		* method will clear all pending facts, lemmas, and phase requirements, as
167		* these will be stale after the solver backtracks.
168		*/
169		void notifyInConflict() override;
170
171		protected:
172		/** A set of pending inferences to be processed as lemmas */
173		std::vector<std::unique_ptr<TheoryInference>> d_pendingLem;
174		/** A set of pending inferences to be processed as facts */
175		std::vector<std::unique_ptr<TheoryInference>> d_pendingFact;
176		/** A map from literals to their pending phase requirement */
177		std::map<Node, bool> d_pendingReqPhase;
178		/**
179		* Whether we are currently processing pending lemmas. This flag ensures
180		* that we do not call pending lemmas recursively, which may lead to
181		* segfaults.
182		*/
183		bool d_processingPendingLemmas;
184		};
185
186		} // namespace theory
187		} // namespace cvc5
188
189		#endif