Head

GCC Code Coverage Report

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


/******************************************************************************
 * Top contributors (to current version):
 *   Gereon Kremer, Makai Mann
 *
 * 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.
 * ****************************************************************************
 *
 * Customized inference manager for the theory of nonlinear arithmetic.
 */

#include "cvc5_private.h"

#ifndef CVC5__THEORY__ARITH__INFERENCE_MANAGER_H
#define CVC5__THEORY__ARITH__INFERENCE_MANAGER_H

#include <vector>

#include "theory/inference_id.h"
#include "theory/inference_manager_buffered.h"

namespace cvc5 {
namespace theory {
namespace arith {

class ArithState;
class TheoryArith;

/**
 * A specialized variant of the InferenceManagerBuffered, tailored to the
 * arithmetic theory.
 *
 * It adds some convenience methods to send ArithLemma and adds a mechanism for
 * waiting lemmas that can be flushed into the pending lemmas of this
 * buffered inference manager.
 * It also extends the caching mechanism of TheoryInferenceManager to cache
 * preprocessing lemmas and non-preprocessing lemmas separately. For the former,
 * it uses the cache provided by the TheoryInferenceManager base class.
 */
class InferenceManager : public InferenceManagerBuffered
{
  using NodeSet = context::CDHashSet<Node>;

 public:
  InferenceManager(TheoryArith& ta, ArithState& astate, ProofNodeManager* pnm);

  /**
   * Add a lemma as pending lemma to this inference manager.
   * If isWaiting is true, the lemma is first stored as waiting lemma and only
   * added as pending lemma when calling flushWaitingLemmas.
   */
  void addPendingLemma(std::unique_ptr<SimpleTheoryLemma> lemma,
                       bool isWaiting = false);
  /**
   * Add a lemma as pending lemma to this inference manager.
   * If isWaiting is true, the lemma is first stored as waiting lemma and only
   * added as pending lemma when calling flushWaitingLemmas.
   */
  void addPendingLemma(const SimpleTheoryLemma& lemma, bool isWaiting = false);
  /**
   * Add a lemma as pending lemma to this inference manager.
   * If isWaiting is true, the lemma is first stored as waiting lemma and only
   * added as pending lemma when calling flushWaitingLemmas.
   */
  void addPendingLemma(const Node& lemma,
                       InferenceId inftype,
                       ProofGenerator* pg = nullptr,
                       bool isWaiting = false,
                       LemmaProperty p = LemmaProperty::NONE);

  /**
   * Flush all waiting lemmas to this inference manager (as pending
   * lemmas). To actually send them, call doPendingLemmas() afterwards.
   */
  void flushWaitingLemmas();

  /**
   * Removes all waiting lemmas without sending them anywhere.
   */
  void clearWaitingLemmas();

  /**
   * Checks whether we have made any progress, that is whether a conflict,
   * lemma or fact was added or whether a lemma or fact is pending.
   */
  bool hasUsed() const;

  /** Checks whether we have waiting lemmas. */
  bool hasWaitingLemma() const;

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

  /** Checks whether the given lemma is already present in the cache. */
  virtual bool hasCachedLemma(TNode lem, LemmaProperty p) override;
  /** overrides propagateLit to track which literals have been propagated */
  bool propagateLit(TNode lit) override;
  /**
   * Return true if we have propagated lit already. This call is only valid if
   * d_trackPropLits is true.
   */
  bool hasPropagated(TNode lit) const;

 protected:
  /**
   * Adds the given lemma to the cache. Returns true if it has not been in the
   * cache yet.
   */
  virtual bool cacheLemma(TNode lem, LemmaProperty p) override;

 private:
  /**
   * Checks whether the lemma is entailed to be false. In this case, it is a
   * conflict.
   */
  bool isEntailedFalse(const SimpleTheoryLemma& lem);
  /** The waiting lemmas. */
  std::vector<std::unique_ptr<SimpleTheoryLemma>> d_waitingLem;
  /** Whether we are tracking the set of propagated literals */
  bool d_trackPropLits;
  /** The literals we have propagated */
  NodeSet d_propLits;
};

}  // namespace arith
}  // namespace theory
}  // namespace cvc5

