GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/inst_match.cpp Lines: 26 46 56.5 %
Date: 2021-03-22 Branches: 24 142 16.9 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file inst_match.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Morgan Deters, Francois Bobot
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 inst match class
13
 **/
14
15
#include "theory/quantifiers/inst_match.h"
16
17
#include "theory/quantifiers/instantiate.h"
18
#include "theory/quantifiers/quantifiers_state.h"
19
#include "theory/quantifiers/term_database.h"
20
#include "theory/quantifiers_engine.h"
21
22
namespace CVC4 {
23
namespace theory {
24
namespace inst {
25
26
41572
InstMatch::InstMatch(TNode q)
27
{
28
41572
  d_vals.resize(q[0].getNumChildren());
29
41572
  Assert(!d_vals.empty());
30
  // resize must initialize with null nodes
31
41572
  Assert(d_vals[0].isNull());
32
41572
}
33
34
63483
InstMatch::InstMatch( InstMatch* m ) {
35
63483
  d_vals.insert( d_vals.end(), m->d_vals.begin(), m->d_vals.end() );
36
63483
}
37
38
void InstMatch::add(InstMatch& m)
39
{
40
  for (unsigned i = 0, size = d_vals.size(); i < size; i++)
41
  {
42
    if( d_vals[i].isNull() ){
43
      d_vals[i] = m.d_vals[i];
44
    }
45
  }
46
}
47
48
void InstMatch::debugPrint( const char* c ){
49
  for (unsigned i = 0, size = d_vals.size(); i < size; i++)
50
  {
51
    if( !d_vals[i].isNull() ){
52
      Debug( c ) << "   " << i << " -> " << d_vals[i] << std::endl;
53
    }
54
  }
55
}
56
57
bool InstMatch::isComplete() {
58
  for (Node& v : d_vals)
59
  {
60
    if (v.isNull())
61
    {
62
      return false;
63
    }
64
  }
65
  return true;
66
}
67
68
bool InstMatch::empty() {
69
  for (Node& v : d_vals)
70
  {
71
    if (!v.isNull())
72
    {
73
      return false;
74
    }
75
  }
76
  return true;
77
}
78
79
12436
void InstMatch::clear() {
80
59374
  for( unsigned i=0; i<d_vals.size(); i++ ){
81
46938
    d_vals[i] = Node::null();
82
  }
83
12436
}
84
85
3594817
Node InstMatch::get(size_t i) const
86
{
87
3594817
  Assert(i < d_vals.size());
88
3594817
  return d_vals[i];
89
}
90
91
487793
void InstMatch::setValue(size_t i, TNode n)
92
{
93
487793
  Assert(i < d_vals.size());
94
487793
  d_vals[i] = n;
95
487793
}
96
2076788
bool InstMatch::set(quantifiers::QuantifiersState& qs, size_t i, TNode n)
97
{
98
2076788
  Assert(i < d_vals.size());
99
2076788
  if( !d_vals[i].isNull() ){
100
1370399
    return qs.areEqual(d_vals[i], n);
101
  }
102
706389
  d_vals[i] = n;
103
706389
  return true;
104
}
105
106
}/* CVC4::theory::inst namespace */
107
}/* CVC4::theory namespace */
108
26676
}/* CVC4 namespace */