/*********************                                           -*- C++ -*-  */
/** cvc_parser_black.h
 ** Original author: cconway
 ** Major contributors: none
 ** Minor contributors (to current version): none
 ** This file is part of the CVC4 prototype.
 ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
 ** Courant Institute of Mathematical Sciences
 ** New York University
 ** See the file COPYING in the top-level source directory for licensing
 ** information.
 **
 ** Black box testing of CVC4::parser::CvcParser.
 **/

#include <cxxtest/TestSuite.h>
//#include <string>
#include <sstream>

#include "expr/expr.h"
#include "expr/expr_manager.h"
#include "parser/parser.h"

using namespace CVC4;
using namespace CVC4::parser;
using namespace std;

const string goodInputs[] = {
      "", // empty string is OK
      "ASSERT TRUE;",
      "QUERY TRUE;",
      "CHECKSAT FALSE;",
      "a, b : BOOLEAN;",
      "x, y : INT;",
      "a, b : BOOLEAN; QUERY (a => b) AND a => b;",
      "%% nothing but a comment",
      "% a comment\nASSERT TRUE %a command\n% another comment"
  };

/* The following expressions are good in a context where a, b, and c have been declared as BOOLEAN. */
const string goodBooleanExprs[] = {
    "a AND b",
    "a AND b OR c",
    "(a => b) AND a => b",
    "(a <=> b) AND (NOT a)",
    "(a XOR b) <=> (a OR b) AND (NOT (a AND b))"
};

const string badInputs[] = {
      ";", // no command
      "ASSERT;", // no args
      "QUERY",
      "CHECKSAT;",
      "a, b : boolean;", // lowercase boolean isn't a type
      "0x : INT;", // 0x isn't an identifier
      "a, b : BOOLEAN\nQUERY (a => b) AND a => b;" // no semicolon after decl
  };

/* The following expressions are bad even in a context where a, b, and c have been declared as BOOLEAN. */
const string badBooleanExprs[] = {
    "",
    "a AND", // wrong arity
    "AND(a,b)", // not infix
    "(OR (AND a b) c)", // not infix
    "a IMPLIES b", // should be =>
    "a NOT b", // wrong arity, not infix
    "a and b" // wrong case
};

class CvcParserBlack : public CxxTest::TestSuite {
private:
  ExprManager *d_exprManager;
  Parser::InputLanguage d_lang;

public:
  void setUp() {
    d_exprManager = new ExprManager();
    d_lang = Parser::LANG_CVC4;
  }

  void testGoodInputs() {
    //    cout << "In testGoodInputs()\n";
    for(int i = 0; i < sizeof(goodInputs); ++i) {
      istringstream stream(goodInputs[i]);
      Parser* cvcParser = Parser::getNewParser(d_exprManager, d_lang, stream);
      TS_ASSERT( !cvcParser->done() );
      while(!cvcParser->done()) {
        TS_ASSERT( cvcParser->parseNextCommand() != NULL );
      }
      delete cvcParser;
    }
  }

  void testBadInputs() {
    //    cout << "In testGoodInputs()\n";
    for(int i = 0; i < sizeof(badInputs); ++i) {
      istringstream stream(badInputs[i]);
      Parser* cvcParser = Parser::getNewParser(d_exprManager, d_lang, stream);
      TS_ASSERT_THROWS( cvcParser->parseNextCommand(), ParserException );
      delete cvcParser;
    }
  }

  void testGoodBooleanExprs() {
    //    cout << "In testGoodInputs()\n";
    for(int i = 0; i < sizeof(goodBooleanExprs); ++i) {
      istringstream stream(goodBooleanExprs[i]);
      Parser* cvcParser = Parser::getNewParser(d_exprManager, d_lang, stream);
      TS_ASSERT( !cvcParser->done() );
      while(!cvcParser->done()) {
        TS_ASSERT( !cvcParser->parseNextExpression().isNull() );
      }
      delete cvcParser;
    }
  }

  void testBadBooleanExprs() {
    //    cout << "In testGoodInputs()\n";
    for(int i = 0; i < sizeof(badBooleanExprs); ++i) {
      istringstream stream(badBooleanExprs[i]);
      Parser* cvcParser = Parser::getNewParser(d_exprManager, d_lang, stream);
      TS_ASSERT_THROWS( cvcParser->parseNextExpression(), ParserException );
      delete cvcParser;
    }
  }

};