1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
|
/******************************************************************************
* Top contributors (to current version):
* Aina Niemetz, Andrew Reynolds, Mathias Preiner
*
* This file is part of the cvc5 project.
*
* Copyright (c) 2009-2021 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.
* ****************************************************************************
*
* The preprocessing pass context for passes
*
* Implementation of the preprocessing pass context for passes. This context
* allows preprocessing passes to retrieve information besides the assertions
* from the solver and interact with it without getting full access.
*/
#include "cvc5_private.h"
#ifndef CVC5__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H
#define CVC5__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H
#include "context/cdhashset.h"
#include "smt/smt_engine.h"
#include "theory/trust_substitutions.h"
#include "util/resource_manager.h"
namespace cvc5 {
class SmtEngine;
class TheoryEngine;
namespace theory::booleans {
class CircuitPropagator;
}
namespace prop {
class PropEngine;
}
namespace preprocessing {
class PreprocessingPassContext
{
public:
PreprocessingPassContext(
SmtEngine* smt,
theory::booleans::CircuitPropagator* circuitPropagator,
ProofNodeManager* pnm);
SmtEngine* getSmt() { return d_smt; }
TheoryEngine* getTheoryEngine() { return d_smt->getTheoryEngine(); }
prop::PropEngine* getPropEngine() { return d_smt->getPropEngine(); }
context::Context* getUserContext() { return d_smt->getUserContext(); }
context::Context* getDecisionContext() { return d_smt->getContext(); }
theory::booleans::CircuitPropagator* getCircuitPropagator()
{
return d_circuitPropagator;
}
context::CDHashSet<Node, NodeHashFunction>& getSymsInAssertions()
{
return d_symsInAssertions;
}
void spendResource(Resource r)
{
d_resourceManager->spendResource(r);
}
/** Get the current logic info of the SmtEngine */
const LogicInfo& getLogicInfo() { return d_smt->getLogicInfo(); }
/** Gets a reference to the top-level substitution map */
theory::TrustSubstitutionMap& getTopLevelSubstitutions();
/** Record symbols in assertions
*
* This method is called when a set of assertions is finalized. It adds
* the symbols to d_symsInAssertions that occur in assertions.
*/
void recordSymbolsInAssertions(const std::vector<Node>& assertions);
/**
* Add substitution to theory model. This method should only be called if
* we have already added the substitution to the top-level substitutions
* class. Otherwise, addSubstitution should be called instead.
* @param lhs The node replaced by node 'rhs'
* @param rhs The node to substitute node 'lhs'
*/
void addModelSubstitution(const Node& lhs, const Node& rhs);
/**
* Add substitution to the top-level substitutions and to the theory model.
* @param lhs The node replaced by node 'rhs'
* @param rhs The node to substitute node 'lhs'
* @param pg The proof generator that can provide a proof of lhs == rhs.
*/
void addSubstitution(const Node& lhs,
const Node& rhs,
ProofGenerator* pg = nullptr);
/** The the proof node manager associated with this context, if it exists */
ProofNodeManager* getProofNodeManager();
private:
/** Pointer to the SmtEngine that this context was created in. */
SmtEngine* d_smt;
/** Pointer to the ResourceManager for this context. */
ResourceManager* d_resourceManager;
/* The top level substitutions */
theory::TrustSubstitutionMap d_topLevelSubstitutions;
/** Instance of the circuit propagator */
theory::booleans::CircuitPropagator* d_circuitPropagator;
/** Pointer to the proof node manager, if it exists */
ProofNodeManager* d_pnm;
/**
* The (user-context-dependent) set of symbols that occur in at least one
* assertion in the current user context.
*/
context::CDHashSet<Node, NodeHashFunction> d_symsInAssertions;
}; // class PreprocessingPassContext
} // namespace preprocessing
} // namespace cvc5
#endif /* CVC5__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H */
|
