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

diff --git a/src/parser/cvc/cvc_input.cpp b/src/parser/cvc/cvc_input.cpp
index 1de624f492fda2df5474812db9a7c9fe4d072463..8c7b344106ad375c43a7344b892b1ae8bc371830 100644 (file)
--- 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 098efd58056ea61dc5642c7ee83c0804812efdc8..50be82903cec2c8e97788b7ae8ae1414ec6ad337 100644 (file)
--- 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 5627dc15e7eba4d43ffb1254c981f803a3c03412..f63a55707a7a94a3341e5de96b8ea5eec1f9b5fe 100644 (file)
--- 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 664fa209d7b6a9e11012acd13f0d9103c201b9c3..447fb5d76c9f4f23e178b383dd3ae308080fb4d5 100644 (file)
--- 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 cd70fde0f59a9808e65f575aa05876d5a6b86010..0c1f3822b7a87b188b0684662d652745239c97df 100644 (file)
--- 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 87739789bd7ef73df7718b6a9a570a4c6cfd8494..4e74eefb5c6e6757b7225b658cc9b70441c55b27 100644 (file)
--- 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 e8b736a16161de74c02a89b78ecfa5e1a4e6b18f..9d4ed28570e2bcc73ec0b8ef54ee84ed3a7585d6 100644 (file)
--- 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 ff1a409aeeddd1cbe5c1b45cd98a205b4fcc7b5c..f0bed978e80c9ca731d2c131395d884f2c2a93f2 100644 (file)
--- 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 a0e3e81ef7c0e231b48c8b954264e0196c07754a..39b1616554db2f8fa915dc35fdd389f05625db13 100644 (file)
--- 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 e17e6608ef11554fdebe649e25d41ec8ca8a1cf5..6a4ec0e792a4faf0eca8b67f3572c4d251aff6f6 100644 (file)
--- 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 5205cbc176ace544cb8da6f8c5f3d7f9317322ac..1ca7462989da4a5dc578a555f850436461919b38 100644 (file)
--- 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 3075e358d2a026bffdcb2b2ae23ca27b4b68280f..a9f2052361189267ffb07db09106b947508d5ecd 100644 (file)
--- 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 bfaf8bda0006502dabe7ea423937996f637a544c..e00016f45bc4138e8141f9e65aa3a2cd2c0f3a1d 100644 (file)
--- 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 78e1be7482480086230df43834c734e710bddc79..44bb9293b060b6c58074b97db76e549bd9c5dd38 100644 (file)
--- 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();