GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/quantifiers_state.cpp Lines: 40 80 50.0 %
Date: 2021-03-22 Branches: 61 244 25.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file quantifiers_state.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner, Morgan Deters
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 Utility for quantifiers state
13
 **/
14
15
#include "theory/quantifiers/quantifiers_state.h"
16
17
#include "options/quantifiers_options.h"
18
#include "theory/uf/equality_engine_iterator.h"
19
20
namespace CVC4 {
21
namespace theory {
22
namespace quantifiers {
23
24
8995
QuantifiersState::QuantifiersState(context::Context* c,
25
                                   context::UserContext* u,
26
                                   Valuation val,
27
8995
                                   const LogicInfo& logicInfo)
28
8995
    : TheoryState(c, u, val), d_ierCounterc(c), d_logicInfo(logicInfo)
29
{
30
  // allow theory combination to go first, once initially
31
17990
  d_ierCounter = options::instWhenTcFirst() ? 0 : 1;
32
8995
  d_ierCounterc = d_ierCounter;
33
8995
  d_ierCounterLc = 0;
34
8995
  d_ierCounterLastLc = 0;
35
8995
  d_instWhenPhase =
36
26985
      1 + (options::instWhenPhase() < 1 ? 1 : options::instWhenPhase());
37
8995
}
38
39
26968
void QuantifiersState::incrementInstRoundCounters(Theory::Effort e)
40
{
41
26968
  if (e == Theory::EFFORT_FULL)
42
  {
43
    // increment if a last call happened, we are not strictly enforcing
44
    // interleaving, or already were in phase
45
25008
    if (d_ierCounterLastLc != d_ierCounterLc
46
19234
        || !options::instWhenStrictInterleave()
47
22121
        || d_ierCounter % d_instWhenPhase != 0)
48
    {
49
4459
      d_ierCounter = d_ierCounter + 1;
50
4459
      d_ierCounterLastLc = d_ierCounterLc;
51
4459
      d_ierCounterc = d_ierCounterc.get() + 1;
52
    }
53
  }
54
14464
  else if (e == Theory::EFFORT_LAST_CALL)
55
  {
56
14464
    d_ierCounterLc = d_ierCounterLc + 1;
57
  }
58
26968
}
59
60
47419
bool QuantifiersState::getInstWhenNeedsCheck(Theory::Effort e) const
61
{
62
94838
  Trace("qstate-debug") << "Get inst when needs check, counts=" << d_ierCounter
63
47419
                        << ", " << d_ierCounterLc << std::endl;
64
  // determine if we should perform check, based on instWhenMode
65
47419
  bool performCheck = false;
66
47419
  if (options::instWhenMode() == options::InstWhenMode::FULL)
67
  {
68
12
    performCheck = (e >= Theory::EFFORT_FULL);
69
  }
70
47407
  else if (options::instWhenMode() == options::InstWhenMode::FULL_DELAY)
71
  {
72
    performCheck = (e >= Theory::EFFORT_FULL) && !d_valuation.needCheck();
73
  }
74
47407
  else if (options::instWhenMode() == options::InstWhenMode::FULL_LAST_CALL)
75
  {
76
41781
    performCheck =
77
20614
        ((e == Theory::EFFORT_FULL && d_ierCounter % d_instWhenPhase != 0)
78
81405
         || e == Theory::EFFORT_LAST_CALL);
79
  }
80
11252
  else if (options::instWhenMode()
81
5626
           == options::InstWhenMode::FULL_DELAY_LAST_CALL)
82
  {
83
    performCheck = ((e == Theory::EFFORT_FULL && !d_valuation.needCheck()
84
                     && d_ierCounter % d_instWhenPhase != 0)
85
                    || e == Theory::EFFORT_LAST_CALL);
86
  }
87
5626
  else if (options::instWhenMode() == options::InstWhenMode::LAST_CALL)
88
  {
89
5626
    performCheck = (e >= Theory::EFFORT_LAST_CALL);
90
  }
91
  else
92
  {
93
    performCheck = true;
94
  }
95
47419
  Trace("qstate-debug") << "...returned " << performCheck << std::endl;
96
47419
  return performCheck;
97
}
98
99
uint64_t QuantifiersState::getInstRoundDepth() const
100
{
101
  return d_ierCounterc.get();
102
}
103
104
uint64_t QuantifiersState::getInstRounds() const { return d_ierCounter; }
105
106
void QuantifiersState::debugPrintEqualityEngine(const char* c) const
107
{
108
  bool traceEnabled = Trace.isOn(c);
109
  if (!traceEnabled)
110
  {
111
    return;
112
  }
113
  eq::EqualityEngine* ee = getEqualityEngine();
114
  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee);
115
  std::map<TypeNode, uint64_t> tnum;
116
  while (!eqcs_i.isFinished())
117
  {
118
    TNode r = (*eqcs_i);
119
    TypeNode tr = r.getType();
120
    if (tnum.find(tr) == tnum.end())
121
    {
122
      tnum[tr] = 0;
123
    }
124
    tnum[tr]++;
125
    bool firstTime = true;
126
    Trace(c) << "  " << r;
127
    Trace(c) << " : { ";
128
    eq::EqClassIterator eqc_i = eq::EqClassIterator(r, ee);
129
    while (!eqc_i.isFinished())
130
    {
131
      TNode n = (*eqc_i);
132
      if (r != n)
133
      {
134
        if (firstTime)
135
        {
136
          Trace(c) << std::endl;
137
          firstTime = false;
138
        }
139
        Trace(c) << "    " << n << std::endl;
140
      }
141
      ++eqc_i;
142
    }
143
    if (!firstTime)
144
    {
145
      Trace(c) << "  ";
146
    }
147
    Trace(c) << "}" << std::endl;
148
    ++eqcs_i;
149
  }
150
  Trace(c) << std::endl;
151
  for (const std::pair<const TypeNode, uint64_t>& t : tnum)
152
  {
153
    Trace(c) << "# eqc for " << t.first << " : " << t.second << std::endl;
154
  }
155
}
156
157
3985
const LogicInfo& QuantifiersState::getLogicInfo() const { return d_logicInfo; }
158
159
}  // namespace quantifiers
160
}  // namespace theory
161
63278
}  // namespace CVC4