diff options
Diffstat (limited to 'test/unit/parser/cvc/cvc_parser_black.h')
-rw-r--r-- | test/unit/parser/cvc/cvc_parser_black.h | 46 |
1 files changed, 46 insertions, 0 deletions
diff --git a/test/unit/parser/cvc/cvc_parser_black.h b/test/unit/parser/cvc/cvc_parser_black.h new file mode 100644 index 000000000..b34185e01 --- /dev/null +++ b/test/unit/parser/cvc/cvc_parser_black.h @@ -0,0 +1,46 @@ +/* Black box testing of CVC4::Node. */ + +#include <cxxtest/TestSuite.h> +//#include <string> +#include <sstream> + +#include "expr/expr_manager.h" +#include "parser/cvc/cvc_parser.h" + +using namespace CVC4; +using namespace CVC4::parser; +using namespace std; + +const string d_goodInputs[] = { + "ASSERT TRUE;", + "QUERY TRUE;", + "CHECKSAT FALSE;", + "a, b : BOOLEAN;", + "x, y : INT;", + "a, b : BOOLEAN; QUERY (a => b) AND a => b;" + }; + +class CvcParserBlack : public CxxTest::TestSuite { +private: + + ExprManager *d_exprManager; + + +public: + void setUp() { +// cout << "In setUp()\n"; + d_exprManager = new ExprManager(); +// cout << "Leaving setUp()\n"; + } + + void testGoodInputs() { +// cout << "In testGoodInputs()\n"; + for( int i=0; i < sizeof(d_goodInputs); ++i ) { + istringstream stream(d_goodInputs[i]); + CvcParser cvcParser(d_exprManager,stream); + TS_ASSERT( !cvcParser.done() ); + while( !cvcParser.done() ) { + TS_ASSERT( cvcParser.parseNextCommand() ); + } + } +}; |