1 /******************************************************************************
2 * Top contributors (to current version):
5 * This file is part of the cvc5 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.
11 * ****************************************************************************
13 * Builtin proof checker utility.
16 #include "cvc5_private.h"
18 #ifndef CVC5__THEORY__BUILTIN__PROOF_CHECKER_H
19 #define CVC5__THEORY__BUILTIN__PROOF_CHECKER_H
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"
34 /** A checker for builtin proofs */
35 class BuiltinProofRuleChecker
: public ProofRuleChecker
39 BuiltinProofRuleChecker(Env
& env
);
41 ~BuiltinProofRuleChecker() {}
43 * Apply rewrite on n (in skolem form). This encapsulates the exact behavior
44 * of a REWRITE step in a proof.
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.
51 Node
applyRewrite(TNode n
, MethodId idr
= MethodId::RW_REWRITE
);
53 * Get substitution for literal exp. Updates vars/subs to the substitution
54 * specified by exp for the substitution method ids.
56 static bool getSubstitutionForLit(Node exp
,
59 MethodId ids
= MethodId::SB_DEFAULT
);
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) }.
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
);
76 * Apply substitution on n in skolem form. This encapsulates the exact
77 * behavior of a SUBS step in a proof.
79 * @param n The node to substitute,
80 * @param exp The (set of) equalities/literals/formulas that the substitution
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
87 * @return The substituted form of n.
89 static Node
applySubstitution(Node n
,
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
99 * Combines the above two steps.
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.
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
);
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
);
119 /** Register all rules owned by this rule checker into pc. */
120 void registerTo(ProofChecker
* pc
) override
;
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
;
127 /** extended rewriter object */
128 quantifiers::ExtendedRewriter d_ext_rewriter
;
131 /** Reference to the environment. */
135 } // namespace builtin
136 } // namespace theory
139 #endif /* CVC5__THEORY__BUILTIN__PROOF_CHECKER_H */