diff options
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/main/interactive_shell_black.cpp | 1 | ||||
-rw-r--r-- | test/unit/parser/CMakeLists.txt | 2 | ||||
-rw-r--r-- | test/unit/parser/input_parser_white.cpp | 384 | ||||
-rw-r--r-- | test/unit/parser/parser_black.cpp | 400 | ||||
-rw-r--r-- | test/unit/parser/parser_builder_black.cpp | 142 |
5 files changed, 459 insertions, 470 deletions
diff --git a/test/unit/main/interactive_shell_black.cpp b/test/unit/main/interactive_shell_black.cpp index 8af29a8e4..9fda2f632 100644 --- a/test/unit/main/interactive_shell_black.cpp +++ b/test/unit/main/interactive_shell_black.cpp @@ -22,7 +22,6 @@ #include "options/base_options.h" #include "options/language.h" #include "options/options.h" -#include "parser/parser_builder.h" #include "smt/command.h" #include "test.h" diff --git a/test/unit/parser/CMakeLists.txt b/test/unit/parser/CMakeLists.txt index 890a38f76..649481c0a 100644 --- a/test/unit/parser/CMakeLists.txt +++ b/test/unit/parser/CMakeLists.txt @@ -15,4 +15,4 @@ # Add unit tests. cvc5_add_unit_test_black(parser_black parser) -cvc5_add_unit_test_black(parser_builder_black parser) +cvc5_add_unit_test_white(input_parser_white parser) diff --git a/test/unit/parser/input_parser_white.cpp b/test/unit/parser/input_parser_white.cpp new file mode 100644 index 000000000..47ad422b0 --- /dev/null +++ b/test/unit/parser/input_parser_white.cpp @@ -0,0 +1,384 @@ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Christopher L. Conway, Morgan Deters + * + * This file is part of the cvc5 project. + * + * 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. + * **************************************************************************** + * + * Black box testing of cvc5::parser::Parser for CVC and SMT-LIbv2 inputs. + */ + +#include <sstream> + +#include "api/cpp/cvc5.h" +#include "base/output.h" +#include "expr/symbol_manager.h" +#include "options/base_options.h" +#include "options/language.h" +#include "options/options.h" +#include "options/parser_options.h" +#include "parser/input_parser.h" +#include "parser/parser.h" +#include "parser/smt2/smt2.h" +#include "smt/command.h" +#include "test.h" + +namespace cvc5 { + +using namespace parser; +using namespace language::input; + +namespace test { + +class TestParserWhiteInputParser : public TestInternal +{ + protected: + TestParserWhiteInputParser(InputLanguage lang) : d_lang(lang) + { + d_options.setInputLanguage(d_lang); + } + + virtual ~TestParserWhiteInputParser() {} + + void SetUp() override + { + TestInternal::SetUp(); + d_options.set(options::parseOnly, true); + d_symman.reset(nullptr); + d_solver.reset(new cvc5::api::Solver(&d_options)); + } + + void TearDown() override + { + d_symman.reset(nullptr); + d_solver.reset(nullptr); + } + + void setUp() + { + /* ensure the old symbol manager is deleted */ + d_symman.reset(nullptr); + d_solver.reset(new api::Solver(&d_options)); + } + + /* Set up declaration context for expr inputs */ + void setupContext(ParserState& parser) + { + /* a, b, c: BOOLEAN */ + parser.bindVar("a", d_solver.get()->getBooleanSort()); + parser.bindVar("b", d_solver.get()->getBooleanSort()); + parser.bindVar("c", d_solver.get()->getBooleanSort()); + /* t, u, v: TYPE */ + api::Sort t = parser.mkSort("t"); + api::Sort u = parser.mkSort("u"); + api::Sort v = parser.mkSort("v"); + /* f : t->u; g: u->v; h: v->t; */ + parser.bindVar("f", d_solver.get()->mkFunctionSort(t, u)); + parser.bindVar("g", d_solver.get()->mkFunctionSort(u, v)); + parser.bindVar("h", d_solver.get()->mkFunctionSort(v, t)); + /* x:t; y:u; z:v; */ + parser.bindVar("x", t); + parser.bindVar("y", u); + parser.bindVar("z", v); + } + + void tryGoodInput(const std::string goodInput) + { + d_symman.reset(new SymbolManager(d_solver.get())); + Parser parser(d_solver.get(), d_symman.get(), d_options); + std::unique_ptr<InputParser> inputParser = + parser.parseString("test", goodInput); + ASSERT_FALSE(inputParser->done()); + std::unique_ptr<Command> cmd; + do + { + cmd.reset(inputParser->nextCommand()); + Debug("parser") << "Parsed command: " << (*cmd) << std::endl; + } while (cmd != nullptr); + ASSERT_TRUE(inputParser->done()); + } + + void tryBadInput(const std::string badInput, bool strictMode = false) + { + d_options.set(options::strictParsing, strictMode); + d_symman.reset(new SymbolManager(d_solver.get())); + Parser parser(d_solver.get(), d_symman.get(), d_options); + std::unique_ptr<InputParser> inputParser = + parser.parseString("test", badInput); + ASSERT_THROW( + { + std::unique_ptr<Command> cmd; + do + { + cmd.reset(inputParser->nextCommand()); + Debug("parser") << "Parsed command: " << (*cmd) << std::endl; + } while (cmd != nullptr); + std::cout << "\nBad input succeeded:\n" << badInput << std::endl; + }, + ParserException); + } + + void tryGoodExpr(const std::string goodExpr) + { + d_symman.reset(new SymbolManager(d_solver.get())); + Parser parser(d_solver.get(), d_symman.get(), d_options); + std::unique_ptr<InputParser> inputParser = + parser.parseString("test", goodExpr); + if (d_lang == LANG_SMTLIB_V2) + { + /* Use QF_LIA to make multiplication ("*") available */ + std::unique_ptr<Command> cmd( + static_cast<Smt2*>(parser.d_state.get())->setLogic("QF_LIA")); + } + + ASSERT_FALSE(inputParser->done()); + setupContext(*parser.d_state.get()); + ASSERT_FALSE(inputParser->done()); + api::Term e = inputParser->nextExpression(); + ASSERT_FALSE(e.isNull()); + e = inputParser->nextExpression(); + ASSERT_TRUE(inputParser->done()); + ASSERT_TRUE(e.isNull()); + } + + /** + * NOTE: The check implemented here may fail if a bad expression + * expression string has a prefix that is parseable as a good + * expression. E.g., the bad SMT v2 expression "#b10@@@@@@" will + * actually return the bit-vector 10 and ignore the tail of the + * input. It's more trouble than it's worth to check that the whole + * input was consumed here, so just be careful to avoid valid + * prefixes in tests. + */ + void tryBadExpr(const std::string badExpr, bool strictMode = false) + { + d_symman.reset(new SymbolManager(d_solver.get())); + Parser parser(d_solver.get(), d_symman.get(), d_options); + std::unique_ptr<InputParser> inputParser = + parser.parseString("test", badExpr); + setupContext(*parser.d_state.get()); + ASSERT_FALSE(inputParser->done()); + ASSERT_THROW(api::Term e = inputParser->nextExpression(); + std::cout << std::endl + << "Bad expr succeeded." << std::endl + << "Input: <<" << badExpr << ">>" << std::endl + << "Output: <<" << e << ">>" << std::endl; + , ParserException); + } + + Options d_options; + InputLanguage d_lang; + std::unique_ptr<cvc5::api::Solver> d_solver; + std::unique_ptr<SymbolManager> d_symman; +}; + +/* -------------------------------------------------------------------------- */ + +class TestParserWhiteCvcInputParser : public TestParserWhiteInputParser +{ + protected: + TestParserWhiteCvcInputParser() : TestParserWhiteInputParser(LANG_CVC) {} +}; + +TEST_F(TestParserWhiteCvcInputParser, good_inputs) +{ + tryGoodInput(""); // empty string is OK + tryGoodInput(";"); // no command is OK + tryGoodInput("ASSERT TRUE;"); + tryGoodInput("QUERY TRUE;"); + tryGoodInput("CHECKSAT FALSE;"); + tryGoodInput("a, b : BOOLEAN;"); + tryGoodInput("a, b : BOOLEAN; QUERY (a => b) AND a => b;"); + tryGoodInput("T, U : TYPE; f : T -> U; x : T; y : U; CHECKSAT f(x) = y;"); + tryGoodInput("T : TYPE = BOOLEAN; x : T; CHECKSAT x;"); + tryGoodInput("a : ARRAY INT OF REAL; ASSERT (a WITH [1] := 0.0)[1] = a[0];"); + tryGoodInput("b : BITVECTOR(3); ASSERT b = 0bin101;"); + tryGoodInput("T : TYPE = BOOLEAN; x : T; CHECKSAT x;"); + tryGoodInput( + "T : TYPE; x, y : T; a : BOOLEAN; QUERY (IF a THEN x ELSE y ENDIF) = x;"); + tryGoodInput("CHECKSAT 0bin0000 /= 0hex7;"); + tryGoodInput("%% nothing but a comment"); + tryGoodInput("% a comment\nASSERT TRUE; %a command\n% another comment"); + tryGoodInput("a : BOOLEAN; a: BOOLEAN;"); // double decl, but compatible + tryGoodInput("a : INT = 5; a: INT;"); // decl after define, compatible + tryGoodInput( + "a : TYPE; a : INT;"); // ok, sort and variable symbol spaces distinct + tryGoodInput( + "a : TYPE; a : INT; b : a;"); // ok except a is both INT and sort `a' + tryGoodInput( + "DATATYPE list = nil | cons(car:INT,cdr:list) END; DATATYPE cons = null " + "END;"); + tryGoodInput( + "DATATYPE tree = node(data:list), list = cons(car:tree,cdr:list) | nil " + "END;"); + tryGoodInput( + "DATATYPE trex = Foo | Bar END; DATATYPE tree = " + "node(data:[list,list,ARRAY trex OF list]), list = cons(car:ARRAY list " + "OF tree,cdr:BITVECTOR(32)) END;"); +} + +TEST_F(TestParserWhiteCvcInputParser, bad_inputs) +{ +// competition builds don't do any checking +#ifndef CVC5_COMPETITION_MODE + tryBadInput("ASSERT;"); // no args + tryBadInput("QUERY"); + tryBadInput("CHECKSAT"); + tryBadInput("a, b : boolean;"); // lowercase boolean isn't a type + tryBadInput("0x : INT;"); // 0x isn't an identifier + tryBadInput( + "a, b : BOOLEAN\nQUERY (a => b) AND a => b;"); // no semicolon after decl + tryBadInput("ASSERT 0bin012 /= 0hex0;"); // bad binary literal + tryBadInput("a, b: BOOLEAN; QUERY a(b);"); // non-function used as function + tryBadInput("a : BOOLEAN; a: INT;"); // double decl, incompatible + tryBadInput("A : TYPE; A: TYPE;"); // types can't be double-declared + tryBadInput("a : INT; a: INT = 5;"); // can't define after decl + tryBadInput("a : INT = 5; a: BOOLEAN;"); // decl w/ incompatible type + tryBadInput( + "a : TYPE; a : INT; a : a;"); // ok except a is both INT and sort `a' + tryBadInput( + "DATATYPE list = nil | cons(car:INT,cdr:list) END; DATATYPE list = nil | " + "cons(car:INT,cdr:list) END;"); + tryBadInput( + "DATATYPE list = nil | cons(car:INT,cdr:list) END; DATATYPE list2 = nil " + "END;"); + tryBadInput( + "DATATYPE tree = node(data:(list,list,ARRAY trex OF list)), list = " + "cons(car:ARRAY list OF tree,cdr:BITVECTOR(32)) END;"); +#endif +} + +TEST_F(TestParserWhiteCvcInputParser, good_exprs) +{ + tryGoodExpr("a AND b"); + tryGoodExpr("a AND b OR c"); + tryGoodExpr("(a => b) AND a => b"); + tryGoodExpr("(a <=> b) AND (NOT a)"); + tryGoodExpr("(a XOR b) <=> (a OR b) AND (NOT (a AND b))"); +} + +TEST_F(TestParserWhiteCvcInputParser, bad_exprs) +{ +// competition builds don't do any checking +#ifndef CVC5_COMPETITION_MODE + tryBadInput("a AND"); // wrong arity + tryBadInput("AND(a,b)"); // not infix + tryBadInput("(OR (AND a b) c)"); // not infix + tryBadInput("a IMPLIES b"); // should be => + tryBadInput("a NOT b"); // wrong arity, not infix + tryBadInput("a and b"); // wrong case +#endif +} + +/* -------------------------------------------------------------------------- */ + +class TestParserWhiteSmt2InputParser : public TestParserWhiteInputParser +{ + protected: + TestParserWhiteSmt2InputParser() : TestParserWhiteInputParser(LANG_SMTLIB_V2) + { + } +}; + +TEST_F(TestParserWhiteSmt2InputParser, good_inputs) +{ + tryGoodInput(""); // empty string is OK + tryGoodInput("(set-logic QF_UF)"); + tryGoodInput("(set-info :notes |This is a note, take note!|)"); + tryGoodInput("(set-logic QF_UF) (assert true)"); + tryGoodInput("(check-sat)"); + tryGoodInput("(exit)"); + tryGoodInput("(set-logic QF_UF) (assert false) (check-sat)"); + tryGoodInput( + "(set-logic QF_UF) (declare-fun a () Bool) " + "(declare-fun b () Bool)"); + tryGoodInput( + "(set-logic QF_UF) (declare-fun a () Bool) " + "(declare-fun b () Bool) (assert (=> (and (=> a b) a) b))"); + tryGoodInput( + "(set-logic QF_UF) (declare-sort a 0) " + "(declare-fun f (a) a) (declare-fun x () a) " + "(assert (= (f x) x))"); + tryGoodInput( + "(set-logic QF_UF) (declare-sort a 0) " + "(declare-fun x () a) (declare-fun y () a) " + "(assert (= (ite true x y) x))"); + tryGoodInput(";; nothing but a comment"); + tryGoodInput("; a comment\n(check-sat ; goodbye\n)"); +} + +TEST_F(TestParserWhiteSmt2InputParser, bad_inputs) +{ + // competition builds don't do any checking +#ifndef CVC5_COMPETITION_MODE + // no arguments + tryBadInput("(assert)"); + // illegal character in symbol + tryBadInput("(set-info :notes |Symbols can't contain the | character|)"); + // check-sat should not have an argument + tryBadInput("(set-logic QF_UF) (check-sat true)", true); + // no argument + tryBadInput("(declare-sort a)"); + // double declaration + tryBadInput("(declare-sort a 0) (declare-sort a 0)"); + // should be "(declare-fun p () Bool)" + tryBadInput("(set-logic QF_UF) (declare-fun p Bool)"); + // strict mode + // no set-logic, core theory symbol "true" undefined + tryBadInput("(assert true)", true); + // core theory symbol "Bool" undefined + tryBadInput("(declare-fun p Bool)", true); +#endif +} + +TEST_F(TestParserWhiteSmt2InputParser, good_exprs) +{ + tryGoodExpr("(and a b)"); + tryGoodExpr("(or (and a b) c)"); + tryGoodExpr("(=> (and (=> a b) a) b)"); + tryGoodExpr("(and (= a b) (not a))"); + tryGoodExpr("(= (xor a b) (and (or a b) (not (and a b))))"); + tryGoodExpr("(ite a (f x) y)"); + tryGoodExpr("1"); + tryGoodExpr("0"); + tryGoodExpr("1.5"); + tryGoodExpr("#xfab09c7"); + tryGoodExpr("#b0001011"); + tryGoodExpr("(* 5 1)"); +} + +TEST_F(TestParserWhiteSmt2InputParser, bad_exprs) +{ +// competition builds don't do any checking +#ifndef CVC5_COMPETITION_MODE + tryBadExpr("(and)"); // wrong arity + tryBadExpr("(and a b"); // no closing paren + tryBadExpr("(a and b)"); // infix + tryBadExpr("(implies a b)"); // no implies in v2 + tryBadExpr("(iff a b)"); // no iff in v2 + tryBadExpr("(OR (AND a b) c)"); // wrong case + tryBadExpr("(a IMPLIES b)"); // infix AND wrong case + tryBadExpr("(not a b)"); // wrong arity + tryBadExpr("not a"); // needs parens + tryBadExpr("(ite a x)"); // wrong arity + tryBadExpr("(if_then_else a (f x) y)"); // no if_then_else in v2 + tryBadExpr("(a b)"); // using non-function as function + tryBadExpr(".5"); // rational constants must have integer prefix + tryBadExpr("1."); // rational constants must have fractional suffix + tryBadExpr("#x"); // hex constants must have at least one digit + tryBadExpr("#b"); // ditto binary constants + tryBadExpr("#xg0f"); + tryBadExpr("#b9"); + // Bad strict exprs + tryBadExpr("(and a)", true); // no unary and's + tryBadExpr("(or a)", true); // no unary or's + tryBadExpr("(* 5 01)", true); // '01' is not a valid integer constant +#endif +} +} // namespace test +} // namespace cvc5 diff --git a/test/unit/parser/parser_black.cpp b/test/unit/parser/parser_black.cpp index a0cd0499e..6a3cc03a5 100644 --- a/test/unit/parser/parser_black.cpp +++ b/test/unit/parser/parser_black.cpp @@ -1,6 +1,6 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz, Christopher L. Conway, Morgan Deters + * Aina Niemetz, Christopher L. Conway, Tim King * * This file is part of the cvc5 project. * @@ -10,23 +10,23 @@ * directory for licensing information. * **************************************************************************** * - * Black box testing of cvc5::parser::Parser for CVC and SMT-LIbv2 inputs. + * Black box testing of cvc5::parser::ParserBuilder. */ -#include <sstream> +#include <stdio.h> +#include <string.h> +#include <sys/stat.h> +#include <unistd.h> + +#include <fstream> +#include <iostream> #include "api/cpp/cvc5.h" -#include "base/output.h" #include "expr/symbol_manager.h" -#include "options/base_options.h" #include "options/language.h" -#include "options/options.h" #include "parser/input_parser.h" #include "parser/parser.h" -#include "parser/parser_builder.h" -#include "parser/smt2/smt2.h" -#include "smt/command.h" -#include "test.h" +#include "test_api.h" namespace cvc5 { @@ -35,359 +35,107 @@ using namespace language::input; namespace test { -class TestParserBlackParser : public TestInternal +class TestParserBlackParser : public TestApi { protected: - TestParserBlackParser(InputLanguage lang) : d_lang(lang) {} - - virtual ~TestParserBlackParser() {} - - void SetUp() override - { - TestInternal::SetUp(); - d_options.set(options::parseOnly, true); - d_symman.reset(nullptr); - d_solver.reset(new cvc5::api::Solver(&d_options)); - } + void SetUp() override { d_symman.reset(new SymbolManager(&d_solver)); } - void TearDown() override + void checkEmptyInput(InputParser* inputParser) { - d_symman.reset(nullptr); - d_solver.reset(nullptr); - } - - void setUp() - { - /* ensure the old symbol manager is deleted */ - d_symman.reset(nullptr); - d_solver.reset(new api::Solver(&d_options)); - } - - /* Set up declaration context for expr inputs */ - void setupContext(Parser& parser) - { - /* a, b, c: BOOLEAN */ - parser.bindVar("a", d_solver.get()->getBooleanSort()); - parser.bindVar("b", d_solver.get()->getBooleanSort()); - parser.bindVar("c", d_solver.get()->getBooleanSort()); - /* t, u, v: TYPE */ - api::Sort t = parser.mkSort("t"); - api::Sort u = parser.mkSort("u"); - api::Sort v = parser.mkSort("v"); - /* f : t->u; g: u->v; h: v->t; */ - parser.bindVar("f", d_solver.get()->mkFunctionSort(t, u)); - parser.bindVar("g", d_solver.get()->mkFunctionSort(u, v)); - parser.bindVar("h", d_solver.get()->mkFunctionSort(v, t)); - /* x:t; y:u; z:v; */ - parser.bindVar("x", t); - parser.bindVar("y", u); - parser.bindVar("z", v); - } - - void tryGoodInput(const std::string goodInput) - { - d_symman.reset(new SymbolManager(d_solver.get())); - std::unique_ptr<Parser> parser(ParserBuilder(d_solver.get(), d_symman.get()) - .withOptions(d_options) - .withInputLanguage(d_lang) - .build()); - std::unique_ptr<InputParser> inputParser = - parser->parseString("test", goodInput); - ASSERT_FALSE(parser->done()); - Command* cmd; - while ((cmd = inputParser->nextCommand()) != NULL) - { - Debug("parser") << "Parsed command: " << (*cmd) << std::endl; - delete cmd; - } - - ASSERT_TRUE(parser->done()); - } - - void tryBadInput(const std::string badInput, bool strictMode = false) - { - d_symman.reset(new SymbolManager(d_solver.get())); - std::unique_ptr<Parser> parser(ParserBuilder(d_solver.get(), d_symman.get()) - .withOptions(d_options) - .withInputLanguage(d_lang) - .withStrictMode(strictMode) - .build()); - std::unique_ptr<InputParser> inputParser = - parser->parseString("test", badInput); - ASSERT_THROW( - { - Command* cmd; - while ((cmd = inputParser->nextCommand()) != NULL) - { - Debug("parser") << "Parsed command: " << (*cmd) << std::endl; - delete cmd; - } - std::cout << "\nBad input succeeded:\n" << badInput << std::endl; - }, - ParserException); + api::Term e = inputParser->nextExpression(); + ASSERT_TRUE(e.isNull()); } - void tryGoodExpr(const std::string goodExpr) + void checkTrueInput(InputParser* inputParser) { - d_symman.reset(new SymbolManager(d_solver.get())); - std::unique_ptr<Parser> parser(ParserBuilder(d_solver.get(), d_symman.get()) - .withOptions(d_options) - .withInputLanguage(d_lang) - .build()); - std::unique_ptr<InputParser> inputParser = - parser->parseString("test", goodExpr); - if (d_lang == LANG_SMTLIB_V2) - { - /* Use QF_LIA to make multiplication ("*") available */ - std::unique_ptr<Command> cmd( - static_cast<Smt2*>(parser.get())->setLogic("QF_LIA")); - } - - ASSERT_FALSE(parser->done()); - setupContext(*parser); - ASSERT_FALSE(parser->done()); api::Term e = inputParser->nextExpression(); - ASSERT_FALSE(e.isNull()); + ASSERT_EQ(e, d_solver.mkTrue()); + e = inputParser->nextExpression(); - ASSERT_TRUE(parser->done()); ASSERT_TRUE(e.isNull()); } - /** - * NOTE: The check implemented here may fail if a bad expression - * expression string has a prefix that is parseable as a good - * expression. E.g., the bad SMT v2 expression "#b10@@@@@@" will - * actually return the bit-vector 10 and ignore the tail of the - * input. It's more trouble than it's worth to check that the whole - * input was consumed here, so just be careful to avoid valid - * prefixes in tests. - */ - void tryBadExpr(const std::string badExpr, bool strictMode = false) + char* mkTemp() { - d_symman.reset(new SymbolManager(d_solver.get())); - std::unique_ptr<Parser> parser(ParserBuilder(d_solver.get(), d_symman.get()) - .withOptions(d_options) - .withInputLanguage(d_lang) - .withStrictMode(strictMode) - .build()); - std::unique_ptr<InputParser> inputParser = - parser->parseString("test", badExpr); - setupContext(*parser); - ASSERT_FALSE(parser->done()); - ASSERT_THROW(api::Term e = inputParser->nextExpression(); - std::cout << std::endl - << "Bad expr succeeded." << std::endl - << "Input: <<" << badExpr << ">>" << std::endl - << "Output: <<" << e << ">>" << std::endl; - , ParserException); + char* filename = strdup("/tmp/testinput.XXXXXX"); + int32_t fd = mkstemp(filename); + if (fd == -1) return nullptr; + close(fd); + return filename; } - - Options d_options; - InputLanguage d_lang; - std::unique_ptr<cvc5::api::Solver> d_solver; std::unique_ptr<SymbolManager> d_symman; }; -/* -------------------------------------------------------------------------- */ - -class TestParserBlackCvCParser : public TestParserBlackParser +TEST_F(TestParserBlackParser, empty_file_input) { - protected: - TestParserBlackCvCParser() : TestParserBlackParser(LANG_CVC) {} -}; + char* filename = mkTemp(); + ASSERT_NE(filename, nullptr); -TEST_F(TestParserBlackCvCParser, good_inputs) -{ - tryGoodInput(""); // empty string is OK - tryGoodInput(";"); // no command is OK - tryGoodInput("ASSERT TRUE;"); - tryGoodInput("QUERY TRUE;"); - tryGoodInput("CHECKSAT FALSE;"); - tryGoodInput("a, b : BOOLEAN;"); - tryGoodInput("a, b : BOOLEAN; QUERY (a => b) AND a => b;"); - tryGoodInput("T, U : TYPE; f : T -> U; x : T; y : U; CHECKSAT f(x) = y;"); - tryGoodInput("T : TYPE = BOOLEAN; x : T; CHECKSAT x;"); - tryGoodInput("a : ARRAY INT OF REAL; ASSERT (a WITH [1] := 0.0)[1] = a[0];"); - tryGoodInput("b : BITVECTOR(3); ASSERT b = 0bin101;"); - tryGoodInput("T : TYPE = BOOLEAN; x : T; CHECKSAT x;"); - tryGoodInput( - "T : TYPE; x, y : T; a : BOOLEAN; QUERY (IF a THEN x ELSE y ENDIF) = x;"); - tryGoodInput("CHECKSAT 0bin0000 /= 0hex7;"); - tryGoodInput("%% nothing but a comment"); - tryGoodInput("% a comment\nASSERT TRUE; %a command\n% another comment"); - tryGoodInput("a : BOOLEAN; a: BOOLEAN;"); // double decl, but compatible - tryGoodInput("a : INT = 5; a: INT;"); // decl after define, compatible - tryGoodInput( - "a : TYPE; a : INT;"); // ok, sort and variable symbol spaces distinct - tryGoodInput( - "a : TYPE; a : INT; b : a;"); // ok except a is both INT and sort `a' - tryGoodInput( - "DATATYPE list = nil | cons(car:INT,cdr:list) END; DATATYPE cons = null " - "END;"); - tryGoodInput( - "DATATYPE tree = node(data:list), list = cons(car:tree,cdr:list) | nil " - "END;"); - tryGoodInput( - "DATATYPE trex = Foo | Bar END; DATATYPE tree = " - "node(data:[list,list,ARRAY trex OF list]), list = cons(car:ARRAY list " - "OF tree,cdr:BITVECTOR(32)) END;"); -} + Options options; + options.setInputLanguage(LANG_CVC); + Parser parser(&d_solver, d_symman.get(), options); + std::unique_ptr<InputParser> inputParser = parser.parseFile(filename, false); + checkEmptyInput(inputParser.get()); -TEST_F(TestParserBlackCvCParser, bad_inputs) -{ -// competition builds don't do any checking -#ifndef CVC5_COMPETITION_MODE - tryBadInput("ASSERT;"); // no args - tryBadInput("QUERY"); - tryBadInput("CHECKSAT"); - tryBadInput("a, b : boolean;"); // lowercase boolean isn't a type - tryBadInput("0x : INT;"); // 0x isn't an identifier - tryBadInput( - "a, b : BOOLEAN\nQUERY (a => b) AND a => b;"); // no semicolon after decl - tryBadInput("ASSERT 0bin012 /= 0hex0;"); // bad binary literal - tryBadInput("a, b: BOOLEAN; QUERY a(b);"); // non-function used as function - tryBadInput("a : BOOLEAN; a: INT;"); // double decl, incompatible - tryBadInput("A : TYPE; A: TYPE;"); // types can't be double-declared - tryBadInput("a : INT; a: INT = 5;"); // can't define after decl - tryBadInput("a : INT = 5; a: BOOLEAN;"); // decl w/ incompatible type - tryBadInput( - "a : TYPE; a : INT; a : a;"); // ok except a is both INT and sort `a' - tryBadInput( - "DATATYPE list = nil | cons(car:INT,cdr:list) END; DATATYPE list = nil | " - "cons(car:INT,cdr:list) END;"); - tryBadInput( - "DATATYPE list = nil | cons(car:INT,cdr:list) END; DATATYPE list2 = nil " - "END;"); - tryBadInput( - "DATATYPE tree = node(data:(list,list,ARRAY trex OF list)), list = " - "cons(car:ARRAY list OF tree,cdr:BITVECTOR(32)) END;"); -#endif + remove(filename); + free(filename); } -TEST_F(TestParserBlackCvCParser, good_exprs) +TEST_F(TestParserBlackParser, simple_file_input) { - tryGoodExpr("a AND b"); - tryGoodExpr("a AND b OR c"); - tryGoodExpr("(a => b) AND a => b"); - tryGoodExpr("(a <=> b) AND (NOT a)"); - tryGoodExpr("(a XOR b) <=> (a OR b) AND (NOT (a AND b))"); -} + char* filename = mkTemp(); -TEST_F(TestParserBlackCvCParser, bad_exprs) -{ -// competition builds don't do any checking -#ifndef CVC5_COMPETITION_MODE - tryBadInput("a AND"); // wrong arity - tryBadInput("AND(a,b)"); // not infix - tryBadInput("(OR (AND a b) c)"); // not infix - tryBadInput("a IMPLIES b"); // should be => - tryBadInput("a NOT b"); // wrong arity, not infix - tryBadInput("a and b"); // wrong case -#endif -} + std::fstream fs(filename, std::fstream::out); + fs << "TRUE" << std::endl; + fs.close(); -/* -------------------------------------------------------------------------- */ + Options options; + options.setInputLanguage(LANG_CVC); + Parser parser(&d_solver, d_symman.get(), options); + std::unique_ptr<InputParser> inputParser = parser.parseFile(filename, false); + checkTrueInput(inputParser.get()); -class TestParserBlackSmt2Parser : public TestParserBlackParser -{ - protected: - TestParserBlackSmt2Parser() : TestParserBlackParser(LANG_SMTLIB_V2) {} -}; + remove(filename); + free(filename); +} -TEST_F(TestParserBlackSmt2Parser, good_inputs) +TEST_F(TestParserBlackParser, empty_string_input) { - tryGoodInput(""); // empty string is OK - tryGoodInput("(set-logic QF_UF)"); - tryGoodInput("(set-info :notes |This is a note, take note!|)"); - tryGoodInput("(set-logic QF_UF) (assert true)"); - tryGoodInput("(check-sat)"); - tryGoodInput("(exit)"); - tryGoodInput("(set-logic QF_UF) (assert false) (check-sat)"); - tryGoodInput( - "(set-logic QF_UF) (declare-fun a () Bool) " - "(declare-fun b () Bool)"); - tryGoodInput( - "(set-logic QF_UF) (declare-fun a () Bool) " - "(declare-fun b () Bool) (assert (=> (and (=> a b) a) b))"); - tryGoodInput( - "(set-logic QF_UF) (declare-sort a 0) " - "(declare-fun f (a) a) (declare-fun x () a) " - "(assert (= (f x) x))"); - tryGoodInput( - "(set-logic QF_UF) (declare-sort a 0) " - "(declare-fun x () a) (declare-fun y () a) " - "(assert (= (ite true x y) x))"); - tryGoodInput(";; nothing but a comment"); - tryGoodInput("; a comment\n(check-sat ; goodbye\n)"); + Options options; + options.setInputLanguage(LANG_CVC); + Parser parser(&d_solver, d_symman.get(), options); + std::unique_ptr<InputParser> inputParser = parser.parseString("foo", ""); + checkEmptyInput(inputParser.get()); } -TEST_F(TestParserBlackSmt2Parser, bad_inputs) +TEST_F(TestParserBlackParser, true_string_input) { - // competition builds don't do any checking -#ifndef CVC5_COMPETITION_MODE - // no arguments - tryBadInput("(assert)"); - // illegal character in symbol - tryBadInput("(set-info :notes |Symbols can't contain the | character|)"); - // check-sat should not have an argument - tryBadInput("(set-logic QF_UF) (check-sat true)", true); - // no argument - tryBadInput("(declare-sort a)"); - // double declaration - tryBadInput("(declare-sort a 0) (declare-sort a 0)"); - // should be "(declare-fun p () Bool)" - tryBadInput("(set-logic QF_UF) (declare-fun p Bool)"); - // strict mode - // no set-logic, core theory symbol "true" undefined - tryBadInput("(assert true)", true); - // core theory symbol "Bool" undefined - tryBadInput("(declare-fun p Bool)", true); -#endif + Options options; + options.setInputLanguage(LANG_CVC); + Parser parser(&d_solver, d_symman.get(), options); + std::unique_ptr<InputParser> inputParser = parser.parseString("foo", "TRUE"); + checkTrueInput(inputParser.get()); } -TEST_F(TestParserBlackSmt2Parser, good_exprs) +TEST_F(TestParserBlackParser, empty_stream_input) { - tryGoodExpr("(and a b)"); - tryGoodExpr("(or (and a b) c)"); - tryGoodExpr("(=> (and (=> a b) a) b)"); - tryGoodExpr("(and (= a b) (not a))"); - tryGoodExpr("(= (xor a b) (and (or a b) (not (and a b))))"); - tryGoodExpr("(ite a (f x) y)"); - tryGoodExpr("1"); - tryGoodExpr("0"); - tryGoodExpr("1.5"); - tryGoodExpr("#xfab09c7"); - tryGoodExpr("#b0001011"); - tryGoodExpr("(* 5 1)"); + std::stringstream ss("", std::ios_base::in); + Options options; + options.setInputLanguage(LANG_CVC); + Parser parser(&d_solver, d_symman.get(), options); + std::unique_ptr<InputParser> inputParser = parser.parseStream("foo", ss); + checkEmptyInput(inputParser.get()); } -TEST_F(TestParserBlackSmt2Parser, bad_exprs) +TEST_F(TestParserBlackParser, true_stream_input) { -// competition builds don't do any checking -#ifndef CVC5_COMPETITION_MODE - tryBadExpr("(and)"); // wrong arity - tryBadExpr("(and a b"); // no closing paren - tryBadExpr("(a and b)"); // infix - tryBadExpr("(implies a b)"); // no implies in v2 - tryBadExpr("(iff a b)"); // no iff in v2 - tryBadExpr("(OR (AND a b) c)"); // wrong case - tryBadExpr("(a IMPLIES b)"); // infix AND wrong case - tryBadExpr("(not a b)"); // wrong arity - tryBadExpr("not a"); // needs parens - tryBadExpr("(ite a x)"); // wrong arity - tryBadExpr("(if_then_else a (f x) y)"); // no if_then_else in v2 - tryBadExpr("(a b)"); // using non-function as function - tryBadExpr(".5"); // rational constants must have integer prefix - tryBadExpr("1."); // rational constants must have fractional suffix - tryBadExpr("#x"); // hex constants must have at least one digit - tryBadExpr("#b"); // ditto binary constants - tryBadExpr("#xg0f"); - tryBadExpr("#b9"); - // Bad strict exprs - tryBadExpr("(and a)", true); // no unary and's - tryBadExpr("(or a)", true); // no unary or's - tryBadExpr("(* 5 01)", true); // '01' is not a valid integer constant -#endif + std::stringstream ss("TRUE", std::ios_base::in); + Options options; + options.setInputLanguage(LANG_CVC); + Parser parser(&d_solver, d_symman.get(), options); + std::unique_ptr<InputParser> inputParser = parser.parseStream("foo", ss); + checkTrueInput(inputParser.get()); } + } // namespace test } // namespace cvc5 diff --git a/test/unit/parser/parser_builder_black.cpp b/test/unit/parser/parser_builder_black.cpp deleted file mode 100644 index f8d29efbe..000000000 --- a/test/unit/parser/parser_builder_black.cpp +++ /dev/null @@ -1,142 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Aina Niemetz, Christopher L. Conway, Tim King - * - * This file is part of the cvc5 project. - * - * 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. - * **************************************************************************** - * - * Black box testing of cvc5::parser::ParserBuilder. - */ - -#include <stdio.h> -#include <string.h> -#include <sys/stat.h> -#include <unistd.h> - -#include <fstream> -#include <iostream> - -#include "api/cpp/cvc5.h" -#include "expr/symbol_manager.h" -#include "options/language.h" -#include "parser/input_parser.h" -#include "parser/parser.h" -#include "parser/parser_builder.h" -#include "test_api.h" - -namespace cvc5 { - -using namespace parser; -using namespace language::input; - -namespace test { - -class TestParseBlackParserBuilder : public TestApi -{ - protected: - void SetUp() override { d_symman.reset(new SymbolManager(&d_solver)); } - - void checkEmptyInput(InputParser* inputParser) - { - api::Term e = inputParser->nextExpression(); - ASSERT_TRUE(e.isNull()); - } - - void checkTrueInput(InputParser* inputParser) - { - api::Term e = inputParser->nextExpression(); - ASSERT_EQ(e, d_solver.mkTrue()); - - e = inputParser->nextExpression(); - ASSERT_TRUE(e.isNull()); - } - - char* mkTemp() - { - char* filename = strdup("/tmp/testinput.XXXXXX"); - int32_t fd = mkstemp(filename); - if (fd == -1) return nullptr; - close(fd); - return filename; - } - std::unique_ptr<SymbolManager> d_symman; -}; - -TEST_F(TestParseBlackParserBuilder, empty_file_input) -{ - char* filename = mkTemp(); - ASSERT_NE(filename, nullptr); - - std::unique_ptr<Parser> parser(ParserBuilder(&d_solver, d_symman.get()) - .withInputLanguage(LANG_CVC) - .build()); - std::unique_ptr<InputParser> inputParser = parser->parseFile(filename, false); - checkEmptyInput(inputParser.get()); - - remove(filename); - free(filename); -} - -TEST_F(TestParseBlackParserBuilder, simple_file_input) -{ - char* filename = mkTemp(); - - std::fstream fs(filename, std::fstream::out); - fs << "TRUE" << std::endl; - fs.close(); - - std::unique_ptr<Parser> parser(ParserBuilder(&d_solver, d_symman.get()) - .withInputLanguage(LANG_CVC) - .build()); - std::unique_ptr<InputParser> inputParser = parser->parseFile(filename, false); - checkTrueInput(inputParser.get()); - - remove(filename); - free(filename); -} - -TEST_F(TestParseBlackParserBuilder, empty_string_input) -{ - std::unique_ptr<Parser> parser(ParserBuilder(&d_solver, d_symman.get()) - .withInputLanguage(LANG_CVC) - .build()); - std::unique_ptr<InputParser> inputParser = parser->parseString("foo", ""); - checkEmptyInput(inputParser.get()); -} - -TEST_F(TestParseBlackParserBuilder, true_string_input) -{ - std::unique_ptr<Parser> parser(ParserBuilder(&d_solver, d_symman.get()) - .withInputLanguage(LANG_CVC) - .build()); - std::unique_ptr<InputParser> inputParser = parser->parseString("foo", "TRUE"); - checkTrueInput(inputParser.get()); -} - -TEST_F(TestParseBlackParserBuilder, empty_stream_input) -{ - std::stringstream ss("", std::ios_base::in); - std::unique_ptr<Parser> parser(ParserBuilder(&d_solver, d_symman.get()) - .withInputLanguage(LANG_CVC) - .build()); - std::unique_ptr<InputParser> inputParser = parser->parseStream("foo", ss); - checkEmptyInput(inputParser.get()); -} - -TEST_F(TestParseBlackParserBuilder, true_stream_input) -{ - std::stringstream ss("TRUE", std::ios_base::in); - std::unique_ptr<Parser> parser(ParserBuilder(&d_solver, d_symman.get()) - .withInputLanguage(LANG_CVC) - .build()); - std::unique_ptr<InputParser> inputParser = parser->parseStream("foo", ss); - checkTrueInput(inputParser.get()); -} - -} // namespace test -} // namespace cvc5 |