GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/datatypes/proof_checker.cpp Lines: 58 72 80.6 %
Date: 2021-03-23 Branches: 126 470 26.8 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file proof_checker.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds
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 datatypes proof checker
13
 **/
14
15
#include "theory/datatypes/proof_checker.h"
16
17
#include "expr/dtype_cons.h"
18
#include "theory/datatypes/theory_datatypes_utils.h"
19
#include "theory/rewriter.h"
20
21
namespace CVC4 {
22
namespace theory {
23
namespace datatypes {
24
25
962
void DatatypesProofRuleChecker::registerTo(ProofChecker* pc)
26
{
27
962
  pc->registerChecker(PfRule::DT_UNIF, this);
28
962
  pc->registerChecker(PfRule::DT_INST, this);
29
962
  pc->registerChecker(PfRule::DT_COLLAPSE, this);
30
962
  pc->registerChecker(PfRule::DT_SPLIT, this);
31
962
  pc->registerChecker(PfRule::DT_CLASH, this);
32
  // trusted rules
33
962
  pc->registerTrustedChecker(PfRule::DT_TRUST, this, 2);
34
962
}
35
36
10945
Node DatatypesProofRuleChecker::checkInternal(PfRule id,
37
                                              const std::vector<Node>& children,
38
                                              const std::vector<Node>& args)
39
{
40
10945
  NodeManager* nm = NodeManager::currentNM();
41
10945
  if (id == PfRule::DT_UNIF)
42
  {
43
1042
    Assert(children.size() == 1);
44
1042
    Assert(args.size() == 1);
45
    uint32_t i;
46
2084
    if (children[0].getKind() != kind::EQUAL
47
2084
        || children[0][0].getKind() != kind::APPLY_CONSTRUCTOR
48
2084
        || children[0][1].getKind() != kind::APPLY_CONSTRUCTOR
49
2084
        || children[0][0].getOperator() != children[0][1].getOperator()
50
3126
        || !getUInt32(args[0], i))
51
    {
52
      return Node::null();
53
    }
54
1042
    if (i >= children[0][0].getNumChildren())
55
    {
56
      return Node::null();
57
    }
58
1042
    Assert(children[0][0].getNumChildren() == children[0][1].getNumChildren());
59
1042
    return children[0][0][i].eqNode(children[0][1][i]);
60
  }
61
9903
  else if (id == PfRule::DT_INST)
62
  {
63
3873
    Assert(children.empty());
64
3873
    Assert(args.size() == 2);
65
7746
    Node t = args[0];
66
7746
    TypeNode tn = t.getType();
67
    uint32_t i;
68
3873
    if (!tn.isDatatype() || !getUInt32(args[1], i))
69
    {
70
      return Node::null();
71
    }
72
3873
    const DType& dt = tn.getDType();
73
3873
    if (i >= dt.getNumConstructors())
74
    {
75
      return Node::null();
76
    }
77
7746
    Node tester = utils::mkTester(t, i, dt);
78
7746
    Node ticons = Rewriter::rewrite(utils::getInstCons(t, dt, i));
79
3873
    return tester.eqNode(t.eqNode(ticons));
80
  }
81
6030
  else if (id == PfRule::DT_COLLAPSE)
82
  {
83
3652
    Assert(children.empty());
84
3652
    Assert(args.size() == 1);
85
7304
    Node t = args[0];
86
7304
    if (t.getKind() != kind::APPLY_SELECTOR_TOTAL
87
7304
        || t[0].getKind() != kind::APPLY_CONSTRUCTOR)
88
    {
89
      return Node::null();
90
    }
91
7304
    Node selector = t.getOperator();
92
3652
    size_t constructorIndex = utils::indexOf(t[0].getOperator());
93
3652
    const DType& dt = utils::datatypeOf(selector);
94
3652
    const DTypeConstructor& dtc = dt[constructorIndex];
95
3652
    int selectorIndex = dtc.getSelectorIndexInternal(selector);
96
    Node r =
97
7304
        selectorIndex < 0 ? t.getType().mkGroundTerm() : t[0][selectorIndex];
98
3652
    return t.eqNode(r);
99
  }
100
2378
  else if (id == PfRule::DT_SPLIT)
101
  {
102
1886
    Assert(children.empty());
103
1886
    Assert(args.size() == 1);
104
3772
    TypeNode tn = args[0].getType();
105
1886
    if (!tn.isDatatype())
106
    {
107
      return Node::null();
108
    }
109
1886
    const DType& dt = tn.getDType();
110
1886
    return utils::mkSplit(args[0], dt);
111
  }
112
492
  else if (id == PfRule::DT_CLASH)
113
  {
114
    Assert(children.size() == 2);
115
    Assert(args.empty());
116
    if (children[0].getKind() != kind::APPLY_TESTER
117
        || children[1].getKind() != kind::APPLY_TESTER
118
        || children[0][0] != children[1][0] || children[0] == children[1])
119
    {
120
      return Node::null();
121
    }
122
    return nm->mkConst(false);
123
  }
124
492
  else if (id == PfRule::DT_TRUST)
125
  {
126
492
    Assert(!args.empty());
127
492
    Assert(args[0].getType().isBoolean());
128
492
    return args[0];
129
  }
130
  // no rule
131
  return Node::null();
132
}
133
134
}  // namespace datatypes
135
}  // namespace theory
136
26685
}  // namespace CVC4