11 files changed, 27 insertions, 22 deletions
diff --git a/src/parser/cvc/cvc_input.cpp b/src/parser/cvc/cvc_input.cpp
index 1de624f49..8c7b34410 100644
--- a/src/parser/cvc/cvc_input.cpp
+++ b/src/parser/cvc/cvc_input.cpp
@@ -61,8 +61,9 @@ Command* CvcInput::parseCommand() {
   return d_pCvcParser->parseCommand(d_pCvcParser);
 }
 
-Expr CvcInput::parseExpr() {
-  return d_pCvcParser->parseExpr(d_pCvcParser);
+api::Term CvcInput::parseExpr()
+{
+  return api::Term(d_pCvcParser->parseExpr(d_pCvcParser));
 }
 
 /*
diff --git a/src/parser/cvc/cvc_input.h b/src/parser/cvc/cvc_input.h
index 098efd580..50be82903 100644
--- a/src/parser/cvc/cvc_input.h
+++ b/src/parser/cvc/cvc_input.h
@@ -57,12 +57,12 @@ class CvcInput : public AntlrInput {
    */
   Command* parseCommand() override;
 
-  /** Parse an expression from the input. Returns a null <code>Expr</code>
+  /** Parse an expression from the input. Returns a null <code>api::Term</code>
    * if there is no expression there to parse.
    *
    * @throws ParserException if an error is encountered during parsing.
    */
-  Expr parseExpr() override;
+  api::Term parseExpr() override;
 
  private:
   /** Initialize the class. Called from the constructors once the input stream
diff --git a/src/parser/input.h b/src/parser/input.h
index 5627dc15e..f63a55707 100644
--- a/src/parser/input.h
+++ b/src/parser/input.h
@@ -24,9 +24,10 @@
 #include <string>
 #include <vector>
 
-#include "options/language.h"
+#include "api/cvc4cpp.h"
 #include "expr/expr.h"
 #include "expr/expr_manager.h"
+#include "options/language.h"
 #include "parser/parser_exception.h"
 
 namespace CVC4 {
@@ -164,11 +165,11 @@ class CVC4_PUBLIC Input {
 
   /** Parse an expression from the input by invoking the
    * implementation-specific parsing method. Returns a null
-   * <code>Expr</code> if there is no expression there to parse.
+   * <code>api::Term</code> if there is no expression there to parse.
    *
    * @throws ParserException if an error is encountered during parsing.
    */
-  virtual Expr parseExpr() = 0;
+  virtual api::Term parseExpr() = 0;
 
   /** Set the Parser object for this input. */
   virtual void setParser(Parser& parser) = 0;
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 664fa209d..447fb5d76 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -661,11 +661,11 @@ Command* Parser::nextCommand()
   return cmd;
 }
 
