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
|
/********************* */
/*! \file inference_manager.h
** \verbatim
** Top contributors (to current version):
** Gereon Kremer
** 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 Customized inference manager for the theory of nonlinear arithmetic
**/
#include "cvc4_private.h"
#ifndef CVC4__THEORY__ARITH__INFERENCE_MANAGER_H
#define CVC4__THEORY__ARITH__INFERENCE_MANAGER_H
#include <map>
#include <vector>
#include "theory/arith/arith_state.h"
#include "theory/inference_id.h"
#include "theory/arith/nl/nl_lemma_utils.h"
#include "theory/inference_manager_buffered.h"
namespace CVC4 {
namespace theory {
namespace arith {
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, NodeHashFunction>;
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;
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;
};
} // namespace arith
} // namespace theory
} // namespace CVC4
#endif
|
