src/expr/CMakeLists.txt

   1 #####################
   2 ## CMakeLists.txt
   3 ## Top contributors (to current version):
   4 ##   Mathias Preiner, Andrew Reynolds, Aina Niemetz
   5 ## This file is part of the CVC4 project.
   6 ## Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
   7 ## in the top-level source directory and their institutional affiliations.
   8 ## All rights reserved.  See the file COPYING in the top-level source
   9 ## directory for licensing information.
  10 ##
  11 libcvc4_add_sources(
  12   array_store_all.cpp
  13   array_store_all.h
  14   ascription_type.cpp
  15   ascription_type.h
  16   attribute.h
  17   attribute.cpp
  18   attribute_internals.h
  19   attribute_unique_id.h
  20   bound_var_manager.cpp
  21   bound_var_manager.h
  22   buffered_proof_generator.cpp
  23   buffered_proof_generator.h
  24   emptyset.cpp
  25   emptyset.h
  26   emptybag.cpp
  27   emptybag.h
  28   expr_iomanip.cpp
  29   expr_iomanip.h
  30   kind_map.h
  31   lazy_proof.cpp
  32   lazy_proof.h
  33   lazy_proof_chain.cpp
  34   lazy_proof_chain.h
  35   match_trie.cpp
  36   match_trie.h
  37   node.cpp
  38   node.h
  39   node_algorithm.cpp
  40   node_algorithm.h
  41   node_builder.h
  42   node_manager.cpp
  43   node_manager.h
  44   node_manager_attributes.h
  45   node_self_iterator.h
  46   node_trie.cpp
  47   node_trie.h
  48   node_traversal.cpp
  49   node_traversal.h
  50   node_value.cpp
  51   node_value.h
  52   sequence.cpp
  53   sequence.h
  54   node_visitor.h
  55   proof.cpp
  56   proof.h
  57   proof_checker.cpp
  58   proof_checker.h
  59   proof_ensure_closed.cpp
  60   proof_ensure_closed.h
  61   proof_generator.cpp
  62   proof_generator.h
  63   proof_node.cpp
  64   proof_node.h
  65   proof_node_algorithm.cpp
  66   proof_node_algorithm.h
  67   proof_node_to_sexpr.cpp
  68   proof_node_to_sexpr.h
  69   proof_node_manager.cpp
  70   proof_node_manager.h
  71   proof_node_updater.cpp
  72   proof_node_updater.h
  73   proof_rule.cpp
  74   proof_rule.h
  75   proof_set.h
  76   proof_step_buffer.cpp
  77   proof_step_buffer.h
  78   skolem_manager.cpp
  79   skolem_manager.h
  80   symbol_manager.cpp
  81   symbol_manager.h
  82   symbol_table.cpp
  83   symbol_table.h
  84   tconv_seq_proof_generator.cpp
  85   tconv_seq_proof_generator.h
  86   term_canonize.cpp
  87   term_canonize.h
  88   term_context.cpp
  89   term_context.h
  90   term_context_node.cpp
  91   term_context_node.h
  92   term_context_stack.cpp
  93   term_context_stack.h
  94   term_conversion_proof_generator.cpp
  95   term_conversion_proof_generator.h
  96   type_checker.h
  97   type_matcher.cpp
  98   type_matcher.h
  99   type_node.cpp
 100   type_node.h
 101   datatype_index.h
 102   datatype_index.cpp
 103   dtype.h
 104   dtype.cpp
 105   dtype_cons.h
 106   dtype_cons.cpp
 107   dtype_selector.h
 108   dtype_selector.cpp
 109   record.cpp
 110   record.h
 111   sequence.cpp
 112   sequence.h
 113   subs.cpp
 114   subs.h
 115   sygus_datatype.cpp
 116   sygus_datatype.h
 117   uninterpreted_constant.cpp
 118   uninterpreted_constant.h
 119 )
 120
 121 libcvc4_add_sources(GENERATED
 122   kind.cpp
 123   kind.h
 124   metakind.cpp
 125   metakind.h
 126   type_checker.cpp
 127   type_properties.h
 128 )
 129
 130 #
 131 # Generate code for kinds.
 132 #
 133
 134 set(mkkind_script ${CMAKE_CURRENT_LIST_DIR}/mkkind)
 135 set(mkmetakind_script ${CMAKE_CURRENT_LIST_DIR}/mkmetakind)
 136 set(mkexpr_script ${CMAKE_CURRENT_LIST_DIR}/mkexpr)
 137
 138 add_custom_command(
 139   OUTPUT kind.h
 140   COMMAND
 141     ${mkkind_script}
 142     ${CMAKE_CURRENT_LIST_DIR}/kind_template.h
 143     ${KINDS_FILES}
 144     > ${CMAKE_CURRENT_BINARY_DIR}/kind.h
 145   DEPENDS mkkind kind_template.h ${KINDS_FILES}
 146 )
 147
 148 add_custom_command(
 149   OUTPUT kind.cpp
 150   COMMAND
 151     ${mkkind_script}
 152     ${CMAKE_CURRENT_LIST_DIR}/kind_template.cpp
 153     ${KINDS_FILES}
 154     > ${CMAKE_CURRENT_BINARY_DIR}/kind.cpp
 155   DEPENDS mkkind kind_template.cpp kind.h ${KINDS_FILES}
 156 )
 157
 158 add_custom_command(
 159   OUTPUT type_properties.h
 160   COMMAND
 161     ${mkkind_script}
 162     ${CMAKE_CURRENT_LIST_DIR}/type_properties_template.h
 163     ${KINDS_FILES}
 164     > ${CMAKE_CURRENT_BINARY_DIR}/type_properties.h
 165   DEPENDS mkkind type_properties_template.h ${KINDS_FILES}
 166 )
 167
 168 add_custom_command(
 169   OUTPUT metakind.h
 170   COMMAND
 171     ${mkmetakind_script}
 172     ${CMAKE_CURRENT_LIST_DIR}/metakind_template.h
 173     ${KINDS_FILES}
 174     > ${CMAKE_CURRENT_BINARY_DIR}/metakind.h
 175   DEPENDS mkmetakind metakind_template.h ${KINDS_FILES}
 176 )
 177
 178 add_custom_command(
 179   OUTPUT metakind.cpp
 180   COMMAND
 181     ${mkmetakind_script}
 182     ${CMAKE_CURRENT_LIST_DIR}/metakind_template.cpp
 183     ${KINDS_FILES}
 184     > ${CMAKE_CURRENT_BINARY_DIR}/metakind.cpp
 185   DEPENDS mkmetakind metakind_template.cpp metakind.h ${KINDS_FILES}
 186 )
 187
 188 add_custom_command(
 189   OUTPUT type_checker.cpp
 190   COMMAND
 191     ${mkexpr_script}
 192     ${CMAKE_CURRENT_LIST_DIR}/type_checker_template.cpp
 193     ${KINDS_FILES}
 194     > ${CMAKE_CURRENT_BINARY_DIR}/type_checker.cpp
 195   DEPENDS mkexpr type_checker_template.cpp ${KINDS_FILES}
 196 )
 197
 198 add_custom_target(gen-expr
 199   DEPENDS
 200     kind.cpp
 201     kind.h
 202     metakind.cpp
 203     metakind.h
 204     type_checker.cpp
 205     type_properties.h
 206 )