fix some Java compatibility-layer interface problems; also fix some Mac OS X build issues

1 files changed, 13 insertions, 0 deletions

diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index bf9bfbb38..9d0b8d34a 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -305,6 +305,19 @@ public:
    */
   Expr mkAssociative(Kind kind, const std::vector<Expr>& children);
 
+  /**
+   * Determine whether Exprs of a particular Kind have operators.
+   * @returns true if Exprs of Kind k have operators.
+   */
+  static bool hasOperator(Kind k);
+
+  /**
+   * Get the (singleton) operator of an OPERATOR-kinded kind.  The
+   * returned Expr e will have kind BUILTIN, and calling
+   * e.getConst<CVC4::Kind>() will yield k.
+   */
+  Expr operatorOf(Kind k);
+
   /** Make a function type from domain to range. */
   FunctionType mkFunctionType(Type domain, Type range);