Split NlSolver in multiple subsolvers (#5315)

The NlSolver started as one place for nonlinear reasoning, but has grown significantly since. This PR splits the NlSolver class into multiple smaller classes.

1 files changed, 0 insertions, 88 deletions

diff --git a/src/theory/arith/nl/nl_constraint.h b/src/theory/arith/nl/nl_constraint.h
deleted file mode 100644
index b126eeb64..000000000
--- a/src/theory/arith/nl/nl_constraint.h
+++ /dev/null
@@ -1,88 +0,0 @@
-/*********************                                                        */
-/*! \file nl_constraint.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Utilities for non-linear constraints
- **/
-
-#ifndef CVC4__THEORY__ARITH__NL__NL_CONSTRAINT_H
-#define CVC4__THEORY__ARITH__NL__NL_CONSTRAINT_H
-
-#include <map>
-#include <vector>
-
-#include "expr/kind.h"
-#include "expr/node.h"
-#include "theory/arith/nl/nl_monomial.h"
-
-namespace CVC4 {
-namespace theory {
-namespace arith {
-namespace nl {
-
-/** constraint information
- *
- * The struct ( d_rhs, d_coeff, d_type ) represents that a literal is of the
- * form (d_coeff * x) <d_type> d_rhs.
- */
-struct ConstraintInfo
-{
- public:
-  /** The term on the right hand side of the constraint */
-  Node d_rhs;
-  /** The coefficent */
-  Node d_coeff;
-  /** The type (relation) of the constraint */
-  Kind d_type;
-}; /* struct ConstraintInfo */
-
-/** A database for constraints */
-class ConstraintDb
-{
- public:
-  ConstraintDb(MonomialDb& mdb);
-  ~ConstraintDb() {}
-  /** register constraint
-   *
-   * This ensures that atom is in the domain of the constraints maintained by
-   * this database.
-   */
-  void registerConstraint(Node atom);
-  /** get constraints
-   *
-   * Returns a map m such that whenever
-   * m[lit][x] = ( r, coeff, k ), then
-   * ( lit <=>  (coeff * x) <k> r )
-   */
-  const std::map<Node, std::map<Node, ConstraintInfo> >& getConstraints();
-  /** Returns true if m is of maximal degree in atom
-   *
-   * For example, for atom x^2 + x*y + y >=0, the monomials x^2 and x*y
-   * are of maximal degree (2).
-   */
-  bool isMaximal(Node atom, Node m) const;
-
- private:
-  /** Reference to a monomial database */
-  MonomialDb& d_mdb;
-  /** List of all constraints */
-  std::vector<Node> d_constraints;
-  /** Is maximal degree */
-  std::map<Node, std::map<Node, bool> > d_c_info_maxm;
-  /** Constraint information */
-  std::map<Node, std::map<Node, ConstraintInfo> > d_c_info;
-};
-
-}  // namespace nl
-}  // namespace arith
-}  // namespace theory
-}  // namespace CVC4
-
-#endif /* CVC4__THEORY__ARITH__NL_SOLVER_H */