Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/inference_manager.h	Lines:	1	1	100.0 %
Date:	2021-09-17	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(Env& env,
                   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	9939	class InferenceManager : public InferenceManagerBuffered
45		{
46		using NodeSet = context::CDHashSet<Node>;
47
48		public:
49		InferenceManager(Env& env,
50		TheoryArith& ta,
51		ArithState& astate,
52		ProofNodeManager* pnm);
53
54		/**
55		* Add a lemma as pending lemma to this inference manager.
56		* If isWaiting is true, the lemma is first stored as waiting lemma and only
57		* added as pending lemma when calling flushWaitingLemmas.
58		*/
59		void addPendingLemma(std::unique_ptr<SimpleTheoryLemma> lemma,
60		bool isWaiting = false);
61		/**
62		* Add a lemma as pending lemma to this inference manager.
63		* If isWaiting is true, the lemma is first stored as waiting lemma and only
64		* added as pending lemma when calling flushWaitingLemmas.
65		*/
66		void addPendingLemma(const SimpleTheoryLemma& lemma, bool isWaiting = false);
67		/**
68		* Add a lemma as pending lemma to this inference manager.
69		* If isWaiting is true, the lemma is first stored as waiting lemma and only
70		* added as pending lemma when calling flushWaitingLemmas.
71		*/
72		void addPendingLemma(const Node& lemma,
73		InferenceId inftype,
74		ProofGenerator* pg = nullptr,
75		bool isWaiting = false,
76		LemmaProperty p = LemmaProperty::NONE);
77
78		/**
79		* Flush all waiting lemmas to this inference manager (as pending
80		* lemmas). To actually send them, call doPendingLemmas() afterwards.
81		*/
82		void flushWaitingLemmas();
83
84		/**
85		* Removes all waiting lemmas without sending them anywhere.
86		*/
87		void clearWaitingLemmas();
88
89		/**
90		* Checks whether we have made any progress, that is whether a conflict,
91		* lemma or fact was added or whether a lemma or fact is pending.
92		*/
93		bool hasUsed() const;
94
95		/** Checks whether we have waiting lemmas. */
96		bool hasWaitingLemma() const;
97
98		/** Returns the number of pending lemmas. */
99		std::size_t numWaitingLemmas() const;
100
101		/** Checks whether the given lemma is already present in the cache. */
102		virtual bool hasCachedLemma(TNode lem, LemmaProperty p) override;
103		/** overrides propagateLit to track which literals have been propagated */
104		bool propagateLit(TNode lit) override;
105		/**
106		* Return true if we have propagated lit already. This call is only valid if
107		* d_trackPropLits is true.
108		*/
109		bool hasPropagated(TNode lit) const;
110
111		protected:
112		/**
113		* Adds the given lemma to the cache. Returns true if it has not been in the
114		* cache yet.
115		*/
116		virtual bool cacheLemma(TNode lem, LemmaProperty p) override;
117
118		private:
119		/**
120		* Checks whether the lemma is entailed to be false. In this case, it is a
121		* conflict.
122		*/
123		bool isEntailedFalse(const SimpleTheoryLemma& lem);
124		/** The waiting lemmas. */
125		std::vector<std::unique_ptr<SimpleTheoryLemma>> d_waitingLem;
126		/** Whether we are tracking the set of propagated literals */
127		bool d_trackPropLits;
128		/** The literals we have propagated */
129		NodeSet d_propLits;
130		};
131
132		} // namespace arith
133		} // namespace theory
134		} // namespace cvc5
135
136		#endif