GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus/sygus_invariance.cpp Lines: 111 138 80.4 %
Date: 2021-03-23 Branches: 203 532 38.2 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sygus_invariance.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner
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 techniques for sygus invariance tests.
13
 **/
14
15
#include "theory/quantifiers/sygus/sygus_invariance.h"
16
17
#include "theory/quantifiers/sygus/sygus_pbe.h"
18
#include "theory/quantifiers/sygus/synth_conjecture.h"
19
#include "theory/quantifiers/sygus/term_database_sygus.h"
20
#include "theory/rewriter.h"
21
22
using namespace CVC4::kind;
23
using namespace std;
24
25
namespace CVC4 {
26
namespace theory {
27
namespace quantifiers {
28
29
23395
void EvalSygusInvarianceTest::init(Node conj, Node var, Node res)
30
{
31
23395
  d_terms.clear();
32
  // simple miniscope
33
23395
  if ((conj.getKind() == AND || conj.getKind() == OR) && res.isConst())
34
  {
35
3576
    for (const Node& c : conj)
36
    {
37
2386
      d_terms.push_back(c);
38
    }
39
1190
    d_kind = conj.getKind();
40
1190
    d_is_conjunctive = res.getConst<bool>() == (d_kind == AND);
41
  }
42
  else
43
  {
44
22205
    d_terms.push_back(conj);
45
22205
    d_is_conjunctive = true;
46
  }
47
23395
  d_var = var;
48
23395
  d_result = res;
49
23395
}
50
51
102393
Node EvalSygusInvarianceTest::doEvaluateWithUnfolding(TermDbSygus* tds, Node n)
52
{
53
102393
  return tds->evaluateWithUnfolding(n, d_visited);
54
}
55
56
72093
bool EvalSygusInvarianceTest::invariant(TermDbSygus* tds, Node nvn, Node x)
57
{
58
144186
  TNode tnvn = nvn;
59
144186
  std::unordered_map<TNode, TNode, TNodeHashFunction> cache;
60
80298
  for (const Node& c : d_terms)
61
  {
62
81338
    Node conj_subs = c.substitute(d_var, tnvn, cache);
63
81338
    Node conj_subs_unfold = doEvaluateWithUnfolding(tds, conj_subs);
64
146266
    Trace("sygus-cref-eval2-debug")
65
73133
        << "  ...check unfolding : " << conj_subs_unfold << std::endl;
66
146266
    Trace("sygus-cref-eval2-debug")
67
73133
        << "  ......from : " << conj_subs << std::endl;
68
73133
    if (conj_subs_unfold != d_result)
69
    {
70
64928
      if (d_is_conjunctive)
71
      {
72
        // ti /--> true  implies and( t1, ..., tn ) /--> true, where "/-->" is
73
        // "does not evaluate to".
74
64928
        return false;
75
      }
76
    }
77
8205
    else if (!d_is_conjunctive)
78
    {
79
      // ti --> true  implies or( t1, ..., tn ) --> true
80
      return true;
81
    }
82
16410
    Trace("sygus-cref-eval2") << "Evaluation min explain : " << conj_subs
83
8205
                              << " still evaluates to " << d_result
84
8205
                              << " regardless of ";
85
8205
    Trace("sygus-cref-eval2") << x << std::endl;
86
  }
87
7165
  return d_is_conjunctive;
88
}
89
90
2659
void EquivSygusInvarianceTest::init(
91
    TermDbSygus* tds, TypeNode tn, SynthConjecture* aconj, Node e, Node bvr)
92
{
93
  // compute the current examples
94
2659
  d_bvr = bvr;
95
2659
  Assert(tds != nullptr);
96
2659
  if (aconj != nullptr)
97
  {
98
2659
    ExampleEvalCache* eec = aconj->getExampleEvalCache(e);
99
2659
    if (eec != nullptr)
100
    {
101
      // get the result of evaluating bvr on the examples of enumerator e.
102
200
      eec->evaluateVec(bvr, d_exo, false);
103
200
      d_conj = aconj;
104
200
      d_enum = e;
105
    }
106
  }
107
2659
}
108
109
9055
bool EquivSygusInvarianceTest::invariant(TermDbSygus* tds, Node nvn, Node x)
110
{
111
18110
  TypeNode tn = nvn.getType();
112
18110
  Node nbv = tds->sygusToBuiltin(nvn, tn);
113
18110
  Node nbvr = tds->getExtRewriter()->extendedRewrite(nbv);
114
18110
  Trace("sygus-sb-mexp-debug") << "  min-exp check : " << nbv << " -> " << nbvr
115
9055
                               << std::endl;
116
9055
  bool exc_arg = false;
117
  // equivalent / singular up to normalization
118
9055
  if (nbvr == d_bvr)
119
  {
120
    // gives the same result : then the explanation for the child is irrelevant
121
120
    exc_arg = true;
122
240
    Trace("sygus-sb-mexp") << "sb-min-exp : " << tds->sygusToBuiltin(nvn)
123
120
                           << " is rewritten to " << nbvr;
124
240
    Trace("sygus-sb-mexp") << " regardless of the content of "
125
120
                           << tds->sygusToBuiltin(x) << std::endl;
126
  }
127
  else
128
  {
129
8935
    if (nbvr.isVar())
130
    {
131
444
      TypeNode xtn = x.getType();
132
222
      if (xtn == tn)
133
      {
134
416
        Node bx = tds->sygusToBuiltin(x, xtn);
135
208
        Assert(bx.getType() == nbvr.getType());
136
208
        if (nbvr == bx)
137
        {
138
416
          Trace("sygus-sb-mexp") << "sb-min-exp : " << tds->sygusToBuiltin(nvn)
139
208
                                 << " always rewrites to argument " << nbvr
140
208
                                 << std::endl;
141
          // rewrites to the variable : then the explanation of this is
142
          // irrelevant as well
143
208
          exc_arg = true;
144
208
          d_bvr = nbvr;
145
        }
146
      }
147
    }
148
  }
149
  // equivalent under examples
150
9055
  if (!exc_arg)
151
  {
152
8727
    if (!d_enum.isNull())
153
    {
154
622
      bool ex_equiv = true;
155
622
      ExampleEvalCache* eec = d_conj->getExampleEvalCache(d_enum);
156
622
      Assert(eec != nullptr);
157
664
      for (unsigned j = 0, esize = d_exo.size(); j < esize; j++)
158
      {
159
702
        Node nbvr_ex = eec->evaluate(nbvr, j);
160
660
        if (nbvr_ex != d_exo[j])
161
        {
162
618
          ex_equiv = false;
163
618
          break;
164
        }
165
      }
166
622
      if (ex_equiv)
167
      {
168
4
        Trace("sygus-sb-mexp") << "sb-min-exp : " << tds->sygusToBuiltin(nvn);
169
8
        Trace("sygus-sb-mexp")
170
4
            << " is the same w.r.t. examples regardless of the content of "
171
4
            << tds->sygusToBuiltin(x) << std::endl;
172
4
        exc_arg = true;
173
      }
174
    }
175
  }
176
18110
  return exc_arg;
177
}
178
179
bool DivByZeroSygusInvarianceTest::invariant(TermDbSygus* tds, Node nvn, Node x)
180
{
181
  TypeNode tn = nvn.getType();
182
  Node nbv = tds->sygusToBuiltin(nvn, tn);
183
  Node nbvr = tds->getExtRewriter()->extendedRewrite(nbv);
184
  if (tds->involvesDivByZero(nbvr))
185
  {
186
    Trace("sygus-sb-mexp") << "sb-min-exp : " << tds->sygusToBuiltin(nvn)
187
                           << " involves div-by-zero regardless of "
188
                           << tds->sygusToBuiltin(x) << std::endl;
189
    return true;
190
  }
191
  return false;
192
}
193
194
96
void NegContainsSygusInvarianceTest::init(Node e,
195
                                          std::vector<std::vector<Node> >& ex,
196
                                          std::vector<Node>& exo,
197
                                          std::vector<unsigned>& ncind)
198
{
199
96
  Assert(ex.size() == exo.size());
200
96
  d_enum = e;
201
96
  d_ex.insert(d_ex.end(), ex.begin(), ex.end());
202
96
  d_exo.insert(d_exo.end(), exo.begin(), exo.end());
203
96
  d_neg_con_indices.insert(d_neg_con_indices.end(), ncind.begin(), ncind.end());
204
96
}
205
206
130
bool NegContainsSygusInvarianceTest::invariant(TermDbSygus* tds,
207
                                               Node nvn,
208
                                               Node x)
209
{
210
130
  if (!d_enum.isNull())
211
  {
212
254
    TypeNode tn = nvn.getType();
213
254
    Node nbv = tds->sygusToBuiltin(nvn, tn);
214
254
    Node nbvr = tds->getExtRewriter()->extendedRewrite(nbv);
215
    // if for any of the examples, it is not contained, then we can exclude
216
11934
    for (unsigned i = 0; i < d_neg_con_indices.size(); i++)
217
    {
218
11810
      unsigned ii = d_neg_con_indices[i];
219
11810
      Assert(ii < d_exo.size());
220
23614
      Node nbvre = tds->evaluateBuiltin(tn, nbvr, d_ex[ii]);
221
23614
      Node out = d_exo[ii];
222
      Node cont =
223
23614
          NodeManager::currentNM()->mkNode(kind::STRING_STRCTN, out, nbvre);
224
11810
      Trace("sygus-pbe-cterm-debug") << "Check: " << cont << std::endl;
225
23614
      Node contr = Rewriter::rewrite(cont);
226
11810
      if (!contr.isConst())
227
      {
228
11810
        if (d_isUniversal)
229
        {
230
6
          return false;
231
        }
232
      }
233
      else if (contr.getConst<bool>() == d_isUniversal)
234
      {
235
        if (Trace.isOn("sygus-pbe-cterm"))
236
        {
237
          Trace("sygus-pbe-cterm")
238
              << "PBE-cterm : enumerator : do not consider ";
239
          Trace("sygus-pbe-cterm")
240
              << nbv << " for any " << tds->sygusToBuiltin(x) << " since "
241
              << std::endl;
242
          Trace("sygus-pbe-cterm") << "   PBE-cterm :    for input example : ";
243
          for (unsigned j = 0, size = d_ex[ii].size(); j < size; j++)
244
          {
245
            Trace("sygus-pbe-cterm") << d_ex[ii][j] << " ";
246
          }
247
          Trace("sygus-pbe-cterm") << std::endl;
248
          Trace("sygus-pbe-cterm")
249
              << "   PBE-cterm :     this rewrites to : " << nbvre << std::endl;
250
          Trace("sygus-pbe-cterm")
251
              << "   PBE-cterm : and is not in output : " << out << std::endl;
252
        }
253
        return !d_isUniversal;
254
      }
255
23608
      Trace("sygus-pbe-cterm-debug2")
256
11804
          << "...check failed, rewrites to : " << contr << std::endl;
257
    }
258
  }
259
124
  return d_isUniversal;
260
}
261
262
} /* CVC4::theory::quantifiers namespace */
263
} /* CVC4::theory namespace */
264
26685
} /* CVC4 namespace */