GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bags/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
 **   Mudathir Mohamed
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 The inference manager for the theory of bags.
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__BAGS__INFERENCE_MANAGER_H
18
#define CVC4__THEORY__BAGS__INFERENCE_MANAGER_H
19
20
#include "theory/inference_manager_buffered.h"
21
22
namespace CVC4 {
23
namespace theory {
24
namespace bags {
25
26
class SolverState;
27
28
/** Inference manager
29
 *
30
 * This class manages inferences produced by the theory of bags. It manages
31
 * whether inferences are processed as external lemmas on the output channel
32
 * of theory of bags or internally as literals asserted to the equality engine
33
 * of theory of bags. The latter literals are referred to as "facts".
34
 */
35
8994
class InferenceManager : public InferenceManagerBuffered
36
{
37
  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
38
39
 public:
40
  InferenceManager(Theory& t, SolverState& s, ProofNodeManager* pnm);
41
42
  /**
43
   * Do pending method. This processes all pending facts, lemmas and pending
44
   * phase requests based on the policy of this manager. This means that
45
   * we process the pending facts first and abort if in conflict. Otherwise, we
46
   * process the pending lemmas and then the pending phase requirements.
47
   * Notice that we process the pending lemmas even if there were facts.
48
   */
49
  // TODO issue #78: refactor this with theory of strings
50
  void doPending();
51
52
 private:
53
  /** constants */
54
  Node d_true;
55
  Node d_false;
56
  /**
57
   * Reference to the state object for the theory of bags. We store the
58
   * (derived) state here, since it has additional methods required in this
59
   * class.
60
   */
61
  SolverState& d_state;
62
};
63
64
}  // namespace bags
65
}  // namespace theory
66
}  // namespace CVC4
67
68
#endif /* CVC4__THEORY__BAGS__INFERENCE_MANAGER_H */