GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/builtin/proof_checker.h Lines: 2 2 100.0 %
Date: 2021-03-23 Branches: 1 2 50.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file proof_checker.h
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 Equality proof checker utility
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__BUILTIN__PROOF_CHECKER_H
18
#define CVC4__THEORY__BUILTIN__PROOF_CHECKER_H
19
20
#include "expr/node.h"
21
#include "expr/proof_checker.h"
22
#include "expr/proof_node.h"
23
#include "theory/quantifiers/extended_rewrite.h"
24
25
namespace CVC4 {
26
namespace theory {
27
28
/**
29
 * Identifiers for rewriters and substitutions, which we abstractly
30
 * classify as "methods".  Methods have a unique identifier in the internal
31
 * proof calculus implemented by the checker below.
32
 *
33
 * A "rewriter" is abstractly a method from Node to Node, where the output
34
 * is semantically equivalent to the input. The identifiers below list
35
 * various methods that have this contract. This identifier is used
36
 * in a number of the builtin rules.
37
 *
38
 * A substitution is a method for turning a formula into a substitution.
39
 */
40
enum class MethodId : uint32_t
41
{
42
  //---------------------------- Rewriters
43
  // Rewriter::rewrite(n)
44
  RW_REWRITE,
45
  // d_ext_rew.extendedRewrite(n);
46
  RW_EXT_REWRITE,
47
  // Rewriter::rewriteExtEquality(n)
48
  RW_REWRITE_EQ_EXT,
49
  // Evaluator::evaluate(n)
50
  RW_EVALUATE,
51
  // identity
52
  RW_IDENTITY,
53
  // theory preRewrite, note this is only intended to be used as an argument
54
  // to THEORY_REWRITE in the final proof. It is not implemented in
55
  // applyRewrite below, see documentation in proof_rule.h for THEORY_REWRITE.
56
  RW_REWRITE_THEORY_PRE,
57
  // same as above, for theory postRewrite
58
  RW_REWRITE_THEORY_POST,
59
  //---------------------------- Substitutions
60
  // (= x y) is interpreted as x -> y, using Node::substitute
61
  SB_DEFAULT,
62
  // P, (not P) are interpreted as P -> true, P -> false using Node::substitute
63
  SB_LITERAL,
64
  // P is interpreted as P -> true using Node::substitute
65
  SB_FORMULA,
66
};
67
/** Converts a rewriter id to a string. */
68
const char* toString(MethodId id);
69
/** Write a rewriter id to out */
70
std::ostream& operator<<(std::ostream& out, MethodId id);
71
/** Make a method id node */
72
Node mkMethodId(MethodId id);
73
74
namespace builtin {
75
76
/** A checker for builtin proofs */
77
class BuiltinProofRuleChecker : public ProofRuleChecker
78
{
79
 public:
80
8997
  BuiltinProofRuleChecker() {}
81
8994
  ~BuiltinProofRuleChecker() {}
82
  /**
83
   * Apply rewrite on n (in skolem form). This encapsulates the exact behavior
84
   * of a REWRITE step in a proof.
85
   *
86
   * @param n The node to rewrite,
87
   * @param idr The method identifier of the rewriter, by default RW_REWRITE
88
   * specifying a call to Rewriter::rewrite.
89
   * @return The rewritten form of n.
90
   */
91
  Node applyRewrite(Node n, MethodId idr = MethodId::RW_REWRITE);
92
  /**
93
   * Get substitution for literal exp. Updates vars/subs to the substitution
94
   * specified by exp for the substitution method ids.
95
   */
96
  static bool getSubstitutionForLit(Node exp,
97
                                    TNode& var,
98
                                    TNode& subs,
99
                                    MethodId ids = MethodId::SB_DEFAULT);
100
  /**
101
   * Get substitution for formula exp. Adds to vars/subs to the substitution
102
   * specified by exp for the substitution method ids, which may be multiple
103
   * substitutions if exp is of kind AND and ids is SB_DEFAULT (note the other
104
   * substitution types always interpret applications of AND as a formula).
105
   * The vector "from" are the literals from exp that each substitution in
106
   * vars/subs are based on. For example, if exp is (and (= x t) (= y s)), then
107
   * vars = { x, y }, subs = { t, s }, from = { (= x y), (= y s) }.
108
   */
109
  static bool getSubstitutionFor(Node exp,
110
                                 std::vector<TNode>& vars,
111
                                 std::vector<TNode>& subs,
112
                                 std::vector<TNode>& from,
113
                                 MethodId ids = MethodId::SB_DEFAULT);
114
115
  /**
116
   * Apply substitution on n in skolem form. This encapsulates the exact
117
   * behavior of a SUBS step in a proof.
118
   *
119
   * @param n The node to substitute,
120
   * @param exp The (set of) equalities/literals/formulas that the substitution
121
   * is derived from
122
   * @param ids The method identifier of the substitution, by default SB_DEFAULT
123
   * specifying that lhs/rhs of equalities are interpreted as a substitution.
124
   * @return The substituted form of n.
125
   */
126
  static Node applySubstitution(Node n,
127
                                Node exp,
128
                                MethodId ids = MethodId::SB_DEFAULT);
129
  static Node applySubstitution(Node n,
130
                                const std::vector<Node>& exp,
131
                                MethodId ids = MethodId::SB_DEFAULT);
132
  /** Apply substitution + rewriting
133
   *
134
   * Combines the above two steps.
135
   *
136
   * @param n The node to substitute and rewrite,
137
   * @param exp The (set of) equalities corresponding to the substitution
138
   * @param ids The method identifier of the substitution.
139
   * @param idr The method identifier of the rewriter.
140
   * @return The substituted, rewritten form of n.
141
   */
142
  Node applySubstitutionRewrite(Node n,
143
                                const std::vector<Node>& exp,
144
                                MethodId ids = MethodId::SB_DEFAULT,
145
                                MethodId idr = MethodId::RW_REWRITE);
146
  /** get a method identifier from a node, return false if we fail */
147
  static bool getMethodId(TNode n, MethodId& i);
148
  /**
149
   * Get method identifiers from args starting at the given index. Store their
150
   * values into ids, idr. This method returns false if args does not contain
151
   * valid method identifiers at position index in args.
152
   */
153
  bool getMethodIds(const std::vector<Node>& args,
154
                    MethodId& ids,
155
                    MethodId& idr,
156
                    size_t index);
157
  /**
158
   * Add method identifiers ids and idr as nodes to args. This does not add ids
159
   * or idr if their values are the default ones.
160
   */
161
  static void addMethodIds(std::vector<Node>& args, MethodId ids, MethodId idr);
162
163
  /** get a TheoryId from a node, return false if we fail */
164
  static bool getTheoryId(TNode n, TheoryId& tid);
165
  /** Make a TheoryId into a node */
166
  static Node mkTheoryIdNode(TheoryId tid);
167
168
  /** Register all rules owned by this rule checker into pc. */
169
  void registerTo(ProofChecker* pc) override;
170
 protected:
171
  /** Return the conclusion of the given proof step, or null if it is invalid */
172
  Node checkInternal(PfRule id,
173
                     const std::vector<Node>& children,
174
                     const std::vector<Node>& args) override;
175
176
  /** extended rewriter object */
177
  quantifiers::ExtendedRewriter d_ext_rewriter;
178
};
179
180
}  // namespace builtin
181
}  // namespace theory
182
}  // namespace CVC4
183
184
#endif /* CVC4__THEORY__BUILTIN__PROOF_CHECKER_H */