1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Gereon Kremer, Andrew Reynolds |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS |
8 |
|
* in the top-level source directory and their institutional affiliations. |
9 |
|
* All rights reserved. See the file COPYING in the top-level source |
10 |
|
* directory for licensing information. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Proof set utility. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "cvc5_private.h" |
17 |
|
|
18 |
|
#ifndef CVC5__EXPR__PROOF_SET_H |
19 |
|
#define CVC5__EXPR__PROOF_SET_H |
20 |
|
|
21 |
|
#include <memory> |
22 |
|
|
23 |
|
#include "context/cdlist.h" |
24 |
|
#include "context/context.h" |
25 |
|
#include "expr/proof_node_manager.h" |
26 |
|
|
27 |
|
namespace cvc5 { |
28 |
|
|
29 |
|
/** |
30 |
|
* A (context-dependent) set of proofs, which is used for memory |
31 |
|
* management purposes. |
32 |
|
*/ |
33 |
|
template <typename T> |
34 |
15939 |
class CDProofSet |
35 |
|
{ |
36 |
|
public: |
37 |
15939 |
CDProofSet(ProofNodeManager* pnm, |
38 |
|
context::Context* c, |
39 |
|
std::string namePrefix = "Proof") |
40 |
15939 |
: d_pnm(pnm), d_proofs(c), d_namePrefix(namePrefix) |
41 |
|
{ |
42 |
15939 |
} |
43 |
|
/** |
44 |
|
* Allocate a new proof. |
45 |
|
* |
46 |
|
* This returns a fresh proof object that remains alive in the context given |
47 |
|
* to this class. Internally, this adds a new proof of type T to a |
48 |
|
* context-dependent list of proofs and passes the following arguments to the |
49 |
|
* T constructor: |
50 |
|
* pnm, args..., name |
51 |
|
* where pnm is the proof node manager |
52 |
|
* provided to this proof set upon construction, args... are the arguments to |
53 |
|
* allocateProof() and name is the namePrefix with an appended index. |
54 |
|
*/ |
55 |
|
template <typename... Args> |
56 |
3726 |
T* allocateProof(Args&&... args) |
57 |
|
{ |
58 |
3726 |
d_proofs.push_back(std::make_shared<T>( |
59 |
|
d_pnm, |
60 |
|
std::forward<Args>(args)..., |
61 |
|
d_namePrefix + "_" + std::to_string(d_proofs.size()))); |
62 |
3726 |
return d_proofs.back().get(); |
63 |
|
} |
64 |
|
|
65 |
|
protected: |
66 |
|
/** The proof node manager */ |
67 |
|
ProofNodeManager* d_pnm; |
68 |
|
/** A context-dependent list of lazy proofs. */ |
69 |
|
context::CDList<std::shared_ptr<T>> d_proofs; |
70 |
|
/** The name prefix of the lazy proofs */ |
71 |
|
std::string d_namePrefix; |
72 |
|
}; |
73 |
|
|
74 |
|
} // namespace cvc5 |
75 |
|
|
76 |
|
#endif /* CVC5__EXPR__LAZY_PROOF_SET_H */ |