1 files changed, 11 insertions, 1 deletions
diff --git a/src/util/boolean_simplification.h b/src/util/boolean_simplification.h
index c2da8af5b..b3dffa475 100644
--- a/src/util/boolean_simplification.h
+++ b/src/util/boolean_simplification.h
@@ -2,7 +2,7 @@
 /*! \file boolean_simplification.h
  ** \verbatim
  ** Original author: taking
- ** Major contributors: none
+ ** Major contributors: mdeters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
@@ -198,6 +198,16 @@ public:
   }
 
   /**
+   * Negates an Expr, doing all the double-negation elimination that's
+   * possible.
+   *
+   * @param e the Expr to negate (cannot be the null Expr)
+   */
+  static Expr negate(Expr e) throw(AssertionException) {
+    return negate(Node::fromExpr(e)).toExpr();
+  }
+
+  /**
    * Simplify an OR, AND, or IMPLIES.  This function is the identity
    * for all other kinds.
    */