1 files changed, 88 insertions, 0 deletions
diff --git a/src/theory/arith/nl/nl_constraint.h b/src/theory/arith/nl/nl_constraint.h
new file mode 100644
index 000000000..113c573d8
--- /dev/null
+++ b/src/theory/arith/nl/nl_constraint.h
@@ -0,0 +1,88 @@
+/*********************                                                        */
+/*! \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 */