GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/strings/infer_info.cpp Lines: 23 33 69.7 %
Date: 2021-03-23 Branches: 39 106 36.8 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file infer_info.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mudathir Mohamed, 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/strings/infer_info.h"
16
17
#include "theory/strings/inference_manager.h"
18
#include "theory/strings/theory_strings_utils.h"
19
20
namespace CVC4 {
21
namespace theory {
22
namespace strings {
23
24
50705
InferInfo::InferInfo(InferenceId id): TheoryInference(id), d_sim(nullptr), d_idRev(false)
25
{
26
50705
}
27
28
14852
TrustNode InferInfo::processLemma(LemmaProperty& p)
29
{
30
14852
  return d_sim->processLemma(*this, p);
31
}
32
33
13355
Node InferInfo::processFact(std::vector<Node>& exp, ProofGenerator*& pg)
34
{
35
55370
  for (const Node& ec : d_premises)
36
  {
37
42015
    utils::flattenOp(kind::AND, ec, exp);
38
  }
39
13355
  d_sim->processFact(*this, pg);
40
13355
  return d_conc;
41
}
42
43
43762
bool InferInfo::isTrivial() const
44
{
45
43762
  Assert(!d_conc.isNull());
46
43762
  return d_conc.isConst() && d_conc.getConst<bool>();
47
}
48
49
43762
bool InferInfo::isConflict() const
50
{
51
43762
  Assert(!d_conc.isNull());
52
43762
  return d_conc.isConst() && !d_conc.getConst<bool>() && d_noExplain.empty();
53
}
54
55
15313
bool InferInfo::isFact() const
56
{
57
15313
  Assert(!d_conc.isNull());
58
30626
  TNode atom = d_conc.getKind() == kind::NOT ? d_conc[0] : d_conc;
59
  // we could process inferences with conjunctive conclusions as facts, where
60
  // the explanation is copied. However, for simplicity, we always send these
61
  // as lemmas. This case happens very infrequently.
62
30612
  return !atom.isConst() && atom.getKind() != kind::OR
63
44829
         && atom.getKind() != kind::AND && d_noExplain.empty();
64
}
65
66
26710
Node InferInfo::getPremises() const
67
{
68
  // d_noExplain is a subset of d_ant
69
26710
  return utils::mkAnd(d_premises);
70
}
71
72
std::ostream& operator<<(std::ostream& out, const InferInfo& ii)
73
{
74
  out << "(infer " << ii.getId() << " " << ii.d_conc;
75
  if (ii.d_idRev)
76
  {
77
    out << " :rev";
78
  }
79
  if (!ii.d_premises.empty())
80
  {
81
    out << " :ant (" << ii.d_premises << ")";
82
  }
83
  if (!ii.d_noExplain.empty())
84
  {
85
    out << " :no-explain (" << ii.d_noExplain << ")";
86
  }
87
  out << ")";
88
  return out;
89
}
90
91
}  // namespace strings
92
}  // namespace theory
93
26685
}  // namespace CVC4