First draft implementation of mkAssociative

1 files changed, 17 insertions, 0 deletions

diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index 3c17507cf..b2e45533a 100644
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -292,6 +292,23 @@ ${metakind_ubchildren}
   return ubs[k];
 }
 
+/** Returns true if the given kind is associative. This is used by ExprManager to
+ * decide whether it's safe to modify big expressions by changing the grouping of
+ * the arguments. */
+/* TODO: This could be generated. */
+inline bool isAssociative(::CVC4::Kind k) {
+  switch(k) {
+  case kind::AND:
+  case kind::OR:
+  case kind::MULT:
+  case kind::PLUS:
+    return true;
+
+  default:
+    return false;
+  }
+}
+
 }/* CVC4::kind::metakind namespace */
 }/* CVC4::kind namespace */
 }/* CVC4 namespace */