Refactor ouroborous API test to not use Expr. (#6079)

diff --git a/test/api/ouroborous.cpp b/test/api/ouroborous.cpp
index 1a23acd297767574eb634def0197f294ad231bf3..ca8adaf4dacd29ed0ffcc997db0210ec9042c33f 100644 (file)
--- a/test/api/ouroborous.cpp
+++ b/test/api/ouroborous.cpp
@@ -2,9 +2,9 @@
 /*! \file ouroborous.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Andrew Reynolds, Tim King
+ **   Aina Niemetz, Morgan Deters, Christopher L. Conway
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -25,7 +25,6 @@
  **/
 
 #include <iostream>
-#include <sstream>
 #include <string>
 
 #include "api/cvc4cpp.h"
@@ -39,101 +38,140 @@
 using namespace CVC4;
 using namespace CVC4::parser;
 using namespace CVC4::language;
-using namespace std;
-
-const string declarations = "\
-(declare-sort U 0)\n\
-(declare-fun f (U) U)\n\
-(declare-fun x () U)\n\
-(declare-fun y () U)\n\
-(assert (= (f x) x))\n\
-(declare-fun a () (Array U (Array U U)))\n\
-";
-
-Parser* psr = NULL;
 
 int runTest();
 
-int main() {
-  try {
+int main()
+{
+  try
+  {
     return runTest();
-  } catch(Exception& e) {
-    cerr << e << endl;
-  } catch(...) {
-    cerr << "non-cvc4 exception thrown." << endl;
+  }
+  catch (api::CVC4ApiException& e)
+  {
+    std::cerr << e.getMessage() << std::endl;
+  }
+  catch (parser::ParserException& e)
+  {
+    std::cerr << e.getMessage() << std::endl;
+  }
+  catch (...)
+  {
+    std::cerr << "non-cvc4 exception thrown" << std::endl;
   }
   return 1;
 }
 
-string translate(string in, InputLanguage inlang, OutputLanguage outlang) {
-  cout << "==============================================" << endl
-       << "translating from " << inlang << " to " << outlang << " this string:" << endl
-       << in << endl;
-  psr->setInput(Input::newStringInput(inlang, in, "internal-buffer"));
-  Expr e = psr->nextExpression().getExpr();
-  stringstream ss;
-  ss << language::SetLanguage(outlang) << expr::ExprSetDepth(-1) << e;
-  assert(psr->nextExpression().isNull());// next expr should be null
-  assert(psr->done());// parser should be done
-  string s = ss.str();
-  cout << "got this:" << endl
-       << s << endl
-       << "reparsing as " << outlang << endl;
-
-  psr->setInput(Input::newStringInput(toInputLanguage(outlang), s, "internal-buffer"));
-  Expr f = psr->nextExpression().getExpr();
-  assert(e == f);
-  cout << "got same expressions " << e.getId() << " and " << f.getId() << endl
-       << "==============================================" << endl;
-
-  return s;
-}
-
-void runTestString(std::string instr, InputLanguage instrlang = input::LANG_SMTLIB_V2) {
-  cout << endl
-       << "starting with: " << instr << endl
-       << "   in language " << instrlang << endl;
-  string smt2 = translate(instr, instrlang, output::LANG_SMTLIB_V2);
-  cout << "in SMT2      : " << smt2 << endl;
-  /* -- SMT-LIBv1 doesn't have a functional printer yet
-  string smt1 = translate(smt2, input::LANG_SMTLIB_V2, output::LANG_SMTLIB);
-  cout << "in SMT1      : " << smt1 << endl;
-  */
-  string cvc = translate(smt2, input::LANG_SMTLIB_V2, output::LANG_CVC4);
-  cout << "in CVC       : " << cvc << endl;
-  string out = translate(cvc, input::LANG_CVC4, output::LANG_SMTLIB_V2);
-  cout << "back to SMT2 : " << out << endl << endl;
-
-  assert(out == smt2);// differences in output
-}
-
-
-int runTest() {
-  std::unique_ptr<api::Solver> solver =
-      std::unique_ptr<api::Solver>(new api::Solver());
-  std::unique_ptr<SymbolManager> symman(new SymbolManager(solver.get()));
-  psr = ParserBuilder(solver.get(), symman.get(), "internal-buffer")
-            .withStringInput(declarations)
-            .withInputLanguage(input::LANG_SMTLIB_V2)
-            .build();
+std::string parse(std::string instr,
+                  std::string input_language,
+                  std::string output_language)
+{
+  assert(input_language == "smt2" || input_language == "cvc4");
+  assert(output_language == "smt2" || output_language == "cvc4");
+
+  std::string declarations;
+
+  if (input_language == "smt2")
+  {
+    declarations =
+        "\
+  (declare-sort U 0)\n\
+  (declare-fun f (U) U)\n\
+  (declare-fun x () U)\n\
+  (declare-fun y () U)\n\
+  (assert (= (f x) x))\n\
+  (declare-fun a () (Array U (Array U U)))\n\
+  ";
+  }
+  else
+  {
+    declarations =
+        "\
+      U: TYPE;\n\
+      f: U -> U;\n\
+      x,y: U;\n\
+      a: ARRAY U OF (ARRAY U OF U);\n\
+      ASSERT f(x) = x;\n\
+  ";
+  }
 
-  // we don't need to execute them, but we DO need to parse them to
+  api::Solver solver;
+  InputLanguage ilang =
+      input_language == "smt2" ? input::LANG_SMTLIB_V2 : input::LANG_CVC4;
+
+  solver.setOption("input-language", input_language);
+  solver.setOption("output-language", output_language);
+  SymbolManager symman(&solver);
+  Parser* parser = ParserBuilder(&solver, &symman, "internal-buffer")
+                       .withStringInput(declarations)
+                       .withInputLanguage(ilang)
+                       .build();
+  // we don't need to execute the commands, but we DO need to parse them to
   // get the declarations
-  while(Command* c = psr->nextCommand()) {
+  while (Command* c = parser->nextCommand())
+  {
     delete c;
   }
+  assert(parser->done());  // parser should be done
+  parser->setInput(Input::newStringInput(ilang, instr, "internal-buffer"));
+  api::Term e = parser->nextExpression();
+  std::string s = e.toString();
+  assert(parser->nextExpression().isNull());  // next expr should be null
+  delete parser;
+  return s;
+}
 
-  assert(psr->done());// parser should be done
-
-  cout << expr::ExprSetDepth(-1);
-
-  runTestString("(= (f (f y)) x)");
-  runTestString("~BVPLUS(3, 0bin00, 0bin11)[2:1] = 0bin10", input::LANG_CVC4);
-  runTestString("~BVPLUS(3, BVMULT(2, 0bin01, 0bin11), 0bin11)[2:0]", input::LANG_CVC4);
-  runTestString("a[x][y] = a[y][x]", input::LANG_CVC4);
+std::string translate(std::string instr,
+                      std::string input_language,
+                      std::string output_language)
+{
+  assert(input_language == "smt2" || input_language == "cvc4");
+  assert(output_language == "smt2" || output_language == "cvc4");
+
+  std::cout << "==============================================" << std::endl
+            << "translating from "
+            << (input_language == "smt2" ? input::LANG_SMTLIB_V2
+                                         : input::LANG_CVC4)
+            << " to "
+            << (output_language == "smt2" ? output::LANG_SMTLIB_V2
+                                          : output::LANG_CVC4)
+            << " this string:" << std::endl
+            << instr << std::endl;
+  std::string outstr = parse(instr, input_language, output_language);
+  std::cout << "got this:" << std::endl
+            << outstr << std::endl
+            << "reparsing as "
+            << (output_language == "smt2" ? input::LANG_SMTLIB_V2
+                                          : input::LANG_CVC4)
+            << std::endl;
+  std::string poutstr = parse(outstr, output_language, output_language);
+  assert(outstr == poutstr);
+  std::cout << "got same expressions " << outstr << " and " << poutstr
+            << std::endl
+            << "==============================================" << std::endl;
+  return outstr;
+}
 
-  delete psr;
-  psr = NULL;
+void runTestString(std::string instr, std::string instr_language)
+{
+  std::cout << std::endl
+            << "starting with: " << instr << std::endl
+            << "   in language " << input::LANG_SMTLIB_V2 << std::endl;
+  std::string smt2str = translate(instr, instr_language, "smt2");
+  std::cout << "in SMT2      : " << smt2str << std::endl;
+  std::string cvcstr = translate(smt2str, "smt2", "cvc4");
+  std::cout << "in CVC       : " << cvcstr << std::endl;
+  std::string outstr = translate(cvcstr, "cvc4", "smt2");
+  std::cout << "back to SMT2 : " << outstr << std::endl << std::endl;
+
+  assert(outstr == smt2str);  // differences in output
+}
 
+int32_t runTest()
+{
+  runTestString("(= (f (f y)) x)", "smt2");
+  runTestString("~BVPLUS(3, 0bin00, 0bin11)[2:1] = 0bin10", "cvc4");
+  runTestString("~BVPLUS(3, BVMULT(2, 0bin01, 0bin11), 0bin11)[2:0]", "cvc4");
+  runTestString("a[x][y] = a[y][x]", "cvc4");
   return 0;
 }