summaryrefslogtreecommitdiff
path: root/test/unit
diff options
context:
space:
mode:
Diffstat (limited to 'test/unit')
-rw-r--r--test/unit/main/interactive_shell_black.cpp1
-rw-r--r--test/unit/parser/CMakeLists.txt2
-rw-r--r--test/unit/parser/input_parser_white.cpp384
-rw-r--r--test/unit/parser/parser_black.cpp400
-rw-r--r--test/unit/parser/parser_builder_black.cpp142
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback