Minor mixed-bag commit. Expected performance impact negligible.

* Fixed hole in arrays typechecking.
* Fixed "make dist".
* Better ouroborous test, and some printer fixes.
* Continued cleanup in CVC parser, removed some warnings.
* Better output.

1 files changed, 55 insertions, 26 deletions

diff --git a/test/system/ouroborous.cpp b/test/system/ouroborous.cpp
index 821b43a2f..abce24751 100644
--- a/test/system/ouroborous.cpp
+++ b/test/system/ouroborous.cpp
@@ -13,11 +13,17 @@
  **
  ** \brief "Ouroborous" test: does CVC4 read its own output?
  **
- ** The "Ouroborous" test, named after the serpent that swallows its own
- ** tail, ensures that CVC4 can parse some input, output it again (in any
- ** of its languages) and then parse it again.  The result of the first
- ** parse must be equal to the result of the second parse (up to renaming
- ** variables), or the test fails.
+ ** The "Ouroborous" test, named after the serpent that swallows its
+ ** own tail, ensures that CVC4 can parse some input, output it again
+ ** (in any of its languages) and then parse it again.  The result of
+ ** the first parse must be equal to the result of the second parse;
+ ** both strings and expressions are compared for equality.
+ **
+ ** To add a new test, simply add a call to runTestString() under
+ ** runTest(), below.  If you don't specify an input language,
+ ** LANG_SMTLIB_V2 is used.  If your example depends on variables,
+ ** you'll need to declare them in the "declarations" global, just
+ ** below, in SMT-LIBv2 form (but they're good for all languages).
  **/
 
 #include <iostream>
@@ -40,8 +46,11 @@ const string declarations = "\
 (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() {
@@ -55,25 +64,52 @@ int main() {
   return 1;
 }
 
-string translate(Parser* parser, string in, InputLanguage inlang, OutputLanguage outlang) {
+string translate(string in, InputLanguage inlang, OutputLanguage outlang) {
   cout << "==============================================" << endl
        << "translating from " << inlang << " to " << outlang << " this string:" << endl
        << in << endl;
-  parser->setInput(Input::newStringInput(inlang, in, "internal-buffer"));
+  psr->setInput(Input::newStringInput(inlang, in, "internal-buffer"));
+  Expr e = psr->nextExpression();
   stringstream ss;
-  ss << Expr::setlanguage(outlang) << parser->nextExpression();
-  AlwaysAssert(parser->nextExpression().isNull(), "next expr should be null");
-  AlwaysAssert(parser->done(), "parser should be done");
+  ss << Expr::setlanguage(outlang) << Expr::setdepth(-1) << e;
+  AlwaysAssert(psr->nextExpression().isNull(), "next expr should be null");
+  AlwaysAssert(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();
+  AlwaysAssert(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;
+
+  AlwaysAssert(out == smt2, "differences in output");
+}
+
+
 int runTest() {
   ExprManager em;
-  Parser* parser =
+  psr =
     ParserBuilder(&em, "internal-buffer")
       .withStringInput(declarations)
       .withInputLanguage(input::LANG_SMTLIB_V2)
@@ -81,27 +117,20 @@ int runTest() {
 
   // we don't need to execute them, but we DO need to parse them to
   // get the declarations
-  while(Command* c = parser->nextCommand()) {
+  while(Command* c = psr->nextCommand()) {
     delete c;
   }
 
-  AlwaysAssert(parser->done(), "parser should be done");
+  AlwaysAssert(psr->done(), "parser should be done");
 
-  string instr = "(= (f (f y)) x)";
-  cout << "starting with: " << instr << endl;
-  string smt2 = translate(parser, instr, input::LANG_SMTLIB_V2, output::LANG_SMTLIB_V2);
-  cout << "in SMT2      : " << smt2 << endl;
-  string smt1 = translate(parser, smt2, input::LANG_SMTLIB_V2, output::LANG_SMTLIB);
-  cout << "in SMT1      : " << smt1 << endl;
-  string cvc = translate(parser, smt1, input::LANG_SMTLIB, output::LANG_CVC4);
-  cout << "in CVC       : " << cvc << endl;
-  string out = translate(parser, cvc, input::LANG_CVC4, output::LANG_SMTLIB_V2);
-  cout << "back to SMT2 : " << out << endl;
+  cout << Expr::setdepth(-1);
 
-  AlwaysAssert(out == smt2, "differences in output");
+  runTestString("(= (f (f y)) x)");
+  runTestString("~BVPLUS(3, 0bin00, 0bin11)[2:1] = 0bin10", input::LANG_CVC4);
+  runTestString("a[x][y] = a[y][x]", input::LANG_CVC4);
 
-  delete parser;
+  delete psr;
+  psr = NULL;
 
   return 0;
 }
-