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

Line Exec Source
1
/*********************                                                        */
2
/*! \file inference_manager.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Gereon Kremer
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 sets.
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__SETS__INFERENCE_MANAGER_H
18
#define CVC4__THEORY__SETS__INFERENCE_MANAGER_H
19
20
#include "theory/inference_manager_buffered.h"
21
#include "theory/sets/solver_state.h"
22
23
namespace CVC4 {
24
namespace theory {
25
namespace sets {
26
27
class TheorySetsPrivate;
28
29
/** Inference manager
30
 *
31
 * This class manages inferences produced by the theory of sets. It manages
32
 * whether inferences are processed as external lemmas on the output channel
33
 * of theory of sets or internally as literals asserted to the equality engine
34
 * of theory of sets. The latter literals are referred to as "facts".
35
 */
36
8992
class InferenceManager : public InferenceManagerBuffered
37
{
38
  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
39
40
 public:
41
  InferenceManager(Theory& t, SolverState& s, ProofNodeManager* pnm);
42
  /**
43
   * Add facts corresponding to ( exp => fact ) via calls to the assertFact
44
   * method of TheorySetsPrivate.
45
   *
46
   * The portions of fact that were unable to be processed as facts are added
47
   * to the data member d_pendingLemmas.
48
   *
49
   * The argument inferType is used for overriding the policy on whether
50
   * fact is processed as a lemma, where inferType=1 forces fact to be
51
   * set as a lemma, and inferType=-1 forces fact to be processed as a fact
52
   * (if possible).
53
   */
54
  void assertInference(Node fact,
55
                       InferenceId id,
56
                       Node exp,
57
                       int inferType = 0);
58
  /** same as above, where exp is interpreted as a conjunction */
59
  void assertInference(Node fact,
60
                       InferenceId id,
61
                       std::vector<Node>& exp,
62
                       int inferType = 0);
63
  /** same as above, where conc is interpreted as a conjunction */
64
  void assertInference(std::vector<Node>& conc,
65
                       InferenceId id,
66
                       Node exp,
67
                       int inferType = 0);
68
  /** same as above, where both exp and conc are interpreted as conjunctions */
69
  void assertInference(std::vector<Node>& conc,
70
                       InferenceId id,
71
                       std::vector<Node>& exp,
72
                       int inferType = 0);
73
74
  /** flush the splitting lemma ( n OR (NOT n) )
75
   *
76
   * If reqPol is not 0, then a phase requirement for n is requested with
77
   * polarity ( reqPol>0 ).
78
   */
79
  void split(Node n, InferenceId id, int reqPol = 0);
80
81
 private:
82
  /** constants */
83
  Node d_true;
84
  Node d_false;
85
  /**
86
   * Reference to the state object for the theory of sets. We store the
87
   * (derived) state here, since it has additional methods required in this
88
   * class.
89
   */
90
  SolverState& d_state;
91
  /** Assert fact recursive
92
   *
93
   * This is a helper function for assertInference, which calls assertFact
94
   * in theory of sets and adds to d_pendingLemmas based on fact.
95
   * The argument inferType determines the policy on whether fact is processed
96
   * as a fact or as a lemma (see assertInference above).
97
   */
98
  bool assertFactRec(Node fact, InferenceId id, Node exp, int inferType = 0);
99
};
100
101
}  // namespace sets
102
}  // namespace theory
103
}  // namespace CVC4
104
105
#endif /* CVC4__THEORY__SETS__INFERENCE_MANAGER_H */