-Expr Parser::nextExpression()
+api::Term Parser::nextExpression()
 {
   Debug("parser") << "nextExpression()" << std::endl;
   d_resourceManager->spendResource(ResourceManager::Resource::ParseStep);
-  Expr result;
+  api::Term result;
   if (!done()) {
     try {
       result = d_input->parseExpr();
diff --git a/src/parser/parser.h b/src/parser/parser.h
index cd70fde0f..0c1f3822b 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -718,7 +718,7 @@ public:
   Command* nextCommand();
 
   /** Parse and return the next expression. */
-  Expr nextExpression();
+  api::Term nextExpression();
 
   /** Issue a warning to the user. */
   void warning(const std::string& msg) { d_input->warning(msg); }
@@ -845,7 +845,7 @@ public:
   public:
     ExprStream(Parser* parser) : d_parser(parser) {}
     ~ExprStream() { delete d_parser; }
-    Expr nextExpr() override { return d_parser->nextExpression(); }
+    Expr nextExpr() override { return d_parser->nextExpression().getExpr(); }
   };/* class Parser::ExprStream */
   
   //------------------------ operator overloading
diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp
index 87739789b..4e74eefb5 100644
--- a/src/parser/smt2/smt2_input.cpp
+++ b/src/parser/smt2/smt2_input.cpp
@@ -62,8 +62,9 @@ Command* Smt2Input::parseCommand() {
   return d_pSmt2Parser->parseCommand(d_pSmt2Parser);
 }
 
-Expr Smt2Input::parseExpr() {
-  return d_pSmt2Parser->parseExpr(d_pSmt2Parser);
+api::Term Smt2Input::parseExpr()
+{
+  return api::Term(d_pSmt2Parser->parseExpr(d_pSmt2Parser));
 }
 
 }/* CVC4::parser namespace */
diff --git a/src/parser/smt2/smt2_input.h b/src/parser/smt2/smt2_input.h
index e8b736a16..9d4ed2857 100644
--- a/src/parser/smt2/smt2_input.h
+++ b/src/parser/smt2/smt2_input.h
@@ -76,7 +76,7 @@ class Smt2Input : public AntlrInput {
    *
    * @throws ParserException if an error is encountered during parsing.
    */
-  Expr parseExpr() override;
+  api::Term parseExpr() override;
 
 };/* class Smt2Input */
 
diff --git a/src/parser/smt2/sygus_input.cpp b/src/parser/smt2/sygus_input.cpp
index ff1a409ae..f0bed978e 100644
--- a/src/parser/smt2/sygus_input.cpp
+++ b/src/parser/smt2/sygus_input.cpp
@@ -63,8 +63,9 @@ Command* SygusInput::parseCommand() {
   return d_pSmt2Parser->parseSygus(d_pSmt2Parser);
 }
 
-Expr SygusInput::parseExpr() {
-  return d_pSmt2Parser->parseExpr(d_pSmt2Parser);
+api::Term SygusInput::parseExpr()
+{
+  return api::Term(d_pSmt2Parser->parseExpr(d_pSmt2Parser));
 }
 
 }/* CVC4::parser namespace */
diff --git a/src/parser/smt2/sygus_input.h b/src/parser/smt2/sygus_input.h
index a0e3e81ef..39b161655 100644
--- a/src/parser/smt2/sygus_input.h
+++ b/src/parser/smt2/sygus_input.h
@@ -72,11 +72,11 @@ class SygusInput : public AntlrInput {
 
   /**
    * Parse an expression from the input. Returns a null
-   * <code>Expr</code> if there is no expression there to parse.
+   * <code>api::Term</code> if there is no expression there to parse.
    *
    * @throws ParserException if an error is encountered during parsing.
    */
-  Expr parseExpr() override;
+  api::Term parseExpr() override;
 
 };/* class SygusInput */
 
diff --git a/src/parser/tptp/tptp_input.cpp b/src/parser/tptp/tptp_input.cpp
index e17e6608e..6a4ec0e79 100644
--- a/src/parser/tptp/tptp_input.cpp
+++ b/src/parser/tptp/tptp_input.cpp
@@ -64,8 +64,9 @@ Command* TptpInput::parseCommand() {
   return d_pTptpParser->parseCommand(d_pTptpParser);
 }
 
-Expr TptpInput::parseExpr() {
-  return d_pTptpParser->parseExpr(d_pTptpParser);
+api::Term TptpInput::parseExpr()
+{
+  return api::Term(d_pTptpParser->parseExpr(d_pTptpParser));
 }
 
 }/* CVC4::parser namespace */
diff --git a/src/parser/tptp/tptp_input.h b/src/parser/tptp/tptp_input.h
index 5205cbc17..1ca746298 100644
--- a/src/parser/tptp/tptp_input.h
+++ b/src/parser/tptp/tptp_input.h
@@ -72,11 +72,11 @@ class TptpInput : public AntlrInput {
 
   /**
    * Parse an expression from the input. Returns a null
-   * <code>Expr</code> if there is no expression there to parse.
+   * <code>api::Term</code> if there is no expression there to parse.
    *
    * @throws ParserException if an error is encountered during parsing.
    */
-  Expr parseExpr() override;
+  api::Term parseExpr() override;
 
 };/* class TptpInput */