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
|
/******************************************************************************
* Top contributors (to current version):
* Gereon Kremer, Makai Mann
*
* 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.
* ****************************************************************************
*
* Customized inference manager for the theory of nonlinear arithmetic.
*/
#include "cvc5_private.h"
#ifndef CVC5__THEORY__ARITH__INFERENCE_MANAGER_H
#define CVC5__THEORY__ARITH__INFERENCE_MANAGER_H
#include <vector>
#include "theory/inference_id.h"
#include "theory/inference_manager_buffered.h"
namespace cvc5 {
namespace theory {
namespace arith {
class ArithState;
class TheoryArith;
/**
* A specialized variant of the InferenceManagerBuffered, tailored to the
* arithmetic theory.
*
* It adds some convenience methods to send ArithLemma and adds a mechanism for
* waiting lemmas that can be flushed into the pending lemmas of this
* buffered inference manager.
* It also extends the caching mechanism of TheoryInferenceManager to cache
* preprocessing lemmas and non-preprocessing lemmas separately. For the former,
* it uses the cache provided by the TheoryInferenceManager base class.
*/
class InferenceManager : public InferenceManagerBuffered
{
using NodeSet = context::CDHashSet<Node>;
public:
InferenceManager(TheoryArith& ta, ArithState& astate, ProofNodeManager* pnm);
/**
* Add a lemma as pending lemma to this inference manager.
* If isWaiting is true, the lemma is first stored as waiting lemma and only
* added as pending lemma when calling flushWaitingLemmas.
*/
void addPendingLemma(std::unique_ptr<SimpleTheoryLemma> lemma,
bool isWaiting = false);
/**
* Add a lemma as pending lemma to this inference manager.
* If isWaiting is true, the lemma is first stored as waiting lemma and only
* added as pending lemma when calling flushWaitingLemmas.
*/
void addPendingLemma(const SimpleTheoryLemma& lemma, bool isWaiting = false);
/**
* Add a lemma as pending lemma to this inference manager.
* If isWaiting is true, the lemma is first stored as waiting lemma and only
* added as pending lemma when calling flushWaitingLemmas.
*/
void addPendingLemma(const Node& lemma,
InferenceId inftype,
ProofGenerator* pg = nullptr,
bool isWaiting = false,
LemmaProperty p = LemmaProperty::NONE);
/**
* Flush all waiting lemmas to this inference manager (as pending
* lemmas). To actually send them, call doPendingLemmas() afterwards.
*/
void flushWaitingLemmas();
/**
* Removes all waiting lemmas without sending them anywhere.
*/
void clearWaitingLemmas();
/**
* Checks whether we have made any progress, that is whether a conflict,
* lemma or fact was added or whether a lemma or fact is pending.
*/
bool hasUsed() const;
/** Checks whether we have waiting lemmas. */
bool hasWaitingLemma() const;
/** Returns the number of pending lemmas. */
std::size_t numWaitingLemmas() const;
/** Checks whether the given lemma is already present in the cache. */
virtual bool hasCachedLemma(TNode lem, LemmaProperty p) override;
/** overrides propagateLit to track which literals have been propagated */
bool propagateLit(TNode lit) override;
/**
* Return true if we have propagated lit already. This call is only valid if
* d_trackPropLits is true.
*/
bool hasPropagated(TNode lit) const;
protected:
/**
* Adds the given lemma to the cache. Returns true if it has not been in the
* cache yet.
*/
virtual bool cacheLemma(TNode lem, LemmaProperty p) override;
private:
/**
* Checks whether the lemma is entailed to be false. In this case, it is a
* conflict.
*/
bool isEntailedFalse(const SimpleTheoryLemma& lem);
/** The waiting lemmas. */
std::vector<std::unique_ptr<SimpleTheoryLemma>> d_waitingLem;
/** Whether we are tracking the set of propagated literals */
bool d_trackPropLits;
/** The literals we have propagated */
NodeSet d_propLits;
};
} // namespace arith
} // namespace theory
} // namespace cvc5
#endif
|
