GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/quant_split.cpp Lines: 98 100 98.0 %
Date: 2021-03-22 Branches: 198 386 51.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file quant_split.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 Implementation of dynamic quantifiers splitting
13
 **/
14
15
#include "theory/quantifiers/quant_split.h"
16
17
#include "expr/dtype.h"
18
#include "expr/dtype_cons.h"
19
#include "theory/quantifiers/term_database.h"
20
#include "theory/quantifiers_engine.h"
21
#include "theory/quantifiers/first_order_model.h"
22
#include "options/quantifiers_options.h"
23
24
using namespace std;
25
using namespace CVC4;
26
using namespace CVC4::kind;
27
using namespace CVC4::context;
28
using namespace CVC4::theory;
29
using namespace CVC4::theory::quantifiers;
30
31
5006
QuantDSplit::QuantDSplit(QuantifiersEngine* qe,
32
                         QuantifiersState& qs,
33
                         QuantifiersInferenceManager& qim,
34
5006
                         QuantifiersRegistry& qr)
35
5006
    : QuantifiersModule(qs, qim, qr, qe), d_added_split(qs.getUserContext())
36
{
37
5006
}
38
39
11455
void QuantDSplit::checkOwnership(Node q)
40
{
41
  // If q is non-standard (marked as sygus, quantifier elimination, etc.), then
42
  // do no split it.
43
22102
  QAttributes qa;
44
11455
  QuantAttributes::computeQuantAttributes(q, qa);
45
11455
  if (!qa.isStandard())
46
  {
47
808
    return;
48
  }
49
10647
  bool takeOwnership = false;
50
10647
  bool doSplit = false;
51
10647
  QuantifiersBoundInference& qbi = d_qreg.getQuantifiersBoundInference();
52
10647
  Trace("quant-dsplit-debug") << "Check split quantified formula : " << q << std::endl;
53
34159
  for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
54
48088
    TypeNode tn = q[0][i].getType();
55
24576
    if( tn.isDatatype() ){
56
4157
      const DType& dt = tn.getDType();
57
4157
      if (dt.isRecursiveSingleton(tn))
58
      {
59
        Trace("quant-dsplit-debug") << "Datatype " << dt.getName() << " is recursive singleton." << std::endl;
60
      }
61
      else
62
      {
63
4157
        if (options::quantDynamicSplit() == options::QuantDSplitMode::AGG)
64
        {
65
          // split if it is a finite datatype
66
          doSplit = dt.isInterpretedFinite(tn);
67
        }
68
8314
        else if (options::quantDynamicSplit()
69
4157
                 == options::QuantDSplitMode::DEFAULT)
70
        {
71
4157
          if (!qbi.isFiniteBound(q, q[0][i]))
72
          {
73
4052
            if (dt.isInterpretedFinite(tn))
74
            {
75
              // split if goes from being unhandled -> handled by finite
76
              // instantiation. An example is datatypes with uninterpreted sort
77
              // fields which are "interpreted finite" but not "finite".
78
34
              doSplit = true;
79
              // we additionally take ownership of this formula, in other words,
80
              // we mark it reduced.
81
34
              takeOwnership = true;
82
            }
83
4018
            else if (dt.getNumConstructors() == 1 && !dt.isCodatatype())
84
            {
85
              // split if only one constructor
86
1030
              doSplit = true;
87
            }
88
          }
89
        }
90
4157
        if (doSplit)
91
        {
92
          // store the index to split
93
1064
          d_quant_to_reduce[q] = i;
94
2128
          Trace("quant-dsplit-debug")
95
2128
              << "Split at index " << i << " based on datatype " << dt.getName()
96
1064
              << std::endl;
97
1064
          break;
98
        }
99
6186
        Trace("quant-dsplit-debug")
100
3093
            << "Do not split based on datatype " << dt.getName() << std::endl;
101
      }
102
    }
103
  }
104
105
10647
  if (takeOwnership)
106
  {
107
34
    Trace("quant-dsplit-debug") << "Will take ownership." << std::endl;
108
34
    d_qreg.setOwner(q, this);
109
  }
110
  // Notice we may not take ownership in some cases, meaning that both the
111
  // original quantified formula and the split one are generated. This may
112
  // increase our ability to answer "unsat", since quantifier instantiation
113
  // heuristics may be more effective for one or the other (see issues #993
114
  // and 3481).
