diff options
Diffstat (limited to 'src/theory/arith/nl/nonlinear_extension.h')
| -rw-r--r-- | src/theory/arith/nl/nonlinear_extension.h | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h index fba9e8e87..6a38021a0 100644 --- a/src/theory/arith/nl/nonlinear_extension.h +++ b/src/theory/arith/nl/nonlinear_extension.h @@ -21,10 +21,7 @@ #include <map> #include <vector> -#include "context/cdlist.h" -#include "expr/kind.h" #include "expr/node.h" -#include "theory/arith/inference_manager.h" #include "theory/arith/nl/cad_solver.h" #include "theory/arith/nl/ext/factoring_check.h" #include "theory/arith/nl/ext/monomial_bounds_check.h" @@ -35,19 +32,25 @@ #include "theory/arith/nl/ext_theory_callback.h" #include "theory/arith/nl/iand_solver.h" #include "theory/arith/nl/icp/icp_solver.h" -#include "theory/arith/nl/nl_lemma_utils.h" #include "theory/arith/nl/nl_model.h" #include "theory/arith/nl/stats.h" #include "theory/arith/nl/strategy.h" #include "theory/arith/nl/transcendental/transcendental_solver.h" #include "theory/ext_theory.h" -#include "theory/uf/equality_engine.h" namespace CVC4 { namespace theory { +namespace eq { + class EqualityEngine; +} namespace arith { + +class InferenceManager; + namespace nl { +class NlLemma; + /** Non-linear extension class * * This class implements model-based refinement schemes |