mirror of
https://github.com/AdaCore/cvc5.git
synced 2026-02-12 12:32:16 -08:00
343 lines
11 KiB
C++
343 lines
11 KiB
C++
/******************************************************************************
|
|
* Top contributors (to current version):
|
|
* Andrew Reynolds, Aina Niemetz, Mudathir Mohamed
|
|
*
|
|
* This file is part of the cvc5 project.
|
|
*
|
|
* Copyright (c) 2009-2025 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::InputParser SMT-LIbv2 inputs.
|
|
*/
|
|
|
|
#include <cvc5/cvc5.h>
|
|
#include <cvc5/cvc5_parser.h>
|
|
|
|
#include <sstream>
|
|
|
|
#include "base/output.h"
|
|
#include "options/base_options.h"
|
|
#include "options/language.h"
|
|
#include "options/options.h"
|
|
#include "test_parser.h"
|
|
|
|
using namespace cvc5::parser;
|
|
|
|
namespace cvc5::internal {
|
|
namespace test {
|
|
|
|
class TestApiBlackInputParser : public TestParser
|
|
{
|
|
protected:
|
|
TestApiBlackInputParser() {}
|
|
virtual ~TestApiBlackInputParser() {}
|
|
|
|
Command parseLogicCommand(InputParser& p, const std::string& logic)
|
|
{
|
|
p.setIncrementalStringInput(modes::InputLanguage::SMT_LIB_2_6,
|
|
"input_parser_black");
|
|
std::stringstream ss;
|
|
ss << "(set-logic " << logic << ")" << std::endl;
|
|
p.appendIncrementalStringInput(ss.str());
|
|
return p.nextCommand();
|
|
}
|
|
};
|
|
|
|
TEST_F(TestApiBlackInputParser, constructSymbolManager)
|
|
{
|
|
(void)SymbolManager(d_tm);
|
|
}
|
|
|
|
TEST_F(TestApiBlackInputParser, getSolver)
|
|
{
|
|
InputParser p(d_solver.get());
|
|
ASSERT_EQ(p.getSolver(), d_solver.get());
|
|
}
|
|
|
|
TEST_F(TestApiBlackInputParser, getSymbolManager)
|
|
{
|
|
InputParser p(d_solver.get());
|
|
// a symbol manager is allocated
|
|
ASSERT_NE(p.getSymbolManager(), nullptr);
|
|
|
|
InputParser p2(d_solver.get(), d_symman.get());
|
|
ASSERT_EQ(p2.getSymbolManager(), d_symman.get());
|
|
}
|
|
|
|
TEST_F(TestApiBlackInputParser, setFileInput)
|
|
{
|
|
InputParser p(d_solver.get());
|
|
ASSERT_THROW(
|
|
p.setFileInput(modes::InputLanguage::SMT_LIB_2_6, "nonexistent.smt2"),
|
|
CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackInputParser, setStreamInput)
|
|
{
|
|
InputParser p(d_solver.get());
|
|
std::stringstream ss;
|
|
ss << "(set-logic QF_LIA)" << std::endl;
|
|
ss << "(declare-fun a () Bool)" << std::endl;
|
|
ss << "(declare-fun b () Int)" << std::endl;
|
|
p.setStreamInput(modes::InputLanguage::SMT_LIB_2_6, ss, "input_parser_black");
|
|
ASSERT_EQ(p.done(), false);
|
|
Command cmd;
|
|
std::stringstream out;
|
|
while (true)
|
|
{
|
|
cmd = p.nextCommand();
|
|
if (cmd.isNull())
|
|
{
|
|
break;
|
|
}
|
|
ASSERT_NO_THROW(cmd.invoke(d_solver.get(), d_symman.get(), out));
|
|
}
|
|
ASSERT_EQ(p.done(), true);
|
|
}
|
|
|
|
TEST_F(TestApiBlackInputParser, setAndAppendIncrementalStringInput)
|
|
{
|
|
std::stringstream out;
|
|
InputParser p(d_solver.get());
|
|
p.setIncrementalStringInput(modes::InputLanguage::SMT_LIB_2_6,
|
|
"input_parser_black");
|
|
ASSERT_EQ(p.done(), false);
|
|
Command cmd;
|
|
p.appendIncrementalStringInput("(set-logic ALL)");
|
|
p.appendIncrementalStringInput("(declare-fun a () Bool)");
|
|
p.appendIncrementalStringInput("(declare-fun b () Int)");
|
|
cmd = p.nextCommand();
|
|
ASSERT_NE(cmd.isNull(), true);
|
|
ASSERT_NO_THROW(cmd.invoke(d_solver.get(), d_symman.get(), out));
|
|
cmd = p.nextCommand();
|
|
ASSERT_NE(cmd.isNull(), true);
|
|
ASSERT_NO_THROW(cmd.invoke(d_solver.get(), d_symman.get(), out));
|
|
cmd = p.nextCommand();
|
|
ASSERT_NE(cmd.isNull(), true);
|
|
ASSERT_NO_THROW(cmd.invoke(d_solver.get(), d_symman.get(), out));
|
|
ASSERT_EQ(p.done(), false);
|
|
cmd = p.nextCommand();
|
|
ASSERT_TRUE(cmd.isNull());
|
|
ASSERT_EQ(p.done(), true);
|
|
}
|
|
|
|
TEST_F(TestApiBlackInputParser, setAndAppendIncrementalStringInputInterleave)
|
|
{
|
|
std::stringstream out;
|
|
InputParser p(d_solver.get());
|
|
p.setIncrementalStringInput(modes::InputLanguage::SMT_LIB_2_6,
|
|
"input_parser_black");
|
|
ASSERT_EQ(p.done(), false);
|
|
Command cmd;
|
|
p.appendIncrementalStringInput("(set-logic ALL)");
|
|
cmd = p.nextCommand();
|
|
ASSERT_NE(cmd.isNull(), true);
|
|
ASSERT_NO_THROW(cmd.invoke(d_solver.get(), d_symman.get(), out));
|
|
p.appendIncrementalStringInput("(declare-fun a () Bool)");
|
|
cmd = p.nextCommand();
|
|
ASSERT_NE(cmd.isNull(), true);
|
|
ASSERT_NO_THROW(cmd.invoke(d_solver.get(), d_symman.get(), out));
|
|
p.appendIncrementalStringInput("(declare-fun b () Int)");
|
|
cmd = p.nextCommand();
|
|
ASSERT_NE(cmd.isNull(), true);
|
|
ASSERT_NO_THROW(cmd.invoke(d_solver.get(), d_symman.get(), out));
|
|
ASSERT_EQ(p.done(), false);
|
|
cmd = p.nextCommand();
|
|
ASSERT_TRUE(cmd.isNull());
|
|
ASSERT_EQ(p.done(), true);
|
|
}
|
|
|
|
TEST_F(TestApiBlackInputParser, appendIncrementalNoSet)
|
|
{
|
|
InputParser p(d_solver.get());
|
|
ASSERT_THROW(p.appendIncrementalStringInput("(set-logic ALL)"),
|
|
CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackInputParser, setStringInput)
|
|
{
|
|
std::stringstream out;
|
|
InputParser p(d_solver.get());
|
|
Command cmd;
|
|
p.setStringInput(modes::InputLanguage::SMT_LIB_2_6,
|
|
"(set-logic ALL)",
|
|
"input_parser_black");
|
|
cmd = p.nextCommand();
|
|
ASSERT_NE(cmd.isNull(), true);
|
|
ASSERT_NO_THROW(cmd.invoke(d_solver.get(), d_symman.get(), out));
|
|
cmd = p.nextCommand();
|
|
ASSERT_EQ(cmd.isNull(), true);
|
|
}
|
|
|
|
TEST_F(TestApiBlackInputParser, nextCommand)
|
|
{
|
|
InputParser p(d_solver.get());
|
|
ASSERT_THROW(p.nextCommand(), CVC5ApiException);
|
|
std::stringstream ss;
|
|
p.setStreamInput(modes::InputLanguage::SMT_LIB_2_6, ss, "input_parser_black");
|
|
Command cmd = p.nextCommand();
|
|
ASSERT_EQ(cmd.isNull(), true);
|
|
}
|
|
|
|
TEST_F(TestApiBlackInputParser, nextCommandNoInput)
|
|
{
|
|
InputParser p(d_solver.get());
|
|
p.setIncrementalStringInput(modes::InputLanguage::SMT_LIB_2_6,
|
|
"input_parser_black");
|
|
Command cmd = p.nextCommand();
|
|
ASSERT_EQ(cmd.isNull(), true);
|
|
Term t = p.nextTerm();
|
|
ASSERT_EQ(t.isNull(), true);
|
|
}
|
|
|
|
TEST_F(TestApiBlackInputParser, nextTerm)
|
|
{
|
|
InputParser p(d_solver.get());
|
|
ASSERT_THROW(p.nextTerm(), CVC5ApiException);
|
|
std::stringstream ss;
|
|
p.setStreamInput(modes::InputLanguage::SMT_LIB_2_6, ss, "input_parser_black");
|
|
ASSERT_EQ(p.nextTerm().isNull(), true);
|
|
}
|
|
|
|
TEST_F(TestApiBlackInputParser, nextTerm2)
|
|
{
|
|
std::stringstream out;
|
|
InputParser p(d_solver.get(), d_symman.get());
|
|
p.setIncrementalStringInput(modes::InputLanguage::SMT_LIB_2_6,
|
|
"input_parser_black");
|
|
// parse a declaration command
|
|
p.appendIncrementalStringInput("(declare-fun a () Int)\n");
|
|
Command cmd = p.nextCommand();
|
|
ASSERT_NE(cmd.isNull(), true);
|
|
ASSERT_NO_THROW(cmd.invoke(d_solver.get(), d_symman.get(), out));
|
|
// now parse some terms
|
|
Term t;
|
|
p.appendIncrementalStringInput("45\n");
|
|
ASSERT_NO_THROW(t = p.nextTerm());
|
|
ASSERT_EQ(t.isNull(), false);
|
|
p.appendIncrementalStringInput("(+ a 1)\n");
|
|
ASSERT_NO_THROW(t = p.nextTerm());
|
|
ASSERT_EQ(t.isNull(), false);
|
|
ASSERT_EQ(t.getKind(), Kind::ADD);
|
|
p.appendIncrementalStringInput("(+ b 1)\n");
|
|
ASSERT_THROW(t = p.nextTerm(), ParserException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackInputParser, multipleParsers)
|
|
{
|
|
std::stringstream out;
|
|
InputParser p(d_solver.get(), d_symman.get());
|
|
// set a logic for the parser
|
|
Command cmd = parseLogicCommand(p, "QF_LIA");
|
|
ASSERT_NO_THROW(cmd.invoke(d_solver.get(), d_symman.get(), out));
|
|
ASSERT_EQ(d_solver->isLogicSet(), true);
|
|
ASSERT_EQ(d_solver->getLogic(), "QF_LIA");
|
|
ASSERT_EQ(d_symman->isLogicSet(), true);
|
|
ASSERT_EQ(d_symman->getLogic(), "QF_LIA");
|
|
// cannot set logic on solver now
|
|
ASSERT_THROW(d_solver->setLogic("QF_LRA"), CVC5ApiException);
|
|
|
|
// possible to construct another parser with the same solver and symbol
|
|
// manager
|
|
InputParser p2(d_solver.get(), p.getSymbolManager());
|
|
|
|
// possible to construct another parser with a fresh solver
|
|
Solver s2(d_tm);
|
|
InputParser p3(&s2, d_symman.get());
|
|
p3.setIncrementalStringInput(modes::InputLanguage::SMT_LIB_2_6,
|
|
"input_parser_black");
|
|
// logic is automatically set on the solver
|
|
ASSERT_EQ(s2.isLogicSet(), true);
|
|
ASSERT_EQ(s2.getLogic(), "QF_LIA");
|
|
// we cannot set the logic since it has already been set
|
|
ASSERT_THROW(parseLogicCommand(p3, "QF_LRA"), ParserException);
|
|
|
|
// using a solver with the same logic is allowed
|
|
Solver s3(d_tm);
|
|
s3.setLogic("QF_LIA");
|
|
InputParser p4(&s3, d_symman.get());
|
|
p4.setIncrementalStringInput(modes::InputLanguage::SMT_LIB_2_6,
|
|
"input_parser_black");
|
|
|
|
// using a solver with a different logic is not allowed
|
|
Solver s4(d_tm);
|
|
s4.setLogic("QF_LRA");
|
|
InputParser p5(&s4, d_symman.get());
|
|
ASSERT_THROW(p5.setIncrementalStringInput(modes::InputLanguage::SMT_LIB_2_6,
|
|
"input_parser_black"),
|
|
CVC5ApiException);
|
|
}
|
|
|
|
TEST_F(TestApiBlackInputParser, ParserExceptions)
|
|
{
|
|
ParserException defaultConstructor;
|
|
std::string message = "error";
|
|
const char* cMessage = "error";
|
|
std::string filename = "file.smt2";
|
|
ParserException stringConstructor(message);
|
|
ParserException cStringConstructor(cMessage);
|
|
ParserException exception(message, filename, 10, 11);
|
|
std::stringstream ss;
|
|
exception.toStream(ss);
|
|
ASSERT_EQ(message, exception.getMessage());
|
|
ASSERT_EQ(message, exception.getMessage());
|
|
ASSERT_EQ(filename, exception.getFilename());
|
|
ASSERT_EQ(10, exception.getLine());
|
|
ASSERT_EQ(11, exception.getColumn());
|
|
|
|
ParserEndOfFileException eofDefault;
|
|
ParserEndOfFileException eofString(message);
|
|
ParserEndOfFileException eofCMessage(cMessage);
|
|
ParserEndOfFileException eof(message, filename, 10, 11);
|
|
}
|
|
|
|
TEST_F(TestApiBlackInputParser, incrementalSetString)
|
|
{
|
|
InputParser p(d_solver.get(), d_symman.get());
|
|
Command cmd;
|
|
std::stringstream out;
|
|
std::vector<std::string> strs{"(set-logic ALL)",
|
|
"(push)",
|
|
"(declare-fun x () Int)",
|
|
"(pop)",
|
|
"(declare-fun x () Int)"};
|
|
for (size_t i = 0; i < strs.size(); i++)
|
|
{
|
|
p.setStringInput(
|
|
modes::InputLanguage::SMT_LIB_2_6, strs[i], "input_parser_black");
|
|
cmd = p.nextCommand();
|
|
ASSERT_NE(cmd.isNull(), true);
|
|
ASSERT_NO_THROW(cmd.invoke(d_solver.get(), d_symman.get(), out));
|
|
}
|
|
ASSERT_EQ(out.str().empty(), true);
|
|
}
|
|
|
|
TEST_F(TestApiBlackInputParser, getDeclaredTermsAndSorts)
|
|
{
|
|
InputParser p(d_solver.get(), d_symman.get());
|
|
Command cmd;
|
|
std::stringstream out;
|
|
p.setIncrementalStringInput(modes::InputLanguage::SMT_LIB_2_6,
|
|
"input_parser_black");
|
|
p.appendIncrementalStringInput("(set-logic ALL)");
|
|
p.appendIncrementalStringInput("(declare-sort U 0)");
|
|
p.appendIncrementalStringInput("(declare-fun x () U)");
|
|
for (size_t i = 0; i < 3; i++)
|
|
{
|
|
cmd = p.nextCommand();
|
|
ASSERT_NE(cmd.isNull(), true);
|
|
ASSERT_NO_THROW(cmd.invoke(d_solver.get(), d_symman.get(), out));
|
|
}
|
|
std::vector<Sort> sorts = d_symman->getDeclaredSorts();
|
|
std::vector<Term> terms = d_symman->getDeclaredTerms();
|
|
ASSERT_EQ(sorts.size(), 1);
|
|
ASSERT_EQ(terms.size(), 1);
|
|
ASSERT_EQ(terms[0].getSort(), sorts[0]);
|
|
}
|
|
|
|
} // namespace test
|
|
} // namespace cvc5::internal
|