1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
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. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Builtin proof checker utility. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "cvc5_private.h" |
17 |
|
|
18 |
|
#ifndef CVC5__THEORY__BUILTIN__PROOF_CHECKER_H |
19 |
|
#define CVC5__THEORY__BUILTIN__PROOF_CHECKER_H |
20 |
|
|
21 |
|
#include "expr/node.h" |
22 |
|
#include "proof/method_id.h" |
23 |
|
#include "proof/proof_checker.h" |
24 |
|
#include "proof/proof_node.h" |
25 |
|
#include "theory/quantifiers/extended_rewrite.h" |
26 |
|
|
27 |
|
namespace cvc5 { |
28 |
|
|
29 |
|
class Env; |
30 |
|
|
31 |
|
namespace theory { |
32 |
|
namespace builtin { |
33 |
|
|
34 |
|
/** A checker for builtin proofs */ |
35 |
|
class BuiltinProofRuleChecker : public ProofRuleChecker |
36 |
|
{ |
37 |
|
public: |
38 |
|
/** Constructor. */ |
39 |
|
BuiltinProofRuleChecker(Env& env); |
40 |
|
/** Destructor. */ |
41 |
9923 |
~BuiltinProofRuleChecker() {} |
42 |
|
/** |
43 |
|
* Apply rewrite on n (in skolem form). This encapsulates the exact behavior |
44 |
|
* of a REWRITE step in a proof. |
45 |
|
* |
46 |
|
* @param n The node to rewrite, |
47 |
|
* @param idr The method identifier of the rewriter, by default RW_REWRITE |
48 |
|
* specifying a call to Rewriter::rewrite. |
49 |
|
* @return The rewritten form of n. |
50 |
|
*/ |
51 |
|
Node applyRewrite(TNode n, MethodId idr = MethodId::RW_REWRITE); |
52 |
|
/** |
53 |
|
* Get substitution for literal exp. Updates vars/subs to the substitution |
54 |
|
* specified by exp for the substitution method ids. |
55 |
|
*/ |
56 |
|
static bool getSubstitutionForLit(Node exp, |
57 |
|
TNode& var, |
58 |
|
TNode& subs, |
59 |
|
MethodId ids = MethodId::SB_DEFAULT); |
60 |
|
/** |
61 |
|
* Get substitution for formula exp. Adds to vars/subs to the substitution |
62 |
|
* specified by exp for the substitution method ids, which may be multiple |
63 |
|
* substitutions if exp is of kind AND and ids is SB_DEFAULT (note the other |
64 |
|
* substitution types always interpret applications of AND as a formula). |
65 |
|
* The vector "from" are the literals from exp that each substitution in |
66 |
|
* vars/subs are based on. For example, if exp is (and (= x t) (= y s)), then |
67 |
|
* vars = { x, y }, subs = { t, s }, from = { (= x y), (= y s) }. |
68 |
|
*/ |
69 |
|
static bool getSubstitutionFor(Node exp, |
70 |
|
std::vector<TNode>& vars, |
71 |
|
std::vector<TNode>& subs, |
72 |
|
std::vector<TNode>& from, |
73 |
|
MethodId ids = MethodId::SB_DEFAULT); |
74 |
|
|
75 |
|
/** |
76 |
|
* Apply substitution on n in skolem form. This encapsulates the exact |
77 |
|
* behavior of a SUBS step in a proof. |
78 |
|
* |
79 |
|
* @param n The node to substitute, |
80 |
|
* @param exp The (set of) equalities/literals/formulas that the substitution |
81 |
|
* is derived from |
82 |
|
* @param ids The method identifier of the substitution, by default SB_DEFAULT |
83 |
|
* specifying that lhs/rhs of equalities are interpreted as a substitution. |
84 |
|
* @param ida The method identifier of the substitution application, by |
85 |
|
* default SB_SEQUENTIAL specifying that substitutions are to be applied |
86 |
|
* sequentially |
87 |
|
* @return The substituted form of n. |
88 |
|
*/ |
89 |
|
static Node applySubstitution(Node n, |
90 |
|
Node exp, |
91 |
|
MethodId ids = MethodId::SB_DEFAULT, |
92 |
|
MethodId ida = MethodId::SBA_SEQUENTIAL); |
93 |
|
static Node applySubstitution(Node n, |
94 |
|
const std::vector<Node>& exp, |
95 |
|
MethodId ids = MethodId::SB_DEFAULT, |
96 |
|
MethodId ida = MethodId::SBA_SEQUENTIAL); |
97 |
|
/** Apply substitution + rewriting |
98 |
|
* |
99 |
|
* Combines the above two steps. |
100 |
|
* |
101 |
|
* @param n The node to substitute and rewrite, |
102 |
|
* @param exp The (set of) equalities corresponding to the substitution |
103 |
|
* @param ids The method identifier of the substitution. |
104 |
|
* @param ida The method identifier of the substitution application. |
105 |
|
* @param idr The method identifier of the rewriter. |
106 |
|
* @return The substituted, rewritten form of n. |
107 |
|
*/ |
108 |
|
Node applySubstitutionRewrite(Node n, |
109 |
|
const std::vector<Node>& exp, |
110 |
|
MethodId ids = MethodId::SB_DEFAULT, |
111 |
|
MethodId ida = MethodId::SBA_SEQUENTIAL, |
112 |
|
MethodId idr = MethodId::RW_REWRITE); |
113 |
|
|
114 |
|
/** get a TheoryId from a node, return false if we fail */ |
115 |
|
static bool getTheoryId(TNode n, TheoryId& tid); |
116 |
|
/** Make a TheoryId into a node */ |
117 |
|
static Node mkTheoryIdNode(TheoryId tid); |
118 |
|
|
119 |
|
/** Register all rules owned by this rule checker into pc. */ |
120 |
|
void registerTo(ProofChecker* pc) override; |
121 |
|
protected: |
122 |
|
/** Return the conclusion of the given proof step, or null if it is invalid */ |
123 |
|
Node checkInternal(PfRule id, |
124 |
|
const std::vector<Node>& children, |
125 |
|
const std::vector<Node>& args) override; |
126 |
|
|
127 |
|
/** extended rewriter object */ |
128 |
|
quantifiers::ExtendedRewriter d_ext_rewriter; |
129 |
|
|
130 |
|
private: |
131 |
|
/** Reference to the environment. */ |
132 |
|
Env& d_env; |
133 |
|
}; |
134 |
|
|
135 |
|
} // namespace builtin |
136 |
|
} // namespace theory |
137 |
|
} // namespace cvc5 |
138 |
|
|
139 |
|
#endif /* CVC5__THEORY__BUILTIN__PROOF_CHECKER_H */ |