1 files changed, 80 insertions, 0 deletions
diff --git a/src/theory/arith/nl/cad/projections.h b/src/theory/arith/nl/cad/projections.h
new file mode 100644
index 000000000..39d2b1221
--- /dev/null
+++ b/src/theory/arith/nl/cad/projections.h
@@ -0,0 +1,80 @@
+/*********************                                                        */
+/*! \file projections.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Gereon Kremer
+ ** 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
+ **
+ ** 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 Implements utilities for CAD projection operators.
+ **
+ ** Implements utilities for CAD projection operators.
+ **/
+
+#ifndef CVC4__THEORY__ARITH__NL__CAD_PROJECTIONS_H
+#define CVC4__THEORY__ARITH__NL__CAD_PROJECTIONS_H
+
+#include "util/real_algebraic_number.h"
+
+#ifdef CVC4_USE_POLY
+
+#include <poly/polyxx.h>
+
+#include <algorithm>
+#include <iostream>
+#include <vector>
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+namespace nl {
+namespace cad {
+
+/** Sort and remove duplicates from the list of polynomials. */
+void reduce_projection_polynomials(std::vector<poly::Polynomial>& polys);
+
+/**
+ * Adds a polynomial to the list of projection polynomials.
+ * Before adding, it factorizes the polynomials and removed constant factors.
+ */
+void add_polynomial(std::vector<poly::Polynomial>& polys,
+                    const poly::Polynomial& poly);
+
+/** Adds a list of polynomials using add_polynomial(). */
+void add_polynomials(std::vector<poly::Polynomial>& polys,
+                     const std::vector<poly::Polynomial>& p);
+
+/** Make a set of polynomials a finest square-free basis. */
+void make_finest_square_free_basis(std::vector<poly::Polynomial>& polys);
+
+/**
+ * Ensure that two sets of polynomials are finest square-free basis relative to
+ * each other.
+ */
+void make_finest_square_free_basis(std::vector<poly::Polynomial>& lhs,
+                                   std::vector<poly::Polynomial>& rhs);
+
+/**
+ * Computes McCallum's projection operator.
+ */
+std::vector<poly::Polynomial> projection_mccallum(
+    const std::vector<poly::Polynomial>& polys);
+
+}  // namespace cad
+}  // namespace nl
+}  // namespace arith
+}  // namespace theory
+}  // namespace CVC4
+
+#endif
+
+#endif