diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-04-16 16:00:25 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-04-16 16:00:25 -0500 |
commit | 51a6be99deb292161b0469b70b4d8410bd7a975f (patch) | |
tree | 3675d28a6a7f44016f14679e274381f97780e517 /src/expr/CMakeLists.txt | |
parent | f0e6c103304fc5c00c9bdfb699ad878ead5c66ed (diff) |
Add ProofNodeManager and ProofChecker (#4317)
Further work on adding core utilities for ProofNode objects, in support of the new proof infrastructure.
ProofNodeManager is analogous to NodeManager. It is a trusted way of generating only "well-formed" ProofNode pointers (according to a checker).
ProofChecker is analogous to TypeChecker. It is intended to be infrastructure for our internal proof checker.
This PR (and 1 more) is required to get to a place where Haniel and I can collaborate on further development for proofs.
Diffstat (limited to 'src/expr/CMakeLists.txt')
-rw-r--r-- | src/expr/CMakeLists.txt | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index aa928fdb7..f21241ef5 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -33,8 +33,12 @@ libcvc4_add_sources( node_value.cpp node_value.h node_visitor.h + proof_checker.cpp + proof_checker.h proof_node.cpp proof_node.h + proof_node_manager.cpp + proof_node_manager.h proof_rule.cpp proof_rule.h symbol_table.cpp |