GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arrays/proof_checker.cpp Lines: 41 61 67.2 %
Date: 2021-03-23 Branches: 103 454 22.7 %

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 arrays proof checker
13
 **/
14
15
#include "theory/arrays/proof_checker.h"
16
#include "expr/skolem_manager.h"
17
#include "theory/arrays/skolem_cache.h"
18
#include "theory/rewriter.h"
19
20
namespace CVC4 {
21
namespace theory {
22
namespace arrays {
23
24
962
void ArraysProofRuleChecker::registerTo(ProofChecker* pc)
25
{
26
962
  pc->registerChecker(PfRule::ARRAYS_READ_OVER_WRITE, this);
27
962
  pc->registerChecker(PfRule::ARRAYS_READ_OVER_WRITE_CONTRA, this);
28
962
  pc->registerChecker(PfRule::ARRAYS_READ_OVER_WRITE_1, this);
29
962
  pc->registerChecker(PfRule::ARRAYS_EXT, this);
30
  // trusted rules
31
962
  pc->registerTrustedChecker(PfRule::ARRAYS_TRUST, this, 2);
32
962
}
33
34
5109
Node ArraysProofRuleChecker::checkInternal(PfRule id,
35
                                           const std::vector<Node>& children,
36
                                           const std::vector<Node>& args)
37
{
38
5109
  NodeManager* nm = NodeManager::currentNM();
39
5109
  if (id == PfRule::ARRAYS_READ_OVER_WRITE)
40
  {
41
1701
    Assert(children.size() == 1);
42
1701
    Assert(args.size() == 1);
43
3402
    Node ideq = children[0];
44
1701
    if (ideq.getKind() != kind::NOT || ideq[0].getKind() != kind::EQUAL)
45
    {
46
      return Node::null();
47
    }
48
3402
    Node lhs = args[0];
49
5103
    if (lhs.getKind() != kind::SELECT || lhs[0].getKind() != kind::STORE
50
5103
        || lhs[0][1] != ideq[0][0])
51
    {
52
      return Node::null();
53
    }
54
3402
    Node rhs = nm->mkNode(kind::SELECT, lhs[0][0], ideq[0][1]);
55
1701
    return lhs.eqNode(rhs);
56
  }
57
3408
  else if (id == PfRule::ARRAYS_READ_OVER_WRITE_CONTRA)
58
  {
59
    Assert(children.size() == 1);
60
    Assert(args.empty());
61
    Node adeq = children[0];
62
    if (adeq.getKind() != kind::NOT || adeq[0].getKind() != kind::EQUAL)
63
    {
64
      return Node::null();
65
    }
66
    Node lhs = adeq[0][0];
67
    Node rhs = adeq[0][1];
68
    if (lhs.getKind() != kind::SELECT || lhs[0].getKind() != kind::STORE
69
        || rhs.getKind() != kind::SELECT || lhs[1] != rhs[1])
70
    {
71
      return Node::null();
72
    }
73
    return lhs[1].eqNode(lhs[0][1]);
74
  }
75
3408
  if (id == PfRule::ARRAYS_READ_OVER_WRITE_1)
76
  {
77
3282
    Assert(children.empty());
78
3282
    Assert(args.size() == 1);
79
6564
    Node lhs = args[0];
80
9846
    if (lhs.getKind() != kind::SELECT || lhs[0].getKind() != kind::STORE
81
9846
        || lhs[0][1] != lhs[1])
82
    {
83
      return Node::null();
84
    }
85
6564
    Node rhs = lhs[0][2];
86
3282
    return lhs.eqNode(rhs);
87
  }
88
126
  if (id == PfRule::ARRAYS_EXT)
89
  {
90
126
    Assert(children.size() == 1);
91
126
    Assert(args.empty());
92
252
    Node adeq = children[0];
93
378
    if (adeq.getKind() != kind::NOT || adeq[0].getKind() != kind::EQUAL
94
378
        || !adeq[0][0].getType().isArray())
95
    {
96
      return Node::null();
97
    }
98
252
    Node k = SkolemCache::getExtIndexSkolem(adeq);
99
252
    Node a = adeq[0][0];
100
252
    Node b = adeq[0][1];
101
252
    Node as = nm->mkNode(kind::SELECT, a, k);
102
252
    Node bs = nm->mkNode(kind::SELECT, b, k);
103
126
    return as.eqNode(bs).notNode();
104
  }
105
  if (id == PfRule::ARRAYS_TRUST)
106
  {
107
    // "trusted" rules
108
    Assert(!args.empty());
109
    Assert(args[0].getType().isBoolean());
110
    return args[0];
111
  }
112
  // no rule
113
  return Node::null();
114
}
115
116
}  // namespace arrays
117
}  // namespace theory
118
26685
}  // namespace CVC4