diff options
Diffstat (limited to 'src/theory/arith/nl/cad_solver.h')
| -rw-r--r-- | src/theory/arith/nl/cad_solver.h | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/src/theory/arith/nl/cad_solver.h b/src/theory/arith/nl/cad_solver.h index 21fbbab2e..b67d78f0d 100644 --- a/src/theory/arith/nl/cad_solver.h +++ b/src/theory/arith/nl/cad_solver.h @@ -17,17 +17,22 @@ #include <vector> +#include "context/context.h" #include "expr/node.h" -#include "theory/arith/inference_manager.h" #include "theory/arith/nl/cad/cdcac.h" #include "theory/arith/nl/cad/proof_checker.h" -#include "theory/arith/nl/nl_model.h" +#include "util/real_algebraic_number.h" namespace CVC4 { namespace theory { namespace arith { + +class InferenceManager; + namespace nl { +class NlModel; + /** * A solver for nonlinear arithmetic that implements the CAD-based method * described in https://arxiv.org/pdf/2003.05633.pdf. |