From 356647c4b7eb2420f6c6b350f0622bb4c863b0a5 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 10 Jun 2020 16:52:46 -0500 Subject: (proof-new) Theory proof step buffer utility (#4580) This is a common class for adding steps for theory-specific proof rules into a ProofStepBuffer. --- src/CMakeLists.txt | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'src/CMakeLists.txt') diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 1820fbb5d..0ed3934a7 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -643,7 +643,6 @@ libcvc4_add_sources( theory/rewriter.h theory/rewriter_attributes.h theory/sep/theory_sep.cpp - theory/theory_rewriter.h theory/sep/theory_sep.h theory/sep/theory_sep_rewriter.cpp theory/sep/theory_sep_rewriter.h @@ -744,6 +743,9 @@ libcvc4_add_sources( theory/theory_model.h theory/theory_model_builder.cpp theory/theory_model_builder.h + theory/theory_proof_step_buffer.cpp + theory/theory_proof_step_buffer.h + theory/theory_rewriter.h theory/theory_registrar.h theory/theory_test_utils.h theory/trust_node.cpp -- cgit v1.2.3