1 files changed, 33 insertions, 7 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 81bd5cb47..698f9ba2e 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -3,9 +3,9 @@
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: dejan
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): cconway
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -23,6 +23,26 @@
 
 #include <vector>
 
+#if SWIG
+%include "cvc4_public.h"
+%include "util/rational.h"
+%include "util/exception.h"
+%include "expr/kind.h"
+%include "util/integer.h"
+%include "util/cardinality.h"
+%include "util/sexpr.h"
+%include "util/language.h"
+%include "expr/type.h"
+%include "expr/expr.h"
+%include "expr/expr_manager.h"
+%{
+#include "util/integer.h"
+#include "expr/expr_manager.h"
+#include "expr/type.h"
+#include "expr/expr.h"
+%}
+#endif
+
 #include "context/cdlist_forward.h"
 #include "context/cdmap_forward.h"
 #include "context/cdset_forward.h"
@@ -253,16 +273,17 @@ public:
   Result assertFormula(const BoolExpr& e);
 
   /**
-   * Add a formula to the current context and call check().  Returns
-   * true iff consistent.
+   * Check validity of an expression with respect to the current set
+   * of assertions by asserting the query expression's negation and
+   * calling check().  Returns valid, invalid, or unknown result.
    */
   Result query(const BoolExpr& e);
 
   /**
-   * Add a formula to the current context and call check().  Returns
-   * true iff consistent.
+   * Assert a formula (if provided) to the current context and call
+   * check().  Returns sat, unsat, or unknown result.
    */
-  Result checkSat(const BoolExpr& e);
+  Result checkSat(const BoolExpr& e = BoolExpr());
 
   /**
    * Simplify a formula without doing "much" work.  Does not involve
@@ -307,6 +328,11 @@ public:
   std::vector<Expr> getAssertions() throw(ModalException, AssertionException);
 
   /**
+   * Get the current context level.
+   */
+  size_t getStackLevel() const;
+
+  /**
    * Push a user-level context.
    */
   void push();