Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Aina Niemetz
       4                 :            :  *
       5                 :            :  * This file is part of the cvc5 project.
       6                 :            :  *
       7                 :            :  * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
       8                 :            :  * in the top-level source directory and their institutional affiliations.
       9                 :            :  * All rights reserved.  See the file COPYING in the top-level source
      10                 :            :  * directory for licensing information.
      11                 :            :  * ****************************************************************************
      12                 :            :  *
      13                 :            :  * Black box testing of solver functions of the C API.
      14                 :            :  */
      15                 :            : 
      16                 :            : extern "C" {
      17                 :            : #include <cvc5/c/cvc5_parser.h>
      18                 :            : }
      19                 :            : 
      20                 :            : #include <sstream>
      21                 :            : 
      22                 :            : #include "gtest/gtest.h"
      23                 :            : 
      24                 :            : namespace cvc5::internal::test {
      25                 :            : 
      26                 :            : class TestCApiBlackCommand : public ::testing::Test
      27                 :            : {
      28                 :            :  protected:
      29                 :         11 :   void SetUp() override
      30                 :            :   {
      31                 :         11 :     d_tm = cvc5_term_manager_new();
      32                 :         11 :     d_solver = cvc5_new(d_tm);
      33                 :         11 :     d_sm = cvc5_symbol_manager_new(d_tm);
      34                 :         11 :     d_parser = cvc5_parser_new(d_solver, d_sm);
      35                 :         11 :     cvc5_parser_set_inc_str_input(
      36                 :            :         d_parser, CVC5_INPUT_LANGUAGE_SMT_LIB_2_6, "command_black");
      37                 :         11 :   }
      38                 :          6 :   void TearDown() override
      39                 :            :   {
      40                 :          6 :     cvc5_parser_delete(d_parser);
      41                 :          6 :     cvc5_symbol_manager_delete(d_sm);
      42                 :          6 :     cvc5_delete(d_solver);
      43                 :          6 :     cvc5_term_manager_delete(d_tm);
      44                 :          6 :   }
      45                 :            : 
      46                 :         20 :   void parse_command(const char* str,
      47                 :            :                      Cvc5Command* cmd,
      48                 :            :                      bool expect_death = false,
      49                 :            :                      const std::string& err = "")
      50                 :            :   {
      51                 :            :     const char* error_msg;
      52                 :         20 :     cvc5_parser_append_inc_str_input(d_parser, str);
      53                 :         20 :     *cmd = cvc5_parser_next_command(d_parser, &error_msg);
      54         [ -  + ]:         20 :     ASSERT_TRUE(expect_death == (error_msg != nullptr));
      55                 :         26 :     ASSERT_TRUE(!expect_death
      56                 :            :                 || (std::string(error_msg).find(err) != std::string::npos));
      57                 :            :   }
      58                 :            : 
      59                 :            :   Cvc5TermManager* d_tm;
      60                 :            :   Cvc5* d_solver;
      61                 :            :   Cvc5SymbolManager* d_sm;
      62                 :            :   Cvc5InputParser* d_parser;
      63                 :            : };
      64                 :            : 
      65                 :         12 : TEST_F(TestCApiBlackCommand, invoke)
      66                 :            : {
      67                 :            :   Cvc5Command cmd;
      68                 :          6 :   parse_command("(set-logic QF_LIA)", &cmd);
      69         [ -  + ]:          6 :   ASSERT_NE(cmd, nullptr);
      70                 :          6 :   (void)cvc5_cmd_invoke(cmd, d_solver, d_sm);
      71                 :            :   // get model not available
      72                 :          6 :   parse_command("(get-model)", &cmd);
      73         [ -  + ]:          6 :   ASSERT_NE(cmd, nullptr);
      74                 :          6 :   const char* out = cvc5_cmd_invoke(cmd, d_solver, d_sm);
      75         [ -  + ]:          6 :   ASSERT_NE(out, nullptr);
      76         [ -  + ]:         12 :   ASSERT_EQ(
      77                 :            :       "(error \"cannot get model unless model generation is enabled (try "
      78                 :            :       "--produce-models)\")\n",
      79                 :            :       std::string(out));
      80                 :          6 :   ASSERT_DEATH(cvc5_cmd_invoke(nullptr, d_solver, d_sm), "invalid command");
      81                 :          5 :   ASSERT_DEATH(cvc5_cmd_invoke(cmd, nullptr, d_sm), "unexpected NULL argument");
      82                 :          4 :   ASSERT_DEATH(cvc5_cmd_invoke(cmd, d_solver, nullptr),
      83                 :            :                "unexpected NULL argument");
      84                 :            :   // logic already set
      85                 :          3 :   parse_command(
      86                 :            :       "(set-logic QF_LRA)", &cmd, true, "Only one set-logic is allowed");
      87                 :            : }
      88                 :            : 
      89                 :          6 : TEST_F(TestCApiBlackCommand, to_string)
      90                 :            : {
      91                 :            :   Cvc5Command cmd;
      92                 :          3 :   parse_command("(set-logic QF_LIA)", &cmd);
      93         [ -  + ]:          3 :   ASSERT_NE(cmd, nullptr);
      94                 :            :   // note normalizes wrt whitespace
      95         [ -  + ]:          3 :   ASSERT_EQ(cvc5_cmd_to_string(cmd), std::string("(set-logic QF_LIA)"));
      96                 :          3 :   ASSERT_DEATH(cvc5_cmd_to_string(nullptr), "invalid command");
      97                 :            : }
      98                 :            : 
      99                 :          4 : TEST_F(TestCApiBlackCommand, get_name)
     100                 :            : {
     101                 :            :   Cvc5Command cmd;
     102                 :          2 :   parse_command("(get-model)", &cmd);
     103         [ -  + ]:          2 :   ASSERT_NE(cmd, nullptr);
     104         [ -  + ]:          2 :   ASSERT_EQ(cvc5_cmd_get_name(cmd), std::string("get-model"));
     105                 :          2 :   ASSERT_DEATH(cvc5_cmd_get_name(nullptr), "invalid command");
     106                 :            : }
     107                 :            : }  // namespace cvc5::internal::test