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
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
|
/********************* */
/*! \file inference_manager.h
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2019 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 The inference manager for the theory of sets.
**/
#include "cvc4_private.h"
#ifndef CVC4__THEORY__SETS__INFERENCE_MANAGER_H
#define CVC4__THEORY__SETS__INFERENCE_MANAGER_H
#include "theory/sets/solver_state.h"
#include "theory/uf/equality_engine.h"
namespace CVC4 {
namespace theory {
namespace sets {
class TheorySetsPrivate;
/** Inference manager
*
* This class manages inferences produced by the theory of sets. It manages
* whether inferences are processed as external lemmas on the output channel
* of theory of sets or internally as literals asserted to the equality engine
* of theory of sets. The latter literals are referred to as "facts".
*/
class InferenceManager
{
typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
public:
InferenceManager(TheorySetsPrivate& p,
SolverState& s,
eq::EqualityEngine& e,
context::Context* c,
context::UserContext* u);
/** reset
*
* Called at the beginning of a full effort check. Resets the information
* related to this class regarding whether facts and lemmas have been
* processed.
*/
void reset();
/**
* Add facts corresponding to ( exp => fact ) via calls to the assertFact
* method of TheorySetsPrivate.
*
* The portions of fact that were unable to be processed as facts are added
* to the data member d_pendingLemmas.
*
* The argument inferType is used for overriding the policy on whether
* fact is processed as a lemma, where inferType=1 forces fact to be
* set as a lemma, and inferType=-1 forces fact to be processed as a fact
* (if possible).
*
* The argument c is the name of the inference, which is used for debugging.
*/
void assertInference(Node fact, Node exp, const char* c, int inferType = 0);
/** same as above, where exp is interpreted as a conjunction */
void assertInference(Node fact,
std::vector<Node>& exp,
const char* c,
int inferType = 0);
/** same as above, where conc is interpreted as a conjunction */
void assertInference(std::vector<Node>& conc,
Node exp,
const char* c,
int inferType = 0);
/** same as above, where both exp and conc are interpreted as conjunctions */
void assertInference(std::vector<Node>& conc,
std::vector<Node>& exp,
const char* c,
int inferType = 0);
/** Flush lemmas
*
* This sends lemmas on the output channel of the theory of sets.
*
* The argument preprocess indicates whether preprocessing should be applied
* (by TheoryEngine) on each of lemmas.
*/
void flushLemmas(std::vector<Node>& lemmas, bool preprocess = false);
/** singular version of above */
void flushLemma(Node lem, bool preprocess = false);
/** Do we have pending lemmas? */
bool hasPendingLemmas() const { return !d_pendingLemmas.empty(); }
/** Applies flushLemmas on d_pendingLemmas */
void flushPendingLemmas(bool preprocess = false);
/** flush the splitting lemma ( n OR (NOT n) )
*
* If reqPol is not 0, then a phase requirement for n is requested with
* polarity ( reqPol>0 ).
*/
void split(Node n, int reqPol = 0);
/** Have we sent a lemma during the current call to a full effort check? */
bool hasSentLemma() const;
/** Have we added a fact during the current call to a full effort check? */
bool hasAddedFact() const;
/** Have we processed an inference (fact, lemma, or conflict)? */
bool hasProcessed() const;
/** Have we sent lem as a lemma in the current user context? */
bool hasLemmaCached(Node lem) const;
private:
/** constants */
Node d_true;
Node d_false;
/** the theory of sets which owns this */
TheorySetsPrivate& d_parent;
/** Reference to the state object for the theory of sets */
SolverState& d_state;
/** Reference to the equality engine of theory of sets */
eq::EqualityEngine& d_ee;
/** pending lemmas */
std::vector<Node> d_pendingLemmas;
/** sent lemma
*
* This flag is set to true during a full effort check if this theory
* called d_out->lemma(...).
*/
bool d_sentLemma;
/** added fact
*
* This flag is set to true during a full effort check if this theory
* added an internal fact to its equality engine.
*/
bool d_addedFact;
/** A user-context-dependent cache of all lemmas produced */
NodeSet d_lemmas_produced;
/**
* A set of nodes to ref-count. Nodes that are facts or are explanations of
* facts must be added to this set since the equality engine does not
* ref count nodes.
*/
NodeSet d_keep;
/** Assert fact recursive
*
* This is a helper function for assertInference, which calls assertFact
* in theory of sets and adds to d_pendingLemmas based on fact.
* The argument inferType determines the policy on whether fact is processed
* as a fact or as a lemma (see assertInference above).
*/
bool assertFactRec(Node fact, Node exp, int inferType = 0);
};
} // namespace sets
} // namespace theory
} // namespace CVC4
#endif /* CVC4__THEORY__SETS__INFERENCE_MANAGER_H */
|
