diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-03-21 08:12:11 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-21 13:12:11 +0000 |
| commit | 09097cd3b9cd3233b938ace34f3513a16ac17f80 (patch) | |
| tree | b889e15b487582e810db61b64dade7e6a14d225b /src/theory/arith | |
| parent | 02dd48563db0c5effd608eda70d4c262309322a6 (diff) | |
Clean up remaining raw uses of output channel (#6161)
After this PR, with only a few exceptions, all calls to output channel for lemmas, conflicts are made through inference manager.
This is work towards standardizing the statistics for theories.
Diffstat (limited to 'src/theory/arith')
| -rw-r--r-- | src/theory/arith/nl/nonlinear_extension.h | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h index 09e3a8370..820c317c5 100644 --- a/src/theory/arith/nl/nonlinear_extension.h +++ b/src/theory/arith/nl/nonlinear_extension.h @@ -74,9 +74,9 @@ class NlLemma; * which is called by TheoryArithPrivate either: * (1) at full effort with no conflicts or lemmas emitted, or * (2) at last call effort. - * In this method, this class calls d_out->lemma(...) + * In this method, this class calls d_im.lemma(...) * for valid arithmetic theory lemmas, based on the current set of assertions, - * where d_out is the output channel of TheoryArith. + * where d_im is the inference manager of TheoryArith. */ class NonlinearExtension { @@ -94,8 +94,8 @@ class NonlinearExtension void preRegisterTerm(TNode n); /** Check at effort level e. * - * This call may result in (possibly multiple) calls to d_out->lemma(...) - * where d_out is the output channel of TheoryArith. + * This call may result in (possibly multiple) calls to d_im.lemma(...) + * where d_im is the inference manager of TheoryArith. * * If e is FULL, then we add lemmas based on context-depedent * simplification (see Reynolds et al FroCoS 2017). |