GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp Lines: 88 89 98.9 %
Date: 2021-03-22 Branches: 114 238 47.9 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file inst_match_generator_multi_linear.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds
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 multi-linear inst match generator class
13
 **/
14
#include "theory/quantifiers/ematching/inst_match_generator_multi_linear.h"
15
16
#include "options/quantifiers_options.h"
17
#include "theory/quantifiers_engine.h"
18
#include "theory/quantifiers/ematching/trigger_trie.h"
19
#include "theory/quantifiers/term_util.h"
20
21
using namespace CVC4::kind;
22
23
namespace CVC4 {
24
namespace theory {
25
namespace inst {
26
27
1225
InstMatchGeneratorMultiLinear::InstMatchGeneratorMultiLinear(
28
1225
    Trigger* tparent, Node q, std::vector<Node>& pats)
29
1225
    : InstMatchGenerator(tparent, Node::null())
30
{
31
  // order patterns to maximize eager matching failures
32
2450
  std::map<Node, std::vector<Node> > var_contains;
33
3981
  for (const Node& pat : pats)
34
  {
35
2756
    quantifiers::TermUtil::computeInstConstContainsForQuant(
36
2756
        q, pat, var_contains[pat]);
37
  }
38
2450
  std::map<Node, std::vector<Node> > var_to_node;
39
3981
  for (std::pair<const Node, std::vector<Node> >& vc : var_contains)
40
  {
41
7761
    for (const Node& n : vc.second)
42
    {
43
5005
      var_to_node[n].push_back(vc.first);
44
    }
45
  }
46
2450
  std::vector<Node> pats_ordered;
47
2450
  std::vector<bool> pats_ordered_independent;
48
2450
  std::map<Node, bool> var_bound;
49
1225
  size_t patsSize = pats.size();
50
6737
  while (pats_ordered.size() < patsSize)
51
  {
52
    // score is lexographic ( bound vars, shared vars )
53
2756
    int score_max_1 = -1;
54
2756
    int score_max_2 = -1;
55
2756
    unsigned score_index = 0;
56
2756
    bool set_score_index = false;
57
9336
    for (size_t i = 0; i < patsSize; i++)
58
    {
59
13160
      Node p = pats[i];
60
19740
      if (std::find(pats_ordered.begin(), pats_ordered.end(), p)
61
19740
          == pats_ordered.end())
62
      {
63
4668
        int score_1 = 0;
64
4668
        int score_2 = 0;
65
12882
        for (unsigned j = 0; j < var_contains[p].size(); j++)
66
        {
67
16428
          Node v = var_contains[p][j];
68
8214
          if (var_bound.find(v) != var_bound.end())
69
          {
70
811
            score_1++;
71
          }
72
7403
          else if (var_to_node[v].size() > 1)
73
          {
74
1478
            score_2++;
75
          }
76
        }
77
4668
        if (!set_score_index || score_1 > score_max_1
78
1779
            || (score_1 == score_max_1 && score_2 > score_max_2))
79
        {
80
2934
          score_index = i;
81
2934
          set_score_index = true;
82
2934
          score_max_1 = score_1;
83
2934
          score_max_2 = score_2;
84
        }
85
      }
86
    }
87
2756
    Assert(set_score_index);
88
    // update the variable bounds
89
5512
    Node mp = pats[score_index];
90
2756
    std::vector<Node>& vcm = var_contains[mp];
91
7761
    for (const Node& vc : vcm)
92
    {
93
5005
      var_bound[vc] = true;
94
    }
95
2756
    pats_ordered.push_back(mp);
96
2756
    pats_ordered_independent.push_back(score_max_1 == 0);
97
  }
98
99
2450
  Trace("multi-trigger-linear")
100
1225
      << "Make children for linear multi trigger." << std::endl;
101
3981
  for (size_t i = 0, poSize = pats_ordered.size(); i < poSize; i++)
102
  {
103
5512
    Node po = pats_ordered[i];
104
2756
    Trace("multi-trigger-linear") << "...make for " << po << std::endl;
105
2756
    InstMatchGenerator* cimg = getInstMatchGenerator(tparent, q, po);
106
2756
    Assert(cimg != nullptr);
107
2756
    d_children.push_back(cimg);
108
    // this could be improved
109
2756
    if (i == 0)
110
    {
111
1225
      cimg->setIndependent();
112
    }
113
  }
114
1225
}
115
116
6514
int InstMatchGeneratorMultiLinear::resetChildren()
117
{
118
16611
  for (InstMatchGenerator* c : d_children)
119
  {
120
12086
    if (!c->reset(Node::null()))
121
    {
122
1989
      return -2;
123
    }
124
  }
125
4525
  return 1;
126
}
127
128
8405
bool InstMatchGeneratorMultiLinear::reset(Node eqc)
129
{
130
8405
  Assert(eqc.isNull());
131
27030
  if (options::multiTriggerLinear())
132
  {
133
8405
    return true;
134
  }
135
  return resetChildren() > 0;
136
}
137
138
6514
int InstMatchGeneratorMultiLinear::getNextMatch(Node q, InstMatch& m)
139
{
140
13028
  Trace("multi-trigger-linear-debug")
141
6514
      << "InstMatchGeneratorMultiLinear::getNextMatch : reset " << std::endl;
142
6514
  if (options::multiTriggerLinear())
143
  {
144
    // reset everyone
145
6514
    int rc_ret = resetChildren();
146
6514
    if (rc_ret < 0)
147
    {
148
1989
      return rc_ret;
149
    }
150
  }
151
9050
  Trace("multi-trigger-linear-debug")
152
4525
      << "InstMatchGeneratorMultiLinear::getNextMatch : continue match "
153
4525
      << std::endl;
154
4525
  Assert(d_next != nullptr);
155
  int ret_val =
156
4525
      continueNextMatch(q, m, InferenceId::QUANTIFIERS_INST_E_MATCHING_MTL);
157
4525
  if (ret_val > 0)
158
  {
159
7412
    Trace("multi-trigger-linear")
160
3706
        << "Successful multi-trigger instantiation." << std::endl;
161
3706
    if (options::multiTriggerLinear())
162
    {
163
      // now, restrict everyone
164
11354
      for (size_t i = 0, csize = d_children.size(); i < csize; i++)
165
      {
166
15296
        Node mi = d_children[i]->getCurrentMatch();
167
15296
        Trace("multi-trigger-linear")
168
7648
            << "   child " << i << " match : " << mi << std::endl;
169
7648
        d_children[i]->excludeMatch(mi);
170
      }
171
    }
172
  }
173
4525
  return ret_val;
174
}
175
176
}  // namespace inst
177
}  // namespace theory
178
45301
}  // namespace CVC4