path: root/test/unit/parser/parser_black.cpp

/*********************                                                        */
/*! \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-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.\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/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