Branch data     Line data    Source code

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