GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/first_order_model.cpp Lines: 149 161 92.5 %
Date: 2021-03-22 Branches: 241 520 46.3 %

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