GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/ematching/inst_match_generator_simple.cpp Lines: 79 90 87.8 %
Date: 2021-03-22 Branches: 187 436 42.9 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file inst_match_generator_simple.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Morgan Deters, 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  simple inst match generator class
13
 **/
14
#include "theory/quantifiers/ematching/inst_match_generator_simple.h"
15
16
#include "options/quantifiers_options.h"
17
#include "theory/quantifiers/ematching/trigger_term_info.h"
18
#include "theory/quantifiers/ematching/trigger_trie.h"
19
#include "theory/quantifiers/instantiate.h"
20
#include "theory/quantifiers/quantifiers_state.h"
21
#include "theory/quantifiers/term_database.h"
22
#include "theory/quantifiers/term_util.h"
23
#include "theory/quantifiers_engine.h"
24
25
using namespace CVC4::kind;
26
27
namespace CVC4 {
28
namespace theory {
29
namespace inst {
30
31
7660
InstMatchGeneratorSimple::InstMatchGeneratorSimple(Trigger* tparent,
32
                                                   Node q,
33
7660
                                                   Node pat)
34
7660
    : IMGenerator(tparent), d_quant(q), d_match_pattern(pat)
35
{
36
7660
  if (d_match_pattern.getKind() == NOT)
37
  {
38
1276
    d_match_pattern = d_match_pattern[0];
39
1276
    d_pol = false;
40
  }
41
  else
42
  {
43
6384
    d_pol = true;
44
  }
45
7660
  if (d_match_pattern.getKind() == EQUAL)
46
  {
47
1276
    d_eqc = d_match_pattern[1];
48
1276
    d_match_pattern = d_match_pattern[0];
49
1276
    Assert(!quantifiers::TermUtil::hasInstConstAttr(d_eqc));
50
  }
51
7660
  Assert(TriggerTermInfo::isSimpleTrigger(d_match_pattern));
52
24755
  for (size_t i = 0, nchild = d_match_pattern.getNumChildren(); i < nchild; i++)
53
  {
54
17095
    if (d_match_pattern[i].getKind() == INST_CONSTANT)
55
    {
56
26652
      if (!options::cegqi()
57
26652
          || quantifiers::TermUtil::getInstConstAttr(d_match_pattern[i]) == q)
58
      {
59
13326
        d_var_num[i] = d_match_pattern[i].getAttribute(InstVarNumAttribute());
60
      }
61
      else
62
      {
63
        d_var_num[i] = -1;
64
      }
65
    }
66
17095
    d_match_pattern_arg_types.push_back(d_match_pattern[i].getType());
67
  }
68
7660
  quantifiers::TermDb* tdb = getQuantifiersEngine()->getTermDatabase();
69
7660
  d_op = tdb->getMatchOperator(d_match_pattern);
70
7660
}
71
72
80694
void InstMatchGeneratorSimple::resetInstantiationRound() {}
73
25761
uint64_t InstMatchGeneratorSimple::addInstantiations(Node q)
74
{
75
25761
  uint64_t addedLemmas = 0;
76
  TNodeTrie* tat;
77
25761
  quantifiers::TermDb* tdb = getQuantifiersEngine()->getTermDatabase();
78
25761
  if (d_eqc.isNull())
79
  {
80
21950
    tat = tdb->getTermArgTrie(d_op);
81
  }
82
  else
83
  {
84
3811
    if (d_pol)
85
    {
86
      tat = tdb->getTermArgTrie(d_eqc, d_op);
87
    }
88
    else
89
    {
90
      // iterate over all classes except r
91
3811
      tat = tdb->getTermArgTrie(Node::null(), d_op);
92
3811
      if (tat && !d_qstate.isInConflict())
93
      {
94
7622
        Node r = d_qstate.getRepresentative(d_eqc);
95
12720
        for (std::pair<const TNode, TNodeTrie>& t : tat->d_data)
96
        {
97
8909
          if (t.first != r)
98
          {
99
12956
            InstMatch m(q);
100
6478
            addInstantiations(m, addedLemmas, 0, &(t.second));
101
6478
            if (d_qstate.isInConflict())
102
            {
103
              break;
104
            }
105
          }
106
        }
107
      }
108
3811
      tat = nullptr;
109
    }
110
  }
111
51522
  Debug("simple-trigger-debug")
112
25761
      << "Adding instantiations based on " << tat << " from " << d_op << " "
113
25761
      << d_eqc << std::endl;
114
25761
  if (tat && !d_qstate.isInConflict())
115
  {
116
27976
    InstMatch m(q);
117
13988
    addInstantiations(m, addedLemmas, 0, tat);
118
  }
119
25761
  return addedLemmas;
120
}
121
122
192347
void InstMatchGeneratorSimple::addInstantiations(InstMatch& m,
123
                                                 uint64_t& addedLemmas,
124
                                                 size_t argIndex,
125
                                                 TNodeTrie* tat)
126
{
127
384694
  Debug("simple-trigger-debug")
128
192347
      << "Add inst " << argIndex << " " << d_match_pattern << std::endl;
129
192347
  if (argIndex == d_match_pattern.getNumChildren())
130
  {
131
68907
    Assert(!tat->d_data.empty());
132
137814
    TNode t = tat->getData();
133
68907
    Debug("simple-trigger") << "Actual term is " << t << std::endl;
134
    // convert to actual used terms
135
176847
    for (const auto& v : d_var_num)
136
    {
137
107940
      if (v.second >= 0)
138
      {
139
107940
        Assert(v.first < t.getNumChildren());
140
215880
        Debug("simple-trigger")
141
107940
            << "...set " << v.second << " " << t[v.first] << std::endl;
142
107940
        m.setValue(v.second, t[v.first]);
143
      }
144
    }
145
    // we do not need the trigger parent for simple triggers (no post-processing
146
    // required)
147
68907
    if (sendInstantiation(m, InferenceId::QUANTIFIERS_INST_E_MATCHING_SIMPLE))
148
    {
149
13560
      addedLemmas++;
150
13560
      Debug("simple-trigger") << "-> Produced instantiation " << m << std::endl;
151
    }
152
68907
    return;
153
  }
154
123440
  if (d_match_pattern[argIndex].getKind() == INST_CONSTANT)
155
  {
156
49139
    int v = d_var_num[argIndex];
157
49139
    if (v != -1)
158
    {
159
213139
      for (std::pair<const TNode, TNodeTrie>& tt : tat->d_data)
160
      {
161
328000
        Node t = tt.first;
162
328000
        Node prev = m.get(v);
163
        // using representatives, just check if equal
164
164000
        Assert(t.getType().isComparableTo(d_match_pattern_arg_types[argIndex]));
165
164000
        if (prev.isNull() || prev == t)
166
        {
167
159792
          m.setValue(v, t);
168
159792
          addInstantiations(m, addedLemmas, argIndex + 1, &(tt.second));
169
159792
          m.setValue(v, prev);
170
159792
          if (d_qstate.isInConflict())
171
          {
172
            break;
173
          }
174
        }
175
      }
176
49139
      return;
177
    }
178
    // inst constant from another quantified formula, treat as ground term?
179
  }
180
148602
  Node r = d_qstate.getRepresentative(d_match_pattern[argIndex]);
181
74301
  std::map<TNode, TNodeTrie>::iterator it = tat->d_data.find(r);
182
74301
  if (it != tat->d_data.end())
183
  {
184
12089
    addInstantiations(m, addedLemmas, argIndex + 1, &(it->second));
185
  }
186
}
187
188
int InstMatchGeneratorSimple::getActiveScore()
189
{
190
  quantifiers::TermDb* tdb = getQuantifiersEngine()->getTermDatabase();
191
  Node f = tdb->getMatchOperator(d_match_pattern);
192
  size_t ngt = tdb->getNumGroundTerms(f);
193
  Trace("trigger-active-sel-debug") << "Number of ground terms for (simple) "
194
                                    << f << " is " << ngt << std::endl;
195
  return static_cast<int>(ngt);
196
}
197
198
}  // namespace inst
199
}  // namespace theory
200
26676
}  // namespace CVC4