diff options
Diffstat (limited to 'src/theory/arith/nl/poly_conversion.h')
-rw-r--r-- | src/theory/arith/nl/poly_conversion.h | 30 |
1 files changed, 15 insertions, 15 deletions
diff --git a/src/theory/arith/nl/poly_conversion.h b/src/theory/arith/nl/poly_conversion.h index 9adc9a996..9aef0db18 100644 --- a/src/theory/arith/nl/poly_conversion.h +++ b/src/theory/arith/nl/poly_conversion.h @@ -30,7 +30,7 @@ #include "expr/node.h" #include "util/real_algebraic_number.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -42,23 +42,23 @@ namespace nl { struct VariableMapper { /** A mapping from CVC4 variables to poly variables. */ - std::map<CVC5::Node, poly::Variable> mVarCVCpoly; + std::map<cvc5::Node, poly::Variable> mVarCVCpoly; /** A mapping from poly variables to CVC4 variables. */ - std::map<poly::Variable, CVC5::Node> mVarpolyCVC; + std::map<poly::Variable, cvc5::Node> mVarpolyCVC; /** Retrieves the according poly variable. */ - poly::Variable operator()(const CVC5::Node& n); + poly::Variable operator()(const cvc5::Node& n); /** Retrieves the according CVC4 variable. */ - CVC5::Node operator()(const poly::Variable& n); + cvc5::Node operator()(const poly::Variable& n); }; -/** Convert a poly univariate polynomial to a CVC5::Node. */ -CVC5::Node as_cvc_upolynomial(const poly::UPolynomial& p, - const CVC5::Node& var); +/** Convert a poly univariate polynomial to a cvc5::Node. */ +cvc5::Node as_cvc_upolynomial(const poly::UPolynomial& p, + const cvc5::Node& var); -/** Convert a CVC5::Node to a poly univariate polynomial. */ -poly::UPolynomial as_poly_upolynomial(const CVC5::Node& n, - const CVC5::Node& var); +/** Convert a cvc5::Node to a poly univariate polynomial. */ +poly::UPolynomial as_poly_upolynomial(const cvc5::Node& n, + const cvc5::Node& var); /** * Constructs a polynomial from the given node. @@ -73,8 +73,8 @@ poly::UPolynomial as_poly_upolynomial(const CVC5::Node& n, * in the context of ICP) the second overload provides the denominator in the * third argument. */ -poly::Polynomial as_poly_polynomial(const CVC5::Node& n, VariableMapper& vm); -poly::Polynomial as_poly_polynomial(const CVC5::Node& n, +poly::Polynomial as_poly_polynomial(const cvc5::Node& n, VariableMapper& vm); +poly::Polynomial as_poly_polynomial(const cvc5::Node& n, VariableMapper& vm, poly::Rational& denominator); @@ -87,7 +87,7 @@ poly::Polynomial as_poly_polynomial(const CVC5::Node& n, * multiplications with one or use NONLINEAR_MULT where regular MULT may be * sufficient), so it may be sensible to rewrite it afterwards. */ -CVC5::Node as_cvc_polynomial(const poly::Polynomial& p, VariableMapper& vm); +cvc5::Node as_cvc_polynomial(const poly::Polynomial& p, VariableMapper& vm); /** * Constructs a constraints (a polynomial and a sign condition) from the given @@ -164,7 +164,7 @@ poly::IntervalAssignment getBounds(VariableMapper& vm, const BoundInference& bi) } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif |