user push/pop support in minisat and simplification; also bindings work

1 files changed, 17 insertions, 0 deletions

diff --git a/src/parser/parser.i b/src/parser/parser.i
index 55119be9a..dd52bfcda 100644
--- a/src/parser/parser.i
+++ b/src/parser/parser.i
@@ -8,7 +8,24 @@ namespace CVC4 {
     enum SymbolType;
     %ignore operator<<(std::ostream&, DeclarationCheck);
     %ignore operator<<(std::ostream&, SymbolType);
+
+  class ParserExprStream : public CVC4::ExprStream {
+    Parser* d_parser;
+  public:
+    ExprStream(Parser* parser) : d_parser(parser) {}
+    ~ExprStream() { delete d_parser; }
+    Expr nextExpr() { return d_parser->nextExpression(); }
+  };/* class Parser::ExprStream */
+
   }/* namespace CVC4::parser */
 }/* namespace CVC4 */
 
 %include "parser/parser.h"
+
+%{
+namespace CVC4 {
+  namespace parser {
+    typedef CVC4::parser::Parser::ExprStream ParserExprStream;
+  }
+}
+%}