diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2020-09-01 19:08:23 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-01 19:08:23 -0300 |
| commit | 8ad308b23c705e73507a42d2425289e999d47f86 (patch) | |
| tree | 29e3ac78844bc57171e0d122d758a8371a292a93 /src/util | |
| parent | 62ec0666dd4d409ee85603ae94d7ab1a2b4c9dcc (diff) | |
Removes old proof code (#4964)
This deletes much of the old proof code. Basically everything but the minimal necessary infra-structure for producing unsat cores. That includes dependency tracking in preprocessing, the prop engine proof and the unsat core computation code in the old proof manager. These should also go once we fully integrate into master the new proof infrastructure.
It also cleans interfaces that were using old-proof-code-specific constructs (such as LemmaProofRecipe). When possible or when it made sense standalone local proof production code was kept, but deactivated (such is in the equality engine and in the arithmetic solver).
Diffstat (limited to 'src/util')
| -rw-r--r-- | src/util/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | src/util/proof.h | 44 |
2 files changed, 0 insertions, 45 deletions
diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index 09bbfc518..0977714c2 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -26,7 +26,6 @@ libcvc4_add_sources( ostream_util.h poly_util.cpp poly_util.h - proof.h random.cpp random.h resource_manager.cpp diff --git a/src/util/proof.h b/src/util/proof.h deleted file mode 100644 index c89a3b0a6..000000000 --- a/src/util/proof.h +++ /dev/null @@ -1,44 +0,0 @@ -/********************* */ -/*! \file proof.h - ** \verbatim - ** Top contributors (to current version): - ** Tim King, Morgan Deters, Mathias Preiner - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "cvc4_public.h" - -#ifndef CVC4__PROOF_H -#define CVC4__PROOF_H - -#include <iosfwd> -#include <unordered_map> - -namespace CVC4 { - -class Expr; -class ProofLetCount; -struct ExprHashFunction; - -typedef std::unordered_map<Expr, ProofLetCount, ExprHashFunction> ProofLetMap; - -class CVC4_PUBLIC Proof -{ - public: - virtual ~Proof() {} - virtual void toStream(std::ostream& out) const = 0; - virtual void toStream(std::ostream& out, const ProofLetMap& map) const = 0; -};/* class Proof */ - -}/* CVC4 namespace */ - -#endif /* CVC4__PROOF_H */ |