GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/proof_checker.cpp Lines: 42 58 72.4 %
Date: 2021-03-23 Branches: 67 270 24.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 quantifiers proof checker
13
 **/
14
15
#include "theory/quantifiers/proof_checker.h"
16
17
#include "expr/node_algorithm.h"
18
#include "expr/skolem_manager.h"
19
#include "theory/builtin/proof_checker.h"
20
21
using namespace CVC4::kind;
22
23
namespace CVC4 {
24
namespace theory {
25
namespace quantifiers {
26
27
962
void QuantifiersProofRuleChecker::registerTo(ProofChecker* pc)
28
{
29
  // add checkers
30
962
  pc->registerChecker(PfRule::SKOLEM_INTRO, this);
31
962
  pc->registerChecker(PfRule::EXISTS_INTRO, this);
32
962
  pc->registerChecker(PfRule::SKOLEMIZE, this);
33
962
  pc->registerChecker(PfRule::INSTANTIATE, this);
34
962
}
35
36
11692
Node QuantifiersProofRuleChecker::checkInternal(
37
    PfRule id, const std::vector<Node>& children, const std::vector<Node>& args)
38
{
39
11692
  NodeManager* nm = NodeManager::currentNM();
40
11692
  SkolemManager* sm = nm->getSkolemManager();
41
  // compute what was proven
42
11692
  if (id == PfRule::EXISTS_INTRO)
43
  {
44
    Assert(children.size() == 1);
45
    Assert(args.size() == 1);
46
    Node p = children[0];
47
    Node exists = args[0];
48
    if (exists.getKind() != kind::EXISTS || exists[0].getNumChildren() != 1)
49
    {
50
      return Node::null();
51
    }
52
    std::unordered_map<Node, Node, NodeHashFunction> subs;
53
    if (!expr::match(exists[1], p, subs))
54
    {
55
      return Node::null();
56
    }
57
    // substitution must contain only the variable of the existential
58
    for (const std::pair<const Node, Node>& s : subs)
59
    {
60
      if (s.first != exists[0][0])
61
      {
62
        return Node::null();
63
      }
64
    }
65
    return exists;
66
  }
67
11692
  else if (id == PfRule::SKOLEM_INTRO)
68
  {
69
2633
    Assert(children.empty());
70
2633
    Assert(args.size() == 1);
71
5266
    Node t = SkolemManager::getOriginalForm(args[0]);
72
2633
    return args[0].eqNode(t);
73
  }
74
9059
  else if (id == PfRule::SKOLEMIZE)
75
  {
76
399
    Assert(children.size() == 1);
77
399
    Assert(args.empty());
78
    // can use either negated FORALL or EXISTS
79
798
    if (children[0].getKind() != EXISTS
80
798
        && (children[0].getKind() != NOT || children[0][0].getKind() != FORALL))
81
    {
82
      return Node::null();
83
    }
84
798
    Node exists;
85
399
    if (children[0].getKind() == EXISTS)
86
    {
87
60
      exists = children[0];
88
    }
89
    else
90
    {
91
678
      std::vector<Node> echildren(children[0][0].begin(), children[0][0].end());
92
339
      echildren[1] = echildren[1].notNode();
93
339
      exists = nm->mkNode(EXISTS, echildren);
94
    }
95
798
    std::vector<Node> skolems;
96
798
    Node res = sm->mkSkolemize(exists, skolems, "k");
97
399
    return res;
98
  }
99
8660
  else if (id == PfRule::INSTANTIATE)
100
  {
101
8660
    Assert(children.size() == 1);
102
17320
    if (children[0].getKind() != FORALL
103
17320
        || args.size() != children[0][0].getNumChildren())
104
    {
105
      return Node::null();
106
    }
107
17320
    Node body = children[0][1];
108
17320
    std::vector<Node> vars;
109
17320
    std::vector<Node> subs;
110
31160
    for (unsigned i = 0, nargs = args.size(); i < nargs; i++)
111
    {
112
22500
      vars.push_back(children[0][0][i]);
113
22500
      subs.push_back(args[i]);
114
    }
115
    Node inst =
116
17320
        body.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
117
8660
    return inst;
118
  }
119
120
  // no rule
121
  return Node::null();
122
}
123
124
}  // namespace quantifiers
125
}  // namespace theory
126
26685
}  // namespace CVC4