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                 :            :  * Check macros for the cvc5 C API.
      11                 :            :  *
      12                 :            :  * These macros implement guards for the cvc5 C API functions.
      13                 :            :  */
      14                 :            : 
      15                 :            : #include "cvc5_private.h"
      16                 :            : 
      17                 :            : #ifndef CVC5__CAPI__CHECKS_H
      18                 :            : #define CVC5__CAPI__CHECKS_H
      19                 :            : 
      20                 :            : #include <cvc5/cvc5.h>
      21                 :            : 
      22                 :            : #include <cstdlib>
      23                 :            : #include <iostream>
      24                 :            : #include <sstream>
      25                 :            : 
      26                 :            : #include "api/cpp/cvc5_checks.h"
      27                 :            : #include "base/check.h"
      28                 :            : 
      29                 :            : namespace cvc5 {
      30                 :            : 
      31                 :            : /* -------------------------------------------------------------------------- */
      32                 :            : 
      33                 :            : class Cvc5CApiAbortStream
      34                 :            : {
      35                 :            :  public:
      36                 :       1012 :   Cvc5CApiAbortStream(const std::string& msg_prefix)
      37                 :       1012 :   {
      38                 :       1012 :     stream() << msg_prefix << " ";
      39                 :       1012 :   }
      40                 :       1012 :   ~Cvc5CApiAbortStream()
      41                 :            :   {
      42                 :       1012 :     std::cerr << d_stream.str() << std::endl;
      43                 :       1012 :     exit(EXIT_FAILURE);
      44                 :            :   }
      45                 :       2024 :   std::ostream& stream() { return d_stream; }
      46                 :            : 
      47                 :            :  private:
      48                 :            :   void flush()
      49                 :            :   {
      50                 :            :     stream() << std::endl;
      51                 :            :     stream().flush();
      52                 :            :   }
      53                 :            :   std::stringstream d_stream;
      54                 :            : };
      55                 :            : 
      56                 :            : #define CVC5_CAPI_ABORT           \
      57                 :            :   cvc5::internal::OstreamVoider() \
      58                 :            :       & cvc5::Cvc5CApiAbortStream("cvc5: error:").stream()
      59                 :            : 
      60                 :            : #define CVC5_CAPI_TRY_CATCH_BEGIN \
      61                 :            :   try                             \
      62                 :            :   {
      63                 :            : #define CVC5_CAPI_TRY_CATCH_END \
      64                 :            :   }                             \
      65                 :            :   catch (cvc5::CVC5ApiException & e) { CVC5_CAPI_ABORT << e.getMessage(); }
      66                 :            : 
      67                 :            : #endif
      68                 :            : 
      69                 :            : #define CVC5_CAPI_CHECK_NOT_NULL(arg)                                          \
      70                 :            :   CVC5_API_CHECK(arg != nullptr) << "invalid call to '" << __PRETTY_FUNCTION__ \
      71                 :            :                                  << "', unexpected NULL argument"
      72                 :            : 
      73                 :            : #define CVC5_CAPI_CHECK_NOT_NULL_AT_IDX(arg, i)     \
      74                 :            :   CVC5_API_CHECK(arg[i] != nullptr)                 \
      75                 :            :       << "invalid call to '" << __PRETTY_FUNCTION__ \
      76                 :            :       << "', unexpected NULL argument at index " << i
      77                 :            : 
      78                 :            : /* -------------------------------------------------------------------------- */
      79                 :            : 
      80                 :            : #define CVC5_CAPI_CHECK_KIND(kind)                 \
      81                 :            :   CVC5_API_CHECK((kind) >= CVC5_KIND_INTERNAL_KIND \
      82                 :            :                  && (kind) < CVC5_KIND_LAST_KIND)  \
      83                 :            :       << "invalid term kind"
      84                 :            : 
      85                 :            : #define CVC5_CAPI_CHECK_SORT_KIND(kind)                      \
      86                 :            :   CVC5_API_CHECK((kind) >= CVC5_SORT_KIND_INTERNAL_SORT_KIND \
      87                 :            :                  && (kind) < CVC5_SORT_KIND_LAST_SORT_KIND)  \
      88                 :            :       << "invalid sort kind"
      89                 :            : 
      90                 :            : #define CVC5_CAPI_CHECK_RM(rm) \
      91                 :            :   CVC5_API_CHECK((rm) >= 0 && (rm) < CVC5_RM_LAST) << "invalid rounding mode"
      92                 :            : 
      93                 :            : #define CVC5_CAPI_CHECK_UNKNOWN_EXPLANATION(e)                    \
      94                 :            :   CVC5_API_CHECK((e) >= 0 && (e) < CVC5_UNKNOWN_EXPLANATION_LAST) \
      95                 :            :       << "invalid unknown explanation kind"
      96                 :            : 
      97                 :            : #define CVC5_CAPI_CHECK_BLOCK_MODELS_MODE(mode)                       \
      98                 :            :   CVC5_API_CHECK((mode) >= 0 && (mode) < CVC5_BLOCK_MODELS_MODE_LAST) \
      99                 :            :       << "invalid block models mode"
     100                 :            : 
     101                 :            : #define CVC5_CAPI_CHECK_FIND_SYNTH_TARGET(target)                         \
     102                 :            :   CVC5_API_CHECK((target) >= 0 && (target) < CVC5_FIND_SYNTH_TARGET_LAST) \
     103                 :            :       << "invalid find synthesis target"
     104                 :            : 
     105                 :            : #define CVC5_CAPI_CHECK_OPTION_CATEGORY(cat)                      \
     106                 :            :   CVC5_API_CHECK((cat) >= 0 && (cat) < CVC5_OPTION_CATEGORY_LAST) \
     107                 :            :       << "invalid option category"
     108                 :            : 
     109                 :            : #define CVC5_CAPI_CHECK_INPUT_LANGUAGE(lang)                       \
     110                 :            :   CVC5_API_CHECK((lang) >= 0 && (lang) < CVC5_INPUT_LANGUAGE_LAST) \
     111                 :            :       << "invalid input language"
     112                 :            : 
     113                 :            : #define CVC5_CAPI_CHECK_LEARNED_LIT_TYPE(type)                       \
     114                 :            :   CVC5_API_CHECK((type) >= 0 && (type) < CVC5_LEARNED_LIT_TYPE_LAST) \
     115                 :            :       << "invalid learned literal type"
     116                 :            : 
     117                 :            : #define CVC5_CAPI_CHECK_PROOF_COMPONENT(pc)                     \
     118                 :            :   CVC5_API_CHECK((pc) >= 0 && (pc) < CVC5_PROOF_COMPONENT_LAST) \
     119                 :            :       << "invalid proof component kind"
     120                 :            : 
     121                 :            : #define CVC5_CAPI_CHECK_PROOF_FORMAT(format)                         \
     122                 :            :   CVC5_API_CHECK((format) >= 0 && (format) < CVC5_PROOF_FORMAT_LAST) \
     123                 :            :       << "invalid proof format"
     124                 :            : 
     125                 :            : #define CVC5_CAPI_CHECK_PROOF_RULE(rule)                       \
     126                 :            :   CVC5_API_CHECK((rule) >= 0 && (rule) < CVC5_PROOF_RULE_LAST) \
     127                 :            :       << "invalid proof rule"
     128                 :            : 
     129                 :            : #define CVC5_CAPI_CHECK_PROOF_REWRITE_RULE(rule)                       \
     130                 :            :   CVC5_API_CHECK((rule) >= 0 && (rule) < CVC5_PROOF_REWRITE_RULE_LAST) \
     131                 :            :       << "invalid proof rewrite rule"
     132                 :            : 
     133                 :            : #define CVC5_CAPI_CHECK_SKOLEM_ID(id)                                          \
     134                 :            :   CVC5_API_CHECK((id) >= 0 && (id) < CVC5_SKOLEM_ID_LAST) << "invalid skolem " \
     135                 :            :                                                              "id"
     136                 :            : 
     137                 :            : /* -------------------------------------------------------------------------- */
     138                 :            : 
     139                 :            : #define CVC5_CAPI_CHECK_SORT(sort) \
     140                 :            :   CVC5_API_CHECK(sort != nullptr) << "invalid sort"
     141                 :            : 
     142                 :            : #define CVC5_CAPI_CHECK_SORT_AT_IDX(sorts, i) \
     143                 :            :   CVC5_API_CHECK(sorts[i] != nullptr) << "invalid sort at index " << i
     144                 :            : 
     145                 :            : /* -------------------------------------------------------------------------- */
     146                 :            : 
     147                 :            : #define CVC5_CAPI_CHECK_DT_DECL(decl) \
     148                 :            :   CVC5_API_CHECK(decl != nullptr) << "invalid datatype declaration"
     149                 :            : 
     150                 :            : #define CVC5_CAPI_CHECK_DT_DECL_AT_IDX(decls, i) \
     151                 :            :   CVC5_API_CHECK(decls[i] != nullptr)            \
     152                 :            :       << "invalid datatype declaration at index " << i
     153                 :            : 
     154                 :            : #define CVC5_CAPI_CHECK_DT_CONS_DECL(decl)                           \
     155                 :            :   CVC5_API_CHECK(decl != nullptr) << "invalid datatype constructor " \
     156                 :            :                                      "declaration"
     157                 :            : 
     158                 :            : #define CVC5_CAPI_CHECK_DT_CONS_DECL_AT_IDX(decls, i) \
     159                 :            :   CVC5_API_CHECK(decls[i] != nullptr)                 \
     160                 :            :       << "invalid datatype constructor declaration at index " << i
     161                 :            : 
     162                 :            : #define CVC5_CAPI_CHECK_DT_SEL(sel) \
     163                 :            :   CVC5_API_CHECK(sel != nullptr) << "invalid datatype selector"
     164                 :            : 
     165                 :            : #define CVC5_CAPI_CHECK_DT_CONS(cons) \
     166                 :            :   CVC5_API_CHECK(cons != nullptr) << "invalid datatype constructor"
     167                 :            : 
     168                 :            : #define CVC5_CAPI_CHECK_DT(dt) \
     169                 :            :   CVC5_API_CHECK(dt != nullptr) << "invalid datatype"
     170                 :            : 
     171                 :            : /* -------------------------------------------------------------------------- */
     172                 :            : 
     173                 :            : #define CVC5_CAPI_CHECK_TERM(term) \
     174                 :            :   CVC5_API_CHECK(term != nullptr) << "invalid term"
     175                 :            : 
     176                 :            : #define CVC5_CAPI_CHECK_TERM_AT_IDX(terms, i) \
     177                 :            :   CVC5_API_CHECK(terms[i] != nullptr) << "invalid term at index " << i
     178                 :            : 
     179                 :            : /* -------------------------------------------------------------------------- */
     180                 :            : 
     181                 :            : #define CVC5_CAPI_CHECK_OP(op) \
     182                 :            :   CVC5_API_CHECK(op != nullptr) << "invalid operator term"
     183                 :            : 
     184                 :            : /* -------------------------------------------------------------------------- */
     185                 :            : 
     186                 :            : #define CVC5_CAPI_CHECK_RESULT(res) \
     187                 :            :   CVC5_API_CHECK(res != nullptr) << "invalid result"
     188                 :            : 
     189                 :            : #define CVC5_CAPI_CHECK_SYNTH_RESULT(res) \
     190                 :            :   CVC5_API_CHECK(res != nullptr) << "invalid synthesis result"
     191                 :            : 
     192                 :            : /* -------------------------------------------------------------------------- */
     193                 :            : 
     194                 :            : #define CVC5_CAPI_CHECK_PROOF(proof) \
     195                 :            :   CVC5_API_CHECK(proof != nullptr) << "invalid proof"
     196                 :            : 
     197                 :            : /* -------------------------------------------------------------------------- */
     198                 :            : 
     199                 :            : #define CVC5_CAPI_CHECK_GRAMMAR(grammar) \
     200                 :            :   CVC5_API_CHECK(grammar != nullptr) << "invalid grammar"
     201                 :            : 
     202                 :            : /* -------------------------------------------------------------------------- */
     203                 :            : 
     204                 :            : #define CVC5_CAPI_CHECK_STAT(stat) \
     205                 :            :   CVC5_API_CHECK(stat != nullptr) << "invalid statistic"
     206                 :            : 
     207                 :            : #define CVC5_CAPI_CHECK_STATS(stat) \
     208                 :            :   CVC5_API_CHECK(stat != nullptr) << "invalid statistics"
     209                 :            : 
     210                 :            : /* -------------------------------------------------------------------------- */
     211                 :            : 
     212                 :            : #define CVC5_CAPI_CHECK_CMD(cmd) \
     213                 :            :   CVC5_API_CHECK(cmd != nullptr) << "invalid command"
     214                 :            : 
     215                 :            : /* -------------------------------------------------------------------------- */
     216                 :            : }