mirror of
https://github.com/Z3Prover/z3
synced 2026-08-01 19:54:04 +00:00
Remove tptp5 example
Remove the examples/tptp project and its references in the CMake examples build, mk_project.py, and the CMake examples CI script. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9
This commit is contained in:
Nikolaj Bjorner
parent
1c8b6cfdb8
commit
3631d1b85c
10 changed files with 0 additions and 9915 deletions
|
|
@ -81,24 +81,6 @@ ExternalProject_Add(cpp_example
|
|||
)
|
||||
set_target_properties(cpp_example PROPERTIES EXCLUDE_FROM_ALL TRUE)
|
||||
|
||||
################################################################################
|
||||
# Build example tptp5 project using libz3's C++ API as an external project
|
||||
################################################################################
|
||||
ExternalProject_Add(z3_tptp5
|
||||
DEPENDS libz3
|
||||
# Configure step
|
||||
SOURCE_DIR "${CMAKE_CURRENT_SOURCE_DIR}/tptp"
|
||||
CMAKE_ARGS
|
||||
"-DZ3_DIR=${PROJECT_BINARY_DIR}"
|
||||
"${EXTERNAL_PROJECT_CMAKE_BUILD_TYPE_ARG}"
|
||||
# Build step
|
||||
BUILD_ALWAYS ON
|
||||
BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/tptp_build_dir"
|
||||
# Install Step
|
||||
INSTALL_COMMAND "${CMAKE_COMMAND}" -E echo "" # Dummy command
|
||||
)
|
||||
set_target_properties(z3_tptp5 PROPERTIES EXCLUDE_FROM_ALL TRUE)
|
||||
|
||||
################################################################################
|
||||
# Build example user-propagator project using libz3's C++ API as an external project
|
||||
################################################################################
|
||||
|
|
|
|||
|
|
@ -1,46 +0,0 @@
|
|||
################################################################################
|
||||
# TPTP example
|
||||
################################################################################
|
||||
project(Z3_TPTP5 CXX)
|
||||
cmake_minimum_required(VERSION 3.4)
|
||||
find_package(Z3
|
||||
REQUIRED
|
||||
CONFIG
|
||||
# `NO_DEFAULT_PATH` is set so that -DZ3_DIR has to be passed to find Z3.
|
||||
# This should prevent us from accidentally picking up an installed
|
||||
# copy of Z3. This is here to benefit Z3's build system when building
|
||||
# this project. When making your own project you probably shouldn't
|
||||
# use this option.
|
||||
NO_DEFAULT_PATH
|
||||
)
|
||||
|
||||
################################################################################
|
||||
# Z3 C++ API bindings require C++11
|
||||
################################################################################
|
||||
set(CMAKE_CXX_STANDARD 11)
|
||||
set(CMAKE_CXX_STANDARD_REQUIRED ON)
|
||||
|
||||
message(STATUS "Z3_FOUND: ${Z3_FOUND}")
|
||||
message(STATUS "Found Z3 ${Z3_VERSION_STRING}")
|
||||
message(STATUS "Z3_DIR: ${Z3_DIR}")
|
||||
|
||||
add_executable(z3_tptp5 tptp5.cpp tptp5.lex.cpp)
|
||||
target_include_directories(z3_tptp5 PRIVATE ${Z3_CXX_INCLUDE_DIRS})
|
||||
target_link_libraries(z3_tptp5 PRIVATE ${Z3_LIBRARIES})
|
||||
|
||||
if (CMAKE_SYSTEM_NAME MATCHES "[Ww]indows")
|
||||
# On Windows we need to copy the Z3 libraries
|
||||
# into the same directory as the executable
|
||||
# so that they can be found.
|
||||
foreach (z3_lib ${Z3_LIBRARIES})
|
||||
message(STATUS "Adding copy rule for ${z3_lib}")
|
||||
add_custom_command(TARGET z3_tptp5
|
||||
POST_BUILD
|
||||
COMMAND
|
||||
${CMAKE_COMMAND} -E copy_if_different
|
||||
$<TARGET_FILE:${z3_lib}>
|
||||
$<TARGET_FILE_DIR:z3_tptp5>
|
||||
)
|
||||
endforeach()
|
||||
endif()
|
||||
|
||||
|
|
@ -1,20 +0,0 @@
|
|||
TPTP front-end and utilities as a sample using the C++ bindings.
|
||||
To build the example execute
|
||||
make examples
|
||||
in the build directory.
|
||||
|
||||
This command will create the executable tptp.
|
||||
On Windows, you can just execute it.
|
||||
On macOS and Linux, you must install z3 first using
|
||||
sudo make install
|
||||
OR update LD_LIBRARY_PATH (Linux) or DYLD_LIBRARY_PATH (macOS)
|
||||
with the build directory. You need that to be able to
|
||||
find the Z3 shared library.
|
||||
|
||||
The sample illustrates using Z3 from the TPTP language.
|
||||
The TPTP language is documented on http://tptp.org
|
||||
It also exposes utilities for converting between SMT-LIB
|
||||
and TPTP format.
|
||||
|
||||
|
||||
|
||||
File diff suppressed because it is too large
Load diff
|
|
@ -1,44 +0,0 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
--*/
|
||||
|
||||
#ifndef TPTP5_H_
|
||||
#define TPTP5_H_
|
||||
|
||||
|
||||
class TreeNode;
|
||||
|
||||
#if 0
|
||||
class named_formulas {
|
||||
expr_ref_vector m_fmls;
|
||||
svector<symbol> m_names;
|
||||
bool m_has_conjecture;
|
||||
unsigned m_conjecture_index;
|
||||
public:
|
||||
named_formulas(ast_manager& m) :
|
||||
m_fmls(m),
|
||||
m_has_conjecture(false),
|
||||
m_conjecture_index(0)
|
||||
{}
|
||||
void push_back(expr* fml, char const* name) {
|
||||
m_fmls.push_back(fml);
|
||||
m_names.push_back(symbol(name));
|
||||
}
|
||||
unsigned size() const { return m_fmls.size(); }
|
||||
expr*const* data() const { return m_fmls.data(); }
|
||||
expr* operator[](unsigned i) { return m_fmls[i].get(); }
|
||||
symbol const& name(unsigned i) { return m_names[i]; }
|
||||
void set_has_conjecture() {
|
||||
m_has_conjecture = true;
|
||||
m_conjecture_index = m_fmls.size();
|
||||
}
|
||||
bool has_conjecture() const { return m_has_conjecture; }
|
||||
unsigned conjecture_index() const { return m_conjecture_index; }
|
||||
};
|
||||
|
||||
bool tptp5_parse(ast_manager& m, char const* filename, named_formulas& fmls);
|
||||
#endif
|
||||
|
||||
#endif
|
||||
File diff suppressed because it is too large
Load diff
File diff suppressed because it is too large
Load diff
|
|
@ -1,138 +0,0 @@
|
|||
/* A Bison parser, made by GNU Bison 2.4.2. */
|
||||
|
||||
/* Skeleton interface for Bison's Yacc-like parsers in C
|
||||
|
||||
Copyright (C) 1984, 1989-1990, 2000-2006, 2009-2010 Free Software
|
||||
Foundation, Inc.
|
||||
|
||||
This program is free software: you can redistribute it and/or modify
|
||||
it under the terms of the GNU General Public License as published by
|
||||
the Free Software Foundation, either version 3 of the License, or
|
||||
(at your option) any later version.
|
||||
|
||||
This program is distributed in the hope that it will be useful,
|
||||
but WITHOUT ANY WARRANTY; without even the implied warranty of
|
||||
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
||||
GNU General Public License for more details.
|
||||
|
||||
You should have received a copy of the GNU General Public License
|
||||
along with this program. If not, see <http://www.gnu.org/licenses/>. */
|
||||
|
||||
/* As a special exception, you may create a larger work that contains
|
||||
part or all of the Bison parser skeleton and distribute that work
|
||||
under terms of your choice, so long as that work isn't itself a
|
||||
parser generator using the skeleton or a modified version thereof
|
||||
as a parser skeleton. Alternatively, if you modify or redistribute
|
||||
the parser skeleton itself, you may (at your option) remove this
|
||||
special exception, which will cause the skeleton and the resulting
|
||||
Bison output files to be licensed under the GNU General Public
|
||||
License without this special exception.
|
||||
|
||||
This special exception was added by the Free Software Foundation in
|
||||
version 2.2 of Bison. */
|
||||
|
||||
|
||||
/* Tokens. */
|
||||
#ifndef YYTOKENTYPE
|
||||
# define YYTOKENTYPE
|
||||
/* Put the tokens into the symbol table, so that GDB and other debuggers
|
||||
know about them. */
|
||||
enum yytokentype {
|
||||
AMPERSAND = 258,
|
||||
AT_SIGN = 259,
|
||||
AT_SIGN_MINUS = 260,
|
||||
AT_SIGN_PLUS = 261,
|
||||
CARET = 262,
|
||||
COLON = 263,
|
||||
COLON_EQUALS = 264,
|
||||
COMMA = 265,
|
||||
EQUALS = 266,
|
||||
EQUALS_GREATER = 267,
|
||||
EXCLAMATION = 268,
|
||||
EXCLAMATION_EQUALS = 269,
|
||||
EXCLAMATION_EXCLAMATION = 270,
|
||||
EXCLAMATION_GREATER = 271,
|
||||
LBRKT = 272,
|
||||
LESS_EQUALS = 273,
|
||||
LESS_EQUALS_GREATER = 274,
|
||||
LESS_TILDE_GREATER = 275,
|
||||
LPAREN = 276,
|
||||
MINUS = 277,
|
||||
MINUS_MINUS_GREATER = 278,
|
||||
PERIOD = 279,
|
||||
QUESTION = 280,
|
||||
QUESTION_QUESTION = 281,
|
||||
QUESTION_STAR = 282,
|
||||
RBRKT = 283,
|
||||
RPAREN = 284,
|
||||
STAR = 285,
|
||||
TILDE = 286,
|
||||
TILDE_AMPERSAND = 287,
|
||||
TILDE_VLINE = 288,
|
||||
VLINE = 289,
|
||||
_DLR_cnf = 290,
|
||||
_DLR_fof = 291,
|
||||
_DLR_fot = 292,
|
||||
_DLR_itef = 293,
|
||||
_DLR_itetf = 294,
|
||||
_DLR_itett = 295,
|
||||
_DLR_tff = 296,
|
||||
_DLR_thf = 297,
|
||||
_LIT_cnf = 298,
|
||||
_LIT_fof = 299,
|
||||
_LIT_include = 300,
|
||||
_LIT_tff = 301,
|
||||
_LIT_thf = 302,
|
||||
arrow = 303,
|
||||
comment = 304,
|
||||
comment_line = 305,
|
||||
decimal = 306,
|
||||
decimal_exponent = 307,
|
||||
decimal_fraction = 308,
|
||||
distinct_object = 309,
|
||||
dollar_dollar_word = 310,
|
||||
dollar_word = 311,
|
||||
dot_decimal = 312,
|
||||
integer = 313,
|
||||
less_sign = 314,
|
||||
lower_word = 315,
|
||||
plus = 316,
|
||||
positive_decimal = 317,
|
||||
rational = 318,
|
||||
real = 319,
|
||||
signed_integer = 320,
|
||||
signed_rational = 321,
|
||||
signed_real = 322,
|
||||
single_quoted = 323,
|
||||
star = 324,
|
||||
unrecognized = 325,
|
||||
unsigned_integer = 326,
|
||||
unsigned_rational = 327,
|
||||
unsigned_real = 328,
|
||||
upper_word = 329,
|
||||
vline = 330
|
||||
};
|
||||
#endif
|
||||
|
||||
|
||||
|
||||
#if ! defined YYSTYPE && ! defined YYSTYPE_IS_DECLARED
|
||||
typedef union YYSTYPE
|
||||
{
|
||||
|
||||
/* Line 1685 of yacc.c */
|
||||
#line 148 "tptp5.y"
|
||||
int ival; double dval; char* sval; TreeNode* pval;
|
||||
|
||||
|
||||
/* Line 1685 of yacc.c */
|
||||
#line 130 "tptp5.tab.h"
|
||||
} YYSTYPE;
|
||||
# define YYSTYPE_IS_TRIVIAL 1
|
||||
# define yystype YYSTYPE /* obsolescent; will be withdrawn */
|
||||
# define YYSTYPE_IS_DECLARED 1
|
||||
#endif
|
||||
|
||||
extern YYSTYPE yylval;
|
||||
|
||||
|
||||
|
|
@ -117,7 +117,6 @@ def init_project_def():
|
|||
add_js()
|
||||
# Examples
|
||||
add_cpp_example('cpp_example', 'c++')
|
||||
add_cpp_example('z3_tptp', 'tptp')
|
||||
add_c_example('c_example', 'c')
|
||||
add_c_example('maxsat')
|
||||
add_dotnet_example('dotnet_example', 'dotnet')
|
||||
|
|
|
|||
|
|
@ -4,11 +4,9 @@ steps:
|
|||
cd build
|
||||
ninja c_example
|
||||
ninja cpp_example
|
||||
ninja z3_tptp5
|
||||
ninja c_maxsat_example
|
||||
examples/c_example_build_dir/c_example
|
||||
examples/cpp_example_build_dir/cpp_example
|
||||
examples/tptp_build_dir/z3_tptp5 -help
|
||||
examples/c_maxsat_example_build_dir/c_maxsat_example ../examples/maxsat/ex.smt
|
||||
cd ..
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue