GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus/sygus_grammar_red.cpp Lines: 77 79 97.5 %
Date: 2021-03-23 Branches: 171 382 44.8 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sygus_grammar_red.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Haniel Barbosa
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 sygus_grammar_red
13
 **/
14
15
#include "theory/quantifiers/sygus/sygus_grammar_red.h"
16
17
#include "expr/dtype.h"
18
#include "expr/dtype_cons.h"
19
#include "expr/sygus_datatype.h"
20
#include "options/quantifiers_options.h"
21
#include "theory/quantifiers/sygus/term_database_sygus.h"
22
#include "theory/quantifiers/term_util.h"
23
24
using namespace std;
25
using namespace CVC4::kind;
26
27
namespace CVC4 {
28
namespace theory {
29
namespace quantifiers {
30
31
729
void SygusRedundantCons::initialize(TermDbSygus* tds, TypeNode tn)
32
{
33
729
  Assert(tds != nullptr);
34
729
  Trace("sygus-red") << "Compute redundant cons for " << tn << std::endl;
35
729
  d_type = tn;
36
729
  Assert(tn.isDatatype());
37
729
  tds->registerSygusType(tn);
38
729
  const DType& dt = tn.getDType();
39
729
  Assert(dt.isSygus());
40
1458
  TypeNode btn = dt.getSygusType();
41
4158
  for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
42
  {
43
6858
    Trace("sygus-red") << "  Is " << dt[i].getName() << " a redundant operator?"
44
3429
                       << std::endl;
45
6858
    Node sop = dt[i].getSygusOp();
46
3429
    if (sop.getAttribute(SygusAnyConstAttribute()))
47
    {
48
      // the any constant constructor is never redundant
49
      d_sygus_red_status.push_back(0);
50
      continue;
51
    }
52
6858
    std::map<int, Node> pre;
53
    // We do not do beta reduction, since we want the arguments to match the
54
    // the types of the datatype.
55
6858
    Node g = tds->mkGeneric(dt, i, pre, false);
56
3429
    Trace("sygus-red-debug") << "  ...pre-rewrite : " << g << std::endl;
57
3429
    d_gen_terms[i] = g;
58
    // is the operator a lambda of the form (lambda x1...xn. f(x1...xn))?
59
3429
    bool lamInOrder = false;
60
3429
    if (sop.getKind() == LAMBDA && sop[0].getNumChildren() == sop[1].getNumChildren())
61
    {
62
1595
      Assert(g.getNumChildren()==sop[0].getNumChildren());
63
1595
      lamInOrder = true;
64
4628
      for (size_t j = 0, nchild = sop[1].getNumChildren(); j < nchild; j++)
65
      {
66
3039
        if (sop[0][j] != sop[1][j])
67
        {
68
          // arguments not in order
69
6
          lamInOrder = false;
70
6
          break;
71
        }
72
      }
73
    }
74
    // a list of variants of the generic term (see getGenericList).
75
6858
    std::vector<Node> glist;
76
3429
    if (lamInOrder)
77
    {
78
      // If it is a lambda whose arguments are one-to-one with the datatype
79
      // arguments, then we can add variants of this operator by permuting
80
      // the argument list (see getGenericList).
81
1589
      Assert(g.getNumChildren()==dt[i].getNumArgs());
82
4620
      for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
83
      {
84
3031
        pre[j] = g[j];
85
      }
86
1589
      getGenericList(tds, dt, i, 0, pre, glist);
87
    }
88
    else
89
    {
90
      // It is a builtin (possibly) ground term. Its children do not correspond
91
      // one-to-one with the arugments of the constructor. Hence, we consider
92
      // only g itself as a variant.
93
1840
      glist.push_back(g);
94
    }
95
    // call the extended rewriter
96
3429
    bool red = false;
97
7999
    for (const Node& gr : glist)
98
    {
99
4609
      Trace("sygus-red-debug") << "  ...variant : " << gr << std::endl;
100
4609
      std::map<Node, unsigned>::iterator itg = d_gen_cons.find(gr);
101
4609
      if (itg != d_gen_cons.end() && itg->second != i)
102
      {
103
39
        red = true;
104
78
        Trace("sygus-red") << "  ......redundant, since a variant of " << g
105
39
                           << " and " << d_gen_terms[itg->second]
106
39
                           << " both rewrite to " << gr << std::endl;
107
39
        break;
108
      }
109
      else
110
      {
111
4570
        d_gen_cons[gr] = i;
112
4570
        Trace("sygus-red") << "  ......not redundant." << std::endl;
113
      }
114
    }
115
3429
    d_sygus_red_status.push_back(red ? 1 : 0);
116
  }
117
1458
  Trace("sygus-red") << "Compute redundant cons for " << tn << " finished"
118
729
                     << std::endl;
119
729
}
120
121
729
void SygusRedundantCons::getRedundant(std::vector<unsigned>& indices)
122
{
123
729
  const DType& dt = d_type.getDType();
124
4158
  for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
125
  {
126
3429
    if (isRedundant(i))
127
    {
128
39
      indices.push_back(i);
129
    }
130
  }
131
729
}
132
133
3429
bool SygusRedundantCons::isRedundant(unsigned i)
134
{
135
3429
  Assert(i < d_sygus_red_status.size());
136
3429
  return d_sygus_red_status[i] == 1;
137
}
138
139
7160
void SygusRedundantCons::getGenericList(TermDbSygus* tds,
140
                                        const DType& dt,
141
                                        unsigned c,
142
                                        unsigned index,
143
                                        std::map<int, Node>& pre,
144
                                        std::vector<Node>& terms)
145
{
146
7160
  if (index == dt[c].getNumArgs())
147
  {
148
5608
    Node gt = tds->mkGeneric(dt, c, pre);
149
2804
    gt = tds->getExtRewriter()->extendedRewrite(gt);
150
2804
    terms.push_back(gt);
151
2804
    return;
152
  }
153
  // with no swap
154
4356
  getGenericList(tds, dt, c, index + 1, pre, terms);
155
  // swapping is exponential, only use for operators with small # args.
156
4356
  if (dt[c].getNumArgs() <= 5)
157
  {
158
8712
    TypeNode atype = tds->getArgType(dt[c], index);
159
6129
    for (unsigned s = index + 1, nargs = dt[c].getNumArgs(); s < nargs; s++)
160
    {
161
1773
      if (tds->getArgType(dt[c], s) == atype)
162
      {
163
        // swap s and index
164
2430
        Node tmp = pre[s];
165
1215
        pre[s] = pre[index];
166
1215
        pre[index] = tmp;
167
1215
        getGenericList(tds, dt, c, index + 1, pre, terms);
168
        // revert
169
1215
        tmp = pre[s];
170
1215
        pre[s] = pre[index];
171
1215
        pre[index] = tmp;
172
      }
173
    }
174
  }
175
}
176
177
} /* CVC4::theory::quantifiers namespace */
178
} /* CVC4::theory namespace */
179
26685
} /* CVC4 namespace */