GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/relevant_domain.cpp Lines: 198 201 98.5 %
Date: 2021-03-23 Branches: 491 908 54.1 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file relevant_domain.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, 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 Implementation of relevant domain class
13
 **/
14
15
#include "theory/quantifiers/relevant_domain.h"
16
17
#include "theory/arith/arith_msum.h"
18
#include "theory/quantifiers/first_order_model.h"
19
#include "theory/quantifiers/quantifiers_registry.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 quantifiers {
30
31
13986
void RelevantDomain::RDomain::merge( RDomain * r ) {
32
13986
  Assert(!d_parent);
33
13986
  Assert(!r->d_parent);
34
13986
  d_parent = r;
35
15686
  for( unsigned i=0; i<d_terms.size(); i++ ){
36
1700
    r->addTerm( d_terms[i] );
37
  }
38
13986
  d_terms.clear();
39
13986
}
40
41
24576
void RelevantDomain::RDomain::addTerm( Node t ) {
42
24576
  if( std::find( d_terms.begin(), d_terms.end(), t )==d_terms.end() ){
43
4555
    d_terms.push_back( t );
44
  }
45
24576
}
46
47
468677
RelevantDomain::RDomain * RelevantDomain::RDomain::getParent() {
48
468677
  if( !d_parent ){
49
229125
    return this;
50
  }else{
51
239552
    RDomain * p = d_parent->getParent();
52
239552
    d_parent = p;
53
239552
    return p;
54
  }
55
}
56
57
1009
void RelevantDomain::RDomain::removeRedundantTerms(QuantifiersState& qs)
58
{
59
2018
  std::map< Node, Node > rterms;
60
3864
  for( unsigned i=0; i<d_terms.size(); i++ ){
61
5710
    Node r = d_terms[i];
62
2855
    if( !TermUtil::hasInstConstAttr( d_terms[i] ) ){
63
2855
      r = qs.getRepresentative(d_terms[i]);
64
    }
65
2855
    if( rterms.find( r )==rterms.end() ){
66
2333
      rterms[r] = d_terms[i];
67
    }
68
  }
69
1009
  d_terms.clear();
70
3342
  for( std::map< Node, Node >::iterator it = rterms.begin(); it != rterms.end(); ++it ){
71
2333
    d_terms.push_back( it->second );
72
  }
73
1009
}
74
75
79
RelevantDomain::RelevantDomain(QuantifiersEngine* qe, QuantifiersRegistry& qr)
76
79
    : d_qe(qe), d_qreg(qr)
