GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/inference_manager.cpp Lines: 48 65 73.8 %
Date: 2021-03-23 Branches: 48 146 32.9 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file inference_manager.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Gereon Kremer, Makai Mann, Mathias Preiner
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 the inference manager for the theory of strings.
13
 **/
14
15
#include "theory/arith/inference_manager.h"
16
17
#include "options/arith_options.h"
18
#include "theory/arith/arith_state.h"
19
#include "theory/arith/theory_arith.h"
20
#include "theory/rewriter.h"
21
22
namespace CVC4 {
23
namespace theory {
24
namespace arith {
25
26
8997
InferenceManager::InferenceManager(TheoryArith& ta,
27
                                   ArithState& astate,
28
8997
                                   ProofNodeManager* pnm)
29
8997
    : InferenceManagerBuffered(ta, astate, pnm, "theory::arith")
30
{
31
8997
}
32
33
8717
void InferenceManager::addPendingLemma(std::unique_ptr<SimpleTheoryLemma> lemma,
34
                                       bool isWaiting)
35
{
36
17434
  Trace("arith::infman") << "Add " << lemma->getId() << " " << lemma->d_node
37
8717
                         << (isWaiting ? " as waiting" : "") << std::endl;
38
8717
  if (hasCachedLemma(lemma->d_node, lemma->d_property))
39
  {
40
136
    return;
41
  }
42
8581
  if (isEntailedFalse(*lemma))
43
  {
44
    if (isWaiting)
45
    {
46
      d_waitingLem.clear();
47
    }
48
    else
49
    {
50
      d_pendingLem.clear();
51
      d_theoryState.notifyInConflict();
52
    }
53
  }
54
8581
  if (isWaiting)
55
  {
56
2264
    d_waitingLem.emplace_back(std::move(lemma));
57
  }
58
  else
59
  {
60
6317
    d_pendingLem.emplace_back(std::move(lemma));
61
  }
62
}
63
2525
void InferenceManager::addPendingLemma(const SimpleTheoryLemma& lemma,
64
                                       bool isWaiting)
65
{
66
5050
  addPendingLemma(
67
5050
      std::unique_ptr<SimpleTheoryLemma>(new SimpleTheoryLemma(lemma)),
68
      isWaiting);
69
2525
}
70
6192
void InferenceManager::addPendingLemma(const Node& lemma,
71
                                       InferenceId inftype,
72
                                       ProofGenerator* pg,
73
                                       bool isWaiting,
74
                                       LemmaProperty p)
75
{
76
12384
  addPendingLemma(std::unique_ptr<SimpleTheoryLemma>(
77
6192
                      new SimpleTheoryLemma(inftype, lemma, p, pg)),
78
                  isWaiting);
79
6192
}
80
81
494
void InferenceManager::flushWaitingLemmas()
82
{
83
1243
  for (auto& lem : d_waitingLem)
84
  {
85
1498
    Trace("arith::infman") << "Flush waiting lemma to pending: "
86
1498
                           << lem->getId() << " " << lem->d_node
87
749
                           << std::endl;
88
749
    d_pendingLem.emplace_back(std::move(lem));
89
  }
90
494
  d_waitingLem.clear();
91
494
}
92
2807
void InferenceManager::clearWaitingLemmas()
93
{
94
2807
  d_waitingLem.clear();
95
2807
}
96
97
2964
bool InferenceManager::hasUsed() const
98
{
99
2964
  return hasSent() || hasPending();
100
}
101
102
187
bool InferenceManager::hasWaitingLemma() const
103
{
104
187
  return !d_waitingLem.empty();
105
}
106
107
4228
std::size_t InferenceManager::numWaitingLemmas() const
108
{
109
4228
  return d_waitingLem.size();
110
}
111
112
8717
bool InferenceManager::hasCachedLemma(TNode lem, LemmaProperty p)
113
{
114
17434
  Node rewritten = Rewriter::rewrite(lem);
115
17434
  return TheoryInferenceManager::hasCachedLemma(rewritten, p);
116
}
117
118
155749
bool InferenceManager::cacheLemma(TNode lem, LemmaProperty p)
119
{
120
311498
  Node rewritten = Rewriter::rewrite(lem);
121
311498
  return TheoryInferenceManager::cacheLemma(rewritten, p);
122
}
123
124
8581
bool InferenceManager::isEntailedFalse(const SimpleTheoryLemma& lem)
125
{
126
17162
  if (options::nlExtEntailConflicts())
127
  {
128
    Node ch_lemma = lem.d_node.negate();
129
    ch_lemma = Rewriter::rewrite(ch_lemma);
130
    Trace("arith-inf-manager") << "InferenceManager::Check entailment of "
131
                               << ch_lemma << "..." << std::endl;
132
133
    std::pair<bool, Node> et = d_theory.getValuation().entailmentCheck(
134
        options::TheoryOfMode::THEORY_OF_TYPE_BASED, ch_lemma);
135
    Trace("arith-inf-manager") << "entailment test result : " << et.first << " "
136
                               << et.second << std::endl;
137
    if (et.first)
138
    {
139
      Trace("arith-inf-manager")
140
          << "*** Lemma entailed to be in conflict : " << lem.d_node
141
          << std::endl;
142
      return true;
143
    }
144
  }
145
8581
  return false;
146
}
147
148
}  // namespace arith
149
}  // namespace theory
150
35266
}  // namespace CVC4