GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/first_order_model.cpp Lines: 152 164 92.7 %
Date: 2021-03-23 Branches: 244 526 46.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file first_order_model.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, 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 model engine model class
13
 **/
14
15
#include "theory/quantifiers/first_order_model.h"
16
#include "options/base_options.h"
17
#include "options/quantifiers_options.h"
18
#include "theory/quantifiers/fmf/bounded_integers.h"
19
#include "theory/quantifiers/fmf/model_engine.h"
20
#include "theory/quantifiers/quantifiers_attributes.h"
21
#include "theory/quantifiers/term_database.h"
22
#include "theory/quantifiers/term_enumeration.h"
23
#include "theory/quantifiers/term_registry.h"
24
#include "theory/quantifiers/term_util.h"
25
26
using namespace CVC4::kind;
27
using namespace CVC4::context;
28
29
namespace CVC4 {
30
namespace theory {
31
namespace quantifiers {
32
33
struct ModelBasisAttributeId
34
{
35
};
36
using ModelBasisAttribute = expr::Attribute<ModelBasisAttributeId, bool>;
37
// for APPLY_UF terms, 1 : term has direct child with model basis attribute,
38
//                     0 : term has no direct child with model basis attribute.
39
struct ModelBasisArgAttributeId
40
{
41
};
42
using ModelBasisArgAttribute = expr::Attribute<ModelBasisArgAttributeId, uint64_t>;
43
44
8997
FirstOrderModel::FirstOrderModel(QuantifiersState& qs,
45
                                 QuantifiersRegistry& qr,
46
                                 TermRegistry& tr,
47
8997
                                 std::string name)
48
    : TheoryModel(qs.getSatContext(), name, true),
49
      d_qe(nullptr),
50
      d_qreg(qr),
51
      d_treg(tr),
52
      d_eq_query(qs, this),
53
      d_forall_asserts(qs.getSatContext()),
54
8997
      d_forallRlvComputed(false)
55
{
56
8997
}
57
58
//!!!!!!!!!!!!!!!!!!!!! temporary (project #15)
59
8997
void FirstOrderModel::finishInit(QuantifiersEngine* qe) { d_qe = qe; }
60
61
75372
Node FirstOrderModel::getInternalRepresentative(Node a, Node q, size_t index)
62
{
63
75372
  return d_eq_query.getInternalRepresentative(a, q, index);
64
}
65
66
35139
void FirstOrderModel::assertQuantifier( Node n ){
67
35139
  if( n.getKind()==FORALL ){
68
35139
    d_forall_asserts.push_back( n );
69
  }else if( n.getKind()==NOT ){
70
    Assert(n[0].getKind() == FORALL);
71
  }
72
35139
}
73
74
328011
size_t FirstOrderModel::getNumAssertedQuantifiers() const
75
{
76
328011
  return d_forall_asserts.size();
77
}
78
79
651691
Node FirstOrderModel::getAssertedQuantifier( unsigned i, bool ordered ) {
80
651691
  if( !ordered || !d_forallRlvComputed ){
81
449800
    return d_forall_asserts[i];
82
  }
83
  // If we computed the relevant forall assertion vector, in reset_round,
84
  // then it should have the same size as the default assertion vector.
85
201891
  Assert(d_forall_rlv_assert.size() == d_forall_asserts.size());
86
201891
  return d_forall_rlv_assert[i];
87
}
88
89
1592
void FirstOrderModel::initialize() {
90
1592
  processInitialize( true );
91
  //this is called after representatives have been chosen and the equality engine has been built
92
  //for each quantifier, collect all operators we care about
93
10720
  for( unsigned i=0; i<getNumAssertedQuantifiers(); i++ ){
94
18256
    Node f = getAssertedQuantifier( i );
95
9128
    if( d_quant_var_id.find( f )==d_quant_var_id.end() ){
96
2990
      for(unsigned j=0; j<f[0].getNumChildren(); j++){
97
1776
        d_quant_var_id[f][f[0][j]] = j;
98
      }
99
    }
100
9128
    processInitializeQuantifier( f );
101
    //initialize relevant models within bodies of all quantifiers
102
18256
    std::map< Node, bool > visited;
103
9128
    initializeModelForTerm( f[1], visited );
104
  }
105
1592
  processInitialize( false );
106
1592
}
107
108
220761
void FirstOrderModel::initializeModelForTerm( Node n, std::map< Node, bool >& visited ){
109
220761
  if( visited.find( n )==visited.end() ){
110
162901
    visited[n] = true;
111
162901
    processInitializeModelForTerm( n );
112
374534
    for( int i=0; i<(int)n.getNumChildren(); i++ ){
113
211633
      initializeModelForTerm( n[i], visited );
114
    }
115
  }
116
220761
}
117
118
4203
Node FirstOrderModel::getSomeDomainElement(TypeNode tn){
119
  //check if there is even any domain elements at all
120
4203
  if (!d_rep_set.hasType(tn) || d_rep_set.d_type_reps[tn].size() == 0)
121
  {
122
264
    Trace("fm-debug") << "Must create domain element for " << tn << "..."
123
132
                      << std::endl;
124
264
    Node mbt = getModelBasisTerm(tn);
125
132
    Trace("fm-debug") << "Add to representative set..." << std::endl;
126
132
    d_rep_set.add(tn, mbt);
127
  }
128
4203
  return d_rep_set.d_type_reps[tn][0];
129
}
130
131
6079
bool FirstOrderModel::initializeRepresentativesForType(TypeNode tn)
132
{
133
6079
  if (tn.isSort())
134
  {
135
    // must ensure uninterpreted type is non-empty.
136
2160
    if (!d_rep_set.hasType(tn))
137
    {
138
      // terms in rep_set are now constants which mapped to terms through
139
      // TheoryModel. Thus, should introduce a constant and a term.
140
      // For now, we just add an arbitrary term.
141
10
      Node var = getSomeDomainElement(tn);
142
10
      Trace("mkVar") << "RepSetIterator:: Make variable " << var << " : " << tn
143
5
                     << std::endl;
144
5
      d_rep_set.add(tn, var);
145
    }
146
2160
    return true;
147
  }
148
  else
149
  {
150
    // can we complete it?
151
3919
    if (d_qreg.getQuantifiersBoundInference().mayComplete(tn))
152
    {
153
4252
      Trace("fm-debug") << "  do complete, since cardinality is small ("
154
2126
                        << tn.getCardinality() << ")..." << std::endl;
155
2126
      d_rep_set.complete(tn);
156
      // must have succeeded
157
2126
      Assert(d_rep_set.hasType(tn));
158
2126
      return true;
159
    }
160
1793
    Trace("fm-debug") << "  variable cannot be bounded." << std::endl;
161
1793
    return false;
162
  }
163
}
164
165
bool FirstOrderModel::isModelBasis(TNode n)
166
{
167
  return n.getAttribute(ModelBasisAttribute());
168
}
169
170
8997
EqualityQuery* FirstOrderModel::getEqualityQuery() { return &d_eq_query; }
171
172
/** needs check */
173
86229
bool FirstOrderModel::checkNeeded() {
174
86229
  return d_forall_asserts.size()>0;
175
}
176
177
28265
void FirstOrderModel::reset_round() {
178
28265
  d_quant_active.clear();
179
180
  // compute which quantified formulas are asserted if necessary
181
56530
  std::map<Node, bool> qassert;
182
28265
  if (!d_forall_rlv_vec.empty())
183
  {
184
5794
    Trace("fm-relevant-debug")
185
2897
        << "Mark asserted quantified formulas..." << std::endl;
186
135709
    for (const Node& q : d_forall_asserts)
187
    {
188
132812
      qassert[q] = true;
189
    }
190
  }
191
  //order the quantified formulas
192
28265
  d_forall_rlv_assert.clear();
193
28265
  d_forallRlvComputed = false;
194
28265
  if( !d_forall_rlv_vec.empty() ){
195
2897
    d_forallRlvComputed = true;
196
2897
    Trace("fm-relevant") << "Build sorted relevant list..." << std::endl;
197
2897
    Trace("fm-relevant-debug") << "Add relevant asserted formulas..." << std::endl;
198
2897
    std::map<Node, bool>::iterator ita;
199
10009
    for( int i=(int)(d_forall_rlv_vec.size()-1); i>=0; i-- ){
200
14224
      Node q = d_forall_rlv_vec[i];
201
7112
      ita = qassert.find(q);
202
7112
      if (ita != qassert.end())
203
      {
204
6834
        Trace("fm-relevant") << "   " << q << std::endl;
205
6834
        d_forall_rlv_assert.push_back( q );
206
6834
        qassert.erase(ita);
207
      }
208
    }
209
2897
    Trace("fm-relevant-debug") << "Add remaining asserted formulas..." << std::endl;
210
135709
    for (const Node& q : d_forall_asserts)
211
    {
212
      // if we didn't include it above
213
132812
      if (qassert.find(q) != qassert.end())
214
      {
215
125978
        d_forall_rlv_assert.push_back( q );
216
      }else{
217
6834
        Trace("fm-relevant-debug") << "...already included " << q << std::endl;
218
      }
219
    }
220
2897
    Trace("fm-relevant-debug") << "Sizes : " << d_forall_rlv_assert.size() << " " << d_forall_asserts.size() << std::endl;
221
2897
    Assert(d_forall_rlv_assert.size() == d_forall_asserts.size());
222
  }
223
28265
}
224
225
1970
void FirstOrderModel::markRelevant( Node q ) {
226
  // Put q on the back of the vector d_forall_rlv_vec.
227
  // If we were the last quantifier marked relevant, this is a no-op, return.
228
1970
  if( q!=d_last_forall_rlv ){
229
1022
    Trace("fm-relevant") << "Mark relevant : " << q << std::endl;
230
    std::vector<Node>::iterator itr =
231
1022
        std::find(d_forall_rlv_vec.begin(), d_forall_rlv_vec.end(), q);
232
1022
    if (itr != d_forall_rlv_vec.end())
233
    {
234
145
      d_forall_rlv_vec.erase(itr, itr + 1);
235
    }
236
1022
    d_forall_rlv_vec.push_back(q);
237
1022
    d_last_forall_rlv = q;
238
  }
239
1970
}
240
241
1557
void FirstOrderModel::setQuantifierActive( TNode q, bool active ) {
242
1557
  d_quant_active[q] = active;
243
1557
}
244
245
297809
bool FirstOrderModel::isQuantifierActive(TNode q) const
246
{
247
297809
  std::map<TNode, bool>::const_iterator it = d_quant_active.find(q);
248
297809
  if( it==d_quant_active.end() ){
249
297748
    return true;
250
  }
251
61
  return it->second;
252
}
253
254
15386
bool FirstOrderModel::isQuantifierAsserted(TNode q) const
255
{
256
15386
  return std::find( d_forall_asserts.begin(), d_forall_asserts.end(), q )!=d_forall_asserts.end();
257
}
258
259
94714
Node FirstOrderModel::getModelBasisTerm(TypeNode tn)
260
{
261
94714
  if (d_model_basis_term.find(tn) == d_model_basis_term.end())
262
  {
263
1806
    Node mbt;
264
903
    if (tn.isClosedEnumerable())
265
    {
266
410
      mbt = d_treg.getTermEnumeration()->getEnumerateTerm(tn, 0);
267
    }
268
    else
269
    {
270
986
      if (options::fmfFreshDistConst())
271
      {
272
        mbt = d_treg.getTermDatabase()->getOrMakeTypeFreshVariable(tn);
273
      }
274
      else
275
      {
276
        // The model basis term cannot be an interpreted function, or else we
277
        // may produce an inconsistent model by choosing an arbitrary
278
        // equivalence class for it. Hence, we require that it be an existing or
279
        // fresh variable.
280
493
        mbt = d_treg.getTermDatabase()->getOrMakeTypeGroundTerm(tn, true);
281
      }
282
    }
283
    ModelBasisAttribute mba;
284
903
    mbt.setAttribute(mba, true);
285
903
    d_model_basis_term[tn] = mbt;
286
1806
    Trace("model-basis-term") << "Choose " << mbt << " as model basis term for "
287
903
                              << tn << std::endl;
288
  }
289
94714
  return d_model_basis_term[tn];
290
}
291
292
82506
bool FirstOrderModel::isModelBasisTerm(Node n)
293
{
294
82506
  return n == getModelBasisTerm(n.getType());
295
}
296
297
11872
Node FirstOrderModel::getModelBasisOpTerm(Node op)
298
{
299
11872
  if (d_model_basis_op_term.find(op) == d_model_basis_op_term.end())
300
  {
301
1892
    TypeNode t = op.getType();
302
1892
    std::vector<Node> children;
303
946
    children.push_back(op);
304
2358
    for (int i = 0; i < (int)(t.getNumChildren() - 1); i++)
305
    {
306
1412
      children.push_back(getModelBasisTerm(t[i]));
307
    }
308
946
    if (children.size() == 1)
309
    {
310
      d_model_basis_op_term[op] = op;
311
    }
312
    else
313
    {
314
946
      d_model_basis_op_term[op] =
315
1892
          NodeManager::currentNM()->mkNode(APPLY_UF, children);
316
    }
317
  }
318
11872
  return d_model_basis_op_term[op];
319
}
320
321
Node FirstOrderModel::getModelBasis(Node q, Node n)
322
{
323
  // make model basis
324
  if (d_model_basis_terms.find(q) == d_model_basis_terms.end())
325
  {
326
    for (unsigned j = 0; j < q[0].getNumChildren(); j++)
327
    {
328
      d_model_basis_terms[q].push_back(getModelBasisTerm(q[0][j].getType()));
329
    }
330
  }
331
  Node gn = d_qreg.substituteInstConstants(n, q, d_model_basis_terms[q]);
332
  return gn;
333
}
334
335
27003
void FirstOrderModel::computeModelBasisArgAttribute(Node n)
336
{
337
27003
  if (!n.hasAttribute(ModelBasisArgAttribute()))
338
  {
339
    // ensure that the model basis terms have been defined
340
3460
    if (n.getKind() == APPLY_UF)
341
    {
342
3460
      getModelBasisOpTerm(n.getOperator());
343
    }
344
3460
    uint64_t val = 0;
345
    // determine if it has model basis attribute
346
9718
    for (unsigned j = 0, nchild = n.getNumChildren(); j < nchild; j++)
347
    {
348
6258
      if (n[j].getAttribute(ModelBasisAttribute()))
349
      {
350
893
        val++;
351
      }
352
    }
353
    ModelBasisArgAttribute mbaa;
354
3460
    n.setAttribute(mbaa, val);
355
  }
356
27003
}
357
358
27003
unsigned FirstOrderModel::getModelBasisArg(Node n)
359
{
360
27003
  computeModelBasisArgAttribute(n);
361
27003
  return n.getAttribute(ModelBasisArgAttribute());
362
}
363
364
} /* CVC4::theory::quantifiers namespace */
365
} /* CVC4::theory namespace */
366
27178
} /* CVC4 namespace */