GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp Lines: 64 70 91.4 %
Date: 2021-03-22 Branches: 159 317 50.2 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file ceg_dt_instantiator.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Andres Noetzli
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 ceg_dt_instantiator
13
 **/
14
15
#include "theory/quantifiers/cegqi/ceg_dt_instantiator.h"
16
17
#include "expr/dtype.h"
18
#include "expr/dtype_cons.h"
19
#include "expr/node_algorithm.h"
20
#include "theory/datatypes/theory_datatypes_utils.h"
21
22
using namespace std;
23
using namespace CVC4::kind;
24
25
namespace CVC4 {
26
namespace theory {
27
namespace quantifiers {
28
29
43
void DtInstantiator::reset(CegInstantiator* ci,
30
                           SolvedForm& sf,
31
                           Node pv,
32
                           CegInstEffort effort)
33
{
34
43
}
35
36
43
bool DtInstantiator::hasProcessEqualTerm(CegInstantiator* ci,
37
                                         SolvedForm& sf,
38
                                         Node pv,
39
                                         CegInstEffort effort)
40
{
41
43
  return true;
42
}
43
44
31
bool DtInstantiator::processEqualTerms(CegInstantiator* ci,
45
                                       SolvedForm& sf,
46
                                       Node pv,
47
                                       std::vector<Node>& eqc,
48
                                       CegInstEffort effort)
49
{
50
62
  Trace("cegqi-dt-debug") << "try based on constructors in equivalence class."
51
31
                          << std::endl;
52
  // look in equivalence class for a constructor
53
31
  NodeManager* nm = NodeManager::currentNM();
54
62
  for (unsigned k = 0, size = eqc.size(); k < size; k++)
55
  {
56
84
    Node n = eqc[k];
57
53
    if (n.getKind() == APPLY_CONSTRUCTOR)
58
    {
59
44
      Trace("cegqi-dt-debug")
60
22
          << "...try based on constructor term " << n << std::endl;
61
22
      std::vector<Node> children;
62
22
      children.push_back(n.getOperator());
63
22
      const DType& dt = d_type.getDType();
64
22
      unsigned cindex = datatypes::utils::indexOf(n.getOperator());
65
      // now must solve for selectors applied to pv
66
66
      for (unsigned j = 0, nargs = dt[cindex].getNumArgs(); j < nargs; j++)
67
      {
68
        Node c = nm->mkNode(APPLY_SELECTOR_TOTAL,
69
88
                            dt[cindex].getSelectorInternal(d_type, j),
70
176
                            pv);
71
44
        ci->pushStackVariable(c);
72
44
        children.push_back(c);
73
      }
74
22
      Node val = nm->mkNode(kind::APPLY_CONSTRUCTOR, children);
75
22
      TermProperties pv_prop_dt;
76
22
      if (ci->constructInstantiationInc(pv, val, pv_prop_dt, sf))
77
      {
78
22
        return true;
79
      }
80
      // cleanup
81
      for (unsigned j = 0, nargs = dt[cindex].getNumArgs(); j < nargs; j++)
82
      {
83
        ci->popStackVariable();
84
      }
85
      break;
86
    }
87
  }
88
9
  return false;
89
}
90
91
9
bool DtInstantiator::hasProcessEquality(CegInstantiator* ci,
92
                                        SolvedForm& sf,
93
                                        Node pv,
94
                                        CegInstEffort effort)
95
{
96
9
  return true;
97
}
98
99
11
bool DtInstantiator::processEquality(CegInstantiator* ci,
100
                                     SolvedForm& sf,
101
                                     Node pv,
102
                                     std::vector<TermProperties>& term_props,
103
                                     std::vector<Node>& terms,
104
                                     CegInstEffort effort)
105
{
106
22
  Node val = solve_dt(pv, terms[0], terms[1], terms[0], terms[1]);
107
11
  if (!val.isNull())
108
  {
109
1
    TermProperties pv_prop;
110
1
    if (ci->constructInstantiationInc(pv, val, pv_prop, sf))
111
    {
112
1
      return true;
113
    }
114
  }
115
10
  return false;
116
}
117
118
36
Node DtInstantiator::solve_dt(Node v, Node a, Node b, Node sa, Node sb)
119
{
120
72
  Trace("cegqi-arith-debug2") << "Solve dt : " << v << " " << a << " " << b
121
36
                              << " " << sa << " " << sb << std::endl;
122
72
  Node ret;
123
36
  if (!a.isNull() && a == v)
124
  {
125
11
    ret = sb;
126
  }
127
25
  else if (!b.isNull() && b == v)
128
  {
129
    ret = sa;
130
  }
131
25
  else if (!a.isNull() && a.getKind() == APPLY_CONSTRUCTOR)
132
  {
133
13
    if (!b.isNull() && b.getKind() == APPLY_CONSTRUCTOR)
134
    {
135
12
      if (a.getOperator() == b.getOperator())
136
      {
137
36
        for (unsigned i = 0, nchild = a.getNumChildren(); i < nchild; i++)
138
        {
139
48
          Node s = solve_dt(v, a[i], b[i], sa[i], sb[i]);
140
24
          if (!s.isNull())
141
          {
142
            return s;
143
          }
144
        }
145
      }
146
    }
147
    else
148
    {
149
1
      NodeManager* nm = NodeManager::currentNM();
150
1
      unsigned cindex = DType::indexOf(a.getOperator());
151
1
      TypeNode tn = a.getType();
152
1
      const DType& dt = tn.getDType();
153
1
      for (unsigned i = 0, nchild = a.getNumChildren(); i < nchild; i++)
154
      {
155
        Node nn = nm->mkNode(
156
1
            APPLY_SELECTOR_TOTAL, dt[cindex].getSelectorInternal(tn, i), sb);
157
1
        Node s = solve_dt(v, a[i], Node::null(), sa[i], nn);
158
1
        if (!s.isNull())
159
        {
160
1
          return s;
161
        }
162
      }
163
    }
164
  }
165
12
  else if (!b.isNull() && b.getKind() == APPLY_CONSTRUCTOR)
166
  {
167
    // flip sides
168
    return solve_dt(v, b, a, sb, sa);
169
  }
170
35
  if (!ret.isNull())
171
  {
172
    // ensure does not contain v
173
11
    if (expr::hasSubterm(ret, v))
174
    {
175
10
      ret = Node::null();
176
    }
177
  }
178
35
  return ret;
179
}
180
181
}  // namespace quantifiers
182
}  // namespace theory
183
26676
}  // namespace CVC4