GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/quantifiers_attributes.cpp Lines: 148 206 71.8 %
Date: 2021-03-22 Branches: 344 824 41.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file quantifiers_attributes.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Paul Meng, 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 QuantifiersAttributes class
13
 **/
14
15
#include "theory/quantifiers/quantifiers_attributes.h"
16
17
#include "options/quantifiers_options.h"
18
#include "theory/arith/arith_msum.h"
19
#include "theory/quantifiers/sygus/synth_engine.h"
20
#include "theory/quantifiers/term_util.h"
21
22
using namespace std;
23
using namespace CVC4::kind;
24
using namespace CVC4::context;
25
26
namespace CVC4 {
27
namespace theory {
28
namespace quantifiers {
29
30
930919
bool QAttributes::isStandard() const
31
{
32
1848290
  return !d_sygus && !d_quant_elim && !isFunDef() && d_name.isNull()
33
1839287
         && !d_isInternal;
34
}
35
36
8995
QuantAttributes::QuantAttributes() {}
37
38
109
void QuantAttributes::setUserAttribute( const std::string& attr, Node n, std::vector< Node >& node_values, std::string str_value ){
39
109
  Trace("quant-attr-debug") << "Set " << attr << " " << n << std::endl;
40
109
  if (attr == "fun-def")
41
  {
42
    Trace("quant-attr-debug") << "Set function definition " << n << std::endl;
43
    FunDefAttribute fda;
44
    n.setAttribute( fda, true );
45
  }
46
109
  else if (attr == "qid")
47
  {
48
    // using z3 syntax "qid"
49
79
    Trace("quant-attr-debug") << "Set quant-name " << n << std::endl;
50
    QuantNameAttribute qna;
51
79
    n.setAttribute(qna, true);
52
30
  }else if( attr=="quant-inst-max-level" ){
53
    Assert(node_values.size() == 1);
54
    uint64_t lvl = node_values[0].getConst<Rational>().getNumerator().getLong();
55
    Trace("quant-attr-debug") << "Set instantiation level " << n << " to " << lvl << std::endl;
56
    QuantInstLevelAttribute qila;
57
    n.setAttribute( qila, lvl );
58
30
  }else if( attr=="quant-elim" ){
59
27
    Trace("quant-attr-debug") << "Set quantifier elimination " << n << std::endl;
60
    QuantElimAttribute qea;
61
27
    n.setAttribute( qea, true );
62
3
  }else if( attr=="quant-elim-partial" ){
63
3
    Trace("quant-attr-debug") << "Set partial quantifier elimination " << n << std::endl;
64
    QuantElimPartialAttribute qepa;
65
3
    n.setAttribute( qepa, true );
66
  }
67
109
}
68
69
bool QuantAttributes::checkFunDef( Node q ) {
70
  return !getFunDefHead( q ).isNull();
71
}
72
73
bool QuantAttributes::checkFunDefAnnotation( Node ipl ) {
74
  if( !ipl.isNull() ){
75
    for( unsigned i=0; i<ipl.getNumChildren(); i++ ){
76
      if( ipl[i].getKind()==INST_ATTRIBUTE ){
77
        if( ipl[i][0].getAttribute(FunDefAttribute()) ){
78
          return true;
79
        }
80
      }
81
    }
82
  }
83
  return false;
84
}
85
86
643
Node QuantAttributes::getFunDefHead( Node q ) {
87
  //&& q[1].getKind()==EQUAL && q[1][0].getKind()==APPLY_UF &&
88
643
  if( q.getKind()==FORALL && q.getNumChildren()==3 ){
89
248
    Node ipl = q[2];
90
248
    for (unsigned i = 0; i < ipl.getNumChildren(); i++)
91
    {
92
732
      if (ipl[i].getKind() == INST_ATTRIBUTE
93
732
          && ipl[i][0].getAttribute(FunDefAttribute()))
94
      {
95
240
        return ipl[i][0];
96
      }
97
    }
98
  }
99
403
  return Node::null();
100
}
101
120
Node QuantAttributes::getFunDefBody( Node q ) {
102
240
  Node h = getFunDefHead( q );
103
120
  if( !h.isNull() ){
104
120
    if( q[1].getKind()==EQUAL ){
105
116
      if( q[1][0]==h ){
106
65
        return q[1][1];
107
51
      }else if( q[1][1]==h ){
108
50
        return q[1][0];
109
      }
110
1
      else if (q[1][0].getType().isReal())
111
      {
112
        // solve for h in the equality
113
1
        std::map<Node, Node> msum;
114
1
        if (ArithMSum::getMonomialSumLit(q[1], msum))
115
        {
116
1
          Node veq;
117
1
          int res = ArithMSum::isolate(h, msum, veq, EQUAL);
118
1
          if (res != 0)
119
          {
120
1
            Assert(veq.getKind() == EQUAL);
121
1
            return res == 1 ? veq[1] : veq[0];
122
          }
123
        }
124
      }
125
    }else{
126
4
      Node atom = q[1].getKind()==NOT ? q[1][0] : q[1];
127
4
      bool pol = q[1].getKind()!=NOT;
128
4
      if( atom==h ){
129
4
        return NodeManager::currentNM()->mkConst( pol );
130
      }
131
    }
132
  }
133
  return Node::null();
134
}
135
136
6353
bool QuantAttributes::checkSygusConjecture( Node q ) {
137
6353
  return ( q.getKind()==FORALL && q.getNumChildren()==3 ) ? checkSygusConjectureAnnotation( q[2] ) : false;
138
}
139
140
631
bool QuantAttributes::checkSygusConjectureAnnotation( Node ipl ){
141
631
  if( !ipl.isNull() ){
142
754
    for( unsigned i=0; i<ipl.getNumChildren(); i++ ){
143
631
      if( ipl[i].getKind()==INST_ATTRIBUTE ){
144
754
        Node avar = ipl[i][0];
145
631
        if( avar.getAttribute(SygusAttribute()) ){
146
508
          return true;
147
        }
148
      }
149
    }
150
  }
151
123
  return false;
152
}
153
154
bool QuantAttributes::checkQuantElimAnnotation( Node ipl ) {
155
  if( !ipl.isNull() ){
156
    for( unsigned i=0; i<ipl.getNumChildren(); i++ ){
157
      if( ipl[i].getKind()==INST_ATTRIBUTE ){
158
        Node avar = ipl[i][0];
159
        if( avar.getAttribute(QuantElimAttribute()) ){
160
          return true;
161
        }
162
      }
163
    }
164
  }
165
  return false;
166
}
167
168
23487
void QuantAttributes::computeAttributes( Node q ) {
169
23487
  computeQuantAttributes( q, d_qattr[q] );
170
23487
  QAttributes& qa = d_qattr[q];
171
23487
  if (qa.isFunDef())
172
  {
173
190
    Node f = qa.d_fundef_f;
174
95
    if( d_fun_defs.find( f )!=d_fun_defs.end() ){
175
      CVC4Message() << "Cannot define function " << f << " more than once."
176
                    << std::endl;
177
      AlwaysAssert(false);
178
    }
179
95
    d_fun_defs[f] = true;
180
  }
181
23487
}
182
183
186332
void QuantAttributes::computeQuantAttributes( Node q, QAttributes& qa ){
184
186332
  Trace("quant-attr-debug") << "Compute attributes for " << q << std::endl;
185
186332
  if( q.getNumChildren()==3 ){
186
29612
    qa.d_ipl = q[2];
187
60536
    for( unsigned i=0; i<q[2].getNumChildren(); i++ ){
188
30924
      Trace("quant-attr-debug") << "Check : " << q[2][i] << " " << q[2][i].getKind() << std::endl;
189
30924
      if( q[2][i].getKind()==INST_PATTERN || q[2][i].getKind()==INST_NO_PATTERN ){
190
24544
        qa.d_hasPattern = true;
191
6380
      }else if( q[2][i].getKind()==INST_ATTRIBUTE ){
192
12760
        Node avar = q[2][i][0];
193
6380
        if( avar.getAttribute(FunDefAttribute()) ){
194
917
          Trace("quant-attr") << "Attribute : function definition : " << q << std::endl;
195
          //get operator directly from pattern
196
917
          qa.d_fundef_f = q[2][i][0].getOperator();
197
        }
198
6380
        if( avar.getAttribute(SygusAttribute()) ){
199
          //not necessarily nested existential
200
          //Assert( q[1].getKind()==NOT );
201
          //Assert( q[1][0].getKind()==FORALL );
202
3774
          Trace("quant-attr") << "Attribute : sygus : " << q << std::endl;
203
3774
          qa.d_sygus = true;
204
        }
205
6380
        if (avar.hasAttribute(SygusSideConditionAttribute()))
206
        {
207
184
          qa.d_sygusSideCondition =
208
368
              avar.getAttribute(SygusSideConditionAttribute());
209
368
          Trace("quant-attr")
210
184
              << "Attribute : sygus side condition : "
211
184
              << qa.d_sygusSideCondition << " : " << q << std::endl;
212
        }
213
6380
        if (avar.getAttribute(QuantNameAttribute()))
214
        {
215
1000
          Trace("quant-attr") << "Attribute : quantifier name : " << avar
216
500
                              << " for " << q << std::endl;
217
500
          qa.d_name = avar;
218
        }
219
6380
        if( avar.hasAttribute(QuantInstLevelAttribute()) ){
220
          qa.d_qinstLevel = avar.getAttribute(QuantInstLevelAttribute());
221
          Trace("quant-attr") << "Attribute : quant inst level " << qa.d_qinstLevel << " : " << q << std::endl;
222
        }
223
6380
        if( avar.getAttribute(QuantElimAttribute()) ){
224
495
          Trace("quant-attr") << "Attribute : quantifier elimination : " << q << std::endl;
225
495
          qa.d_quant_elim = true;
226
          //don't set owner, should happen naturally
227
        }
228
6380
        if( avar.getAttribute(QuantElimPartialAttribute()) ){
229
17
          Trace("quant-attr") << "Attribute : quantifier elimination partial : " << q << std::endl;
230
17
          qa.d_quant_elim = true;
231
17
          qa.d_quant_elim_partial = true;
232
          //don't set owner, should happen naturally
233
        }
234
6380
        if (avar.getAttribute(InternalQuantAttribute()))
235
        {
236
493
          Trace("quant-attr") << "Attribute : internal : " << q << std::endl;
237
493
          qa.d_isInternal = true;
238
        }
239
6380
        if( avar.hasAttribute(QuantIdNumAttribute()) ){
240
          qa.d_qid_num = avar;
241
          Trace("quant-attr") << "Attribute : id number " << qa.d_qid_num.getAttribute(QuantIdNumAttribute()) << " : " << q << std::endl;
242
        }
243
      }
244
    }
245
  }
246
186332
}
247
248
1112
bool QuantAttributes::isFunDef( Node q ) {
249
1112
  std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
250
1112
  if( it==d_qattr.end() ){
251
    return false;
252
  }else{
253
1112
    return it->second.isFunDef();
254
  }
255
}
256
257
1651
bool QuantAttributes::isSygus( Node q ) {
258
1651
  std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
259
1651
  if( it==d_qattr.end() ){
260
    return false;
261
  }else{
262
1651
    return it->second.d_sygus;
263
  }
264
}
265
266
678
int64_t QuantAttributes::getQuantInstLevel(Node q)
267
{
268
678
  std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
269
678
  if( it==d_qattr.end() ){
270
    return -1;
271
  }else{
272
678
    return it->second.d_qinstLevel;
273
  }
274
}
275
276
bool QuantAttributes::isQuantElim( Node q ) {
277
  std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
278
  if( it==d_qattr.end() ){
279
    return false;
280
  }else{
281
    return it->second.d_quant_elim;
282
  }
283
}
284
285
5019
bool QuantAttributes::isQuantElimPartial( Node q ) {
286
5019
  std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
287
5019
  if( it==d_qattr.end() ){
288
    return false;
289
  }else{
290
5019
    return it->second.d_quant_elim_partial;
291
  }
292
}
293
294
59856
bool QuantAttributes::isInternal(Node q) const
295
{
296
59856
  std::map<Node, QAttributes>::const_iterator it = d_qattr.find(q);
297
59856
  if (it != d_qattr.end())
298
  {
299
59856
    return it->second.d_isInternal;
300
  }
301
  return false;
302
}
303
304
24
Node QuantAttributes::getQuantName(Node q) const
305
{
306
24
  std::map<Node, QAttributes>::const_iterator it = d_qattr.find(q);
307
24
  if (it != d_qattr.end())
308
  {
309
24
    return it->second.d_name;
310
  }
311
  return Node::null();
312
}
313
314
std::string QuantAttributes::quantToString(Node q) const
315
{
316
  std::stringstream ss;
317
  Node name = getQuantName(q);
318
  ss << (name.isNull() ? q : name);
319
  return ss.str();
320
}
321
322
int QuantAttributes::getQuantIdNum( Node q ) {
323
  std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
324
  if( it!=d_qattr.end() ){
325
    if( !it->second.d_qid_num.isNull() ){
326
      return it->second.d_qid_num.getAttribute(QuantIdNumAttribute());
327
    }
328
  }
329
  return -1;
330
}
331
332
Node QuantAttributes::getQuantIdNumNode( Node q ) {
333
  std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
334
  if( it==d_qattr.end() ){
335
    return Node::null();
336
  }else{
337
    return it->second.d_qid_num;
338
  }
339
}
340
341
2358
void QuantAttributes::setInstantiationLevelAttr(Node n, Node qn, uint64_t level)
342
{
343
4716
  Trace("inst-level-debug2") << "IL : " << n << " " << qn << " " << level
344
2358
                             << std::endl;
345
  // if not from the vector of terms we instantiatied
346
2358
  if (qn.getKind() != BOUND_VARIABLE && n != qn)
347
  {
348
    // if this is a new term, without an instantiation level
349
1704
    if (!n.hasAttribute(InstLevelAttribute()))
350
    {
351
      InstLevelAttribute ila;
352
1008
      n.setAttribute(ila, level);
353
2016
      Trace("inst-level-debug") << "Set instantiation level " << n << " to "
354
1008
                                << level << std::endl;
355
1008
      Assert(n.getNumChildren() == qn.getNumChildren());
356
3098
      for (unsigned i = 0; i < n.getNumChildren(); i++)
357
      {
358
2090
        setInstantiationLevelAttr(n[i], qn[i], level);
359
      }
360
    }
361
  }
362
2358
}
363
364
2094
void QuantAttributes::setInstantiationLevelAttr(Node n, uint64_t level)
365
{
366
2094
  if (!n.hasAttribute(InstLevelAttribute()))
367
  {
368
    InstLevelAttribute ila;
369
1104
    n.setAttribute(ila, level);
370
2208
    Trace("inst-level-debug") << "Set instantiation level " << n << " to "
371
1104
                              << level << std::endl;
372
2973
    for (unsigned i = 0; i < n.getNumChildren(); i++)
373
    {
374
1869
      setInstantiationLevelAttr(n[i], level);
375
    }
376
  }
377
2094
}
378
379
} /* CVC4::theory::quantifiers namespace */
380
} /* CVC4::theory namespace */
381
26676
} /* CVC4 namespace */