summaryrefslogtreecommitdiff
path: root/src/theory/arith/nl/poly_conversion.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith/nl/poly_conversion.h')
-rw-r--r--src/theory/arith/nl/poly_conversion.h8
1 files changed, 4 insertions, 4 deletions
diff --git a/src/theory/arith/nl/poly_conversion.h b/src/theory/arith/nl/poly_conversion.h
index 3213df0ce..db64320d5 100644
--- a/src/theory/arith/nl/poly_conversion.h
+++ b/src/theory/arith/nl/poly_conversion.h
@@ -37,17 +37,17 @@ class BoundInference;
namespace nl {
-/** Bijective mapping between CVC4 variables and poly variables. */
+/** Bijective mapping between cvc5 variables and poly variables. */
struct VariableMapper
{
- /** A mapping from CVC4 variables to poly variables. */
+ /** A mapping from cvc5 variables to poly variables. */
std::map<cvc5::Node, poly::Variable> mVarCVCpoly;
- /** A mapping from poly variables to CVC4 variables. */
+ /** A mapping from poly variables to cvc5 variables. */
std::map<poly::Variable, cvc5::Node> mVarpolyCVC;
/** Retrieves the according poly variable. */
poly::Variable operator()(const cvc5::Node& n);
- /** Retrieves the according CVC4 variable. */
+ /** Retrieves the according cvc5 variable. */
cvc5::Node operator()(const poly::Variable& n);
};
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback