diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2020-09-04 16:59:49 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-04 09:59:49 -0500 |
| commit | 0d0c1cdbce4fb46ad5c7d4bc620b712ea014722e (patch) | |
| tree | 5fa7c5d06cbf0a67541c5bdbc82bf692f5d1dd48 /src/theory/arith/inference_manager.cpp | |
| parent | bfb744af4f932f095640d97be8f0bfa9ff60e981 (diff) | |
Use arith::InferenceManager for CAD lemmas (#5015)
This makes the CAD solver use the new arith::InferenceManager instead of the previously used lemma collection scheme.
Diffstat (limited to 'src/theory/arith/inference_manager.cpp')
| -rw-r--r-- | src/theory/arith/inference_manager.cpp | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/theory/arith/inference_manager.cpp b/src/theory/arith/inference_manager.cpp index d03d2ba37..d4c5d17c5 100644 --- a/src/theory/arith/inference_manager.cpp +++ b/src/theory/arith/inference_manager.cpp @@ -87,6 +87,11 @@ void InferenceManager::addConflict(const Node& conf, InferenceId inftype) conflict(Rewriter::rewrite(conf)); } +bool InferenceManager::hasUsed() const +{ + return hasSent() || hasPending(); +} + std::size_t InferenceManager::numWaitingLemmas() const { return d_waitingLem.size(); |