GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/inst_strategy_enumerative.cpp Lines: 80 95 84.2 %
Date: 2021-03-23 Branches: 133 304 43.8 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file inst_strategy_enumerative.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 an enumerative instantiation strategy.
13
 **/
14
15
#include "theory/quantifiers/inst_strategy_enumerative.h"
16
17
#include "options/quantifiers_options.h"
18
#include "theory/quantifiers/instantiate.h"
19
#include "theory/quantifiers/relevant_domain.h"
20
#include "theory/quantifiers/term_database.h"
21
#include "theory/quantifiers/term_tuple_enumerator.h"
22
#include "theory/quantifiers/term_util.h"
23
#include "theory/quantifiers_engine.h"
24
25
namespace CVC4 {
26
27
using namespace kind;
28
using namespace context;
29
30
namespace theory {
31
32
using namespace inst;
33
34
namespace quantifiers {
35
36
79
InstStrategyEnum::InstStrategyEnum(QuantifiersEngine* qe,
37
                                   QuantifiersState& qs,
38
                                   QuantifiersInferenceManager& qim,
39
                                   QuantifiersRegistry& qr,
40
79
                                   RelevantDomain* rd)
41
79
    : QuantifiersModule(qs, qim, qr, qe), d_rd(rd), d_fullSaturateLimit(-1)
42
{
43
79
}
44
79
void InstStrategyEnum::presolve()
45
{
46
164
  d_fullSaturateLimit = options::fullSaturateLimit();
47
79
}
48
5034
bool InstStrategyEnum::needsCheck(Theory::Effort e)
49
{
50
5034
  if (d_fullSaturateLimit == 0)
51
  {
52
    return false;
53
  }
54
17026
  if (options::fullSaturateInterleave())
55
  {
56
    // if interleaved, we run at the same time as E-matching
57
    if (d_qstate.getInstWhenNeedsCheck(e))
58
    {
59
      return true;
60
    }
61
  }
62
17231
  if (options::fullSaturateQuant())
63
  {
64
5034
    if (e >= Theory::EFFORT_LAST_CALL)
65
    {
66
305
      return true;
67
    }
68
  }
69
4729
  return false;
70
}
71
72
1116
void InstStrategyEnum::reset_round(Theory::Effort e) {}
73
983
void InstStrategyEnum::check(Theory::Effort e, QEffort quant_e)
74
{
75
983
  bool doCheck = false;
76
983
  bool fullEffort = false;
77
983
  if (d_fullSaturateLimit != 0)
78
  {
79
983
    if (options::fullSaturateInterleave())
80
    {
81
      // we only add when interleaved with other strategies
82
      doCheck = quant_e == QEFFORT_STANDARD && d_qim.hasPendingLemma();
83
    }
84
983
    if (options::fullSaturateQuant() && !doCheck)
85
    {
86
983
      if (!d_qstate.getValuation().needCheck())
87
      {
88
739
        doCheck = quant_e == QEFFORT_LAST_CALL;
89
739
        fullEffort = true;
90
      }
91
    }
92
  }
93
983
  if (!doCheck)
94
  {
95
856
    return;
96
  }
97
127
  Assert(!d_qstate.isInConflict());
98
127
  double clSet = 0;
99
127
  if (Trace.isOn("fs-engine"))
100
  {
101
    clSet = double(clock()) / double(CLOCKS_PER_SEC);
102
    Trace("fs-engine") << "---Full Saturation Round, effort = " << e << "---"
103
                       << std::endl;
104
  }
105
254
  unsigned rstart = options::fullSaturateQuantRd() ? 0 : 1;
106
127
  unsigned rend = fullEffort ? 1 : rstart;
107
127
  unsigned addedLemmas = 0;
108
  // First try in relevant domain of all quantified formulas, if no
109
  // instantiations exist, try arbitrary ground terms.
110
  // Notice that this stratification of effort levels makes it so that some
111
  // quantified formulas may not be instantiated (if they have no instances
112
  // at effort level r=0 but another quantified formula does). We prefer
113
  // this stratification since effort level r=1 may be highly expensive in the
114
  // case where we have a quantified formula with many entailed instances.
115
127
  FirstOrderModel* fm = d_quantEngine->getModel();
116
127
  unsigned nquant = fm->getNumAssertedQuantifiers();
117
254
  std::map<Node, bool> alreadyProc;
118
359
  for (unsigned r = rstart; r <= rend; r++)
119
  {
120
243
    if (d_rd || r > 0)
121
    {
122
243
      if (r == 0)
123
      {
124
127
        Trace("inst-alg") << "-> Relevant domain instantiate..." << std::endl;
125
127
        Trace("inst-alg-debug") << "Compute relevant domain..." << std::endl;
126
127
        d_rd->compute();
127
127
        Trace("inst-alg-debug") << "...finished" << std::endl;
128
      }
129
      else
130
      {
131
116
        Trace("inst-alg") << "-> Ground term instantiate..." << std::endl;
132
      }
133
2720
      for (unsigned i = 0; i < nquant; i++)
134
      {
135
4954
        Node q = fm->getAssertedQuantifier(i, true);
136
7431
        bool doProcess = d_qreg.hasOwnership(q, this)
137
4926
                         && fm->isQuantifierActive(q)
138
9880
                         && alreadyProc.find(q) == alreadyProc.end();
139
2477
        if (doProcess)
140
        {
141
1965
          if (process(q, fullEffort, r == 0))
142
          {
143
            // don't need to mark this if we are not stratifying
144
2559
            if (!options::fullSaturateStratify())
145
            {
146
653
              alreadyProc[q] = true;
147
            }
148
            // added lemma
149
1163
            addedLemmas++;
150
          }
151
1965
          if (d_qstate.isInConflict())
152
          {
153
            break;
154
          }
155
        }
156
      }
157
486
      if (d_qstate.isInConflict()
158
243
          || (addedLemmas > 0 && options::fullSaturateStratify()))
159
      {
160
        // we break if we are in conflict, or if we added any lemma at this
161
        // effort level and we stratify effort levels.
162
11
        break;
163
      }
164
    }
165
  }
166
127
  if (Trace.isOn("fs-engine"))
167
  {
168
    Trace("fs-engine") << "Added lemmas = " << addedLemmas << std::endl;
169
    double clSet2 = double(clock()) / double(CLOCKS_PER_SEC);
170
    Trace("fs-engine") << "Finished full saturation engine, time = "
171
                       << (clSet2 - clSet) << std::endl;
172
  }
173
127
  if (d_fullSaturateLimit > 0)
174
  {
175
    d_fullSaturateLimit--;
176
  }
177
}
178
179
1965
bool InstStrategyEnum::process(Node quantifier, bool fullEffort, bool isRd)
180
{
181
  // ignore if constant true (rare case of non-standard quantifier whose body
182
  // is rewritten to true)
183
1965
  if (quantifier[1].isConst() && quantifier[1].getConst<bool>())
184
  {
185
    return false;
186
  }
187
188
  TermTupleEnumeratorContext ttec;
189
1965
  ttec.d_quantEngine = d_quantEngine;
190
1965
  ttec.d_rd = d_rd;
191
1965
  ttec.d_fullEffort = fullEffort;
192
3930
  ttec.d_increaseSum = options::fullSaturateSum();
193
1965
  ttec.d_isRd = isRd;
194
  std::unique_ptr<TermTupleEnumeratorInterface> enumerator(
195
3930
      mkTermTupleEnumerator(quantifier, &ttec));
196
3930
  std::vector<Node> terms;
197
3930
  std::vector<bool> failMask;
198
1965
  Instantiate* ie = d_quantEngine->getInstantiate();
199
9775
  for (enumerator->init(); enumerator->hasNext();)
200
  {
201
8973
    if (d_qstate.isInConflict())
202
    {
203
      // could be conflicting for an internal reason
204
      return false;
205
    }
206
8973
    enumerator->next(terms);
207
    // try instantiation
208
8973
    failMask.clear();
209
    /* if (ie->addInstantiation(quantifier, terms)) */
210
8973
    if (ie->addInstantiationExpFail(
211
            quantifier, terms, failMask, InferenceId::QUANTIFIERS_INST_ENUM))
212
    {
213
1163
      Trace("inst-alg-rd") << "Success!" << std::endl;
214
1163
      return true;
215
    }
216
    else
217
    {
218
7810
      enumerator->failureReason(failMask);
219
    }
220
  }
221
802
  return false;
222
  // TODO : term enumerator instantiation?
223
}
224
225
}  // namespace quantifiers
226
}  // namespace theory
227
54447
}  // namespace CVC4