diff options
Diffstat (limited to 'src/theory/builtin/proof_checker.h')
| -rw-r--r-- | src/theory/builtin/proof_checker.h | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/theory/builtin/proof_checker.h b/src/theory/builtin/proof_checker.h index 6dc7023d5..7e46587b7 100644 --- a/src/theory/builtin/proof_checker.h +++ b/src/theory/builtin/proof_checker.h @@ -77,6 +77,17 @@ class BuiltinProofRuleChecker : public ProofRuleChecker */ static Node applyRewrite(Node n, MethodId idr = MethodId::RW_REWRITE); /** + * Apply small-step rewrite on n in skolem form (either pre- or + * post-rewrite). This encapsulates the exact behavior of a THEORY_REWRITE + * step in a proof. + * + * @param n The node to rewrite + * @param preRewrite If true, performs a pre-rewrite or a post-rewrite + * otherwise + * @return The rewritten form of n + */ + static Node applyTheoryRewrite(Node n, bool preRewrite); + /** * Get substitution. Updates vars/subs to the substitution specified by * exp (e.g. as an equality) for the substitution method ids. */ |