GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/equality_query.cpp Lines: 71 91 78.0 %
Date: 2021-03-22 Branches: 167 436 38.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file equality_query.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner, Tim King
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 Utilities used for querying about equality information
13
 **/
14
15
#include "theory/quantifiers/equality_query.h"
16
17
#include "options/quantifiers_options.h"
18
#include "theory/quantifiers/first_order_model.h"
19
#include "theory/quantifiers/quantifiers_attributes.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
8995
EqualityQueryQuantifiersEngine::EqualityQueryQuantifiersEngine(
31
8995
    QuantifiersState& qs, FirstOrderModel* m)
32
    : d_qstate(qs),
33
      d_model(m),
34
      d_eqi_counter(qs.getSatContext()),
35
8995
      d_reset_count(0)
36
{
37
8995
}
38
39
17984
EqualityQueryQuantifiersEngine::~EqualityQueryQuantifiersEngine(){
40
17984
}
41
42
28251
bool EqualityQueryQuantifiersEngine::reset( Theory::Effort e ){
43
28251
  d_int_rep.clear();
44
28251
  d_reset_count++;
45
28251
  return true;
46
}
47
48
75368
Node EqualityQueryQuantifiersEngine::getInternalRepresentative(Node a,
49
                                                               Node q,
50
                                                               int index)
51
{
52
75368
  Assert(q.isNull() || q.getKind() == FORALL);
53
150736
  Node r = d_qstate.getRepresentative(a);
54
75368
  if( options::finiteModelFind() ){
55
66825
    if( r.isConst() && quantifiers::TermUtil::containsUninterpretedConstant( r ) ){
56
      //map back from values assigned by model, if any
57
6038
      if (d_model != nullptr)
58
      {
59
12076
        Node tr = d_model->getRepSet()->getTermForRepresentative(r);
60
6038
        if (!tr.isNull())
61
        {
62
6038
          r = tr;
63
6038
          r = d_qstate.getRepresentative(r);
64
        }else{
65
          if( r.getType().isSort() ){
66
            Trace("internal-rep-warn") << "No representative for UF constant." << std::endl;
67
            //should never happen : UF constants should never escape model
68
            Assert(false);
69
          }
70
        }
71
      }
72
    }
73
  }
74
150736
  TypeNode v_tn = q.isNull() ? a.getType() : q[0][index].getType();
75
197041
  if (options::quantRepMode() == options::QuantRepMode::EE)
76
  {
77
    int score = getRepScore(r, q, index, v_tn);
78
    if (score >= 0)
79
    {
80
      return r;
81
    }
82
    // if we are not a valid representative, try to select one below
83
  }
84
75368
  std::map<Node, Node>& v_int_rep = d_int_rep[v_tn];
85
75368
  std::map<Node, Node>::const_iterator itir = v_int_rep.find(r);
86
75368
  if (itir != v_int_rep.end())
87
  {
88
66742
    return itir->second;
89
  }
90
  // find best selection for representative
91
17252
  Node r_best;
92
17252
  std::vector<Node> eqc;
93
8626
  d_qstate.getEquivalenceClass(r, eqc);
94
17252
  Trace("internal-rep-select")
95
8626
      << "Choose representative for equivalence class : " << eqc
96
8626
      << ", type = " << v_tn << std::endl;
97
8626
  int r_best_score = -1;
98
59333
  for (const Node& n : eqc)
99
  {
100
50707
    int score = getRepScore(n, q, index, v_tn);
101
50707
    if (score != -2)
102
    {
103
92610
      if (r_best.isNull()
104
46305
          || (score >= 0 && (r_best_score < 0 || score < r_best_score)))
105
      {
106
8814
        r_best = n;
107
8814
        r_best_score = score;
108
      }
109
    }
110
  }
111
8626
  if (r_best.isNull())
112
  {
113
    Trace("internal-rep-warn")
114
        << "No valid choice for representative in eqc class " << eqc
115
        << std::endl;
116
    return Node::null();
117
  }
118
  // now, make sure that no other member of the class is an instance
119
17252
  std::unordered_map<TNode, Node, TNodeHashFunction> cache;
120
8626
  r_best = getInstance(r_best, eqc, cache);
121
  // store that this representative was chosen at this point
122
8626
  if (d_rep_score.find(r_best) == d_rep_score.end())
123
  {
124
1527
    d_rep_score[r_best] = d_reset_count;
125
  }
126
17252
  Trace("internal-rep-select")
127
8626
      << "...Choose " << r_best << " with score " << r_best_score
128
8626
      << " and type " << r_best.getType() << std::endl;
129
8626
  Assert(r_best.getType().isSubtypeOf(v_tn));
130
8626
  v_int_rep[r] = r_best;
131
8626
  if (Trace.isOn("internal-rep-debug"))
132
  {
133
    if (r_best != a)
134
    {
135
      Trace("internal-rep-debug")
136
          << "rep( " << a << " ) = " << r << ", " << std::endl;
137
      Trace("internal-rep-debug")
138
          << "int_rep( " << a << " ) = " << r_best << ", " << std::endl;
139
    }
140
  }
141
8626
  return r_best;
142
}
143
144
//helper functions
145
146
13050
Node EqualityQueryQuantifiersEngine::getInstance( Node n, const std::vector< Node >& eqc, std::unordered_map<TNode, Node, TNodeHashFunction>& cache ){
147
13050
  if(cache.find(n) != cache.end()) {
148
491
    return cache[n];
149
  }
150
16972
  for( size_t i=0; i<n.getNumChildren(); i++ ){
151
8837
    Node nn = getInstance( n[i], eqc, cache );
152
4424
    if( !nn.isNull() ){
153
11
      return cache[n] = nn;
154
    }
155
  }
156
12548
  if( std::find( eqc.begin(), eqc.end(), n )!=eqc.end() ){
157
8626
    return cache[n] = n;
158
  }else{
159
3922
    return cache[n] = Node::null();
160
  }
161
}
162
163
//-2 : invalid, -1 : undesired, otherwise : smaller the score, the better
164
50707
int EqualityQueryQuantifiersEngine::getRepScore(Node n,
165
                                                Node q,
166
                                                int index,
167
                                                TypeNode v_tn)
168
{
169
50707
  if( options::cegqi() && quantifiers::TermUtil::hasInstConstAttr(n) ){  //reject
170
    return -2;
171
50707
  }else if( !n.getType().isSubtypeOf( v_tn ) ){  //reject if incorrect type
172
4402
    return -2;
173
46305
  }else if( options::instMaxLevel()!=-1 ){
174
    //score prefer lowest instantiation level
175
    if( n.hasAttribute(InstLevelAttribute()) ){
176
      return n.getAttribute(InstLevelAttribute());
177
    }else{
178
5907
      return options::instLevelInputOnly() ? -1 : 0;
179
    }
180
  }else{
181
46305
    if (options::quantRepMode() == options::QuantRepMode::FIRST)
182
    {
183
      //score prefers earliest use of this term as a representative
184
46305
      return d_rep_score.find( n )==d_rep_score.end() ? -1 : d_rep_score[n];
185
    }
186
    else
187
    {
188
      Assert(options::quantRepMode() == options::QuantRepMode::DEPTH);
189
      return quantifiers::TermUtil::getTermDepth( n );
190
    }
191
  }
192
}
193
194
} /* CVC4::theory::quantifiers namespace */
195
} /* CVC4::theory namespace */
196
154256
} /* CVC4 namespace */