77
{
78
79
  d_is_computed = false;
79
79
}
80
81
237
RelevantDomain::~RelevantDomain() {
82
805
  for( std::map< Node, std::map< int, RDomain * > >::iterator itr = d_rel_doms.begin(); itr != d_rel_doms.end(); ++itr ){
83
5858
    for( std::map< int, RDomain * >::iterator itr2 = itr->second.begin(); itr2 != itr->second.end(); ++itr2 ){
84
5132
      RDomain * current = (*itr2).second;
85
5132
      Assert(current != NULL);
86
5132
      delete current;
87
    }
88
  }
89
158
}
90
91
213373
RelevantDomain::RDomain * RelevantDomain::getRDomain( Node n, int i, bool getParent ) {
92
213373
  if( d_rel_doms.find( n )==d_rel_doms.end() || d_rel_doms[n].find( i )==d_rel_doms[n].end() ){
93
5132
    d_rel_doms[n][i] = new RDomain;
94
5132
    d_rn_map[d_rel_doms[n][i]] = n;
95
5132
    d_ri_map[d_rel_doms[n][i]] = i;
96
  }
97
213373
  return getParent ? d_rel_doms[n][i]->getParent() : d_rel_doms[n][i];
98
}
99
100
1116
bool RelevantDomain::reset( Theory::Effort e ) {
101
1116
  d_is_computed = false;
102
1116
  return true;
103
}
104
105
3689
void RelevantDomain::registerQuantifier(Node q) {}
106
127
void RelevantDomain::compute(){
107
127
  if( !d_is_computed ){
108
127
    d_is_computed = true;
109
1720
    for( std::map< Node, std::map< int, RDomain * > >::iterator it = d_rel_doms.begin(); it != d_rel_doms.end(); ++it ){
110
11492
      for( std::map< int, RDomain * >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
111
9899
        it2->second->reset();
112
      }
113
    }
114
127
    FirstOrderModel* fm = d_qe->getModel();
115
1692
    for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
116
3130
      Node q = fm->getAssertedQuantifier( i );
117
3130
      Node icf = d_qreg.getInstConstantBody(q);
118
1565
      Trace("rel-dom-debug") << "compute relevant domain for " << icf << std::endl;
119
1565
      computeRelevantDomain( q, icf, true, true );
120
    }
121
122
127
    Trace("rel-dom-debug") << "account for ground terms" << std::endl;
123
127
    TermDb * db = d_qe->getTermDatabase();
124
830
    for (unsigned k = 0; k < db->getNumOperators(); k++)
125
    {
126
1406
      Node op = db->getOperator(k);
127
703
      unsigned sz = db->getNumGroundTerms( op );
128
11758
      for( unsigned i=0; i<sz; i++ ){
129
22110
        Node n = db->getGroundTerm(op, i);
130
        //if it is a non-redundant term
131
11055
        if( db->isTermActive( n ) ){
132
26781
          for( unsigned j=0; j<n.getNumChildren(); j++ ){
133
19912
            RDomain * rf = getRDomain( op, j );
134
19912
            rf->addTerm( n[j] );
135
19912
            Trace("rel-dom-debug") << "...add ground term " << n[j] << " to rel dom " << op << "[" << j << "]" << std::endl;
136
          }
137
        }
138
      }
139
    }
140
    //print debug
141
2432
    for( std::map< Node, std::map< int, RDomain * > >::iterator it = d_rel_doms.begin(); it != d_rel_doms.end(); ++it ){
142
2305
      Trace("rel-dom") << "Relevant domain for " << it->first << " : " << std::endl;
143
17300
      for( std::map< int, RDomain * >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
144
14995
        Trace("rel-dom") << "   " << it2->first << " : ";
145
14995
        RDomain * r = it2->second;
146
14995
        RDomain * rp = r->getParent();
147
14995
        if( r==rp ){
148
1009
          r->removeRedundantTerms(d_qe->getState());
149
3342
          for( unsigned i=0; i<r->d_terms.size(); i++ ){
150
2333
            Trace("rel-dom") << r->d_terms[i] << " ";
151
          }
152
        }else{
153
13986
          Trace("rel-dom") << "Dom( " << d_rn_map[rp] << ", " << d_ri_map[rp] << " ) ";
154
        }
155
14995
        Trace("rel-dom") << std::endl;
156
      }
157
    }
158
  }
159
127
}
160
161
107582
void RelevantDomain::computeRelevantDomain( Node q, Node n, bool hasPol, bool pol ) {
162
107582
  Trace("rel-dom-debug") << "Compute relevant domain " << n << "..." << std::endl;
163
215164
  Node op = d_qe->getTermDatabase()->getMatchOperator( n );
164
213788
  for( unsigned i=0; i<n.getNumChildren(); i++ ){
165
106206
    if( !op.isNull() ){
166
81938
      RDomain * rf = getRDomain( op, i );
167
81938
      if( n[i].getKind()==ITE ){
168
        for( unsigned j=1; j<=2; j++ ){
169
          computeRelevantDomainOpCh( rf, n[i][j] );
170
        }
171
      }else{
172
81938
        computeRelevantDomainOpCh( rf, n[i] );
173
      }
174
    }
175
    // do not recurse under nested closures
176
106206
    if (!n[i].isClosure())
177
    {
178
      bool newHasPol;
179
      bool newPol;
180
106017
      QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );
181
106017
      computeRelevantDomain( q, n[i], newHasPol, newPol );
182
    }
183
  }
