GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bags/infer_info.cpp Lines: 14 32 43.8 %
Date: 2021-03-23 Branches: 20 122 16.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file infer_info.cpp
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 Implementation of inference information utility.
13
 **/
14
15
#include "theory/bags/infer_info.h"
16
17
#include "theory/bags/inference_manager.h"
18
19
namespace CVC4 {
20
namespace theory {
21
namespace bags {
22
23
2196
InferInfo::InferInfo(TheoryInferenceManager* im, InferenceId id)
24
2196
    : TheoryInference(id), d_im(im)
25
{
26
2196
}
27
28
2196
TrustNode InferInfo::processLemma(LemmaProperty& p)
29
{
30
2196
  NodeManager* nm = NodeManager::currentNM();
31
4392
  Node pnode = nm->mkAnd(d_premises);
32
4392
  Node lemma = nm->mkNode(kind::IMPLIES, pnode, d_conclusion);
33
34
  // send lemmas corresponding to the skolems introduced
35
3040
  for (const auto& pair : d_skolems)
36
  {
37
1688
    Node n = pair.first.eqNode(pair.second);
38
1688
    TrustNode trustedLemma = TrustNode::mkTrustLemma(n, nullptr);
39
844
    d_im->trustedLemma(trustedLemma, getId(), p);
40
  }
41
42
2196
  Trace("bags::InferInfo::process") << (*this) << std::endl;
43
44
4392
  return TrustNode::mkTrustLemma(lemma, nullptr);
45
}
46
47
bool InferInfo::isTrivial() const
48
{
49
  Assert(!d_conclusion.isNull());
50
  return d_conclusion.isConst() && d_conclusion.getConst<bool>();
51
}
52
53
bool InferInfo::isConflict() const
54
{
55
  Assert(!d_conclusion.isNull());
56
  return d_conclusion.isConst() && !d_conclusion.getConst<bool>();
57
}
58
59
bool InferInfo::isFact() const
60
{
61
  Assert(!d_conclusion.isNull());
62
  TNode atom =
63
      d_conclusion.getKind() == kind::NOT ? d_conclusion[0] : d_conclusion;
64
  return !atom.isConst() && atom.getKind() != kind::OR;
65
}
66
67
std::ostream& operator<<(std::ostream& out, const InferInfo& ii)
68
{
69
  out << "(infer :id " << ii.getId() << std::endl;
70
  out << ":conclusion " << ii.d_conclusion << std::endl;
71
  if (!ii.d_premises.empty())
72
  {
73
    out << " :premise (" << ii.d_premises << ")" << std::endl;
74
  }
75
  out << ":skolems " << ii.d_skolems << std::endl;
76
  out << ")";
77
  return out;
78
}
79
80
}  // namespace bags
81
}  // namespace theory
82
26685
}  // namespace CVC4