GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/datatypes/infer_proof_cons.cpp Lines: 125 139 89.9 %
Date: 2021-03-22 Branches: 367 888 41.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file infer_proof_cons.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Gereon Kremer
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 inference to proof conversion  for datatypes
13
 **/
14
15
#include "theory/datatypes/infer_proof_cons.h"
16
17
#include "expr/proof.h"
18
#include "expr/proof_checker.h"
19
#include "theory/datatypes/theory_datatypes_utils.h"
20
#include "theory/model_manager.h"
21
#include "theory/rewriter.h"
22
23
using namespace CVC4::kind;
24
25
namespace CVC4 {
26
namespace theory {
27
namespace datatypes {
28
29
1719
InferProofCons::InferProofCons(context::Context* c, ProofNodeManager* pnm)
30
1719
    : d_pnm(pnm), d_lazyFactMap(c == nullptr ? &d_context : c)
31
{
32
1719
  Assert(d_pnm != nullptr);
33
1719
}
34
35
14922
void InferProofCons::notifyFact(const std::shared_ptr<DatatypesInference>& di)
36
{
37
29799
  TNode fact = di->d_conc;
38
14922
  if (d_lazyFactMap.find(fact) != d_lazyFactMap.end())
39
  {
40
42
    return;
41
  }
42
29757
  Node symFact = CDProof::getSymmFact(fact);
43
14880
  if (!symFact.isNull() && d_lazyFactMap.find(symFact) != d_lazyFactMap.end())
44
  {
45
3
    return;
46
  }
47
14877
  d_lazyFactMap.insert(fact, di);
48
}
49
50
10901
void InferProofCons::convert(InferenceId infer, TNode conc, TNode exp, CDProof* cdp)
51
{
52
21802
  Trace("dt-ipc") << "convert: " << infer << ": " << conc << " by " << exp
53
10901
                  << std::endl;
54
  // split into vector
55
21802
  std::vector<Node> expv;
56
10901
  if (!exp.isNull() && !exp.isConst())
57
  {
58
9545
    if (exp.getKind() == AND)
59
    {
60
891
      for (const Node& ec : exp)
61
      {
62
630
        expv.push_back(ec);
63
      }
64
    }
65
    else
66
    {
67
9284
      expv.push_back(exp);
68
    }
69
  }
70
10901
  NodeManager* nm = NodeManager::currentNM();
71
10901
  bool success = false;
72
10901
  switch (infer)
73
  {
74
1042
    case InferenceId::DATATYPES_UNIF:
75
    {
76
1042
      Assert(expv.size() == 1);
77
1042
      Assert(exp.getKind() == EQUAL && exp[0].getKind() == APPLY_CONSTRUCTOR
78
             && exp[1].getKind() == APPLY_CONSTRUCTOR
79
             && exp[0].getOperator() == exp[1].getOperator());
80
2084
      Node narg;
81
      // we may be asked for a proof of (not P) coming from (= P false) or
82
      // (= false P), or similarly P from (= P true) or (= true P).
83
1042
      bool concPol = conc.getKind() != NOT;
84
2084
      Node concAtom = concPol ? conc : conc[0];
85
2084
      Node unifConc = conc;
86
1734
      for (size_t i = 0, nchild = exp[0].getNumChildren(); i < nchild; i++)
87
      {
88
1734
        bool argSuccess = false;
89
1734
        if (conc.getKind() == EQUAL)
90
        {
91
1722
          argSuccess = (exp[0][i] == conc[0] && exp[1][i] == conc[1]);
92
        }
93
        else
94
        {
95
30
          for (size_t j = 0; j < 2; j++)
96
          {
97
78
            if (exp[j][i] == concAtom && exp[1 - j][i].isConst()
98
78
                && exp[1 - j][i].getConst<bool>() == concPol)
99
            {
100
6
              argSuccess = true;
101
6
              unifConc = exp[0][i].eqNode(exp[1][i]);
102
6
              break;
103
            }
104
          }
105
        }
106
1734
        if (argSuccess)
107
        {
108
1042
          narg = nm->mkConst(Rational(i));
109
1042
          break;
110
        }
111
      }
112
1042
      if (!narg.isNull())
113
      {
114
1042
        if (conc.getKind() == EQUAL)
115
        {
116
          // normal case where we conclude an equality
117
1036
          cdp->addStep(conc, PfRule::DT_UNIF, {exp}, {narg});
118
        }
119
        else
120
        {
121
          // must use true or false elim to prove the final
122
6
          cdp->addStep(unifConc, PfRule::DT_UNIF, {exp}, {narg});
123
          // may use symmetry
124
12
          Node eq = concAtom.eqNode(nm->mkConst(concPol));
125
12
          cdp->addStep(
126
6
              conc, concPol ? PfRule::TRUE_ELIM : PfRule::FALSE_ELIM, {eq}, {});
127
        }
128
1042
        success = true;
129
1042
      }
130
    }
131
1042
    break;
132
4045
    case InferenceId::DATATYPES_INST:
133
    {
134
4045
      if (expv.size() == 1)
135
      {
136
3873
        Assert(conc.getKind() == EQUAL);
137
3873
        int n = utils::isTester(exp);
138
3873
        if (n >= 0)
139
        {
140
7746
          Node t = exp[0];
141
7746
          Node nn = nm->mkConst(Rational(n));
142
7746
          Node eq = exp.eqNode(conc);
143
3873
          cdp->addStep(eq, PfRule::DT_INST, {}, {t, nn});
144
3873
          cdp->addStep(conc, PfRule::EQ_RESOLVE, {exp, eq}, {});
145
3873
          success = true;
146
        }
147
      }
148
    }
149
4045
    break;
150
1184
    case InferenceId::DATATYPES_SPLIT:
151
    {
152
1184
      Assert(expv.empty());
153
2368
      Node t = conc.getKind() == OR ? conc[0][0] : conc[0];
154
1184
      cdp->addStep(conc, PfRule::DT_SPLIT, {}, {t});
155
2368
      success = true;
156
    }
157
1184
    break;
158
3652
    case InferenceId::DATATYPES_COLLAPSE_SEL:
159
    {
160
3652
      Assert(exp.getKind() == EQUAL);
161
7304
      Node concEq = conc;
162
      // might be a Boolean conclusion
163
3652
      if (conc.getKind() != EQUAL)
164
      {
165
3
        bool concPol = conc.getKind() != NOT;
166
6
        Node concAtom = concPol ? conc : conc[0];
167
3
        concEq = concAtom.eqNode(nm->mkConst(concPol));
168
      }
169
3652
      Assert(concEq.getKind() == EQUAL
170
             && concEq[0].getKind() == APPLY_SELECTOR_TOTAL);
171
3652
      Assert(exp[0].getType().isDatatype());
172
7304
      Node sop = concEq[0].getOperator();
173
7304
      Node sl = nm->mkNode(APPLY_SELECTOR_TOTAL, sop, exp[0]);
174
7304
      Node sr = nm->mkNode(APPLY_SELECTOR_TOTAL, sop, exp[1]);
175
      // exp[0] = exp[1]
176
      // --------------------- CONG        ----------------- DT_COLLAPSE
177
      // s(exp[0]) = s(exp[1])             s(exp[1]) = r
178
      // --------------------------------------------------- TRANS
179
      // s(exp[0]) = r
180
7304
      Node asn = ProofRuleChecker::mkKindNode(APPLY_SELECTOR_TOTAL);
181
7304
      Node seq = sl.eqNode(sr);
182
3652
      cdp->addStep(seq, PfRule::CONG, {exp}, {asn, sop});
183
7304
      Node sceq = sr.eqNode(concEq[1]);
184
3652
      cdp->addStep(sceq, PfRule::DT_COLLAPSE, {}, {sr});
185
3652
      cdp->addStep(sl.eqNode(concEq[1]), PfRule::TRANS, {seq, sceq}, {});
186
3652
      if (conc.getKind() != EQUAL)
187
      {
188
        PfRule eid =
189
3
            conc.getKind() == NOT ? PfRule::FALSE_ELIM : PfRule::TRUE_ELIM;
190
3
        cdp->addStep(conc, eid, {concEq}, {});
191
      }
192
7304
      success = true;
193
    }
194
3652
    break;
195
517
    case InferenceId::DATATYPES_CLASH_CONFLICT:
196
    {
197
517
      cdp->addStep(conc, PfRule::MACRO_SR_PRED_ELIM, {exp}, {});
198
517
      success = true;
199
    }
200
517
    break;
201
144
    case InferenceId::DATATYPES_TESTER_CONFLICT:
202
    {
203
      // rewrites to false under substitution
204
288
      Node fn = nm->mkConst(false);
205
144
      cdp->addStep(fn, PfRule::MACRO_SR_PRED_ELIM, expv, {});
206
288
      success = true;
207
    }
208
144
    break;
209
    case InferenceId::DATATYPES_TESTER_MERGE_CONFLICT:
210
    {
211
      Assert(expv.size() == 3);
212
      Node tester1 = expv[0];
213
      Node tester1c =
214
          nm->mkNode(APPLY_TESTER, expv[1].getOperator(), expv[0][0]);
215
      cdp->addStep(tester1c,
216
                   PfRule::MACRO_SR_PRED_TRANSFORM,
217
                   {expv[1], expv[2]},
218
                   {tester1c});
219
      Node fn = nm->mkConst(false);
220
      cdp->addStep(fn, PfRule::DT_CLASH, {tester1, tester1c}, {});
221
      success = true;
222
    }
223
    break;
224
    // inferences currently not supported
225
317
    case InferenceId::DATATYPES_LABEL_EXH:
226
    case InferenceId::DATATYPES_BISIMILAR:
227
    case InferenceId::DATATYPES_CYCLE:
228
    default:
229
634
      Trace("dt-ipc") << "...no conversion for inference " << infer
230
317
                      << std::endl;
231
317
      break;
232
  }
233
234
10901
  if (!success)
235
  {
236
    // failed to reconstruct, add trust
237
489
    Trace("dt-ipc") << "...failed " << infer << std::endl;
238
489
    cdp->addStep(conc, PfRule::DT_TRUST, expv, {conc});
239
  }
240
  else
241
  {
242
10412
    Trace("dt-ipc") << "...success" << std::endl;
243
  }
244
10901
}
245
246
10901
std::shared_ptr<ProofNode> InferProofCons::getProofFor(Node fact)
247
{
248
10901
  Trace("dt-ipc") << "dt-ipc: Ask proof for " << fact << std::endl;
249
  // temporary proof
250
21802
  CDProof pf(d_pnm);
251
  // get the inference
252
10901
  NodeDatatypesInferenceMap::iterator it = d_lazyFactMap.find(fact);
253
10901
  if (it == d_lazyFactMap.end())
254
  {
255
    Node factSym = CDProof::getSymmFact(fact);
256
    if (!factSym.isNull())
257
    {
258
      // Use the symmetric fact. There is no need to explictly make a
259
      // SYMM proof, as this is handled by CDProof::getProofFor below.
260
      it = d_lazyFactMap.find(factSym);
261
    }
262
  }
263
10901
  AlwaysAssert(it != d_lazyFactMap.end());
264
  // now go back and convert it to proof steps and add to proof
265
21802
  std::shared_ptr<DatatypesInference> di = (*it).second;
266
  // run the conversion
267
10901
  convert(di->getId(), di->d_conc, di->d_exp, &pf);
268
21802
  return pf.getProofFor(fact);
269
}
270
271
23079
std::string InferProofCons::identify() const
272
{
273
23079
  return "datatypes::InferProofCons";
274
}
275
276
}  // namespace datatypes
277
}  // namespace theory
278
26676
}  // namespace CVC4