diff options
Diffstat (limited to 'src/theory/arith/inference_manager.h')
| -rw-r--r-- | src/theory/arith/inference_manager.h | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/arith/inference_manager.h b/src/theory/arith/inference_manager.h index 1c0678e60..33e4f424b 100644 --- a/src/theory/arith/inference_manager.h +++ b/src/theory/arith/inference_manager.h @@ -22,7 +22,7 @@ #include "theory/arith/arith_lemma.h" #include "theory/arith/arith_state.h" -#include "theory/arith/nl/inference.h" +#include "theory/arith/inference_id.h" #include "theory/arith/nl/nl_lemma_utils.h" #include "theory/inference_manager_buffered.h" @@ -69,7 +69,7 @@ class InferenceManager : public InferenceManagerBuffered * added as pending lemma when calling flushWaitingLemmas. */ void addPendingArithLemma(const Node& lemma, - nl::Inference inftype, + InferenceId inftype, bool isWaiting = false); /** @@ -79,7 +79,7 @@ class InferenceManager : public InferenceManagerBuffered void flushWaitingLemmas(); /** Add a conflict to the this inference manager. */ - void addConflict(const Node& conf, nl::Inference inftype); + void addConflict(const Node& conf, InferenceId inftype); /** Returns the number of pending lemmas. */ std::size_t numWaitingLemmas() const; |