#endif


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Gereon Kremer, Makai Mann
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		* Customized inference manager for the theory of nonlinear arithmetic.
14		*/
15
16		#include "cvc5_private.h"
17
18		#ifndef CVC5__THEORY__ARITH__INFERENCE_MANAGER_H
19		#define CVC5__THEORY__ARITH__INFERENCE_MANAGER_H
20
21		#include <vector>
22
23		#include "theory/inference_id.h"
24		#include "theory/inference_manager_buffered.h"
25
26		namespace cvc5 {
27		namespace theory {
28		namespace arith {
29
30		class ArithState;
31		class TheoryArith;
32
33		/**
34		* A specialized variant of the InferenceManagerBuffered, tailored to the
35		* arithmetic theory.
36		*
37		* It adds some convenience methods to send ArithLemma and adds a mechanism for
38		* waiting lemmas that can be flushed into the pending lemmas of this
39		* buffered inference manager.
40		* It also extends the caching mechanism of TheoryInferenceManager to cache
41		* preprocessing lemmas and non-preprocessing lemmas separately. For the former,
42		* it uses the cache provided by the TheoryInferenceManager base class.
43		*/
44	9923	class InferenceManager : public InferenceManagerBuffered
45		{
46		using NodeSet = context::CDHashSet<Node>;
47
48		public:
49		InferenceManager(TheoryArith& ta, ArithState& astate, ProofNodeManager* pnm);
50
51		/**
52		* Add a lemma as pending lemma to this inference manager.
53		* If isWaiting is true, the lemma is first stored as waiting lemma and only
54		* added as pending lemma when calling flushWaitingLemmas.
55		*/
56		void addPendingLemma(std::unique_ptr<SimpleTheoryLemma> lemma,
57		bool isWaiting = false);
58		/**
59		* Add a lemma as pending lemma to this inference manager.
60		* If isWaiting is true, the lemma is first stored as waiting lemma and only
61		* added as pending lemma when calling flushWaitingLemmas.
62		*/
63		void addPendingLemma(const SimpleTheoryLemma& lemma, bool isWaiting = false);
64		/**
65		* Add a lemma as pending lemma to this inference manager.
66		* If isWaiting is true, the lemma is first stored as waiting lemma and only
67		* added as pending lemma when calling flushWaitingLemmas.
68		*/
69		void addPendingLemma(const Node& lemma,
70		InferenceId inftype,
71		ProofGenerator* pg = nullptr,
72		bool isWaiting = false,
73		LemmaProperty p = LemmaProperty::NONE);
74
75		/**
76		* Flush all waiting lemmas to this inference manager (as pending
77		* lemmas). To actually send them, call doPendingLemmas() afterwards.
78		*/
79		void flushWaitingLemmas();
80
81		/**
82		* Removes all waiting lemmas without sending them anywhere.
83		*/
84		void clearWaitingLemmas();
85
86		/**
87		* Checks whether we have made any progress, that is whether a conflict,
88		* lemma or fact was added or whether a lemma or fact is pending.
89		*/
90		bool hasUsed() const;
91
92		/** Checks whether we have waiting lemmas. */
93		bool hasWaitingLemma() const;
94
95		/** Returns the number of pending lemmas. */
96		std::size_t numWaitingLemmas() const;
97
98		/** Checks whether the given lemma is already present in the cache. */
99		virtual bool hasCachedLemma(TNode lem, LemmaProperty p) override;
100		/** overrides propagateLit to track which literals have been propagated */
101		bool propagateLit(TNode lit) override;
102		/**
103		* Return true if we have propagated lit already. This call is only valid if
104		* d_trackPropLits is true.
105		*/
106		bool hasPropagated(TNode lit) const;
107
108		protected:
109		/**
110		* Adds the given lemma to the cache. Returns true if it has not been in the
111		* cache yet.
112		*/
113		virtual bool cacheLemma(TNode lem, LemmaProperty p) override;
114
115		private:
116		/**
117		* Checks whether the lemma is entailed to be false. In this case, it is a
118		* conflict.
119		*/
120		bool isEntailedFalse(const SimpleTheoryLemma& lem);
121		/** The waiting lemmas. */
122		std::vector<std::unique_ptr<SimpleTheoryLemma>> d_waitingLem;
123		/** Whether we are tracking the set of propagated literals */
124		bool d_trackPropLits;
125		/** The literals we have propagated */
126		NodeSet d_propLits;
127		};
128
129		} // namespace arith
130		} // namespace theory
131		} // namespace cvc5
132
133		#endif