184
185
107582
  if( ( ( n.getKind()==EQUAL && !n[0].getType().isBoolean() ) || n.getKind()==GEQ ) && TermUtil::hasInstConstAttr( n ) ){
186
    //compute the information for what this literal does
187
1474
    computeRelevantDomainLit( q, hasPol, pol, n );
188
1474
    if( d_rel_dom_lit[hasPol][pol][n].d_merge ){
189
148
      Assert(d_rel_dom_lit[hasPol][pol][n].d_rd[0] != NULL
190
             && d_rel_dom_lit[hasPol][pol][n].d_rd[1] != NULL);
191
148
      RDomain * rd1 = d_rel_dom_lit[hasPol][pol][n].d_rd[0]->getParent();
192
148
      RDomain * rd2 = d_rel_dom_lit[hasPol][pol][n].d_rd[1]->getParent();
193
148
      if( rd1!=rd2 ){
194
145
        rd1->merge( rd2 );
195
      }
196
    }else{
197
1326
      if( d_rel_dom_lit[hasPol][pol][n].d_rd[0]!=NULL ){
198
736
        RDomain * rd = d_rel_dom_lit[hasPol][pol][n].d_rd[0]->getParent();
199
1469
        for( unsigned i=0; i<d_rel_dom_lit[hasPol][pol][n].d_val.size(); i++ ){
200
733
          rd->addTerm( d_rel_dom_lit[hasPol][pol][n].d_val[i] );
201
        }
202
      }
203
    }
204
  }
205
107582
  Trace("rel-dom-debug") << "...finished Compute relevant domain " << n << std::endl;
