GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/equality_query.cpp Lines: 69 89 77.5 %
Date: 2021-03-23 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/quantifiers_state.h"
21
#include "theory/quantifiers/term_util.h"
22
23
using namespace std;
24
using namespace CVC4::kind;
25
using namespace CVC4::context;
26
27
namespace CVC4 {
28
namespace theory {
29
namespace quantifiers {
30
31
8997
EqualityQuery::EqualityQuery(QuantifiersState& qs, FirstOrderModel* m)
32
    : d_qstate(qs),
33
      d_model(m),
34
      d_eqi_counter(qs.getSatContext()),
35
8997
      d_reset_count(0)
36
{
37
8997
}
38
39
8994
EqualityQuery::~EqualityQuery() {}
40
41
28265
bool EqualityQuery::reset(Theory::Effort e)
42
{
43
28265
  d_int_rep.clear();
44
28265
  d_reset_count++;
45
28265
  return true;
46
}
47
48
75372
Node EqualityQuery::getInternalRepresentative(Node a, Node q, size_t index)
49
{
50
75372
  Assert(q.isNull() || q.getKind() == FORALL);
51
150744
  Node r = d_qstate.getRepresentative(a);
52
75372
  if( options::finiteModelFind() ){
53
66825
    if( r.isConst() && quantifiers::TermUtil::containsUninterpretedConstant( r ) ){
54
      //map back from values assigned by model, if any
55
6038
      if (d_model != nullptr)
56
      {
57
12076
        Node tr = d_model->getRepSet()->getTermForRepresentative(r);
58
6038
        if (!tr.isNull())
59
        {
60
6038
          r = tr;
61
6038
          r = d_qstate.getRepresentative(r);
62
        }else{
63
          if( r.getType().isSort() ){
64
            Trace("internal-rep-warn") << "No representative for UF constant." << std::endl;
65
            //should never happen : UF constants should never escape model
66
            Assert(false);
67
          }
68
        }
69
      }
70
    }
71
  }
72
150744
  TypeNode v_tn = q.isNull() ? a.getType() : q[0][index].getType();
73
197079
  if (options::quantRepMode() == options::QuantRepMode::EE)
74
  {
75
    int32_t score = getRepScore(r, q, index, v_tn);
76
    if (score >= 0)
77
    {
78
      return r;
79
    }
80
    // if we are not a valid representative, try to select one below
81
  }
82
75372
  std::map<Node, Node>& v_int_rep = d_int_rep[v_tn];
83
75372
  std::map<Node, Node>::const_iterator itir = v_int_rep.find(r);
84
75372
  if (itir != v_int_rep.end())
85
  {
86
66742
    return itir->second;
87
  }
88
  // find best selection for representative
89
17260
  Node r_best;
90
17260
  std::vector<Node> eqc;
91
8630
  d_qstate.getEquivalenceClass(r, eqc);
92
17260
  Trace("internal-rep-select")
93
8630
      << "Choose representative for equivalence class : " << eqc
94
8630
      << ", type = " << v_tn << std::endl;
95
8630
  int32_t r_best_score = -1;
96
59367
  for (const Node& n : eqc)
97
  {
98
50737
    int32_t score = getRepScore(n, q, index, v_tn);
99
50737
    if (score != -2)
100
    {
101
92670
      if (r_best.isNull()
102
46335
          || (score >= 0 && (r_best_score < 0 || score < r_best_score)))
103
      {
104
8818
        r_best = n;
105
8818
        r_best_score = score;
106
      }
107
    }
108
  }
109
8630
  if (r_best.isNull())
110
  {
111
    Trace("internal-rep-warn")
112
        << "No valid choice for representative in eqc class " << eqc
113
        << std::endl;
114
    return Node::null();
115
  }
116
  // now, make sure that no other member of the class is an instance
117
17260
  std::unordered_map<TNode, Node, TNodeHashFunction> cache;
118
8630
  r_best = getInstance(r_best, eqc, cache);
119
  // store that this representative was chosen at this point
120
8630
  if (d_rep_score.find(r_best) == d_rep_score.end())
121
  {
122
1529
    d_rep_score[r_best] = d_reset_count;
123
  }
124
17260
  Trace("internal-rep-select")
125
8630
      << "...Choose " << r_best << " with score " << r_best_score
126
8630
      << " and type " << r_best.getType() << std::endl;
127
8630
  Assert(r_best.getType().isSubtypeOf(v_tn));
128
8630
  v_int_rep[r] = r_best;
129
8630
  if (Trace.isOn("internal-rep-debug"))
130
  {
131
    if (r_best != a)
132
    {
133
      Trace("internal-rep-debug")
134
          << "rep( " << a << " ) = " << r << ", " << std::endl;
135
      Trace("internal-rep-debug")
136
          << "int_rep( " << a << " ) = " << r_best << ", " << std::endl;
137
    }
138
  }
139
8630
  return r_best;
140
}
141
142
//helper functions
143
144
13054
Node EqualityQuery::getInstance(
145
    Node n,
146
    const std::vector<Node>& eqc,
147
    std::unordered_map<TNode, Node, TNodeHashFunction>& cache)
148
{
149
13054
  if(cache.find(n) != cache.end()) {
150
491
    return cache[n];
151
  }
152
16976
  for( size_t i=0; i<n.getNumChildren(); i++ ){
153
8837
    Node nn = getInstance( n[i], eqc, cache );
154
4424
    if( !nn.isNull() ){
155
11
      return cache[n] = nn;
156
    }
157
  }
158
12552
  if( std::find( eqc.begin(), eqc.end(), n )!=eqc.end() ){
159
8630
    return cache[n] = n;
160
  }else{
161
3922
    return cache[n] = Node::null();
162
  }
163
}
164
165
//-2 : invalid, -1 : undesired, otherwise : smaller the score, the better
166
50737
int32_t EqualityQuery::getRepScore(Node n, Node q, size_t index, TypeNode v_tn)
167
{
168
50737
  if( options::cegqi() && quantifiers::TermUtil::hasInstConstAttr(n) ){  //reject
169
    return -2;
170
50737
  }else if( !n.getType().isSubtypeOf( v_tn ) ){  //reject if incorrect type
171
4402
    return -2;
172
46335
  }else if( options::instMaxLevel()!=-1 ){
173
    //score prefer lowest instantiation level
174
    if( n.hasAttribute(InstLevelAttribute()) ){
175
      return n.getAttribute(InstLevelAttribute());
176
    }
177
5909
    return options::instLevelInputOnly() ? -1 : 0;
178
  }
179
46335
  else if (options::quantRepMode() == options::QuantRepMode::FIRST)
180
  {
181
    // score prefers earliest use of this term as a representative
182
46335
    return d_rep_score.find(n) == d_rep_score.end() ? -1 : d_rep_score[n];
183
  }
184
  Assert(options::quantRepMode() == options::QuantRepMode::DEPTH);
185
  return quantifiers::TermUtil::getTermDepth(n);
186
}
187
188
} /* CVC4::theory::quantifiers namespace */
189
} /* CVC4::theory namespace */
190
154301
} /* CVC4 namespace */