Convert parser input interface to api::Term (#3809)

14 files changed, 33 insertions, 28 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 */
 
diff --git a/test/system/ouroborous.cpp b/test/system/ouroborous.cpp
index 3075e358d..a9f205236 100644
--- a/test/system/ouroborous.cpp
+++ b/test/system/ouroborous.cpp
@@ -70,7 +70,7 @@ string translate(string in, InputLanguage inlang, OutputLanguage outlang) {
        << "translating from " << inlang << " to " << outlang << " this string:" << endl
        << in << endl;
   psr->setInput(Input::newStringInput(inlang, in, "internal-buffer"));
-  Expr e = psr->nextExpression();
+  Expr e = psr->nextExpression().getExpr();
   stringstream ss;
   ss << language::SetLanguage(outlang) << expr::ExprSetDepth(-1) << e;
   assert(psr->nextExpression().isNull());// next expr should be null
@@ -81,7 +81,7 @@ string translate(string in, InputLanguage inlang, OutputLanguage outlang) {
        << "reparsing as " << outlang << endl;
 
   psr->setInput(Input::newStringInput(toInputLanguage(outlang), s, "internal-buffer"));
-  Expr f = psr->nextExpression();
+  Expr f = psr->nextExpression().getExpr();
   assert(e == f);
   cout << "got same expressions " << e.getId() << " and " << f.getId() << endl
        << "==============================================" << endl;
diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index bfaf8bda0..e00016f45 100644
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -148,7 +148,7 @@ class ParserBlack
       TS_ASSERT(!parser->done());
       setupContext(*parser);
       TS_ASSERT(!parser->done());
-      Expr e = parser->nextExpression();
+      api::Term e = parser->nextExpression();
       TS_ASSERT(!e.isNull());
       e = parser->nextExpression();
       TS_ASSERT(parser->done());
@@ -187,7 +187,7 @@ class ParserBlack
                          .build();
     setupContext(*parser);
     TS_ASSERT(!parser->done());
-    TS_ASSERT_THROWS(Expr e = parser->nextExpression();
+    TS_ASSERT_THROWS(api::Term e = parser->nextExpression();
                      cout << endl
                           << "Bad expr succeeded." << endl
                           << "Input: <<" << badExpr << ">>" << endl
diff --git a/test/unit/parser/parser_builder_black.h b/test/unit/parser/parser_builder_black.h
index 78e1be748..44bb9293b 100644
--- a/test/unit/parser/parser_builder_black.h
+++ b/test/unit/parser/parser_builder_black.h
@@ -99,7 +99,7 @@ class ParserBuilderBlack : public CxxTest::TestSuite
     Parser *parser = builder.build();
     TS_ASSERT(parser != NULL);
 
-    Expr e = parser->nextExpression();
+    api::Term e = parser->nextExpression();
     TS_ASSERT(e.isNull());
 
     delete parser;
@@ -110,7 +110,7 @@ class ParserBuilderBlack : public CxxTest::TestSuite
     Parser *parser = builder.build();
     TS_ASSERT(parser != NULL);
 
-    Expr e = parser->nextExpression();
+    api::Term e = parser->nextExpression();
     TS_ASSERT_EQUALS(e, d_solver->getExprManager()->mkConst(true));
 
     e = parser->nextExpression();