GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/inference_manager.h Lines: 1 1 100.0 %
Date: 2021-03-23 Branches: 0 0 0.0 %

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