--- /dev/null
+/********************* */
+/*! \file parser_black.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Aina Niemetz, Christopher L. Conway, Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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.\endverbatim
+ **
+ ** \brief Black box testing of CVC4::parser::Parser for CVC and SMT-LIBv2
+ ** inputs.
+ **
+ ** Black box testing of CVC4::parser::Parser for CVC and SMT-LIbv2 inputs.
+ **/
+
+#include <sstream>
+
+#include "api/cvc4cpp.h"
+#include "base/output.h"
+#include "expr/expr.h"
+#include "expr/expr_manager.h"
+#include "expr/symbol_manager.h"
+#include "options/base_options.h"
+#include "options/language.h"
+#include "options/options.h"
+#include "parser/parser.h"
+#include "parser/parser_builder.h"
+#include "parser/smt2/smt2.h"
+#include "smt/command.h"
+#include "test.h"
+
+namespace CVC4 {
+
+using namespace parser;
+using namespace language::input;
+
+namespace test {
+
+class TestParserBlackParser : public TestInternal
+{
+ 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 CVC4::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(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()));
+ Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test")
+ .withStringInput(goodInput)
+ .withOptions(d_options)
+ .withInputLanguage(d_lang)
+ .build();
+ ASSERT_FALSE(parser->done());
+ Command* cmd;
+ while ((cmd = parser->nextCommand()) != NULL)
+ {
+ Debug("parser") << "Parsed command: " << (*cmd) << std::endl;
+ delete cmd;
+ }
+
+ ASSERT_TRUE(parser->done());
+ delete parser;
+ }
+
+ void tryBadInput(const std::string badInput, bool strictMode = false)
+ {
+ d_symman.reset(new SymbolManager(d_solver.get()));
+ Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test")
+ .withStringInput(badInput)
+ .withOptions(d_options)
+ .withInputLanguage(d_lang)
+ .withStrictMode(strictMode)
+ .build();
+ ASSERT_THROW(
+ {
+ Command* cmd;
+ while ((cmd = parser->nextCommand()) != NULL)
+ {
+ Debug("parser") << "Parsed command: " << (*cmd) << std::endl;
+ delete cmd;
+ }
+ std::cout << "\nBad input succeeded:\n" << badInput << std::endl;
+ },
+ ParserException);
+ delete parser;
+ }
+
+ void tryGoodExpr(const std::string goodExpr)
+ {
+ d_symman.reset(new SymbolManager(d_solver.get()));
+ Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test")
+ .withStringInput(goodExpr)
+ .withOptions(d_options)
+ .withInputLanguage(d_lang)
+ .build();
+
+ if (d_lang == LANG_SMTLIB_V2)
+ {
+ /* Use QF_LIA to make multiplication ("*") available */
+ std::unique_ptr<Command> cmd(
+ static_cast<Smt2*>(parser)->setLogic("QF_LIA"));
+ }
+
+ ASSERT_FALSE(parser->done());
+ setupContext(*parser);
+ ASSERT_FALSE(parser->done());
+ api::Term e = parser->nextExpression();
+ ASSERT_FALSE(e.isNull());
+ e = parser->nextExpression();
+ ASSERT_TRUE(parser->done());
+ ASSERT_TRUE(e.isNull());
+ delete parser;
+ }
+
+ /**
+ * 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 = ParserBuilder(d_solver.get(), d_symman.get(), "test")
+ .withStringInput(badExpr)
+ .withOptions(d_options)
+ .withInputLanguage(d_lang)
+ .withStrictMode(strictMode)
+ .build();
+ setupContext(*parser);
+ ASSERT_FALSE(parser->done());
+ ASSERT_THROW(api::Term e = parser->nextExpression();
+ std::cout << std::endl
+ << "Bad expr succeeded." << std::endl
+ << "Input: <<" << badExpr << ">>" << std::endl
+ << "Output: <<" << e << ">>" << std::endl;
+ , ParserException);
+ delete parser;
+ }
+
+ Options d_options;
+ InputLanguage d_lang;
+ std::unique_ptr<CVC4::api::Solver> d_solver;
+ std::unique_ptr<SymbolManager> d_symman;
+};
+
+/* -------------------------------------------------------------------------- */
+
+class TestParserBlackCvCParser : public TestParserBlackParser
+{
+ protected:
+ TestParserBlackCvCParser() : TestParserBlackParser(LANG_CVC4) {}
+};
+
+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;");
+}
+
+TEST_F(TestParserBlackCvCParser, bad_inputs)
+{
+// competition builds don't do any checking
+#ifndef CVC4_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(TestParserBlackCvCParser, 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(TestParserBlackCvCParser, bad_exprs)
+{
+// competition builds don't do any checking
+#ifndef CVC4_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 TestParserBlackSmt2Parser : public TestParserBlackParser
+{
+ protected:
+ TestParserBlackSmt2Parser() : TestParserBlackParser(LANG_SMTLIB_V2) {}
+};
+
+TEST_F(TestParserBlackSmt2Parser, 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(TestParserBlackSmt2Parser, bad_inputs)
+{
+ // competition builds don't do any checking
+#ifndef CVC4_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(TestParserBlackSmt2Parser, 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(TestParserBlackSmt2Parser, bad_exprs)
+{
+// competition builds don't do any checking
+#ifndef CVC4_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 CVC4
+++ /dev/null
-/********************* */
-/*! \file parser_black.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Christopher L. Conway, Morgan Deters, Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 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.\endverbatim
- **
- ** \brief Black box testing of CVC4::parser::Parser, including CVC, SMT and
- ** SMT v2 inputs.
- **
- ** Black box testing of CVC4::parser::Parser, including CVC, SMT, and
- ** SMT v2 inputs.
- **/
-
-#include <cxxtest/TestSuite.h>
-#include <sstream>
-
-#include "api/cvc4cpp.h"
-#include "base/output.h"
-#include "expr/expr.h"
-#include "expr/expr_manager.h"
-#include "expr/symbol_manager.h"
-#include "options/base_options.h"
-#include "options/language.h"
-#include "options/options.h"
-#include "parser/parser.h"
-#include "parser/parser_builder.h"
-#include "parser/smt2/smt2.h"
-#include "smt/command.h"
-
-using namespace CVC4;
-using namespace CVC4::parser;
-using namespace CVC4::language::input;
-using namespace std;
-
-class ParserBlack
-{
- protected:
- Options d_options;
-
- /* Set up declaration context for expr inputs */
- virtual void setupContext(Parser& parser) {
- /* a, b, c: BOOLEAN */
- parser.bindVar("a", d_solver->getBooleanSort());
- parser.bindVar("b", d_solver->getBooleanSort());
- parser.bindVar("c", d_solver->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->mkFunctionSort(t, u));
- parser.bindVar("g", d_solver->mkFunctionSort(u, v));
- parser.bindVar("h", d_solver->mkFunctionSort(v, t));
- /* x:t; y:u; z:v; */
- parser.bindVar("x", t);
- parser.bindVar("y", u);
- parser.bindVar("z", v);
- }
-
- void tryGoodInput(const string goodInput)
- {
- try
- {
- // Debug.on("parser");
- // Debug.on("parser-extra");
- // cerr << "Testing good input: <<" << goodInput << ">>" << endl;
- // istringstream stream(goodInputs[i]);
- d_symman.reset(new SymbolManager(d_solver.get()));
- Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test")
- .withStringInput(goodInput)
- .withOptions(d_options)
- .withInputLanguage(d_lang)
- .build();
- TS_ASSERT(!parser->done());
- Command* cmd;
- while ((cmd = parser->nextCommand()) != NULL)
- {
- Debug("parser") << "Parsed command: " << (*cmd) << endl;
- delete cmd;
- }
-
- TS_ASSERT(parser->done());
- delete parser;
- // Debug.off("parser");
- // Debug.off("parser-extra");
- }
- catch (Exception& e)
- {
- cout << "\nGood input failed:\n" << goodInput << endl << e << endl;
- // Debug.off("parser");
- throw;
- }
- }
-
- void tryBadInput(const string badInput, bool strictMode = false)
- {
- // cerr << "Testing bad input: '" << badInput << "'\n";
- // Debug.on("parser");
-
- d_symman.reset(new SymbolManager(d_solver.get()));
- Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test")
- .withStringInput(badInput)
- .withOptions(d_options)
- .withInputLanguage(d_lang)
- .withStrictMode(strictMode)
- .build();
- TS_ASSERT_THROWS(
- {
- Command* cmd;
- while ((cmd = parser->nextCommand()) != NULL)
- {
- Debug("parser") << "Parsed command: " << (*cmd) << endl;
- delete cmd;
- }
- cout << "\nBad input succeeded:\n" << badInput << endl;
- },
- const ParserException&);
- // Debug.off("parser");
- delete parser;
- }
-
- void tryGoodExpr(const string goodExpr)
- {
- // Debug.on("parser");
- // Debug.on("parser-extra");
- try
- {
- // cerr << "Testing good expr: '" << goodExpr << "'\n";
- // Debug.on("parser");
- // istringstream stream(context + goodBooleanExprs[i]);
-
- d_symman.reset(new SymbolManager(d_solver.get()));
- Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test")
- .withStringInput(goodExpr)
- .withOptions(d_options)
- .withInputLanguage(d_lang)
- .build();
-
- if (d_lang == LANG_SMTLIB_V2)
- {
- // Use QF_LIA to make multiplication ("*") available
- std::unique_ptr<Command> cmd(
- static_cast<Smt2*>(parser)->setLogic("QF_LIA"));
- }
-
- TS_ASSERT(!parser->done());
- setupContext(*parser);
- TS_ASSERT(!parser->done());
- api::Term e = parser->nextExpression();
- TS_ASSERT(!e.isNull());
- e = parser->nextExpression();
- TS_ASSERT(parser->done());
- TS_ASSERT(e.isNull());
- delete parser;
- }
- catch (Exception& e)
- {
- cout << endl
- << "Good expr failed." << endl
- << "Input: <<" << goodExpr << ">>" << endl
- << "Output: <<" << e << ">>" << endl;
- throw;
- }
- }
-
- /* 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 string badExpr, bool strictMode = false)
- {
- // Debug.on("parser");
- // Debug.on("parser-extra");
- // cout << "Testing bad expr: '" << badExpr << "'\n";
-
- d_symman.reset(new SymbolManager(d_solver.get()));
- Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test")
- .withStringInput(badExpr)
- .withOptions(d_options)
- .withInputLanguage(d_lang)
- .withStrictMode(strictMode)
- .build();
- setupContext(*parser);
- TS_ASSERT(!parser->done());
- TS_ASSERT_THROWS(api::Term e = parser->nextExpression();
- cout << endl
- << "Bad expr succeeded." << endl
- << "Input: <<" << badExpr << ">>" << endl
- << "Output: <<" << e << ">>" << endl;
- , const ParserException&);
- delete parser;
- // Debug.off("parser");
- }
-
- ParserBlack(InputLanguage lang) :
- d_lang(lang) {
- }
-
- virtual ~ParserBlack() {}
-
- void setUp()
- {
- d_options.set(options::parseOnly, true);
- // ensure the old symbol manager is deleted
- d_symman.reset(nullptr);
- d_solver.reset(new api::Solver(&d_options));
- }
-
- void tearDown()
- {
- d_symman.reset(nullptr);
- d_solver.reset(nullptr);
- }
-
- private:
- InputLanguage d_lang;
- std::unique_ptr<api::Solver> d_solver;
- std::unique_ptr<SymbolManager> d_symman;
-
-}; /* class ParserBlack */
-
-class Cvc4ParserTest : public CxxTest::TestSuite, public ParserBlack {
- typedef ParserBlack super;
-
-public:
- Cvc4ParserTest() : ParserBlack(LANG_CVC4) { }
-
- void setUp() override { super::setUp(); }
-
- void tearDown() override { super::tearDown(); }
-
- void testGoodCvc4Inputs() {
- 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 tree = node(data:[list,list,ARRAY tree OF list]), list = cons(car:ARRAY list OF tree,cdr:BITVECTOR(32)) 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;");
- }
-
- void testBadCvc4Inputs() {
-// competition builds don't do any checking
-#ifndef CVC4_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("a : [1..-1];"); // bad subrange
- //tryBadInput("a : [0. .0];"); // bad subrange
- //tryBadInput("a : [..0];"); // bad subrange
- //tryBadInput("a : [0.0];"); // bad subrange
- 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 /* ! CVC4_COMPETITION_MODE */
- }
-
- void testGoodCvc4Exprs() {
- 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))");
- }
-
- void testBadCvc4Exprs() {
-// competition builds don't do any checking
-#ifndef CVC4_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 /* ! CVC4_COMPETITION_MODE */
- }
-};/* class Cvc4ParserTest */
-
-class Smt2ParserTest : public CxxTest::TestSuite, public ParserBlack {
- typedef ParserBlack super;
-
-public:
- Smt2ParserTest() : ParserBlack(LANG_SMTLIB_V2) { }
-
- void setUp() override { super::setUp(); }
-
- void tearDown() override { super::tearDown(); }
-
- void setupContext(Parser& parser) override
- {
- super::setupContext(parser);
- }
-
- void testGoodSmt2Inputs() {
- 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)");
- }
-
- void testBadSmt2Inputs() {
-// competition builds don't do any checking
-#ifndef CVC4_COMPETITION_MODE
- tryBadInput("(assert)"); // no args
- tryBadInput("(set-info :notes |Symbols can't contain the | character|)");
- tryBadInput("(set-logic QF_UF) (check-sat true)", true); // check-sat shouldn't have an arg
- tryBadInput("(declare-sort a)"); // no arg
- tryBadInput("(declare-sort a 0) (declare-sort a 0)"); // double decl
- tryBadInput("(set-logic QF_UF) (declare-fun p Bool)"); // should be "p () Bool"
- // strict mode
- tryBadInput("(assert true)", true); // no set-logic, core theory symbol "true" undefined
- tryBadInput("(declare-fun p Bool)", true); // core theory symbol "Bool" undefined
-#endif /* ! CVC4_COMPETITION_MODE */
- }
-
- void testGoodSmt2Exprs() {
- 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)");
- }
-
- void testBadSmt2Exprs() {
-// competition builds don't do any checking
-#ifndef CVC4_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 /* ! CVC4_COMPETITION_MODE */
- }
-};/* class Smt2ParserTest */
projects / cvc5.git / commitdiff