GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bags/infer_info.h Lines: 2 2 100.0 %
Date: 2021-03-23 Branches: 3 6 50.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file infer_info.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Mudathir Mohamed, 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 Inference information utility
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__BAGS__INFER_INFO_H
18
#define CVC4__THEORY__BAGS__INFER_INFO_H
19
20
#include <map>
21
#include <vector>
22
23
#include "expr/node.h"
24
#include "theory/inference_id.h"
25
#include "theory/theory_inference.h"
26
27
namespace CVC4 {
28
namespace theory {
29
30
class TheoryInferenceManager;
31
32
namespace bags {
33
34
35
/**
36
 * An inference. This is a class to track an unprocessed call to either
37
 * send a fact, lemma, or conflict that is waiting to be asserted to the
38
 * equality engine or sent on the output channel.
39
 */
40
282
class InferInfo : public TheoryInference
41
{
42
 public:
43
  InferInfo(TheoryInferenceManager* im, InferenceId id);
44
2478
  ~InferInfo() {}
45
  /** Process lemma */
46
  TrustNode processLemma(LemmaProperty& p) override;
47
  /** Pointer to the class used for processing this info */
48
  TheoryInferenceManager* d_im;
49
  /** The conclusion */
50
  Node d_conclusion;
51
  /**
52
   * The premise(s) of the inference, interpreted conjunctively. These are
53
   * literals that currently hold in the equality engine.
54
   */
55
  std::vector<Node> d_premises;
56
57
  /**
58
   * A map of nodes to their skolem variables introduced as a result of this
59
   * inference.
60
   */
61
  std::map<Node, Node> d_skolems;
62
  /**  Is this infer info trivial? True if d_conc is true. */
63
  bool isTrivial() const;
64
  /**
65
   * Does this infer info correspond to a conflict? True if d_conc is false
66
   * and it has no new premises (d_noExplain).
67
   */
68
  bool isConflict() const;
69
  /**
70
   * Does this infer info correspond to a "fact". A fact is an inference whose
71
   * conclusion should be added as an equality or predicate to the equality
72
   * engine with no new external premises (d_noExplain).
73
   */
74
  bool isFact() const;
75
};
76
77
/**
78
 * Writes an inference info to a stream.
79
 *
80
 * @param out The stream to write to
81
 * @param ii The inference info to write to the stream
82
 * @return The stream
83
 */
84
std::ostream& operator<<(std::ostream& out, const InferInfo& ii);
85
86
}  // namespace bags
87
}  // namespace theory
88
}  // namespace CVC4
89
90
#endif /* CVC4__THEORY__BAGS__INFER_INFO_H */