GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp Lines: 51 80 63.8 %
Date: 2021-03-22 Branches: 86 236 36.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file inst_strategy_e_matching_user.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, 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 Implementation of e matching instantiation strategies
13
 **/
14
15
#include "theory/quantifiers/ematching/inst_strategy_e_matching_user.h"
16
17
#include "theory/quantifiers/ematching/pattern_term_selector.h"
18
#include "theory/quantifiers/quantifiers_state.h"
19
#include "theory/quantifiers_engine.h"
20
21
using namespace CVC4::kind;
22
using namespace CVC4::theory::inst;
23
24
namespace CVC4 {
25
namespace theory {
26
namespace quantifiers {
27
28
5823
InstStrategyUserPatterns::InstStrategyUserPatterns(
29
    QuantifiersEngine* ie,
30
    QuantifiersState& qs,
31
    QuantifiersInferenceManager& qim,
32
5823
    QuantifiersRegistry& qr)
33
5823
    : InstStrategy(ie, qs, qim, qr)
34
{
35
5823
}
36
11640
InstStrategyUserPatterns::~InstStrategyUserPatterns() {}
37
38
size_t InstStrategyUserPatterns::getNumUserGenerators(Node q) const
39
{
40
  std::map<Node, std::vector<inst::Trigger*> >::const_iterator it =
41
      d_user_gen.find(q);
42
  if (it == d_user_gen.end())
43
  {
44
    return 0;
45
  }
46
  return it->second.size();
47
}
48
49
inst::Trigger* InstStrategyUserPatterns::getUserGenerator(Node q,
50
                                                          size_t i) const
51
{
52
  std::map<Node, std::vector<inst::Trigger*> >::const_iterator it =
53
      d_user_gen.find(q);
54
  if (it == d_user_gen.end())
55
  {
56
    return nullptr;
57
  }
58
  Assert(i < it->second.size());
59
  return it->second[i];
60
}
61
62
80632
std::string InstStrategyUserPatterns::identify() const
63
{
64
80632
  return std::string("UserPatterns");
65
}
66
67
24165
void InstStrategyUserPatterns::processResetInstantiationRound(
68
    Theory::Effort effort)
69
{
70
24165
  Trace("inst-alg-debug") << "reset user triggers" << std::endl;
71
  // reset triggers
72
147065
  for (std::pair<const Node, std::vector<Trigger*> >& u : d_user_gen)
73
  {
74
182975
    for (Trigger* t : u.second)
75
    {
76
60075
      t->resetInstantiationRound();
77
60075
      t->reset(Node::null());
78
    }
79
  }
80
24165
  Trace("inst-alg-debug") << "done reset user triggers" << std::endl;
81
24165
}
82
83
80632
InstStrategyStatus InstStrategyUserPatterns::process(Node q,
84
                                                     Theory::Effort effort,
85
                                                     int e)
86
{
87
80632
  if (e == 0)
88
  {
89
40316
    return InstStrategyStatus::STATUS_UNFINISHED;
90
  }
91
40316
  options::UserPatMode upm = getInstUserPatMode();
92
40316
  int peffort = upm == options::UserPatMode::RESORT ? 2 : 1;
93
40316
  if (e < peffort)
94
  {
95
    return InstStrategyStatus::STATUS_UNFINISHED;
96
  }
97
40316
  if (e != peffort)
98
  {
99
    return InstStrategyStatus::STATUS_UNKNOWN;
100
  }
101
40316
  d_counter[q]++;
102
103
80632
  Trace("inst-alg") << "-> User-provided instantiate " << q << "..."
104
40316
                    << std::endl;
105
40316
  if (upm == options::UserPatMode::RESORT)
106
  {
107
    std::vector<std::vector<Node> >& ugw = d_user_gen_wait[q];
108
    for (size_t i = 0, usize = ugw.size(); i < usize; i++)
109
    {
110
      Trigger* t = Trigger::mkTrigger(d_quantEngine,
111
                                      d_qstate,
112
                                      d_qim,
113
                                      d_qreg,
114
                                      q,
115
                                      ugw[i],
116
                                      true,
117
                                      Trigger::TR_RETURN_NULL);
118
      if (t)
119
      {
120
        d_user_gen[q].push_back(t);
121
      }
122
    }
123
    ugw.clear();
124
  }
125
126
40316
  std::vector<inst::Trigger*>& ug = d_user_gen[q];
127
52923
  for (Trigger* t : ug)
128
  {
129
12607
    if (Trace.isOn("process-trigger"))
130
    {
131
      Trace("process-trigger") << "  Process (user) ";
132
      t->debugPrint("process-trigger");
133
      Trace("process-trigger") << "..." << std::endl;
134
    }
135
12607
    unsigned numInst = t->addInstantiations();
136
25214
    Trace("process-trigger")
137
12607
        << "  Done, numInst = " << numInst << "." << std::endl;
138
12607
    if (d_qstate.isInConflict())
139
    {
140
      // we are already in conflict
141
      break;
142
    }
143
  }
144
40316
  return InstStrategyStatus::STATUS_UNKNOWN;
145
}
146
147
3748
void InstStrategyUserPatterns::addUserPattern(Node q, Node pat)
148
{
149
3748
  Assert(pat.getKind() == INST_PATTERN);
150
  // add to generators
151
7471
  std::vector<Node> nodes;
152
7688
  for (const Node& p : pat)
153
  {
154
7905
    Node pat_use = PatternTermSelector::getIsUsableTrigger(p, q);
155
3965
    if (pat_use.isNull())
156
    {
157
50
      Trace("trigger-warn") << "User-provided trigger is not usable : " << pat
158
25
                            << " because of " << p << std::endl;
159
25
      return;
160
    }
161
3940
    nodes.push_back(pat_use);
162
  }
163
3723
  Trace("user-pat") << "Add user pattern: " << pat << " for " << q << std::endl;
164
  // check match option
165
3723
  if (getInstUserPatMode() == options::UserPatMode::RESORT)
166
  {
167
    d_user_gen_wait[q].push_back(nodes);
168
    return;
169
  }
170
7446
  Trigger* t = Trigger::mkTrigger(d_quantEngine,
171
                                  d_qstate,
172
                                  d_qim,
173
                                  d_qreg,
174
                                  q,
175
                                  nodes,
176
                                  true,
177
3723
                                  Trigger::TR_MAKE_NEW);
178
3723
  if (t)
179
  {
180
3723
    d_user_gen[q].push_back(t);
181
  }
182
  else
183
  {
184
    Trace("trigger-warn") << "Failed to construct trigger : " << pat
185
                          << " due to variable mismatch" << std::endl;
186
  }
187
}
188
189
}  // namespace quantifiers
190
}  // namespace theory
191
26676
}  // namespace CVC4