diff options
Diffstat (limited to 'src/theory/arith/nl/cad/projections.h')
| -rw-r--r-- | src/theory/arith/nl/cad/projections.h | 26 |
1 files changed, 11 insertions, 15 deletions
diff --git a/src/theory/arith/nl/cad/projections.h b/src/theory/arith/nl/cad/projections.h index 39d2b1221..c4a34ee56 100644 --- a/src/theory/arith/nl/cad/projections.h +++ b/src/theory/arith/nl/cad/projections.h @@ -9,17 +9,13 @@ ** 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. **/ +#include "cvc4_private.h" + #ifndef CVC4__THEORY__ARITH__NL__CAD_PROJECTIONS_H #define CVC4__THEORY__ARITH__NL__CAD_PROJECTIONS_H @@ -40,33 +36,33 @@ namespace nl { namespace cad { /** Sort and remove duplicates from the list of polynomials. */ -void reduce_projection_polynomials(std::vector<poly::Polynomial>& polys); +void reduceProjectionPolynomials(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); +void addPolynomial(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); +void addPolynomials(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); +void makeFinestSquareFreeBasis(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); +void makeFinestSquareFreeBasis(std::vector<poly::Polynomial>& lhs, + std::vector<poly::Polynomial>& rhs); /** * Computes McCallum's projection operator. */ -std::vector<poly::Polynomial> projection_mccallum( +std::vector<poly::Polynomial> projectionMcCallum( const std::vector<poly::Polynomial>& polys); } // namespace cad |