update c-cpp.yml && call Z3 with C++ API instead

Author: alan23273850

.github/workflows/c-cpp.yml

@@ -19,7 +19,7 @@ jobs:
     steps:
     - run: sudo apt-get install libboost-filesystem-dev libboost-test-dev z3
     - run: git clone https://github.com/alan23273850/AutoQ.git
-    - run: cd AutoQ && git checkout CTA_topdown && mkdir build && make debug
+    - run: cd AutoQ && git checkout ${{ github.ref_name }} && mkdir build && make debug
     - run: cp /usr/lib/x86_64-linux-gnu/libboost_unit_test_framework.so.1.74.0 /home/runner/work/AutoQ/AutoQ/AutoQ/build/unit_tests/
     - uses: actions/upload-artifact@v4
       with:
@@ -42,7 +42,7 @@ jobs:
     steps:
     - run: sudo apt-get install libboost-filesystem-dev libboost-test-dev z3
     - run: git clone https://github.com/alan23273850/AutoQ.git
-    - run: cd AutoQ && git checkout CTA_topdown && mkdir build && make release
+    - run: cd AutoQ && git checkout ${{ github.ref_name }} && mkdir build && make release
     - run: cp /usr/lib/x86_64-linux-gnu/libboost_unit_test_framework.so.1.74.0 /home/runner/work/AutoQ/AutoQ/AutoQ/build/unit_tests/
     - uses: actions/upload-artifact@v4
       with:

CMakeLists.txt

@@ -143,7 +143,7 @@ set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -std=c++20")
 #                                 PROJECT
 ##############################################################################
 
-project(libautoq)
+project(autoq)
 
 # Include CTest so that sophisticated testing can be done now
 include(CTest)

Makefile

@@ -3,16 +3,19 @@ MAKE_FLAGS=-j64
 # TEST_FLAGS=-j 8
 TEST_FLAGS=--output-on-failure
 
-.PHONY: debug release clean test
+.PHONY: debug release clean test create_folder
 
-debug:
+create_folder:
+	@mkdir -p $(BUILD_DIR)
+
+debug: create_folder
 	cd $(BUILD_DIR) && cmake -DCMAKE_BUILD_TYPE=Debug .. && $(MAKE) $(MAKE_FLAGS)
 
-release:
+release: create_folder
 	cd $(BUILD_DIR) && cmake -DCMAKE_BUILD_TYPE=Release .. && $(MAKE) $(MAKE_FLAGS)
 
-test:
+test: create_folder
 	cd $(BUILD_DIR) && ctest $(TEST_FLAGS)
 
-clean:
+clean: create_folder
 	cd $(BUILD_DIR) && rm -rf *

include/z3/CMakeLists.txt

@@ -0,0 +1,72 @@
+set(generated_files
+  api_commands.cpp
+  api_log_macros.cpp
+  api_log_macros.h
+)
+
+# Sanity check
+foreach (gen_file ${generated_files})
+  if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/${gen_file}")
+    message(FATAL_ERROR "\"${CMAKE_CURRENT_SOURCE_DIR}/${gen_file}\""
+            ${z3_polluted_tree_msg})
+  endif()
+endforeach()
+
+set(full_path_generated_files "")
+foreach (gen_file ${generated_files})
+  list(APPEND full_path_generated_files "${CMAKE_CURRENT_BINARY_DIR}/${gen_file}")
+endforeach()
+
+add_custom_command(OUTPUT ${generated_files}
+  COMMAND "${Python3_EXECUTABLE}"
+  "${PROJECT_SOURCE_DIR}/scripts/update_api.py"
+  ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
+  "--api_output_dir"
+  "${CMAKE_CURRENT_BINARY_DIR}"
+  DEPENDS "${PROJECT_SOURCE_DIR}/scripts/update_api.py"
+          ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
+          ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
+  COMMENT "Generating ${generated_files}"
+  USES_TERMINAL
+  VERBATIM
+)
+
+z3_add_component(api
+  SOURCES
+    api_algebraic.cpp
+    api_arith.cpp
+    api_array.cpp
+    api_ast.cpp
+    api_ast_map.cpp
+    api_ast_vector.cpp
+    api_bv.cpp
+    api_config_params.cpp
+    api_context.cpp
+    api_datalog.cpp
+    api_datatype.cpp
+    api_fpa.cpp
+    api_goal.cpp
+    api_log.cpp
+    api_model.cpp
+    api_numeral.cpp
+    api_opt.cpp
+    api_params.cpp
+    api_parsers.cpp
+    api_pb.cpp
+    api_polynomial.cpp
+    api_qe.cpp
+    api_quant.cpp
+    api_rcf.cpp
+    api_seq.cpp
+    api_solver.cpp
+    api_special_relations.cpp
+    api_stats.cpp
+    api_tactic.cpp
+    z3_replayer.cpp
+    ${full_path_generated_files}
+  COMPONENT_DEPENDENCIES
+    opt
+    portfolio
+    realclosure
+    extra_cmds
+)