206
107582
}
207
208
81938
void RelevantDomain::computeRelevantDomainOpCh( RDomain * rf, Node n ) {
209
81938
  if( n.getKind()==INST_CONSTANT ){
210
158072
    Node q = TermUtil::getInstConstAttr(n);
211
    //merge the RDomains
212
79036
    unsigned id = n.getAttribute(InstVarNumAttribute());
213
79036
    Assert(q[0][id].getType() == n.getType());
214
79036
    Trace("rel-dom-debug") << n << " is variable # " << id << " for " << q;
215
158072
    Trace("rel-dom-debug") << " with body : " << d_qreg.getInstConstantBody(q)
216
79036
                           << std::endl;
217
79036
    RDomain * rq = getRDomain( q, id );
218
79036
    if( rf!=rq ){
219
13841
      rq->merge( rf );
220
    }
221
2902
  }else if( !TermUtil::hasInstConstAttr( n ) ){
222
2231
    Trace("rel-dom-debug") << "...add ground term to rel dom " << n << std::endl;
223
    //term to add
224
2231
    rf->addTerm( n );
225
  }
226
81938
}
227
228
1474
void RelevantDomain::computeRelevantDomainLit( Node q, bool hasPol, bool pol, Node n ) {
229
1474
  if( d_rel_dom_lit[hasPol][pol].find( n )==d_rel_dom_lit[hasPol][pol].end() ){
230
416
    d_rel_dom_lit[hasPol][pol][n].d_merge = false;
231
416
    int varCount = 0;
232
416
    int varCh = -1;
233
1248
    for( unsigned i=0; i<n.getNumChildren(); i++ ){
234
832
      if( n[i].getKind()==INST_CONSTANT ){
235
        // must get the quantified formula this belongs to, which may be
236
        // different from q
237
508
        Node qi = TermUtil::getInstConstAttr(n[i]);
238
254
        unsigned id = n[i].getAttribute(InstVarNumAttribute());
239
254
        d_rel_dom_lit[hasPol][pol][n].d_rd[i] = getRDomain(qi, id, false);
240
254
        varCount++;
241
254
        varCh = i;
242
      }else{
243
578
        d_rel_dom_lit[hasPol][pol][n].d_rd[i] = NULL;
244
      }
245
    }
246
247
832
    Node r_add;
248
416
    bool varLhs = true;
249
416
    if( varCount==2 ){
250
18
      d_rel_dom_lit[hasPol][pol][n].d_merge = true;
251
    }else{
252
398
      if( varCount==1 ){
253
218
        r_add = n[1-varCh];
254
218
        varLhs = (varCh==0);
255
218
        d_rel_dom_lit[hasPol][pol][n].d_rd[0] = d_rel_dom_lit[hasPol][pol][n].d_rd[varCh];
256
218
        d_rel_dom_lit[hasPol][pol][n].d_rd[1] = NULL;
257
      }else{
258
        //solve the inequality for one/two variables, if possible
259
180
        if( n[0].getType().isReal() ){
260
246
          std::map< Node, Node > msum;
261
123
          if (ArithMSum::getMonomialSumLit(n, msum))
262
          {
263
246
            Node var;
264
246
            Node var2;
265
123
            bool hasNonVar = false;
266
368
            for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
267
722
              if (!it->first.isNull() && it->first.getKind() == INST_CONSTANT
268
545
                  && TermUtil::getInstConstAttr(it->first) == q)
269
              {
270
55
                if( var.isNull() ){
271
33
                  var = it->first;
272
22
                }else if( var2.isNull() ){
273
22
                  var2 = it->first;
274
                }else{
275
                  hasNonVar = true;
276
                }
277
              }else{
278
190
                hasNonVar = true;
279
              }
280
            }
281
123
            if( !var.isNull() ){
282
33
              if( var2.isNull() ){
283
                //single variable solve
284
22
                Node veq_c;
285
22
                Node val;
286
                int ires =
287
11
                    ArithMSum::isolate(var, msum, veq_c, val, n.getKind());
288
11
                if( ires!=0 ){
289
11
                  if( veq_c.isNull() ){
290
3
                    r_add = val;
291
3
                    varLhs = (ires==1);
292
3
                    d_rel_dom_lit[hasPol][pol][n].d_rd[0] = getRDomain( q, var.getAttribute(InstVarNumAttribute()), false );
293
3
                    d_rel_dom_lit[hasPol][pol][n].d_rd[1] = NULL;
294
                  }
295
                }
296
22
              }else if( !hasNonVar ){
297
                //merge the domains
298
9
                d_rel_dom_lit[hasPol][pol][n].d_rd[0] = getRDomain( q, var.getAttribute(InstVarNumAttribute()), false );
299
9
                d_rel_dom_lit[hasPol][pol][n].d_rd[1] = getRDomain( q, var2.getAttribute(InstVarNumAttribute()), false );
300
9
                d_rel_dom_lit[hasPol][pol][n].d_merge = true;
301
              }
302
            }
303
          }
304
        }
305
      }
306
    }
307
416
    if( d_rel_dom_lit[hasPol][pol][n].d_merge ){
308
      //do not merge if constant negative polarity
309
27
      if( hasPol && !pol ){
310
9
        d_rel_dom_lit[hasPol][pol][n].d_merge = false;
311
      }
312
389
    }else if( !r_add.isNull() && !TermUtil::hasInstConstAttr( r_add ) ){
313
204
      Trace("rel-dom-debug") << "...add term " << r_add << ", pol = " << pol << ", kind = " << n.getKind() << std::endl;
314
      //the negative occurrence adds the term to the domain
315
204
      if( !hasPol || !pol ){
316
170
        d_rel_dom_lit[hasPol][pol][n].d_val.push_back( r_add );
317
      }
318
      //the positive occurence adds other terms
319
204
      if( ( !hasPol || pol ) && n[0].getType().isInteger() ){
320
36
        if( n.getKind()==EQUAL ){
321
12
          for( unsigned i=0; i<2; i++ ){
322
16
            d_rel_dom_lit[hasPol][pol][n].d_val.push_back(
323
16
                ArithMSum::offset(r_add, i == 0 ? 1 : -1));
324
          }
325
32
        }else if( n.getKind()==GEQ ){
326
64
          d_rel_dom_lit[hasPol][pol][n].d_val.push_back(
327
64
              ArithMSum::offset(r_add, varLhs ? 1 : -1));
328
        }
329
      }
330
    }else{
331
185
      d_rel_dom_lit[hasPol][pol][n].d_rd[0] = NULL;
332
185
      d_rel_dom_lit[hasPol][pol][n].d_rd[1] = NULL;
333
    }
334
  }
335
1474
}
336
337
}  // namespace quantifiers
338
}  // namespace theory
339
26685
}  // namespace CVC4