projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f980e08) | patch
(proof-new) Add datatypes inference to proof constructor (#5408)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 12 Nov 2020 14:36:28 +0000 (08:36 -0600)
committerGitHub <noreply@github.com>
Thu, 12 Nov 2020 14:36:28 +0000 (08:36 -0600)
commit70c0635bf490d237088b6675254408d965468272
tree1a57b9102ac9772663e2454040ef13a3351d6c4btree
parentf980e08b00ca9691f1f566455db446786994601bcommit | diff
(proof-new) Add datatypes inference to proof constructor (#5408)

This adds the module that constructs proofs from inference steps.

A followup PR will integrate proof support into the datatypes inference manager.
src/theory/datatypes/infer_proof_cons.cpp [new file with mode: 0644] blob
src/theory/datatypes/infer_proof_cons.h [new file with mode: 0644] blob