GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/theory_inference.cpp Lines: 13 17 76.5 %
Date: 2021-03-22 Branches: 8 30 26.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_inference.cpp
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 "theory/theory_inference.h"
16
17
#include "theory/theory_inference_manager.h"
18
19
using namespace CVC4::kind;
20
21
namespace CVC4 {
22
namespace theory {
23
24
90682
SimpleTheoryLemma::SimpleTheoryLemma(InferenceId id,
25
                                     Node n,
26
                                     LemmaProperty p,
27
90682
                                     ProofGenerator* pg)
28
90682
    : TheoryInference(id), d_node(n), d_property(p), d_pg(pg)
29
{
30
90682
}
31
32
88867
TrustNode SimpleTheoryLemma::processLemma(LemmaProperty& p)
33
{
34
88867
  Assert(!d_node.isNull());
35
88867
  p = d_property;
36
88867
  return TrustNode::mkTrustLemma(d_node, d_pg);
37
}
38
39
435864
SimpleTheoryInternalFact::SimpleTheoryInternalFact(InferenceId id,
40
                                                   Node conc,
41
                                                   Node exp,
42
435864
                                                   ProofGenerator* pg)
43
435864
    : TheoryInference(id), d_conc(conc), d_exp(exp), d_pg(pg)
44
{
45
435864
}
46
47
Node SimpleTheoryInternalFact::processFact(std::vector<Node>& exp,
48
                                           ProofGenerator*& pg)
49
{
50
  exp.push_back(d_exp);
51
  pg = d_pg;
52
  return d_conc;
53
}
54
55
}  // namespace theory
56
26676
}  // namespace CVC4