115
}
116
117
/* whether this module needs to check this round */
118
58447
bool QuantDSplit::needsCheck( Theory::Effort e ) {
119
58447
  return e>=Theory::EFFORT_FULL && !d_quant_to_reduce.empty();
120
}
121
122
154
bool QuantDSplit::checkCompleteFor( Node q ) {
123
  // true if we split q
124
154
  return d_added_split.find( q )!=d_added_split.end();
125
}
126
127
/* Call during quantifier engine's check */
128
2780
void QuantDSplit::check(Theory::Effort e, QEffort quant_e)
129
{
130
  //add lemmas ASAP (they are a reduction)
131
2780
  if (quant_e != QEFFORT_CONFLICT)
132
  {
133
1906
    return;
134
  }
135
874
  Trace("quant-dsplit") << "QuantDSplit::check" << std::endl;
136
874
  NodeManager* nm = NodeManager::currentNM();
137
874
  FirstOrderModel* m = d_quantEngine->getModel();
138
1748
  std::vector<Node> lemmas;
139
16260
  for (std::map<Node, int>::iterator it = d_quant_to_reduce.begin();
140
16260
       it != d_quant_to_reduce.end();
141
       ++it)
142
  {
143
30772
    Node q = it->first;
144
15386
    Trace("quant-dsplit") << "- Split quantifier " << q << std::endl;
145
61098
    if (m->isQuantifierAsserted(q) && m->isQuantifierActive(q)
146
61098
        && d_added_split.find(q) == d_added_split.end())
147
    {
148
1056
      d_added_split.insert(q);
149
2112
      std::vector<Node> bvs;
150
4195
      for (unsigned i = 0, nvars = q[0].getNumChildren(); i < nvars; i++)
151
      {
152
3139
        if (static_cast<int>(i) != it->second)
153
        {
154
2083
          bvs.push_back(q[0][i]);
155
        }
156
      }
157
2112
      std::vector<Node> disj;
158
1056
      disj.push_back(q.negate());
159
2112
      TNode svar = q[0][it->second];
160
2112
      TypeNode tn = svar.getType();
161
1056
      Assert(tn.isDatatype());
162
2112
      std::vector<Node> cons;
163
1056
      const DType& dt = tn.getDType();
164
2128
      for (unsigned j = 0, ncons = dt.getNumConstructors(); j < ncons; j++)
165
      {
166
2144
        std::vector<Node> vars;
167
3186
        for (unsigned k = 0, nargs = dt[j].getNumArgs(); k < nargs; k++)
168
        {
169
4228
          TypeNode tns = dt[j][k].getRangeType();
170
4228
          Node v = nm->mkBoundVar(tns);
171
2114
          vars.push_back(v);
172
        }
173
2144
        std::vector<Node> bvs_cmb;
174
1072
        bvs_cmb.insert(bvs_cmb.end(), bvs.begin(), bvs.end());
175
1072
        bvs_cmb.insert(bvs_cmb.end(), vars.begin(), vars.end());
176
1072
        vars.insert(vars.begin(), dt[j].getConstructor());
177
2144
        Node c = nm->mkNode(kind::APPLY_CONSTRUCTOR, vars);
178
2144
        TNode ct = c;
179
2144
        Node body = q[1].substitute(svar, ct);
180
1072
        if (!bvs_cmb.empty())
181
        {
182
2144
          Node bvl = nm->mkNode(kind::BOUND_VAR_LIST, bvs_cmb);
183
2144
          std::vector<Node> children;
184
1072
          children.push_back(bvl);
185
1072
          children.push_back(body);
186
1072
          if (q.getNumChildren() == 3)
187
          {
188
570
            Node ipls = q[2].substitute(svar, ct);
189
285
            children.push_back(ipls);
190
          }
191
1072
          body = nm->mkNode(kind::FORALL, children);
192
        }
193
1072
        cons.push_back(body);
194
      }
195
2112
      Node conc = cons.size() == 1 ? cons[0] : nm->mkNode(kind::AND, cons);
196
1056
      disj.push_back(conc);
197
1056
      lemmas.push_back(disj.size() == 1 ? disj[0] : nm->mkNode(kind::OR, disj));
198
    }
199
  }
200
201
  // add lemmas to quantifiers engine
202
1930
  for (const Node& lem : lemmas)
203
  {
204
1056
    Trace("quant-dsplit") << "QuantDSplit lemma : " << lem << std::endl;
205
1056
    d_qim.addPendingLemma(lem, InferenceId::UNKNOWN);
206
  }
207
874
  Trace("quant-dsplit") << "QuantDSplit::check finished" << std::endl;
208
26676
}
209