summaryrefslogtreecommitdiff
path: root/src/parser
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2020-10-29 10:00:08 -0500
committerGitHub <noreply@github.com>2020-10-29 10:00:08 -0500
commit6898ab93a3858e78b20af38e537fe48ee9140c58 (patch)
treea2458fef28a0137110b4326fe7052701b56c9b8e /src/parser
parent0cebb4e9b2a5caa8fafa6ebd562a25aa18de9d43 (diff)
(proof-new) Update the strings inference manager for proofs (#5220)
This updates the inference manager in strings in two ways: (1) It now inherits from InferenceManagerBuffered, meaning that the custom methods for process the current pending lemma/fact vectors are removed in favor of the standard ones. (2) It has support for proof generation via the InferProofCons utility. This PR standardizes three methods processFact, processLemma, and processConflict which take InferInfo and processes any string-specific behavior pertaining to processing facts, lemmas and conflicts with the inference manager. These methods are intended to preserve the previous behavior of this class.
Diffstat (limited to 'src/parser')
0 files changed, 0 insertions, 0 deletions
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback