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