projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a69b6eb) | patch
(proof-new) Add the strings proof constructor (#4903)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 7 Oct 2020 12:23:53 +0000 (07:23 -0500)
committerGitHub <noreply@github.com>
Wed, 7 Oct 2020 12:23:53 +0000 (07:23 -0500)
commit1a97c19443833604d57f1453a1bebfe0714d3d8e
tree18bb2f3a12f46de9920118713f973fc89860f126tree
parenta69b6eb561fadb4c2c9f09b700950af7ce43b378commit | diff
(proof-new) Add the strings proof constructor (#4903)

This is the method for converting strings InferInfo into instructions for building ProofNode. Notice that this is done as a standalone module, and thus the theory of strings uses Inferences only, not PfRule.

The next step will be to integrate this utility into InferenceManager.
src/CMakeLists.txt diff | blob | history
src/theory/strings/infer_info.h diff | blob | history
src/theory/strings/infer_proof_cons.cpp [new file with mode: 0644] blob
src/theory/strings/infer_proof_cons.h [new file with mode: 0644] blob
src/theory/strings/sequences_stats.cpp diff | blob | history
src/theory/strings/sequences_stats.h diff | blob | history