GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/theory_inference.h Lines: 8 11 72.7 %
Date: 2021-03-22 Branches: 1 2 50.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_inference.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 theory inference utility
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__THEORY_INFERENCE_H
18
#define CVC4__THEORY__THEORY_INFERENCE_H
19
20
#include "expr/node.h"
21
#include "theory/inference_id.h"
22
#include "theory/output_channel.h"
23
24
namespace CVC4 {
25
namespace theory {
26
27
class TheoryInferenceManager;
28
29
/**
30
 * A theory inference base class. This class is an abstract data structure for
31
 * storing pending lemmas or facts in the buffered inference manager. It can
32
 * be seen a single use object capturing instructions for making a single
33
 * call to TheoryInferenceManager for lemmas or facts.
34
 */
35
61043
class TheoryInference
36
{
37
 public:
38
579437
  TheoryInference(InferenceId id) : d_id(id) {}
39
639847
  virtual ~TheoryInference() {}
40
41
  /**
42
   * Process lemma, return the trust node to pass to
43
   * TheoryInferenceManager::trustedLemma. In addition, the inference should
44
   * process any internal side effects of the lemma.
45
   *
46
   * @param p The property of the lemma which will be passed to trustedLemma
47
   * for this inference. If this call does not update p, the default value will
48
   * be used.
49
   * @return The trust node (of kind TrustNodeKind::LEMMA) corresponding to the
50
   * lemma and its proof generator.
51
   */
52
  virtual TrustNode processLemma(LemmaProperty& p) { return TrustNode::null(); }
53
  /**
54
   * Process internal fact, return the conclusion to pass to
55
   * TheoryInferenceManager::assertInternalFact. In addition, the inference
56
   * should process any internal side effects of the fact.
57
   *
58
   * @param exp The explanation for the returned conclusion. Each node added to
59
   * exp should be a (conjunction of) literals that hold in the current equality
60
   * engine.
61
   * @return The (possibly negated) conclusion.
62
   */
63
  virtual Node processFact(std::vector<Node>& exp, ProofGenerator*& pg)
64
  {
65
    return Node::null();
66
  }
67
68
  /** Get the InferenceId of this theory inference. */
69
1077421
  InferenceId getId() const { return d_id; }
70
  /** Set the InferenceId of this theory inference. */
71
13472
  void setId(InferenceId id) { d_id = id; }
72
73
 private:
74
  InferenceId d_id;
75
};
76
77
/**
78
 * A simple theory lemma with no side effects. Makes a single call to
79
 * trustedLemma in its process method.
80
 */
81
4441
class SimpleTheoryLemma : public TheoryInference
82
{
83
 public:
84
  SimpleTheoryLemma(InferenceId id, Node n, LemmaProperty p, ProofGenerator* pg);
85
185650
  virtual ~SimpleTheoryLemma() {}
86
  /** Process lemma */
87
  TrustNode processLemma(LemmaProperty& p) override;
88
  /** The lemma to send */
89
  Node d_node;
90
  /** The lemma property (see OutputChannel::lemma) */
91
  LemmaProperty d_property;
92
  /**
93
   * The proof generator for this lemma, which if non-null, is wrapped in a
94
   * TrustNode to be set on the output channel via trustedLemma at the time
95
   * the lemma is sent. This proof generator must be able to provide a proof
96
   * for d_node in the remainder of the user context.
97
   */
98
  ProofGenerator* d_pg;
99
};
100
101
/**
102
 * A simple internal fact with no side effects. Makes a single call to
103
 * assertInternalFact in its process method.
104
 */
105
class SimpleTheoryInternalFact : public TheoryInference
106
{
107
 public:
108
  SimpleTheoryInternalFact(InferenceId id, Node conc, Node exp, ProofGenerator* pg);
109
435864
  virtual ~SimpleTheoryInternalFact() {}
110
  /** Process internal fact */
111
  Node processFact(std::vector<Node>& exp, ProofGenerator*& pg) override;
112
  /** The lemma to send */
113
  Node d_conc;
114
  /** The explanation */
115
  Node d_exp;
116
  /** The proof generator */
117
  ProofGenerator* d_pg;
118
};
119
120
}  // namespace theory
121
}  // namespace CVC4
122
123
#endif