diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-10-02 09:06:02 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-02 09:06:02 -0500 |
| commit | 3051fd4ea618348da9a0b856b7bb07fcda027839 (patch) | |
| tree | ff7870f6eb4eb875da499bcb285007fdc33a9a74 /src/theory/arith/congruence_manager.h | |
| parent | d3fcaabbafdfebe17aa20f656ff2d3922d0dcb96 (diff) | |
Decouple modules from TheoryArithPrivate (#5184)
This decouples the arithmetic rewriter, the operator eliminator and the non-linear extension from TheoryArithPrivate and performs some minor cleanup.
This is in preparation for further refactoring of (lazy) arithmetic operator elimination.
Diffstat (limited to 'src/theory/arith/congruence_manager.h')
| -rw-r--r-- | src/theory/arith/congruence_manager.h | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h index 67df9237c..6115fec8a 100644 --- a/src/theory/arith/congruence_manager.h +++ b/src/theory/arith/congruence_manager.h @@ -38,11 +38,6 @@ namespace CVC4 { namespace theory { - -namespace quantifiers { -class EqualityInference; -} - namespace arith { class ArithCongruenceManager { |