mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 13:53:39 +00:00
Code Activity

Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt

Browse source
This commit is contained in:
Nikolaj Bjorner 2017-07-27 18:42:16 -07:00
commit 1946441e17
444 changed files with 9311 additions and 4882 deletions
Download patch file Download diff file Expand all files Collapse all files

261
src/CMakeLists.txt Normal file
View file

@ -0,0 +1,261 @@
################################################################################
# API header files
################################################################################
# This lists the API header files that are scanned by
# some of the build rules to generate some files needed
# by the build
set(Z3_API_HEADER_FILES_TO_SCAN
z3_api.h
z3_ast_containers.h
z3_algebraic.h
z3_polynomial.h
z3_rcf.h
z3_fixedpoint.h
z3_optimization.h
z3_interp.h
z3_fpa.h
)
set(Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN "")
foreach (header_file ${Z3_API_HEADER_FILES_TO_SCAN})
set(full_path_api_header_file "${CMAKE_CURRENT_SOURCE_DIR}/api/${header_file}")
list(APPEND Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN "${full_path_api_header_file}")
if (NOT EXISTS "${full_path_api_header_file}")
message(FATAL_ERROR "API header file \"${full_path_api_header_file}\" does not exist")
endif()
endforeach()
################################################################################
# Traverse directories each adding a Z3 component
################################################################################
# I'm duplicating the order in ``mk_project.py`` for now to help us keep
# the build systems in sync.
#
# The components in these directory explicitly declare their dependencies so
# you may be able to re-order some of these directories but an error will be
# raised if you try to declare a component is dependent on another component
# that has not yet been declared.
add_subdirectory(util)
add_subdirectory(math/polynomial)
add_subdirectory(sat)
add_subdirectory(nlsat)
add_subdirectory(util/lp)
add_subdirectory(math/hilbert)
add_subdirectory(math/simplex)
add_subdirectory(math/automata)
add_subdirectory(math/interval)
add_subdirectory(math/realclosure)
add_subdirectory(math/subpaving)
add_subdirectory(ast)
add_subdirectory(ast/rewriter)
add_subdirectory(ast/normal_forms)
add_subdirectory(model)
add_subdirectory(tactic)
add_subdirectory(ast/substitution)
add_subdirectory(parsers/util)
add_subdirectory(math/grobner)
add_subdirectory(math/euclid)
add_subdirectory(tactic/core)
add_subdirectory(sat/tactic)
add_subdirectory(tactic/arith)
add_subdirectory(nlsat/tactic)
add_subdirectory(math/subpaving/tactic)
add_subdirectory(tactic/aig)
add_subdirectory(solver)
add_subdirectory(ackermannization)
add_subdirectory(interp)
add_subdirectory(cmd_context)
add_subdirectory(cmd_context/extra_cmds)
add_subdirectory(parsers/smt2)
add_subdirectory(ast/proof_checker)
## Simplifier module will be deleted in the future.
## It has been replaced with rewriter component.
add_subdirectory(ast/simplifier)
add_subdirectory(ast/fpa)
add_subdirectory(ast/macros)
add_subdirectory(ast/pattern)
add_subdirectory(ast/rewriter/bit_blaster)
add_subdirectory(smt/params)
add_subdirectory(smt/proto_model)
add_subdirectory(smt)
add_subdirectory(tactic/bv)
add_subdirectory(smt/tactic)
add_subdirectory(tactic/sls)
add_subdirectory(qe)
add_subdirectory(duality)
add_subdirectory(muz/base)
add_subdirectory(muz/dataflow)
add_subdirectory(muz/transforms)
add_subdirectory(muz/rel)
add_subdirectory(muz/pdr)
add_subdirectory(muz/clp)
add_subdirectory(muz/tab)
add_subdirectory(muz/bmc)
add_subdirectory(muz/ddnf)
add_subdirectory(muz/duality)
add_subdirectory(muz/fp)
add_subdirectory(tactic/nlsat_smt)
add_subdirectory(tactic/ufbv)
add_subdirectory(sat/sat_solver)
add_subdirectory(tactic/smtlogics)
add_subdirectory(tactic/fpa)
add_subdirectory(tactic/portfolio)
add_subdirectory(parsers/smt)
add_subdirectory(opt)
add_subdirectory(api)
add_subdirectory(api/dll)
################################################################################
# libz3
################################################################################
get_property(Z3_LIBZ3_COMPONENTS_LIST GLOBAL PROPERTY Z3_LIBZ3_COMPONENTS)
set (object_files "")
foreach (component ${Z3_LIBZ3_COMPONENTS_LIST})
list(APPEND object_files $<TARGET_OBJECTS:${component}>)
endforeach()
if (BUILD_LIBZ3_SHARED)
set(lib_type "SHARED")
else()
set(lib_type "STATIC")
endif()
add_library(libz3 ${lib_type} ${object_files})
set_target_properties(libz3 PROPERTIES
# VERSION determines the version in the filename of the shared library.
# SOVERSION determines the value of the DT_SONAME field on ELF platforms.
# On ELF platforms the final compiled filename will be libz3.so.W.X.Y.Z
# but symlinks will be made to this file from libz3.so and also from
# libz3.so.W.X.
# This indicates that no breaking API changes will be made within a single
# minor version.
VERSION ${Z3_VERSION}
SOVERSION ${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR})
if (NOT MSVC)
# On UNIX like platforms if we don't change the OUTPUT_NAME
# the library gets a name like ``liblibz3.so`` so we change it
# here. We don't do a rename with MSVC because we get file naming
# conflicts (the z3 executable also has this OUTPUT_NAME) with
# ``.ilk``, ``.pdb``, ``.lib`` and ``.exp`` files sharing the same
# prefix.
set_target_properties(libz3 PROPERTIES OUTPUT_NAME z3)
endif()
# The `PRIVATE` usage requirement is specified so that when building Z3 as a
# shared library the dependent libraries are specified on the link command line
# so that if those are also shared libraries they are referenced by `libz3.so`.
target_link_libraries(libz3 PRIVATE ${Z3_DEPENDENT_LIBS})
# This is currently only for the OpenMP flags. It needs to be set
# via `target_link_libraries()` rather than `z3_append_linker_flag_list_to_target()`
# because when building the `libz3` as a static library when the target is exported
# the link dependencies need to be exported too.
foreach (flag_name ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS})
target_link_libraries(libz3 PRIVATE ${flag_name})
endforeach()
# Declare which header file are the public header files of libz3
# these will automatically installed when the libz3 target is installed
set (libz3_public_headers
z3_algebraic.h
z3_api.h
z3_ast_containers.h
z3_fixedpoint.h
z3_fpa.h
z3.h
c++/z3++.h
z3_interp.h
z3_macros.h
z3_optimization.h
z3_polynomial.h
z3_rcf.h
z3_v1.h
)
foreach (header ${libz3_public_headers})
set_property(TARGET libz3 APPEND PROPERTY
PUBLIC_HEADER "${CMAKE_SOURCE_DIR}/src/api/${header}")
endforeach()
install(TARGETS libz3
EXPORT Z3_EXPORTED_TARGETS
LIBRARY DESTINATION "${CMAKE_INSTALL_LIBDIR}"
ARCHIVE DESTINATION "${CMAKE_INSTALL_LIBDIR}" # On Windows this installs ``libz3.lib`` which CMake calls the "corresponding import library". Do we want this installed?
RUNTIME DESTINATION "${CMAKE_INSTALL_LIBDIR}" # For Windows. DLLs are runtime targets for CMake
PUBLIC_HEADER DESTINATION "${CMAKE_INSTALL_INCLUDEDIR}"
)
if (MSVC)
# Handle settings dll exports when using MSVC
# FIXME: This seems unnecessarily complicated but I'm doing
# this because this is what the python build system does.
# CMake has a much more elegant (see ``GenerateExportHeader.cmake``)
# way of handling this.
set(dll_module_exports_file "${CMAKE_CURRENT_BINARY_DIR}/api_dll.def")
add_custom_command(OUTPUT "${dll_module_exports_file}"
COMMAND
"${PYTHON_EXECUTABLE}"
"${CMAKE_SOURCE_DIR}/scripts/mk_def_file.py"
"${dll_module_exports_file}"
"libz3"
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
DEPENDS
"${CMAKE_SOURCE_DIR}/scripts/mk_def_file.py"
${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
COMMENT "Generating \"${dll_module_exports_file}\""
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
VERBATIM
)
add_custom_target(libz3_extra_depends
DEPENDS "${dll_module_exports_file}"
)
add_dependencies(libz3 libz3_extra_depends)
z3_append_linker_flag_list_to_target(libz3 "/DEF:${dll_module_exports_file}")
endif()
################################################################################
# Z3 executable
################################################################################
add_subdirectory(shell)
################################################################################
# z3-test
################################################################################
add_subdirectory(test)
################################################################################
# Z3 API bindings
################################################################################
option(BUILD_PYTHON_BINDINGS "Build Python bindings for Z3" OFF)
if (BUILD_PYTHON_BINDINGS)
if (NOT BUILD_LIBZ3_SHARED)
message(FATAL_ERROR "The python bindings will not work with a static libz3. "
"You either need to disable BUILD_PYTHON_BINDINGS or enable BUILD_LIBZ3_SHARED")
endif()
add_subdirectory(api/python)
endif()
################################################################################
# .NET bindings
################################################################################
option(BUILD_DOTNET_BINDINGS "Build .NET bindings for Z3" OFF)
if (BUILD_DOTNET_BINDINGS)
if (NOT BUILD_LIBZ3_SHARED)
message(FATAL_ERROR "The .NET bindings will not work with a static libz3. "
"You either need to disable BUILD_DOTNET_BINDINGS or enable BUILD_LIBZ3_SHARED")
endif()
add_subdirectory(api/dotnet)
endif()
################################################################################
# Java bindings
################################################################################
option(BUILD_JAVA_BINDINGS "Build Java bindings for Z3" OFF)
if (BUILD_JAVA_BINDINGS)
if (NOT BUILD_LIBZ3_SHARED)
message(FATAL_ERROR "The Java bindings will not work with a static libz3. "
"You either need to disable BUILD_JAVA_BINDINGS or enable BUILD_LIBZ3_SHARED")
endif()
add_subdirectory(api/java)
endif()
# TODO: Implement support for other bindigns

23
src/ackermannization/CMakeLists.txt Normal file
View file

@ -0,0 +1,23 @@
z3_add_component(ackermannization
SOURCES
ackermannize_bv_model_converter.cpp
ackermannize_bv_tactic.cpp
ackr_bound_probe.cpp
ackr_helper.cpp
ackr_model_converter.cpp
lackr.cpp
lackr_model_constructor.cpp
lackr_model_converter_lazy.cpp
COMPONENT_DEPENDENCIES
ast
model
rewriter
solver
tactic
PYG_FILES
ackermannization_params.pyg
ackermannize_bv_tactic_params.pyg
TACTIC_HEADERS
ackermannize_bv_tactic.h
ackr_bound_probe.h
)

74
src/api/CMakeLists.txt Normal file
View file

@ -0,0 +1,74 @@
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 "${PYTHON_EXECUTABLE}"
"${CMAKE_SOURCE_DIR}/scripts/update_api.py"
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
"--api_output_dir"
"${CMAKE_CURRENT_BINARY_DIR}"
DEPENDS "${CMAKE_SOURCE_DIR}/scripts/update_api.py"
${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
# FIXME: When update_api.py no longer uses ``mk_util`` drop this dependency
"${CMAKE_SOURCE_DIR}/scripts/mk_util.py"
COMMENT "Generating ${generated_files}"
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
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_interp.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_quant.cpp
api_rcf.cpp
api_seq.cpp
api_solver.cpp
api_stats.cpp
api_tactic.cpp
z3_replayer.cpp
${full_path_generated_files}
COMPONENT_DEPENDENCIES
interp
opt
portfolio
realclosure
smtparser
)

11
src/api/api_ast.cpp
View file

@ -558,6 +558,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_get_sort(c, a);
RESET_ERROR_CODE();
CHECK_IS_EXPR(a, 0);
Z3_sort r = of_sort(mk_c(c)->m().get_sort(to_expr(a)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
@ -821,9 +822,13 @@ extern "C" {
RESET_ERROR_CODE();
std::ostringstream buffer;
switch (mk_c(c)->get_print_mode()) {
case Z3_PRINT_SMTLIB_FULL:
buffer << mk_pp(to_ast(a), mk_c(c)->m());
case Z3_PRINT_SMTLIB_FULL: {
params_ref p;
p.set_uint("max_depth", 4294967295u);
p.set_uint("min_alias_size", 4294967295u);
buffer << mk_pp(to_ast(a), mk_c(c)->m(), p);
break;
}
case Z3_PRINT_LOW_LEVEL:
buffer << mk_ll_pp(to_ast(a), mk_c(c)->m());
break;
@ -1066,7 +1071,7 @@ extern "C" {
case OP_BIT2BOOL: return Z3_OP_BIT2BOOL;
case OP_BSMUL_NO_OVFL: return Z3_OP_BSMUL_NO_OVFL;
case OP_BUMUL_NO_OVFL: return Z3_OP_BUMUL_NO_OVFL;
case OP_BSMUL_NO_UDFL: return Z3_OP_BSMUL_NO_UDFL;
case OP_BSMUL_NO_UDFL: return Z3_OP_BSMUL_NO_UDFL;
case OP_BSDIV_I: return Z3_OP_BSDIV_I;
case OP_BUDIV_I: return Z3_OP_BUDIV_I;
case OP_BSREM_I: return Z3_OP_BSREM_I;

10
src/api/api_datatype.cpp
View file

@ -52,7 +52,7 @@ extern "C" {
{
datatype_decl * dt = mk_datatype_decl(to_symbol(name), 1, constrs);
bool is_ok = mk_c(c)->get_dt_plugin()->mk_datatypes(1, &dt, tuples);
bool is_ok = mk_c(c)->get_dt_plugin()->mk_datatypes(1, &dt, 0, 0, tuples);
del_datatype_decl(dt);
if (!is_ok) {
@ -119,7 +119,7 @@ extern "C" {
{
datatype_decl * dt = mk_datatype_decl(to_symbol(name), n, constrs.c_ptr());
bool is_ok = mk_c(c)->get_dt_plugin()->mk_datatypes(1, &dt, sorts);
bool is_ok = mk_c(c)->get_dt_plugin()->mk_datatypes(1, &dt, 0, 0, sorts);
del_datatype_decl(dt);
if (!is_ok) {
@ -180,7 +180,7 @@ extern "C" {
sort_ref_vector sorts(m);
{
datatype_decl * decl = mk_datatype_decl(to_symbol(name), 2, constrs);
bool is_ok = mk_c(c)->get_dt_plugin()->mk_datatypes(1, &decl, sorts);
bool is_ok = mk_c(c)->get_dt_plugin()->mk_datatypes(1, &decl, 0, 0, sorts);
del_datatype_decl(decl);
if (!is_ok) {
@ -357,7 +357,7 @@ extern "C" {
sort_ref_vector sorts(m);
{
datatype_decl * data = mk_datatype_decl(c, name, num_constructors, constructors);
bool is_ok = mk_c(c)->get_dt_plugin()->mk_datatypes(1, &data, sorts);
bool is_ok = mk_c(c)->get_dt_plugin()->mk_datatypes(1, &data, 0, 0, sorts);
del_datatype_decl(data);
if (!is_ok) {
@ -420,7 +420,7 @@ extern "C" {
datas.push_back(mk_datatype_decl(c,sort_names[i], cl->size(), reinterpret_cast<Z3_constructor*>(cl->c_ptr())));
}
sort_ref_vector _sorts(m);
bool ok = mk_c(c)->get_dt_plugin()->mk_datatypes(datas.size(), datas.c_ptr(), _sorts);
bool ok = mk_c(c)->get_dt_plugin()->mk_datatypes(datas.size(), datas.c_ptr(), 0, 0, _sorts);
del_datatype_decls(datas.size(), datas.c_ptr());
if (!ok) {

4
src/api/c++/z3++.h
View file

@ -87,7 +87,7 @@ namespace z3 {
inline std::ostream & operator<<(std::ostream & out, exception const & e) { out << e.msg(); return out; }
#if !defined(Z3_THROW)
#if __cpp_exceptions || _CPPUNWIND
#if __cpp_exceptions || _CPPUNWIND || __EXCEPTIONS
#define Z3_THROW(x) throw x
#else
#define Z3_THROW(x) {}
@ -2796,6 +2796,6 @@ namespace z3 {
/*@}*/
/*@}*/
#undef Z3_THROW
#endif

13
src/api/dll/CMakeLists.txt Normal file
View file

@ -0,0 +1,13 @@
set(api_dll_deps api extra_cmds sat)
z3_add_component(api_dll
SOURCES
dll.cpp
"${CMAKE_CURRENT_BINARY_DIR}/gparams_register_modules.cpp"
"${CMAKE_CURRENT_BINARY_DIR}/install_tactic.cpp"
"${CMAKE_CURRENT_BINARY_DIR}/mem_initializer.cpp"
COMPONENT_DEPENDENCIES
${api_dll_deps}
)
z3_add_install_tactic_rule(${api_dll_deps})
z3_add_memory_initializer_rule(${api_dll_deps})
z3_add_gparams_register_modules_rule(${api_dll_deps})

16
src/api/dotnet/AST.cs
View file

@ -14,7 +14,7 @@ Author:
Christoph Wintersteiger (cwinter) 2012-03-16
Notes:
--*/
using System;
@ -25,7 +25,7 @@ using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// The abstract syntax tree (AST) class.
/// The abstract syntax tree (AST) class.
/// </summary>
[ContractVerification(true)]
public class AST : Z3Object, IComparable
@ -35,7 +35,7 @@ namespace Microsoft.Z3
/// </summary>
/// <param name="a">An AST</param>
/// <param name="b">An AST</param>
/// <returns>True if <paramref name="a"/> and <paramref name="b"/> are from the same context
/// <returns>True if <paramref name="a"/> and <paramref name="b"/> are from the same context
/// and represent the same sort; false otherwise.</returns>
public static bool operator ==(AST a, AST b)
{
@ -51,7 +51,7 @@ namespace Microsoft.Z3
/// </summary>
/// <param name="a">An AST</param>
/// <param name="b">An AST</param>
/// <returns>True if <paramref name="a"/> and <paramref name="b"/> are not from the same context
/// <returns>True if <paramref name="a"/> and <paramref name="b"/> are not from the same context
/// or represent different sorts; false otherwise.</returns>
public static bool operator !=(AST a, AST b)
{
@ -120,12 +120,12 @@ namespace Microsoft.Z3
if (ReferenceEquals(Context, ctx))
return this;
else
return new AST(ctx, Native.Z3_translate(Context.nCtx, NativeObject, ctx.nCtx));
return Create(ctx, Native.Z3_translate(Context.nCtx, NativeObject, ctx.nCtx));
}
/// <summary>
/// The kind of the AST.
/// </summary>
/// </summary>
public Z3_ast_kind ASTKind
{
get { return (Z3_ast_kind)Native.Z3_get_ast_kind(Context.nCtx, NativeObject); }
@ -224,10 +224,10 @@ namespace Microsoft.Z3
{
Native.Z3_dec_ref(ctx.nCtx, obj);
}
};
};
internal override void IncRef(IntPtr o)
{
{
// Console.WriteLine("AST IncRef()");
if (Context == null || o == IntPtr.Zero)
return;

291
src/api/dotnet/CMakeLists.txt Normal file
View file

@ -0,0 +1,291 @@
find_package(DotNetToolchain REQUIRED)
# Configure AssemblyInfo.cs
set(VER_MAJOR "${Z3_VERSION_MAJOR}")
set(VER_MINOR "${Z3_VERSION_MINOR}")
set(VER_BUILD "${Z3_VERSION_PATCH}")
set(VER_REVISION "${Z3_VERSION_TWEAK}")
set(Z3_DOTNET_ASSEMBLY_INFO_FILE "${CMAKE_CURRENT_BINARY_DIR}/Properties/AssemblyInfo.cs")
configure_file("Properties/AssemblyInfo.cs.in" "${Z3_DOTNET_ASSEMBLY_INFO_FILE}" @ONLY)
# Generate Native.cs
set(Z3_DOTNET_NATIVE_FILE "${CMAKE_CURRENT_BINARY_DIR}/Native.cs")
add_custom_command(OUTPUT "${Z3_DOTNET_NATIVE_FILE}"
COMMAND "${PYTHON_EXECUTABLE}"
"${CMAKE_SOURCE_DIR}/scripts/update_api.py"
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
"--dotnet-output-dir"
"${CMAKE_CURRENT_BINARY_DIR}"
DEPENDS
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
"${CMAKE_SOURCE_DIR}/scripts/update_api.py"
${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
# FIXME: When update_api.py no longer uses ``mk_util`` drop this dependency
"${CMAKE_SOURCE_DIR}/scripts/mk_util.py"
COMMENT "Generating ${Z3_DOTNET_NATIVE_FILE}"
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
)
# Generate Enumerations.cs
set(Z3_DOTNET_CONST_FILE "${CMAKE_CURRENT_BINARY_DIR}/Enumerations.cs")
add_custom_command(OUTPUT "${Z3_DOTNET_CONST_FILE}"
COMMAND "${PYTHON_EXECUTABLE}"
"${CMAKE_SOURCE_DIR}/scripts/mk_consts_files.py"
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
"--dotnet-output-dir"
"${CMAKE_CURRENT_BINARY_DIR}"
DEPENDS
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
"${CMAKE_SOURCE_DIR}/scripts/mk_consts_files.py"
${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
COMMENT "Generating ${Z3_DOTNET_CONST_FILE}"
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
)
set(Z3_DOTNET_ASSEMBLY_SOURCES_IN_SRC_TREE
AlgebraicNum.cs
ApplyResult.cs
ArithExpr.cs
ArithSort.cs
ArrayExpr.cs
ArraySort.cs
AST.cs
ASTMap.cs
ASTVector.cs
BitVecExpr.cs
BitVecNum.cs
BitVecSort.cs
BoolExpr.cs
BoolSort.cs
Constructor.cs
ConstructorList.cs
Context.cs
DatatypeExpr.cs
DatatypeSort.cs
Deprecated.cs
EnumSort.cs
Expr.cs
FiniteDomainExpr.cs
FiniteDomainNum.cs
FiniteDomainSort.cs
Fixedpoint.cs
FPExpr.cs
FPNum.cs
FPRMExpr.cs
FPRMNum.cs
FPRMSort.cs
FPSort.cs
FuncDecl.cs
FuncInterp.cs
Global.cs
Goal.cs
IDecRefQueue.cs
InterpolationContext.cs
IntExpr.cs
IntNum.cs
IntSort.cs
IntSymbol.cs
ListSort.cs
Log.cs
Model.cs
Optimize.cs
ParamDescrs.cs
Params.cs
Pattern.cs
Probe.cs
Quantifier.cs
RatNum.cs
RealExpr.cs
RealSort.cs
ReExpr.cs
RelationSort.cs
ReSort.cs
SeqExpr.cs
SeqSort.cs
SetSort.cs
Solver.cs
Sort.cs
Statistics.cs
Status.cs
StringSymbol.cs
Symbol.cs
Tactic.cs
TupleSort.cs
UninterpretedSort.cs
Version.cs
Z3Exception.cs
Z3Object.cs
)
set(Z3_DOTNET_ASSEMBLY_SOURCES "")
# Make paths to source files absolute
foreach (csfile ${Z3_DOTNET_ASSEMBLY_SOURCES_IN_SRC_TREE})
list(APPEND Z3_DOTNET_ASSEMBLY_SOURCES "${CMAKE_CURRENT_SOURCE_DIR}/${csfile}")
endforeach()
# Add generated files
list(APPEND Z3_DOTNET_ASSEMBLY_SOURCES
"${Z3_DOTNET_CONST_FILE}"
"${Z3_DOTNET_NATIVE_FILE}"
"${Z3_DOTNET_ASSEMBLY_INFO_FILE}"
)
# ``csc.exe`` doesn't like UNIX style paths so convert them
# if necessary first to native paths.
set(Z3_DOTNET_ASSEMBLY_SOURCES_NATIVE_PATH "")
foreach (csfile_path ${Z3_DOTNET_ASSEMBLY_SOURCES})
file(TO_NATIVE_PATH "${csfile_path}" csfile_path_native)
list(APPEND Z3_DOTNET_ASSEMBLY_SOURCES_NATIVE_PATH "${csfile_path_native}")
endforeach()
set(CSC_FLAGS "")
if (DOTNET_TOOLCHAIN_IS_WINDOWS)
# FIXME: Why use these flags?
# Note these flags have been copied from the Python build system.
list(APPEND CSC_FLAGS
"/noconfig"
"/nostdlib+"
"/reference:mscorlib.dll"
)
# FIXME: This flag only works when the working directory of csc.exe is
# the directory containing the ``libz3`` target. I can't get this to work
# correctly with multi-configuration generators (i.e. Visual Studio) so
# just don't set the flag for now.
#list(APPEND CSC_FLAGS "/linkresource:$<TARGET_FILE_NAME:libz3>")
elseif (DOTNET_TOOLCHAIN_IS_MONO)
# We need to give the assembly a strong name so that it can be installed
# into the GAC.
list(APPEND CSC_FLAGS
"/keyfile:${CMAKE_CURRENT_SOURCE_DIR}/Microsoft.Z3.snk"
)
else()
message(FATAL_ERROR "Unknown .NET toolchain")
endif()
# Common flags
list(APPEND CSC_FLAGS
"/unsafe+"
"/nowarn:1701,1702"
"/errorreport:prompt"
"/warn:4"
"/reference:System.Core.dll"
"/reference:System.dll"
"/reference:System.Numerics.dll"
"/filealign:512" # Why?
"/target:library"
)
# Set the build type flags. The build type for the assembly roughly corresponds
# with the native code build type.
list(APPEND CSC_FLAGS
# Debug flags, expands to nothing if we aren't doing a debug build
"$<$<CONFIG:Debug>:/debug+>"
"$<$<CONFIG:Debug>:/debug:full>"
"$<$<CONFIG:Debug>:/optimize->"
# This has to be quoted otherwise the ``;`` is interpreted as a command separator
"$<$<CONFIG:Debug>:\"/define:DEBUG$<SEMICOLON>TRACE\">"
# Release flags, expands to nothing if we are doing a debug build
"$<$<NOT:$<CONFIG:Debug>>:/optimize+>"
)
# Mono's gacutil crashes when trying to install an assembly if we set the
# platform in some cases, so only set it on Windows. This bug has been
# reported at https://bugzilla.xamarin.com/show_bug.cgi?id=39955 . However mono
# ignores the platform of an assembly when running it (
# http://lists.ximian.com/pipermail/mono-devel-list/2015-November/043370.html )
# so this shouldn't matter in practice.
if (DOTNET_TOOLCHAIN_IS_WINDOWS)
# Set platform for assembly
if ("${TARGET_ARCHITECTURE}" STREQUAL "x86_64")
list(APPEND CSC_FLAGS "/platform:x64")
elseif ("${TARGET_ARCHITECTURE}" STREQUAL "i686")
list(APPEND CSC_FLAGS "/platform:x86")
endif()
endif()
# FIXME: Ideally we should emit files into a configuration specific directory
# when using multi-configuration generators so that the files generated by each
# configuration don't clobber each other. Unfortunately the ``get_property()``
# command only works correctly for single configuration generators so we can't
# use it. We also can't use ``$<TARGET_FILE_DIR:libz3>`` because the ``OUTPUT``
# argument to ``add_custom_commands()`` won't accept it.
# See http://public.kitware.com/pipermail/cmake/2016-March/063101.html
#
# For now just output file to the root binary directory like the Python build
# system does and emit a warning when appropriate.
if (DEFINED CMAKE_CONFIGURATION_TYPES)
# Multi-configuration build (e.g. Visual Studio and Xcode).
message(WARNING "You are using a multi-configuration generator. The build rules for"
" the \".NET\" bindings currently do not emit files per configuration so previously"
" generated files for other configurations will be overwritten.")
endif()
set(Z3_DOTNET_ASSEMBLY_OUTPUT_DIR "${CMAKE_BINARY_DIR}")
set(Z3_DOTNET_ASSEMBLY_NAME "Microsoft.Z3.dll")
set(Z3_DOTNET_ASSEMBLY_DLL "${Z3_DOTNET_ASSEMBLY_OUTPUT_DIR}/${Z3_DOTNET_ASSEMBLY_NAME}")
# csc.exe doesn't work with UNIX style paths so convert to native path
file(TO_NATIVE_PATH "${Z3_DOTNET_ASSEMBLY_DLL}" Z3_DOTNET_ASSEMBLY_DLL_NATIVE_PATH)
set(Z3_DOTNET_ASSEMBLY_DLL_DOC "${Z3_DOTNET_ASSEMBLY_OUTPUT_DIR}/Microsoft.Z3.xml")
file(TO_NATIVE_PATH "${Z3_DOTNET_ASSEMBLY_DLL_DOC}" Z3_DOTNET_ASSEMBLY_DLL_DOC_NATIVE_PATH)
add_custom_command(OUTPUT "${Z3_DOTNET_ASSEMBLY_DLL}" "${Z3_DOTNET_ASSEMBLY_DLL_DOC}"
COMMAND
"${DOTNET_CSC_EXECUTABLE}"
${CSC_FLAGS}
"/out:${Z3_DOTNET_ASSEMBLY_DLL_NATIVE_PATH}"
"/doc:${Z3_DOTNET_ASSEMBLY_DLL_DOC_NATIVE_PATH}"
${Z3_DOTNET_ASSEMBLY_SOURCES_NATIVE_PATH}
DEPENDS
${Z3_DOTNET_ASSEMBLY_SOURCES}
libz3
WORKING_DIRECTORY "${Z3_DOTNET_ASSEMBLY_OUTPUT_DIR}"
COMMENT "Building \"${Z3_DOTNET_ASSEMBLY_DLL}\""
)
# Convenient top-level target
add_custom_target(build_z3_dotnet_bindings
ALL
DEPENDS
"${Z3_DOTNET_ASSEMBLY_DLL}"
)
###############################################################################
# Install
###############################################################################
option(INSTALL_DOTNET_BINDINGS "Install .NET bindings when invoking install target" ON)
set(GAC_PKG_NAME "Microsoft.Z3.Sharp")
set(PREFIX "${CMAKE_INSTALL_PREFIX}")
set(VERSION "${Z3_VERSION}")
set(Z3_DOTNET_PKGCONFIG_FILE "${CMAKE_CURRENT_BINARY_DIR}/Microsoft.Z3.Sharp.pc")
configure_file("Microsoft.Z3.Sharp.pc.in" "${Z3_DOTNET_PKGCONFIG_FILE}" @ONLY)
if (DOTNET_TOOLCHAIN_IS_MONO)
message(STATUS "Emitting install rules for .NET bindings")
# Install pkgconfig file for the assembly. This is needed by Monodevelop
# to find the assembly
install(FILES "${Z3_DOTNET_PKGCONFIG_FILE}" DESTINATION "${CMAKE_INSTALL_PKGCONFIGDIR}")
# Configure the install and uninstall scripts.
# Note: If multi-configuration generator support is ever fixed then these
# scripts will be broken.
configure_file(cmake_install_gac.cmake.in cmake_install_gac.cmake @ONLY)
configure_file(cmake_uninstall_gac.cmake.in cmake_uninstall_gac.cmake @ONLY)
# Tell CMake to Invoke a script to install assembly to the GAC during install
install(SCRIPT "${CMAKE_CURRENT_BINARY_DIR}/cmake_install_gac.cmake")
# Add custom target to uninstall the assembly from the GAC
add_custom_target(remove_dotnet_dll_from_gac
COMMAND "${CMAKE_COMMAND}" "-P" "${CMAKE_CURRENT_BINARY_DIR}/cmake_uninstall_gac.cmake"
COMMENT "Uninstalling ${Z3_DOTNET_ASSEMBLY_NAME} from the GAC"
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
)
add_dependencies(uninstall remove_dotnet_dll_from_gac)
elseif(DOTNET_TOOLCHAIN_IS_WINDOWS)
# Don't install Z3_DOTNET_ASSEMBLY_DLL into the gac. Instead just copy into
# installation directory.
install(FILES "${Z3_DOTNET_ASSEMBLY_DLL}" DESTINATION "${CMAKE_INSTALL_LIBDIR}")
install(FILES "${Z3_DOTNET_ASSEMBLY_DLL_DOC}" DESTINATION "${CMAKE_INSTALL_LIBDIR}")
else()
message(FATAL_ERROR "Unknown .NET toolchain")
endif()

65
src/api/dotnet/Expr.cs
View file

@ -163,13 +163,7 @@ namespace Microsoft.Z3
/// <returns>A copy of the term which is associated with <paramref name="ctx"/></returns>
new public Expr Translate(Context ctx)
{
Contract.Requires(ctx != null);
Contract.Ensures(Contract.Result<Expr>() != null);
if (ReferenceEquals(Context, ctx))
return this;
else
return Expr.Create(ctx, Native.Z3_translate(Context.nCtx, NativeObject, ctx.nCtx));
return (Expr)base.Translate(ctx);
}
/// <summary>
@ -809,7 +803,62 @@ namespace Microsoft.Z3
/// Retrieve string corresponding to string constant.
/// </summary>
/// <remarks>the expression should be a string constant, (IsString should be true).</remarks>
public string String { get { return Native.Z3_get_string(Context.nCtx, NativeObject); } }
public string String { get { return Native.Z3_get_string(Context.nCtx, NativeObject); } }
/// <summary>
/// Check whether expression is a concatentation.
/// </summary>
/// <returns>a Boolean</returns>
public bool IsConcat { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_CONCAT; } }
/// <summary>
/// Check whether expression is a prefix.
/// </summary>
/// <returns>a Boolean</returns>
public bool IsPrefix { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_PREFIX; } }
/// <summary>
/// Check whether expression is a suffix.
/// </summary>
/// <returns>a Boolean</returns>
public bool IsSuffix { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_SUFFIX; } }
/// <summary>
/// Check whether expression is a contains.
/// </summary>
/// <returns>a Boolean</returns>
public bool IsContains { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_CONTAINS; } }
/// <summary>
/// Check whether expression is an extract.
/// </summary>
/// <returns>a Boolean</returns>
public bool IsExtract { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_EXTRACT; } }
/// <summary>
/// Check whether expression is a replace.
/// </summary>
/// <returns>a Boolean</returns>
public bool IsReplace { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_REPLACE; } }
/// <summary>
/// Check whether expression is an at.
/// </summary>
/// <returns>a Boolean</returns>
public bool IsAt { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_AT; } }
/// <summary>
/// Check whether expression is a sequence length.
/// </summary>
/// <returns>a Boolean</returns>
public bool IsLength { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_LENGTH; } }
/// <summary>
/// Check whether expression is a sequence index.
/// </summary>
/// <returns>a Boolean</returns>
public bool IsIndex { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_INDEX; } }
#endregion

20
src/api/dotnet/FuncDecl.cs
View file

@ -14,7 +14,7 @@ Author:
Christoph Wintersteiger (cwinter) 2012-03-16
Notes:
--*/
using System;
@ -23,7 +23,7 @@ using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// Function declarations.
/// Function declarations.
/// </summary>
[ContractVerification(true)]
public class FuncDecl : AST
@ -62,7 +62,7 @@ namespace Microsoft.Z3
/// <summary>
/// A hash code.
/// </summary>
/// </summary>
public override int GetHashCode()
{
return base.GetHashCode();
@ -205,7 +205,7 @@ namespace Microsoft.Z3
}
/// <summary>
/// Function declarations can have Parameters associated with them.
/// Function declarations can have Parameters associated with them.
/// </summary>
public class Parameter
{
@ -315,6 +315,17 @@ namespace Microsoft.Z3
#endif
#endregion
/// <summary>
/// Translates (copies) the function declaration to the Context <paramref name="ctx"/>.
/// </summary>
/// <param name="ctx">A context</param>
/// <returns>A copy of the function declaration which is associated with <paramref name="ctx"/></returns>
new public FuncDecl Translate(Context ctx)
{
return (FuncDecl) base.Translate(ctx);
}
/// <summary>
/// Create expression that applies function to arguments.
/// </summary>
@ -342,6 +353,5 @@ namespace Microsoft.Z3
Context.CheckContextMatch<Expr>(args);
return Expr.Create(Context, this, args);
}
}
}

12
src/api/dotnet/Quantifier.cs
View file

@ -14,7 +14,7 @@ Author:
Christoph Wintersteiger (cwinter) 2012-03-19
Notes:
--*/
using System;
@ -157,6 +157,16 @@ namespace Microsoft.Z3
}
}
/// <summary>
/// Translates (copies) the quantifier to the Context <paramref name="ctx"/>.
/// </summary>
/// <param name="ctx">A context</param>
/// <returns>A copy of the quantifier which is associated with <paramref name="ctx"/></returns>
new public Quantifier Translate(Context ctx)
{
return (Quantifier)base.Translate(ctx);
}
#region Internal
[ContractVerification(false)] // F: Clousot ForAll decompilation gets confused below. Setting verification off until I fixed the bug
internal Quantifier(Context ctx, bool isForall, Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)

20
src/api/dotnet/Sort.cs
View file

@ -14,7 +14,7 @@ Author:
Christoph Wintersteiger (cwinter) 2012-03-15
Notes:
--*/
using System;
@ -33,7 +33,7 @@ namespace Microsoft.Z3
/// </summary>
/// <param name="a">A Sort</param>
/// <param name="b">A Sort</param>
/// <returns>True if <paramref name="a"/> and <paramref name="b"/> are from the same context
/// <returns>True if <paramref name="a"/> and <paramref name="b"/> are from the same context
/// and represent the same sort; false otherwise.</returns>
public static bool operator ==(Sort a, Sort b)
{
@ -49,7 +49,7 @@ namespace Microsoft.Z3
/// </summary>
/// <param name="a">A Sort</param>
/// <param name="b">A Sort</param>
/// <returns>True if <paramref name="a"/> and <paramref name="b"/> are not from the same context
/// <returns>True if <paramref name="a"/> and <paramref name="b"/> are not from the same context
/// or represent different sorts; false otherwise.</returns>
public static bool operator !=(Sort a, Sort b)
{
@ -113,10 +113,20 @@ namespace Microsoft.Z3
return Native.Z3_sort_to_string(Context.nCtx, NativeObject);
}
/// <summary>
/// Translates (copies) the sort to the Context <paramref name="ctx"/>.
/// </summary>
/// <param name="ctx">A context</param>
/// <returns>A copy of the sort which is associated with <paramref name="ctx"/></returns>
new public Sort Translate(Context ctx)
{
return (Sort)base.Translate(ctx);
}
#region Internal
/// <summary>
/// Sort constructor
/// </summary>
/// </summary>
internal Sort(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
#if DEBUG
@ -154,5 +164,5 @@ namespace Microsoft.Z3
}
}
#endregion
}
}
}

18
src/api/dotnet/cmake_install_gac.cmake.in Normal file
View file

@ -0,0 +1,18 @@
# Install assembly to the GAC
set(GAC_ROOT "$ENV{DESTDIR}@CMAKE_INSTALL_FULL_LIBDIR@")
execute_process(COMMAND
"@DOTNET_GACUTIL_EXECUTABLE@"
"-i"
"@Z3_DOTNET_ASSEMBLY_DLL@"
"-f"
"-package" "@GAC_PKG_NAME@"
"-root" "${GAC_ROOT}"
WORKING_DIRECTORY "@CMAKE_CURRENT_BINARY_DIR@"
RESULT_VARIABLE gacutil_exit_code
)
if ("${gacutil_exit_code}" EQUAL 0)
message(STATUS "Installed \"@Z3_DOTNET_ASSEMBLY_DLL@\" to the GAC")
else()
message(FATAL_ERROR "Failed to install \"@Z3_DOTNET_ASSEMBLY_DLL@\" to the GAC")
endif()

20
src/api/dotnet/cmake_uninstall_gac.cmake.in Normal file
View file

@ -0,0 +1,20 @@
# Uninstall assembly from the GAC
set(GAC_ROOT "$ENV{DESTDIR}@CMAKE_INSTALL_FULL_LIBDIR@")
execute_process(COMMAND
"@DOTNET_GACUTIL_EXECUTABLE@"
# Note ``-us`` takes assembly file name rather than
# ``-u`` which takes an assembly display name
"-us"
"@Z3_DOTNET_ASSEMBLY_NAME@"
"-f"
"-package" "@GAC_PKG_NAME@"
"-root" "${GAC_ROOT}"
WORKING_DIRECTORY "@CMAKE_CURRENT_BINARY_DIR@"
RESULT_VARIABLE gacutil_exit_code
)
if ("${gacutil_exit_code}" EQUAL 0)
message(STATUS "Uninstalled \"@Z3_DOTNET_ASSEMBLY_NAME@\" from the GAC")
else()
message(FATAL_ERROR "Failed to uninstall \"@Z3_DOTNET_ASSEMBLY_NAME@\" from the GAC")
endif()

4
src/api/java/AST.java
View file

@ -87,12 +87,10 @@ public class AST extends Z3Object implements Comparable<AST>
**/
public AST translate(Context ctx)
{
if (getContext() == ctx) {
return this;
} else {
return new AST(ctx, Native.translate(getContext().nCtx(),
getNativeObject(), ctx.nCtx()));
return create(ctx, Native.translate(getContext().nCtx(), getNativeObject(), ctx.nCtx()));
}
}

236
src/api/java/CMakeLists.txt Normal file
View file

@ -0,0 +1,236 @@
find_package(Java REQUIRED)
find_package(JNI REQUIRED)
include(UseJava)
# Sanity check for dirty source tree
foreach (file_name "enumerations" "Native.cpp" "Native.java")
if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/${file_name}")
message(FATAL_ERROR "\"${CMAKE_CURRENT_SOURCE_DIR}/${file_name}\""
${z3_polluted_tree_msg})
endif()
endforeach()
set(Z3_JAVA_PACKAGE_NAME "com.microsoft.z3")
# Rule to generate ``Native.java`` and ``Native.cpp``
set(Z3_JAVA_NATIVE_JAVA "${CMAKE_CURRENT_BINARY_DIR}/Native.java")
set(Z3_JAVA_NATIVE_CPP "${CMAKE_CURRENT_BINARY_DIR}/Native.cpp")
add_custom_command(OUTPUT "${Z3_JAVA_NATIVE_JAVA}" "${Z3_JAVA_NATIVE_CPP}"
COMMAND "${PYTHON_EXECUTABLE}"
"${CMAKE_SOURCE_DIR}/scripts/update_api.py"
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
"--java-output-dir"
"${CMAKE_CURRENT_BINARY_DIR}"
"--java-package-name"
${Z3_JAVA_PACKAGE_NAME}
DEPENDS
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
"${CMAKE_SOURCE_DIR}/scripts/update_api.py"
${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
# FIXME: When update_api.py no longer uses ``mk_util`` drop this dependency
"${CMAKE_SOURCE_DIR}/scripts/mk_util.py"
COMMENT "Generating \"${Z3_JAVA_NATIVE_JAVA}\" and \"${Z3_JAVA_NATIVE_CPP}\""
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
)
# Add rule to build native code that provides a bridge between
# ``Native.java`` and libz3's interfac3.
add_library(z3java SHARED ${Z3_JAVA_NATIVE_CPP})
target_link_libraries(z3java PRIVATE libz3)
# FIXME:
# Not sure if using all the flags used by the Z3 components is really necessary
# here. At the bare minimum setting _AMD64_ depending on the target is
# necessary but seeing as the Python build system uses all the flags used for building
# Z3's components to build ``Native.cpp`` lets do the same for now.
target_compile_options(z3java PRIVATE ${Z3_COMPONENT_CXX_FLAGS})
target_compile_definitions(z3java PRIVATE ${Z3_COMPONENT_CXX_DEFINES})
target_include_directories(z3java PRIVATE
"${CMAKE_SOURCE_DIR}/src/api"
"${CMAKE_BINARY_DIR}/src/api"
${JNI_INCLUDE_DIRS}
)
# FIXME: Should this library have SONAME and VERSION set?
# This prevents CMake from automatically defining ``z3java_EXPORTS``
set_property(TARGET z3java PROPERTY DEFINE_SYMBOL "")
# Rule to generate the ``com.microsoft.z3.enumerations`` package
# FIXME: This list of files is fragile
set(Z3_JAVA_ENUMERATION_PACKAGE_FILES
Z3_ast_kind.java
Z3_ast_print_mode.java
Z3_decl_kind.java
Z3_error_code.java
Z3_goal_prec.java
Z3_lbool.java
Z3_param_kind.java
Z3_parameter_kind.java
Z3_sort_kind.java
Z3_symbol_kind.java
)
set(Z3_JAVA_ENUMERATION_PACKAGE_FILES_FULL_PATH "")
foreach (enum_file ${Z3_JAVA_ENUMERATION_PACKAGE_FILES})
list(APPEND Z3_JAVA_ENUMERATION_PACKAGE_FILES_FULL_PATH
"${CMAKE_CURRENT_BINARY_DIR}/enumerations/${enum_file}"
)
endforeach()
add_custom_command(OUTPUT ${Z3_JAVA_ENUMERATION_PACKAGE_FILES_FULL_PATH}
COMMAND "${PYTHON_EXECUTABLE}"
"${CMAKE_SOURCE_DIR}/scripts/mk_consts_files.py"
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
"--java-output-dir"
"${CMAKE_CURRENT_BINARY_DIR}"
"--java-package-name"
${Z3_JAVA_PACKAGE_NAME}
DEPENDS
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
"${CMAKE_SOURCE_DIR}/scripts/mk_consts_files.py"
${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
COMMENT "Generating ${Z3_JAVA_PACKAGE_NAME}.enumerations package"
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
)
set(Z3_JAVA_JAR_SOURCE_FILES
AlgebraicNum.java
ApplyResultDecRefQueue.java
ApplyResult.java
ArithExpr.java
ArithSort.java
ArrayExpr.java
ArraySort.java
ASTDecRefQueue.java
AST.java
AstMapDecRefQueue.java
ASTMap.java
AstVectorDecRefQueue.java
ASTVector.java
BitVecExpr.java
BitVecNum.java
BitVecSort.java
BoolExpr.java
BoolSort.java
ConstructorDecRefQueue.java
Constructor.java
ConstructorListDecRefQueue.java
ConstructorList.java
Context.java
DatatypeExpr.java
DatatypeSort.java
EnumSort.java
Expr.java
FiniteDomainExpr.java
FiniteDomainNum.java
FiniteDomainSort.java
FixedpointDecRefQueue.java
Fixedpoint.java
FPExpr.java
FPNum.java
FPRMExpr.java
FPRMNum.java
FPRMSort.java
FPSort.java
FuncDecl.java
FuncInterpDecRefQueue.java
FuncInterpEntryDecRefQueue.java
FuncInterp.java
Global.java
GoalDecRefQueue.java
Goal.java
IDecRefQueue.java
InterpolationContext.java
IntExpr.java
IntNum.java
IntSort.java
IntSymbol.java
ListSort.java
Log.java
ModelDecRefQueue.java
Model.java
OptimizeDecRefQueue.java
Optimize.java
ParamDescrsDecRefQueue.java
ParamDescrs.java
ParamsDecRefQueue.java
Params.java
Pattern.java
ProbeDecRefQueue.java
Probe.java
Quantifier.java
RatNum.java
RealExpr.java
RealSort.java
ReExpr.java
RelationSort.java
ReSort.java
SeqExpr.java
SeqSort.java
SetSort.java
SolverDecRefQueue.java
Solver.java
Sort.java
StatisticsDecRefQueue.java
Statistics.java
Status.java
StringSymbol.java
Symbol.java
TacticDecRefQueue.java
Tactic.java
TupleSort.java
UninterpretedSort.java
Version.java
Z3Exception.java
Z3Object.java
)
set(Z3_JAVA_JAR_SOURCE_FILES_FULL_PATH "")
foreach (java_src_file ${Z3_JAVA_JAR_SOURCE_FILES})
list(APPEND Z3_JAVA_JAR_SOURCE_FILES_FULL_PATH "${CMAKE_CURRENT_SOURCE_DIR}/${java_src_file}")
endforeach()
# Add generated files to list
list(APPEND Z3_JAVA_JAR_SOURCE_FILES_FULL_PATH
${Z3_JAVA_NATIVE_JAVA}
${Z3_JAVA_ENUMERATION_PACKAGE_FILES_FULL_PATH}
)
# Convenient top-level target
add_custom_target(build_z3_java_bindings
ALL
DEPENDS
z3java
z3JavaJar
)
# Rule to build ``com.microsoft.z3.jar``
# TODO: Should we set ``CMAKE_JNI_TARGET`` to ``TRUE``?
add_jar(z3JavaJar
SOURCES ${Z3_JAVA_JAR_SOURCE_FILES_FULL_PATH}
OUTPUT_NAME ${Z3_JAVA_PACKAGE_NAME}
OUTPUT_DIR "${CMAKE_BINARY_DIR}"
VERSION "${Z3_VERSION}"
)
###############################################################################
# Install
###############################################################################
option(INSTALL_JAVA_BINDINGS "Install Java bindings when invoking install target" ON)
if (INSTALL_JAVA_BINDINGS)
# Provide cache variables for the install locations that the user can change.
# This defaults to ``/usr/local/java`` which seems to be the location for ``.jar``
# files on Linux distributions
set(Z3_JAVA_JAR_INSTALLDIR
"${CMAKE_INSTALL_DATAROOTDIR}/java"
CACHE
PATH
"Directory to install Z3 Java jar file relative to install prefix"
)
# FIXME: I don't think this the right installation location
set(Z3_JAVA_JNI_LIB_INSTALLDIR
"${CMAKE_INSTALL_LIBDIR}"
CACHE
PATH
"Directory to install Z3 Java JNI bridge library relative to install prefix"
)
install(TARGETS z3java DESTINATION "${Z3_JAVA_JNI_LIB_INSTALLDIR}")
# Note: Don't use ``DESTINATION`` here as the version of ``UseJava.cmake`` shipped
# with CMake 2.8.12.2 handles that incorrectly.
install_jar(z3JavaJar "${Z3_JAVA_JAR_INSTALLDIR}")
endif()

6
src/api/java/Context.java
View file

@ -25,6 +25,12 @@ import java.util.Map;
/**
* The main interaction with Z3 happens via the Context.
* For applications that spawn an unbounded number of contexts,
* the proper use is within a try-with-resources
* scope so that the Context object gets garbage collected in
* a predictable way. Contexts maintain all data-structures
* related to terms and formulas that are created relative
* to them.
**/
public class Context implements AutoCloseable {
private final long m_ctx;

18
src/api/java/Expr.java
View file

@ -194,14 +194,7 @@ public class Expr extends AST
**/
public Expr translate(Context ctx)
{
if (getContext() == ctx) {
return this;
} else {
return Expr.create(
ctx,
Native.translate(getContext().nCtx(), getNativeObject(),
ctx.nCtx()));
}
return (Expr) super.translate(ctx);
}
/**
@ -1297,6 +1290,15 @@ public class Expr extends AST
return Native.getString(getContext().nCtx(), getNativeObject());
}
/**
* Check whether expression is a concatenation
* @return a boolean
*/
public boolean isConcat()
{
return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SEQ_CONCAT;
}
/**
* Indicates whether the term is a binary equivalence modulo namings.
* Remarks: This binary predicate is used in proof terms. It captures

2
src/api/java/Fixedpoint.java
View file

@ -88,6 +88,7 @@ public class Fixedpoint extends Z3Object
/**
* Add rule into the fixedpoint solver.
*
* @param rule implication (Horn clause) representing rule
* @param name Nullable rule name.
* @throws Z3Exception
**/
@ -178,6 +179,7 @@ public class Fixedpoint extends Z3Object
/**
* Update named rule into in the fixedpoint solver.
*
* @param rule implication (Horn clause) representing rule
* @param name Nullable rule name.
* @throws Z3Exception
**/

26
src/api/java/FuncDecl.java
View file

@ -1,6 +1,6 @@
/**
Copyright (c) 2012-2014 Microsoft Corporation
Module Name:
FuncDecl.java
@ -12,8 +12,8 @@ Author:
@author Christoph Wintersteiger (cwinter) 2012-03-15
Notes:
**/
**/
package com.microsoft.z3;
@ -59,6 +59,18 @@ public class FuncDecl extends AST
return Native.getFuncDeclId(getContext().nCtx(), getNativeObject());
}
/**
* Translates (copies) the function declaration to the Context {@code ctx}.
* @param ctx A context
*
* @return A copy of the function declaration which is associated with {@code ctx}
* @throws Z3Exception on error
**/
public FuncDecl translate(Context ctx)
{
return (FuncDecl) super.translate(ctx);
}
/**
* The arity of the function declaration
**/
@ -68,7 +80,7 @@ public class FuncDecl extends AST
}
/**
* The size of the domain of the function declaration
* The size of the domain of the function declaration
* @see #getArity
**/
public int getDomainSize()
@ -324,7 +336,7 @@ public class FuncDecl extends AST
}
FuncDecl(Context ctx, Symbol name, Sort[] domain, Sort range)
{
super(ctx, Native.mkFuncDecl(ctx.nCtx(), name.getNativeObject(),
AST.arrayLength(domain), AST.arrayToNative(domain),
@ -333,7 +345,7 @@ public class FuncDecl extends AST
}
FuncDecl(Context ctx, String prefix, Sort[] domain, Sort range)
{
super(ctx, Native.mkFreshFuncDecl(ctx.nCtx(), prefix,
AST.arrayLength(domain), AST.arrayToNative(domain),
@ -351,7 +363,7 @@ public class FuncDecl extends AST
}
/**
* Create expression that applies function to arguments.
* Create expression that applies function to arguments.
**/
public Expr apply(Expr ... args)
{

13
src/api/java/Quantifier.java
View file

@ -145,6 +145,19 @@ public class Quantifier extends BoolExpr
.nCtx(), getNativeObject()));
}
/**
* Translates (copies) the quantifier to the Context {@code ctx}.
*
* @param ctx A context
*
* @return A copy of the quantifier which is associated with {@code ctx}
* @throws Z3Exception on error
**/
public Quantifier translate(Context ctx)
{
return (Quantifier) super.translate(ctx);
}
/**
* Create a quantified expression.
*

13
src/api/java/Sort.java
View file

@ -87,6 +87,19 @@ public class Sort extends AST
return Native.sortToString(getContext().nCtx(), getNativeObject());
}
/**
* Translates (copies) the sort to the Context {@code ctx}.
*
* @param ctx A context
*
* @return A copy of the sort which is associated with {@code ctx}
* @throws Z3Exception on error
**/
public Sort translate(Context ctx)
{
return (Sort) super.translate(ctx);
}
/**
* Sort constructor
**/

143
src/api/python/CMakeLists.txt Normal file
View file

@ -0,0 +1,143 @@
message(STATUS "Emitting rules to build Z3 python bindings")
###############################################################################
# Add target to build python bindings for the build directory
###############################################################################
# This allows the python bindings to be used directly from the build directory
set(z3py_files
z3/__init__.py
z3/z3.py
z3/z3num.py
z3/z3poly.py
z3/z3printer.py
z3/z3rcf.py
z3test.py
z3/z3types.py
z3/z3util.py
)
set(z3py_bindings_build_dest "${CMAKE_BINARY_DIR}/python")
file(MAKE_DIRECTORY "${z3py_bindings_build_dest}")
file(MAKE_DIRECTORY "${z3py_bindings_build_dest}/z3")
set(build_z3_python_bindings_target_depends "")
foreach (z3py_file ${z3py_files})
add_custom_command(OUTPUT "${z3py_bindings_build_dest}/${z3py_file}"
COMMAND "${CMAKE_COMMAND}" "-E" "copy"
"${CMAKE_CURRENT_SOURCE_DIR}/${z3py_file}"
"${z3py_bindings_build_dest}/${z3py_file}"
DEPENDS "${CMAKE_CURRENT_SOURCE_DIR}/${z3py_file}"
COMMENT "Copying \"${z3py_file}\" to ${z3py_bindings_build_dest}/${z3py_file}"
)
list(APPEND build_z3_python_bindings_target_depends "${z3py_bindings_build_dest}/${z3py_file}")
endforeach()
# Generate z3core.py
add_custom_command(OUTPUT "${z3py_bindings_build_dest}/z3/z3core.py"
COMMAND "${PYTHON_EXECUTABLE}"
"${CMAKE_SOURCE_DIR}/scripts/update_api.py"
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
"--z3py-output-dir"
"${z3py_bindings_build_dest}"
DEPENDS
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
"${CMAKE_SOURCE_DIR}/scripts/update_api.py"
${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
# FIXME: When update_api.py no longer uses ``mk_util`` drop this dependency
"${CMAKE_SOURCE_DIR}/scripts/mk_util.py"
COMMENT "Generating z3core.py"
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
)
list(APPEND build_z3_python_bindings_target_depends "${z3py_bindings_build_dest}/z3/z3core.py")
# Generate z3consts.py
add_custom_command(OUTPUT "${z3py_bindings_build_dest}/z3/z3consts.py"
COMMAND "${PYTHON_EXECUTABLE}"
"${CMAKE_SOURCE_DIR}/scripts/mk_consts_files.py"
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
"--z3py-output-dir"
"${z3py_bindings_build_dest}"
DEPENDS
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
"${CMAKE_SOURCE_DIR}/scripts/mk_consts_files.py"
${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
COMMENT "Generating z3consts.py"
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
)
list(APPEND build_z3_python_bindings_target_depends "${z3py_bindings_build_dest}/z3/z3consts.py")
if (UNIX)
set(LINK_COMMAND "create_symlink")
else()
set(LINK_COMMAND "copy")
endif()
# Link libz3 into the python directory so bindings work out of the box
add_custom_command(OUTPUT "${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_MODULE_SUFFIX}"
COMMAND "${CMAKE_COMMAND}" "-E" "${LINK_COMMAND}"
"${CMAKE_BINARY_DIR}/libz3${CMAKE_SHARED_MODULE_SUFFIX}"
"${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_MODULE_SUFFIX}"
DEPENDS libz3
COMMENT "Linking libz3 into python directory"
)
# Convenient top-level target
add_custom_target(build_z3_python_bindings
ALL
DEPENDS
${build_z3_python_bindings_target_depends}
"${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_MODULE_SUFFIX}"
)
###############################################################################
# Install
###############################################################################
option(INSTALL_PYTHON_BINDINGS "Install Python bindings when invoking install target" ON)
if (INSTALL_PYTHON_BINDINGS)
message(STATUS "Emitting rules to install Z3 python bindings")
# Try to guess the installation path for the bindings
if (NOT DEFINED CMAKE_INSTALL_PYTHON_PKG_DIR)
message(STATUS "CMAKE_INSTALL_PYTHON_PKG_DIR not set. Trying to guess")
execute_process(
COMMAND "${PYTHON_EXECUTABLE}" "-c"
"import distutils.sysconfig; print(distutils.sysconfig.get_python_lib())"
RESULT_VARIABLE exit_code
OUTPUT_VARIABLE CMAKE_INSTALL_PYTHON_PKG_DIR
OUTPUT_STRIP_TRAILING_WHITESPACE
)
if (NOT ("${exit_code}" EQUAL 0))
message(FATAL_ERROR "Failed to determine your Python package directory")
endif()
message(STATUS "Detected Python package directory: \"${CMAKE_INSTALL_PYTHON_PKG_DIR}\"")
# Set a cache variable that the user can modify if needed
set(CMAKE_INSTALL_PYTHON_PKG_DIR
"${CMAKE_INSTALL_PYTHON_PKG_DIR}"
CACHE PATH
"Path to install python bindings. This can be relative or absolute.")
mark_as_advanced(CMAKE_INSTALL_PYTHON_PKG_DIR)
else()
message(STATUS "CMAKE_INSTALL_PYTHON_PKG_DIR already set (\"${CMAKE_INSTALL_PYTHON_PKG_DIR}\")"
". Not trying to guess.")
endif()
# Check if path exists under the install prefix if it is absolute. If the
# path is relative it will be installed under the install prefix so there
# if nothing to check
if (IS_ABSOLUTE "${CMAKE_INSTALL_PYTHON_PKG_DIR}")
string(FIND "${CMAKE_INSTALL_PYTHON_PKG_DIR}" "${CMAKE_INSTALL_PREFIX}" position)
if (NOT ("${position}" EQUAL 0))
message(WARNING "The directory to install the python bindings \"${CMAKE_INSTALL_PYTHON_PKG_DIR}\" "
"is not under the install prefix \"${CMAKE_INSTALL_PREFIX}\"."
" Running the install target may lead to a broken installation. "
"To change the install directory modify the CMAKE_INSTALL_PYTHON_PKG_DIR cache variable."
)
endif()
endif()
# Using DESTDIR still seems to work even if we use an absolute path
message(STATUS "Python bindings will be installed to \"${CMAKE_INSTALL_PYTHON_PKG_DIR}\"")
install(FILES ${build_z3_python_bindings_target_depends}
DESTINATION "${CMAKE_INSTALL_PYTHON_PKG_DIR}/z3"
)
else()
message(STATUS "Not emitting rules to install Z3 python bindings")
endif()

86
src/api/python/z3/z3.py
View file

@ -12,7 +12,7 @@
Several online tutorials for Z3Py are available at:
http://rise4fun.com/Z3Py/tutorial/guide
Please send feedback, comments and/or corrections to leonardo@microsoft.com. Your comments are very valuable.
Please send feedback, comments and/or corrections on the Issue tracker for https://github.com/Z3prover/z3.git. Your comments are very valuable.
Small example:
@ -50,6 +50,7 @@ from fractions import Fraction
import sys
import io
import math
import copy
if sys.version < '3':
def _is_int(v):
@ -288,6 +289,9 @@ class AstRef(Z3PPObject):
if self.ctx.ref() is not None:
Z3_dec_ref(self.ctx.ref(), self.as_ast())
def __deepcopy__(self, memo={}):
return _to_ast_ref(self.ast, self.ctx)
def __str__(self):
return obj_to_string(self)
@ -314,7 +318,7 @@ class AstRef(Z3PPObject):
raise Z3Exception("Symbolic expressions cannot be cast to concrete Boolean values.")
def sexpr(self):
"""Return an string representing the AST node in s-expression notation.
"""Return a string representing the AST node in s-expression notation.
>>> x = Int('x')
>>> ((x + 1)*x).sexpr()
@ -4357,6 +4361,11 @@ class Datatype:
self.name = name
self.constructors = []
def __deepcopy__(self, memo={}):
r = Datatype(self.name, self.ctx)
r.constructors = copy.deepcopy(self.constructors)
return r
def declare_core(self, name, rec_name, *args):
if __debug__:
_z3_assert(isinstance(name, str), "String expected")
@ -4647,11 +4656,17 @@ class ParamsRef:
Consider using the function `args2params` to create instances of this object.
"""
def __init__(self, ctx=None):
def __init__(self, ctx=None, params=None):
self.ctx = _get_ctx(ctx)
self.params = Z3_mk_params(self.ctx.ref())
if params is None:
self.params = Z3_mk_params(self.ctx.ref())
else:
self.params = params
Z3_params_inc_ref(self.ctx.ref(), self.params)
def __deepcopy__(self, memo={}):
return ParamsRef(self.ctx, self.params)
def __del__(self):
if self.ctx.ref() is not None:
Z3_params_dec_ref(self.ctx.ref(), self.params)
@ -4711,6 +4726,9 @@ class ParamDescrsRef:
self.descr = descr
Z3_param_descrs_inc_ref(self.ctx.ref(), self.descr)
def __deepcopy__(self, memo={}):
return ParamsDescrsRef(self.descr, self.ctx)
def __del__(self):
if self.ctx.ref() is not None:
Z3_param_descrs_dec_ref(self.ctx.ref(), self.descr)
@ -4772,6 +4790,9 @@ class Goal(Z3PPObject):
self.goal = Z3_mk_goal(self.ctx.ref(), models, unsat_cores, proofs)
Z3_goal_inc_ref(self.ctx.ref(), self.goal)
def __deepcopy__(self, memo={}):
return Goal(False, False, False, self.ctx, self.goal)
def __del__(self):
if self.goal is not None and self.ctx.ref() is not None:
Z3_goal_dec_ref(self.ctx.ref(), self.goal)
@ -5034,6 +5055,9 @@ class AstVector(Z3PPObject):
self.ctx = ctx
Z3_ast_vector_inc_ref(self.ctx.ref(), self.vector)
def __deepcopy__(self, memo={}):
return AstVector(self.vector, self.ctx)
def __del__(self):
if self.vector is not None and self.ctx.ref() is not None:
Z3_ast_vector_dec_ref(self.ctx.ref(), self.vector)
@ -5169,6 +5193,9 @@ class AstMap:
self.ctx = ctx
Z3_ast_map_inc_ref(self.ctx.ref(), self.map)
def __deepcopy__(self, memo={}):
return AstMap(self.map, self.ctx)
def __del__(self):
if self.map is not None and self.ctx.ref() is not None:
Z3_ast_map_dec_ref(self.ctx.ref(), self.map)
@ -5284,6 +5311,9 @@ class FuncEntry:
self.ctx = ctx
Z3_func_entry_inc_ref(self.ctx.ref(), self.entry)
def __deepcopy__(self, memo={}):
return FuncEntry(self.entry, self.ctx)
def __del__(self):
if self.ctx.ref() is not None:
Z3_func_entry_dec_ref(self.ctx.ref(), self.entry)
@ -5390,6 +5420,9 @@ class FuncInterp(Z3PPObject):
if self.f is not None:
Z3_func_interp_inc_ref(self.ctx.ref(), self.f)
def __deepcopy__(self, memo={}):
return FuncInterp(self.f, self.ctx)
def __del__(self):
if self.f is not None and self.ctx.ref() is not None:
Z3_func_interp_dec_ref(self.ctx.ref(), self.f)
@ -5500,6 +5533,9 @@ class ModelRef(Z3PPObject):
self.ctx = ctx
Z3_model_inc_ref(self.ctx.ref(), self.model)
def __deepcopy__(self, memo={}):
return ModelRef(self.m, self.ctx)
def __del__(self):
if self.ctx.ref() is not None:
Z3_model_dec_ref(self.ctx.ref(), self.model)
@ -5776,6 +5812,9 @@ class Statistics:
self.ctx = ctx
Z3_stats_inc_ref(self.ctx.ref(), self.stats)
def __deepcopy__(self, memo={}):
return Statistics(self.stats, self.ctx)
def __del__(self):
if self.ctx.ref() is not None:
Z3_stats_dec_ref(self.ctx.ref(), self.stats)
@ -5910,6 +5949,9 @@ class CheckSatResult:
def __init__(self, r):
self.r = r
def __deepcopy__(self, memo={}):
return CheckSatResult(self.r)
def __eq__(self, other):
return isinstance(other, CheckSatResult) and self.r == other.r
@ -5949,6 +5991,9 @@ class Solver(Z3PPObject):
self.solver = solver
Z3_solver_inc_ref(self.ctx.ref(), self.solver)
def __deepcopy__(self, memo={}):
return Solver(self.solver, self.ctx)
def __del__(self):
if self.solver is not None and self.ctx.ref() is not None:
Z3_solver_dec_ref(self.ctx.ref(), self.solver)
@ -6009,6 +6054,24 @@ class Solver(Z3PPObject):
"""
Z3_solver_pop(self.ctx.ref(), self.solver, num)
def num_scopes(self):
"""Return the current number of backtracking points.
>>> s = Solver()
>>> s.num_scopes()
0L
>>> s.push()
>>> s.num_scopes()
1L
>>> s.push()
>>> s.num_scopes()
2L
>>> s.pop()
>>> s.num_scopes()
1L
"""
return Z3_solver_get_num_scopes(self.ctx.ref(), self.solver)
def reset(self):
"""Remove all asserted constraints and backtracking points created using `push()`.
@ -6384,6 +6447,9 @@ class Fixedpoint(Z3PPObject):
Z3_fixedpoint_inc_ref(self.ctx.ref(), self.fixedpoint)
self.vars = []
def __deepcopy__(self, memo={}):
return FixedPoint(self.fixedpoint, self.ctx)
def __del__(self):
if self.fixedpoint is not None and self.ctx.ref() is not None:
Z3_fixedpoint_dec_ref(self.ctx.ref(), self.fixedpoint)
@ -6758,6 +6824,9 @@ class Optimize(Z3PPObject):
self.optimize = Z3_mk_optimize(self.ctx.ref())
Z3_optimize_inc_ref(self.ctx.ref(), self.optimize)
def __deepcopy__(self, memo={}):
return Optimize(self.optimize, self.ctx)
def __del__(self):
if self.optimize is not None and self.ctx.ref() is not None:
Z3_optimize_dec_ref(self.ctx.ref(), self.optimize)
@ -6910,6 +6979,9 @@ class ApplyResult(Z3PPObject):
self.ctx = ctx
Z3_apply_result_inc_ref(self.ctx.ref(), self.result)
def __deepcopy__(self, memo={}):
return ApplyResult(self.result, self.ctx)
def __del__(self):
if self.ctx.ref() is not None:
Z3_apply_result_dec_ref(self.ctx.ref(), self.result)
@ -7038,6 +7110,9 @@ class Tactic:
raise Z3Exception("unknown tactic '%s'" % tactic)
Z3_tactic_inc_ref(self.ctx.ref(), self.tactic)
def __deepcopy__(self, memo={}):
return Tactic(self.tactic, self.ctx)
def __del__(self):
if self.tactic is not None and self.ctx.ref() is not None:
Z3_tactic_dec_ref(self.ctx.ref(), self.tactic)
@ -7310,6 +7385,9 @@ class Probe:
raise Z3Exception("unknown probe '%s'" % probe)
Z3_probe_inc_ref(self.ctx.ref(), self.probe)
def __deepcopy__(self, memo={}):
return Probe(self.probe, self.ctx)
def __del__(self):
if self.probe is not None and self.ctx.ref() is not None:
Z3_probe_dec_ref(self.ctx.ref(), self.probe)

80
src/api/z3_api.h
View file

@ -48,6 +48,7 @@ DEFINE_TYPE(Z3_rcf_num);
/*@{*/
/** @name Types
@{
Most of the types in the C API are opaque pointers.
@ -395,6 +396,33 @@ typedef enum
The meaning is given by the equivalence
(xor3 l1 l2 l3) <=> (xor (xor l1 l2) l3)
- Z3_OP_BSMUL_NO_OVFL: a predicate to check that bit-wise signed multiplication does not overflow.
Signed multiplication overflows if the operands have the same sign and the result of multiplication
does not fit within the available bits. \sa Z3_mk_bvmul_no_overflow.
- Z3_OP_BUMUL_NO_OVFL: check that bit-wise unsigned multiplication does not overflow.
Unsigned multiplication overflows if the result does not fit within the available bits.
\sa Z3_mk_bvmul_no_overflow.
- Z3_OP_BSMUL_NO_UDFL: check that bit-wise signed multiplication does not underflow.
Signed multiplication underflows if the operands have opposite signs and the result of multiplication
does not fit within the avaialble bits. Z3_mk_bvmul_no_underflow.
- Z3_OP_BSDIV_I: Binary signed division.
It has the same semantics as Z3_OP_BSDIV, but created in a context where the second operand can be assumed to be non-zero.
- Z3_OP_BUDIV_I: Binary unsigned division.
It has the same semantics as Z3_OP_BUDIV, but created in a context where the second operand can be assumed to be non-zero.
- Z3_OP_BSREM_I: Binary signed remainder.
It has the same semantics as Z3_OP_BSREM, but created in a context where the second operand can be assumed to be non-zero.
- Z3_OP_BUREM_I: Binary unsigned remainder.
It has the same semantics as Z3_OP_BUREM, but created in a context where the second operand can be assumed to be non-zero.
- Z3_OP_BSMOD_I: Binary signed modulus.
It has the same semantics as Z3_OP_BSMOD, but created in a context where the second operand can be assumed to be non-zero.
- Z3_OP_PR_UNDEF: Undef/Null proof object.
- Z3_OP_PR_TRUE: Proof for the expression 'true'.
@ -5238,7 +5266,6 @@ extern "C" {
def_API('Z3_get_error_msg', STRING, (_in(CONTEXT), _in(ERROR_CODE)))
*/
Z3_string Z3_API Z3_get_error_msg(Z3_context c, Z3_error_code err);
/*@}*/
/**
\brief Return a string describing the given error code.
@ -5349,6 +5376,13 @@ extern "C" {
/**
\brief Add a new formula \c a to the given goal.
The formula is split according to the following procedure that is applied
until a fixed-point:
Conjunctions are split into separate formulas.
Negations are distributed over disjunctions, resulting in separate formulas.
If the goal is \c false, adding new formulas is a no-op.
If the formula \c a is \c true, then nothing is added.
If the formula \c a is \c false, then the entire goal is replaced by the formula \c false.
def_API('Z3_goal_assert', VOID, (_in(CONTEXT), _in(GOAL), _in(AST)))
*/
@ -5791,9 +5825,35 @@ extern "C" {
/** @name Solvers*/
/*@{*/
/**
\brief Create a new (incremental) solver. This solver also uses a
set of builtin tactics for handling the first check-sat command, and
check-sat commands that take more than a given number of milliseconds to be solved.
\brief Create a new solver. This solver is a "combined solver" (see
combined_solver module) that internally uses a non-incremental (solver1) and an
incremental solver (solver2). This combined solver changes its behaviour based
on how it is used and how its parameters are set.
If the solver is used in a non incremental way (i.e. no calls to
`Z3_solver_push()` or `Z3_solver_pop()`, and no calls to
`Z3_solver_assert()` or `Z3_solver_assert_and_track()` after checking
satisfiability without an intervening `Z3_solver_reset()`) then solver1
will be used. This solver will apply Z3's "default" tactic.
The "default" tactic will attempt to probe the logic used by the
assertions and will apply a specialized tactic if one is supported.
Otherwise the general `(and-then simplify smt)` tactic will be used.
If the solver is used in an incremental way then the combined solver
will switch to using solver2 (which behaves similarly to the general
"smt" tactic).
Note however it is possible to set the `solver2_timeout`,
`solver2_unknown`, and `ignore_solver1` parameters of the combined
solver to change its behaviour.
The function #Z3_solver_get_model retrieves a model if the
assertions is satisfiable (i.e., the result is \c
Z3_L_TRUE) and model construction is enabled.
The function #Z3_solver_get_model can also be used even
if the result is \c Z3_L_UNDEF, but the returned model
is not guaranteed to satisfy quantified assertions.
\remark User must use #Z3_solver_inc_ref and #Z3_solver_dec_ref to manage solver objects.
Even if the context was created using #Z3_mk_context instead of #Z3_mk_context_rc.
@ -5803,7 +5863,17 @@ extern "C" {
Z3_solver Z3_API Z3_mk_solver(Z3_context c);
/**
\brief Create a new (incremental) solver.
\brief Create a new incremental solver.
This is equivalent to applying the "smt" tactic.
Unlike `Z3_mk_solver()` this solver
- Does not attempt to apply any logic specific tactics.
- Does not change its behaviour based on whether it used
incrementally/non-incrementally.
Note that these differences can result in very different performance
compared to `Z3_mk_solver()`.
The function #Z3_solver_get_model retrieves a model if the
assertions is satisfiable (i.e., the result is \c

4
src/api/z3_optimization.h
View file

@ -75,7 +75,7 @@ extern "C" {
\brief Add a maximization constraint.
\param c - context
\param o - optimization context
\param a - arithmetical term
\param t - arithmetical term
def_API('Z3_optimize_maximize', UINT, (_in(CONTEXT), _in(OPTIMIZE), _in(AST)))
*/
unsigned Z3_API Z3_optimize_maximize(Z3_context c, Z3_optimize o, Z3_ast t);
@ -84,7 +84,7 @@ extern "C" {
\brief Add a minimization constraint.
\param c - context
\param o - optimization context
\param a - arithmetical term
\param t - arithmetical term
def_API('Z3_optimize_minimize', UINT, (_in(CONTEXT), _in(OPTIMIZE), _in(AST)))
*/

48
src/ast/CMakeLists.txt Normal file
View file

@ -0,0 +1,48 @@
z3_add_component(ast
SOURCES
act_cache.cpp
arith_decl_plugin.cpp
array_decl_plugin.cpp
ast.cpp
ast_ll_pp.cpp
ast_lt.cpp
ast_pp_util.cpp
ast_printer.cpp
ast_smt2_pp.cpp
ast_smt_pp.cpp
ast_translation.cpp
ast_util.cpp
bv_decl_plugin.cpp
datatype_decl_plugin.cpp
decl_collector.cpp
dl_decl_plugin.cpp
expr2polynomial.cpp
expr2var.cpp
expr_abstract.cpp
expr_functors.cpp
expr_map.cpp
expr_stat.cpp
expr_substitution.cpp
for_each_ast.cpp
for_each_expr.cpp
format.cpp
fpa_decl_plugin.cpp
func_decl_dependencies.cpp
has_free_vars.cpp
macro_substitution.cpp
num_occurs.cpp
occurs.cpp
pb_decl_plugin.cpp
pp.cpp
reg_decl_plugins.cpp
seq_decl_plugin.cpp
shared_occs.cpp
static_features.cpp
used_vars.cpp
well_sorted.cpp
COMPONENT_DEPENDENCIES
polynomial
util # Unnecessary? polynomial already depends on util
PYG_FILES
pp_params.pyg
)

2
src/ast/arith_decl_plugin.h
View file

@ -275,7 +275,9 @@ public:
bool is_uminus(expr const * n) const { return is_app_of(n, m_afid, OP_UMINUS); }
bool is_mul(expr const * n) const { return is_app_of(n, m_afid, OP_MUL); }
bool is_div(expr const * n) const { return is_app_of(n, m_afid, OP_DIV); }
bool is_div0(expr const * n) const { return is_app_of(n, m_afid, OP_DIV_0); }
bool is_idiv(expr const * n) const { return is_app_of(n, m_afid, OP_IDIV); }
bool is_idiv0(expr const * n) const { return is_app_of(n, m_afid, OP_IDIV_0); }
bool is_mod(expr const * n) const { return is_app_of(n, m_afid, OP_MOD); }
bool is_rem(expr const * n) const { return is_app_of(n, m_afid, OP_REM); }
bool is_to_real(expr const * n) const { return is_app_of(n, m_afid, OP_TO_REAL); }

4
src/ast/ast.h
View file

@ -667,6 +667,8 @@ public:
expr * get_arg(unsigned idx) const { SASSERT(idx < m_num_args); return m_args[idx]; }
expr * const * get_args() const { return m_args; }
unsigned get_size() const { return get_obj_size(get_num_args()); }
expr * const * begin() const { return m_args; }
expr * const * end() const { return m_args + m_num_args; }
unsigned get_depth() const { return flags()->m_depth; }
bool is_ground() const { return flags()->m_ground; }
@ -2082,6 +2084,7 @@ public:
bool is_undef_proof(expr const * e) const { return e == m_undef_proof; }
bool is_asserted(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_ASSERTED); }
bool is_hypothesis (expr const *e) const {return is_app_of (e, m_basic_family_id, PR_HYPOTHESIS);}
bool is_goal(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_GOAL); }
bool is_modus_ponens(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_MODUS_PONENS); }
bool is_reflexivity(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_REFLEXIVITY); }
@ -2112,6 +2115,7 @@ public:
bool is_skolemize(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_SKOLEMIZE); }
MATCH_UNARY(is_asserted);
MATCH_UNARY(is_hypothesis);
MATCH_UNARY(is_lemma);
bool has_fact(proof const * p) const {

30
src/ast/ast_smt2_pp.cpp
View file

@ -429,8 +429,18 @@ format_ns::format * smt2_pp_environment::pp_sort(sort * s) {
if ((get_sutil().is_seq(s) || get_sutil().is_re(s)) && !get_sutil().is_string(s)) {
ptr_buffer<format> fs;
fs.push_back(pp_sort(to_sort(s->get_parameter(0).get_ast())));
return mk_seq1(m, fs.begin(), fs.end(), f2f(), get_sutil().is_seq(s)?"Seq":"Re");
return mk_seq1(m, fs.begin(), fs.end(), f2f(), get_sutil().is_seq(s)?"Seq":"RegEx");
}
#if 0
if (get_dtutil().is_datatype(s)) {
ptr_buffer<format> fs;
unsigned sz = get_dtutil().get_datatype_num_parameter_sorts(s);
for (unsigned i = 0; i < sz; i++) {
fs.push_back(pp_sort(get_dtutil().get_datatype_parameter_sort(s, i)));
}
return mk_seq1(m, fs.begin(), fs.end(), f2f(), s->get_name().str().c_str());
}
#endif
return format_ns::mk_string(get_manager(), s->get_name().str().c_str());
}
@ -557,7 +567,14 @@ class smt2_printer {
format * f;
if (v->get_idx() < m_var_names.size()) {
symbol s = m_var_names[m_var_names.size() - v->get_idx() - 1];
f = mk_string(m(), s.str().c_str());
std::string vname;
if (is_smt2_quoted_symbol (s)) {
vname = mk_smt2_quoted_symbol (s);
}
else {
vname = s.str();
}
f = mk_string(m(), vname.c_str ());
}
else {
// fallback... it is not supposed to happen when the printer is correctly used.
@ -884,7 +901,14 @@ class smt2_printer {
symbol * it = m_var_names.end() - num_decls;
for (unsigned i = 0; i < num_decls; i++, it++) {
format * fs[1] = { m_env.pp_sort(q->get_decl_sort(i)) };
buf.push_back(mk_seq1<format**,f2f>(m(), fs, fs+1, f2f(), it->str().c_str()));
std::string var_name;
if (is_smt2_quoted_symbol (*it)) {
var_name = mk_smt2_quoted_symbol (*it);
}
else {
var_name = it->str ();\
}
buf.push_back(mk_seq1<format**,f2f>(m(), fs, fs+1, f2f(), var_name.c_str ()));
}
return mk_seq5(m(), buf.begin(), buf.end(), f2f());
}

6
src/ast/ast_smt2_pp.h
View file

@ -30,6 +30,7 @@ Revision History:
#include"fpa_decl_plugin.h"
#include"dl_decl_plugin.h"
#include"seq_decl_plugin.h"
#include"datatype_decl_plugin.h"
#include"smt2_util.h"
class smt2_pp_environment {
@ -50,6 +51,7 @@ public:
virtual fpa_util & get_futil() = 0;
virtual seq_util & get_sutil() = 0;
virtual datalog::dl_decl_util& get_dlutil() = 0;
virtual datatype_util& get_dtutil() = 0;
virtual bool uses(symbol const & s) const = 0;
virtual format_ns::format * pp_fdecl(func_decl * f, unsigned & len);
virtual format_ns::format * pp_bv_literal(app * t, bool use_bv_lits, bool bv_neg);
@ -74,9 +76,10 @@ class smt2_pp_environment_dbg : public smt2_pp_environment {
array_util m_arutil;
fpa_util m_futil;
seq_util m_sutil;
datatype_util m_dtutil;
datalog::dl_decl_util m_dlutil;
public:
smt2_pp_environment_dbg(ast_manager & m):m_manager(m), m_autil(m), m_bvutil(m), m_arutil(m), m_futil(m), m_sutil(m), m_dlutil(m) {}
smt2_pp_environment_dbg(ast_manager & m):m_manager(m), m_autil(m), m_bvutil(m), m_arutil(m), m_futil(m), m_sutil(m), m_dtutil(m), m_dlutil(m) {}
virtual ast_manager & get_manager() const { return m_manager; }
virtual arith_util & get_autil() { return m_autil; }
virtual bv_util & get_bvutil() { return m_bvutil; }
@ -84,6 +87,7 @@ public:
virtual array_util & get_arutil() { return m_arutil; }
virtual fpa_util & get_futil() { return m_futil; }
virtual datalog::dl_decl_util& get_dlutil() { return m_dlutil; }
virtual datatype_util& get_dtutil() { return m_dtutil; }
virtual bool uses(symbol const & s) const { return false; }
};

17
src/ast/ast_smt_pp.cpp
View file

@ -366,7 +366,22 @@ class smt_printer {
return;
}
else if (s->is_sort_of(m_dt_fid, DATATYPE_SORT)) {
m_out << m_renaming.get_symbol(s->get_name());
m_out << m_renaming.get_symbol(s->get_name());
#if 0
datatype_util util(m_manager);
unsigned num_sorts = util.get_datatype_num_parameter_sorts(s);
if (num_sorts > 0) {
m_out << "(";
}
if (num_sorts > 0) {
for (unsigned i = 0; i < num_sorts; ++i) {
m_out << " ";
visit_sort(util.get_datatype_parameter_sort(s, i));
}
m_out << ")";
}
#endif
return;
}
else {

2
src/ast/bv_decl_plugin.cpp
View file

@ -732,7 +732,7 @@ void bv_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const
op_names.push_back(builtin_name("bvudiv_i", OP_BUDIV_I));
op_names.push_back(builtin_name("bvsrem_i", OP_BSREM_I));
op_names.push_back(builtin_name("bvurem_i", OP_BUREM_I));
op_names.push_back(builtin_name("bvumod_i", OP_BSMOD_I));
op_names.push_back(builtin_name("bvsmod_i", OP_BSMOD_I));
op_names.push_back(builtin_name("ext_rotate_left",OP_EXT_ROTATE_LEFT));
op_names.push_back(builtin_name("ext_rotate_right",OP_EXT_ROTATE_RIGHT));

85
src/ast/datatype_decl_plugin.cpp
View file

@ -20,6 +20,7 @@ Revision History:
#include"warning.h"
#include"ast_smt2_pp.h"
/**
\brief Auxiliary class used to declare inductive datatypes.
*/
@ -124,6 +125,7 @@ static parameter const & read(unsigned num_parameters, parameter const * paramet
static int read_int(unsigned num_parameters, parameter const * parameters, unsigned idx, bool_buffer & read_pos) {
const parameter & r = read(num_parameters, parameters, idx, read_pos);
if (!r.is_int()) {
TRACE("datatype", tout << "expected integer parameter at position " << idx << " got: " << r << "\n";);
throw invalid_datatype();
}
return r.get_int();
@ -132,11 +134,25 @@ static int read_int(unsigned num_parameters, parameter const * parameters, unsig
static symbol read_symbol(unsigned num_parameters, parameter const * parameters, unsigned idx, bool_buffer & read_pos) {
parameter const & r = read(num_parameters, parameters, idx, read_pos);
if (!r.is_symbol()) {
TRACE("datatype", tout << "expected symol parameter at position " << idx << " got: " << r << "\n";);
throw invalid_datatype();
}
return r.get_symbol();
}
static sort* read_sort(unsigned num_parameters, parameter const * parameters, unsigned idx, bool_buffer & read_pos) {
parameter const & r = read(num_parameters, parameters, idx, read_pos);
if (!r.is_ast()) {
TRACE("datatype", tout << "expected ast parameter at position " << idx << " got: " << r << "\n";);
throw invalid_datatype();
}
ast* a = r.get_ast();
if (!is_sort(a)) {
throw invalid_datatype();
}
return to_sort(a);
}
enum status {
WHITE,
GRAY,
@ -160,7 +176,7 @@ static bool is_recursive_datatype(parameter const * parameters) {
continue;
}
already_found[tid] = GRAY;
unsigned o = parameters[2 + 2*tid + 1].get_int(); // constructor offset
unsigned o = datatype_decl_plugin::constructor_offset(parameters, tid); // constructor offset
unsigned num_constructors = parameters[o].get_int();
bool can_process = true;
for (unsigned s = 1; s <= num_constructors; s++) {
@ -210,7 +226,7 @@ static sort_size get_datatype_size(parameter const * parameters) {
continue;
}
already_found[tid] = GRAY;
unsigned o = parameters[2 + 2*tid + 1].get_int(); // constructor offset
unsigned o = datatype_decl_plugin::constructor_offset(parameters, tid);
unsigned num_constructors = parameters[o].get_int();
bool is_very_big = false;
bool can_process = true;
@ -296,7 +312,7 @@ static bool is_well_founded(parameter const * parameters) {
changed = false;
for (unsigned tid = 0; tid < num_types; tid++) {
if (!well_founded[tid]) {
unsigned o = parameters[2 + 2*tid + 1].get_int(); // constructor offset
unsigned o = datatype_decl_plugin::constructor_offset(parameters, tid); // constructor offset
unsigned num_constructors = parameters[o].get_int();
for (unsigned s = 1; s <= num_constructors; s++) {
unsigned k_i = parameters[o + s].get_int();
@ -350,9 +366,14 @@ sort * datatype_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, param
throw invalid_datatype();
}
unsigned tid = read_int(num_parameters, parameters, 1, found);
unsigned num_sort_params = read_int(num_parameters, parameters, 2, found);
for (unsigned j = 0; j < num_sort_params; ++j) {
read_sort(num_parameters, parameters, 3 + j, found);
}
unsigned c_offset = constructor_offset(parameters);
for (unsigned j = 0; j < num_types; j++) {
read_symbol(num_parameters, parameters, 2 + 2*j, found); // type name
unsigned o = read_int(num_parameters, parameters, 2 + 2*j + 1, found);
read_symbol(num_parameters, parameters, c_offset + 2*j, found); // type name
unsigned o = read_int(num_parameters, parameters, c_offset + 2*j + 1, found);
unsigned num_constructors = read_int(num_parameters, parameters, o, found);
if (num_constructors == 0) {
throw invalid_datatype();
@ -368,9 +389,9 @@ sort * datatype_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, param
parameter const & a_type = read(num_parameters, parameters, first_accessor + 2*r + 1, found); // accessort type
if (!a_type.is_int() && !a_type.is_ast()) {
throw invalid_datatype();
if (a_type.is_ast() && !is_sort(a_type.get_ast())) {
throw invalid_datatype();
}
}
if (a_type.is_ast() && !is_sort(a_type.get_ast())) {
throw invalid_datatype();
}
}
}
@ -387,7 +408,7 @@ sort * datatype_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, param
// compute datatype size
sort_size ts = get_datatype_size(parameters);
symbol const & tname = parameters[2+2*tid].get_symbol();
symbol const & tname = parameters[c_offset + 2*tid].get_symbol();
return m_manager->mk_sort(tname,
sort_info(m_family_id, k, ts, num_parameters, parameters, true));
}
@ -489,7 +510,7 @@ func_decl * datatype_decl_plugin::mk_func_decl(decl_kind k, unsigned num_paramet
}
unsigned c_idx = parameters[1].get_int();
unsigned tid = datatype->get_parameter(1).get_int();
unsigned o = datatype->get_parameter(2 + 2 * tid + 1).get_int();
unsigned o = datatype_decl_plugin::constructor_offset(datatype, tid);
unsigned num_constructors = datatype->get_parameter(o).get_int();
if (c_idx >= num_constructors) {
m_manager->raise_exception("invalid parameters for datatype operator");
@ -504,8 +525,6 @@ func_decl * datatype_decl_plugin::mk_func_decl(decl_kind k, unsigned num_paramet
return 0;
}
else {
symbol c_name = datatype->get_parameter(k_i).get_symbol();
unsigned num_accessors = datatype->get_parameter(k_i + 2).get_int();
if (num_accessors != arity) {
@ -577,16 +596,22 @@ func_decl * datatype_decl_plugin::mk_func_decl(decl_kind k, unsigned num_paramet
}
}
bool datatype_decl_plugin::mk_datatypes(unsigned num_datatypes, datatype_decl * const * datatypes, sort_ref_vector & new_types) {
bool datatype_decl_plugin::mk_datatypes(unsigned num_datatypes, datatype_decl * const * datatypes, unsigned num_params, sort* const* sort_params, sort_ref_vector & new_types) {
buffer<parameter> p;
p.push_back(parameter(num_datatypes));
p.push_back(parameter(-1));
p.push_back(parameter(num_params));
for (unsigned i = 0; i < num_params; ++i) {
p.push_back(parameter(sort_params[i]));
}
unsigned c_offset = constructor_offset(p.c_ptr());
for (unsigned i = 0; i < num_datatypes; i++) {
p.push_back(parameter(datatypes[i]->get_name()));
p.push_back(parameter(-1)); // offset is unknown at this point
}
for (unsigned i = 0; i < num_datatypes; i++) {
p[3+2*i] = parameter(p.size()); // save offset to constructor table
p[c_offset + 1 + 2*i] = parameter(p.size()); // save offset to constructor table
ptr_vector<constructor_decl> const & constructors = datatypes[i]->get_constructors();
unsigned num_constructors = constructors.size();
p.push_back(parameter(num_constructors));
@ -595,7 +620,7 @@ bool datatype_decl_plugin::mk_datatypes(unsigned num_datatypes, datatype_decl *
}
}
for (unsigned i = 0; i < num_datatypes; i++) {
unsigned o = p[3+2*i].get_int();
unsigned o = constructor_offset(p.c_ptr(), i);
ptr_vector<constructor_decl> const & constructors = datatypes[i]->get_constructors();
unsigned num_constructors = constructors.size();
for (unsigned j = 0; j < num_constructors; j++) {
@ -655,7 +680,7 @@ bool datatype_decl_plugin::is_fully_interp(sort const * s) const {
parameter const * parameters = s->get_parameters();
unsigned num_types = parameters[0].get_int();
for (unsigned tid = 0; tid < num_types; tid++) {
unsigned o = parameters[2 + 2*tid + 1].get_int(); // constructor offset
unsigned o = datatype_decl_plugin::constructor_offset(s, tid);
unsigned num_constructors = parameters[o].get_int();
for (unsigned si = 1; si <= num_constructors; si++) {
unsigned k_i = parameters[o + si].get_int();
@ -692,6 +717,28 @@ bool datatype_decl_plugin::is_value_visit(expr * arg, ptr_buffer<app> & todo) co
}
}
unsigned datatype_decl_plugin::constructor_offset(sort const* s) {
return constructor_offset(s->get_parameters());
}
unsigned datatype_decl_plugin::constructor_offset(parameter const& p) {
return 3 + p.get_int();
}
unsigned datatype_decl_plugin::constructor_offset(parameter const* ps) {
return constructor_offset(ps[2]);
}
unsigned datatype_decl_plugin::constructor_offset(sort const* s, unsigned tid) {
unsigned c_offset = constructor_offset(s->get_parameters());
return s->get_parameter(c_offset + 1 + 2*tid).get_int();
}
unsigned datatype_decl_plugin::constructor_offset(parameter const* ps, unsigned tid) {
unsigned c_offset = constructor_offset(ps[2]);
return ps[c_offset + 1 + 2*tid].get_int();
}
bool datatype_decl_plugin::is_value(app * e) const {
TRACE("dt_is_value", tout << "checking\n" << mk_ismt2_pp(e, *m_manager) << "\n";);
if (!get_util().is_constructor(e))
@ -742,7 +789,7 @@ datatype_util::~datatype_util() {
func_decl * datatype_util::get_constructor(sort * ty, unsigned c_id) {
unsigned tid = ty->get_parameter(1).get_int();
unsigned o = ty->get_parameter(3 + 2*tid).get_int();
unsigned o = datatype_decl_plugin::constructor_offset(ty, tid);
unsigned k_i = ty->get_parameter(o + c_id + 1).get_int();
unsigned num_accessors = ty->get_parameter(k_i + 2).get_int();
parameter p[2] = { parameter(ty), parameter(c_id) };
@ -765,7 +812,7 @@ ptr_vector<func_decl> const * datatype_util::get_datatype_constructors(sort * ty
m_vectors.push_back(r);
m_datatype2constructors.insert(ty, r);
unsigned tid = ty->get_parameter(1).get_int();
unsigned o = ty->get_parameter(3 + 2*tid).get_int();
unsigned o = datatype_decl_plugin::constructor_offset(ty, tid);
unsigned num_constructors = ty->get_parameter(o).get_int();
for (unsigned c_id = 0; c_id < num_constructors; c_id++) {
func_decl * c = get_constructor(ty, c_id);
@ -880,7 +927,7 @@ ptr_vector<func_decl> const * datatype_util::get_constructor_accessors(func_decl
unsigned c_id = constructor->get_parameter(1).get_int();
sort * datatype = constructor->get_range();
unsigned tid = datatype->get_parameter(1).get_int();
unsigned o = datatype->get_parameter(3 + 2*tid).get_int();
unsigned o = datatype_decl_plugin::constructor_offset(datatype, tid);
unsigned k_i = datatype->get_parameter(o + c_id + 1).get_int();
unsigned num_accessors = datatype->get_parameter(k_i+2).get_int();
parameter p[3] = { parameter(datatype), parameter(c_id), parameter(-1) };

33
src/ast/datatype_decl_plugin.h
View file

@ -100,10 +100,16 @@ public:
Contract for sort:
parameters[0] - (int) n - number of recursive types.
parameters[1] - (int) i - index 0..n-1 of which type is defined.
parameters[2] - (int) p - number of type parameters.
for j = 0..p-1
parameters[3 + j] - (sort) s - type parameter
c_offset := 3 + p
for j in 0..n-1
parameters[2 + 2*j] - (symbol) name of the type
parameters[2 + 2*j + 1] - (int) o - offset where the constructors are defined.
parameters[c_offset + 2*j] - (symbol) name of the type
parameters[c_offset + 2*j + 1] - (int) o - offset where the constructors are defined.
for each offset o at parameters[2 + 2*j + 1] for some j in 0..n-1
parameters[o] - (int) m - number of constructors
@ -140,7 +146,7 @@ public:
virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
bool mk_datatypes(unsigned num_datatypes, datatype_decl * const * datatypes, sort_ref_vector & new_sorts);
bool mk_datatypes(unsigned num_datatypes, datatype_decl * const * datatypes, unsigned num_params, sort* const* sort_params, sort_ref_vector & new_sorts);
virtual expr * get_some_value(sort * s);
@ -152,6 +158,13 @@ public:
virtual void get_op_names(svector<builtin_name> & op_names, symbol const & logic);
static unsigned constructor_offset(sort const* s);
static unsigned constructor_offset(parameter const& p);
static unsigned constructor_offset(parameter const* ps);
static unsigned constructor_offset(sort const* s, unsigned tid);
static unsigned constructor_offset(parameter const* ps, unsigned tid);
private:
bool is_value_visit(expr * arg, ptr_buffer<app> & todo) const;
@ -201,9 +214,18 @@ public:
unsigned get_datatype_num_constructors(sort * ty) {
SASSERT(is_datatype(ty));
unsigned tid = ty->get_parameter(1).get_int();
unsigned o = ty->get_parameter(3 + 2 * tid).get_int();
unsigned o = datatype_decl_plugin::constructor_offset(ty, tid);
return ty->get_parameter(o).get_int();
}
unsigned get_datatype_num_parameter_sorts(sort * ty) {
SASSERT(is_datatype(ty));
return ty->get_parameter(2).get_int();
}
sort* get_datatype_parameter_sort(sort * ty, unsigned idx) {
SASSERT(is_datatype(ty));
SASSERT(idx < get_datatype_num_parameter_sorts(ty));
return to_sort(ty->get_parameter(3 + idx).get_ast());
}
unsigned get_constructor_idx(func_decl * f) const { SASSERT(is_constructor(f)); return f->get_parameter(1).get_int(); }
unsigned get_recognizer_constructor_idx(func_decl * f) const { SASSERT(is_recognizer(f)); return f->get_parameter(1).get_int(); }
func_decl * get_non_rec_constructor(sort * ty);
@ -218,6 +240,7 @@ public:
void reset();
void display_datatype(sort *s, std::ostream& strm);
};
#endif /* DATATYPE_DECL_PLUGIN_H_ */

9
src/ast/expr_map.h
View file

@ -35,6 +35,13 @@ class expr_map {
obj_map<expr, expr*> m_expr2expr;
obj_map<expr, proof*> m_expr2pr;
public:
typedef obj_map<expr, expr*> Map;
typedef Map::iterator iterator;
typedef Map::key key;
typedef Map::value value;
typedef Map::data data;
typedef Map::entry entry;
expr_map(ast_manager & m);
expr_map(ast_manager & m, bool store_proofs);
~expr_map();
@ -44,6 +51,8 @@ public:
void erase(expr * k);
void reset();
void flush();
iterator begin () const { return m_expr2expr.begin (); }
iterator end () const {return m_expr2expr.end (); }
void set_store_proofs(bool f) {
if (m_store_proofs != f) flush();
m_store_proofs = f;

13
src/ast/fpa/CMakeLists.txt Normal file
View file

@ -0,0 +1,13 @@
z3_add_component(fpa
SOURCES
bv2fpa_converter.cpp
fpa2bv_converter.cpp
fpa2bv_rewriter.cpp
COMPONENT_DEPENDENCIES
ast
simplifier
model
util
PYG_FILES
fpa2bv_rewriter_params.pyg
)

35
src/ast/fpa/fpa2bv_converter.cpp
View file

@ -1632,8 +1632,6 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args,
res_exp = e_exp;
// Result could overflow into 4.xxx ...
family_id bvfid = m_bv_util.get_fid();
expr_ref res_sgn_c1(m), res_sgn_c2(m), res_sgn_c3(m);
expr_ref not_e_sgn(m), not_f_sgn(m), not_sign_bv(m);
@ -1646,11 +1644,34 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args,
expr * res_sgn_or_args[3] = { res_sgn_c1, res_sgn_c2, res_sgn_c3 };
res_sgn = m_bv_util.mk_bv_or(3, res_sgn_or_args);
// Result could have overflown into 4.xxx.
SASSERT(m_bv_util.get_bv_size(sig_abs) == 2 * sbits + 2);
expr_ref ovfl_into_4(m);
ovfl_into_4 = m.mk_eq(m_bv_util.mk_extract(2 * sbits + 1, 2 * sbits, sig_abs),
m_bv_util.mk_numeral(1, 2));
dbg_decouple("fpa2bv_fma_ovfl_into_4", ovfl_into_4);
if (sbits > 5) {
sticky_raw = m_bv_util.mk_extract(sbits - 5, 0, sig_abs);
sticky = m_bv_util.mk_zero_extend(sbits + 3, m.mk_app(bvfid, OP_BREDOR, sticky_raw.get()));
expr * res_or_args[2] = { m_bv_util.mk_extract(2 * sbits - 1, sbits - 4, sig_abs), sticky };
res_sig = m_bv_util.mk_bv_or(2, res_or_args);
expr_ref sticky_raw(m), sig_upper(m), sticky_redd(m), res_sig_norm(m);
sticky_raw = m_bv_util.mk_extract(sbits - 4, 0, sig_abs);
sig_upper = m_bv_util.mk_extract(2 * sbits, sbits - 3, sig_abs);
SASSERT(m_bv_util.get_bv_size(sig_upper) == sbits + 4);
sticky_redd = m.mk_app(bvfid, OP_BREDOR, sticky_raw.get());
sticky = m_bv_util.mk_zero_extend(sbits + 3, sticky_redd);
expr * res_or_args[2] = { sig_upper, sticky };
res_sig_norm = m_bv_util.mk_bv_or(2, res_or_args);
expr_ref sticky_raw_ovfl(m), sig_upper_ovfl(m), sticky_redd_ovfl(m), sticky_ovfl(m), res_sig_ovfl(m);
sticky_raw_ovfl = m_bv_util.mk_extract(sbits - 4, 0, sig_abs);
sig_upper_ovfl = m_bv_util.mk_extract(2 * sbits, sbits - 3, sig_abs);
SASSERT(m_bv_util.get_bv_size(sig_upper_ovfl) == sbits + 4);
sticky_redd_ovfl = m.mk_app(bvfid, OP_BREDOR, sticky_raw_ovfl.get());
sticky_ovfl = m_bv_util.mk_zero_extend(sbits + 3, sticky_redd_ovfl);
expr * res_or_args_ovfl[2] = { sig_upper_ovfl, sticky_ovfl };
res_sig_ovfl = m_bv_util.mk_bv_or(2, res_or_args_ovfl);
res_sig = m.mk_ite(ovfl_into_4, res_sig_ovfl, res_sig_norm);
res_exp = m.mk_ite(ovfl_into_4, m_bv_util.mk_bv_add(res_exp, m_bv_util.mk_numeral(1, ebits+2)),
res_exp);
}
else {
unsigned too_short = 6 - sbits;
@ -1658,6 +1679,8 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args,
res_sig = m_bv_util.mk_extract(sbits + 3, 0, sig_abs);
}
dbg_decouple("fpa2bv_fma_add_sum_sticky", sticky);
dbg_decouple("fpa2bv_fma_sig_abs", sig_abs);
dbg_decouple("fpa2bv_fma_res_sig", res_sig);
SASSERT(m_bv_util.get_bv_size(res_sig) == sbits + 4);
expr_ref is_zero_sig(m), nil_sbits4(m);

9
src/ast/macros/CMakeLists.txt Normal file
View file

@ -0,0 +1,9 @@
z3_add_component(macros
SOURCES
macro_finder.cpp
macro_manager.cpp
macro_util.cpp
quasi_macros.cpp
COMPONENT_DEPENDENCIES
simplifier
)

13
src/ast/normal_forms/CMakeLists.txt Normal file
View file

@ -0,0 +1,13 @@
z3_add_component(normal_forms
SOURCES
defined_names.cpp
name_exprs.cpp
nnf.cpp
pull_quant.cpp
COMPONENT_DEPENDENCIES
rewriter
PYG_FILES
nnf_params.pyg
EXTRA_REGISTER_MODULE_HEADERS
nnf.h
)

36
src/ast/pattern/CMakeLists.txt Normal file
View file

@ -0,0 +1,36 @@
# If this code for adding the rule to generate the database file is ever needed
# for other components then we should refactor this code into
# z3_add_component()
if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/database.h")
message(FATAL_ERROR "The generated file \"${CMAKE_CURRENT_SOURCE_DIR}/database.h\""
${z3_polluted_tree_msg})
endif()
add_custom_command(OUTPUT "database.h"
COMMAND "${PYTHON_EXECUTABLE}"
"${CMAKE_SOURCE_DIR}/scripts/mk_pat_db.py"
"${CMAKE_CURRENT_SOURCE_DIR}/database.smt2"
"${CMAKE_CURRENT_BINARY_DIR}/database.h"
MAIN_DEPENDENCY "${CMAKE_CURRENT_SOURCE_DIR}/database.smt2"
DEPENDS "${CMAKE_SOURCE_DIR}/scripts/mk_pat_db.py"
${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
COMMENT "Generating \"database.h\""
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
VERBATIM
)
z3_add_component(pattern
SOURCES
expr_pattern_match.cpp
pattern_inference.cpp
pattern_inference_params.cpp
# Let CMake know this target depends on this generated
# header file
${CMAKE_CURRENT_BINARY_DIR}/database.h
COMPONENT_DEPENDENCIES
normal_forms
simplifier
smt2parser
PYG_FILES
pattern_inference_params_helper.pyg
)

1
src/ast/pb_decl_plugin.h
View file

@ -109,6 +109,7 @@ public:
bool is_ge(func_decl* a) const;
bool is_ge(expr* a) const { return is_app(a) && is_ge(to_app(a)->get_decl()); }
bool is_ge(expr* a, rational& k) const;
bool is_aux_bool(func_decl* f) const { return is_decl_of(f, m_fid, OP_PB_AUX_BOOL); }
bool is_aux_bool(expr* e) const { return is_app_of(e, m_fid, OP_PB_AUX_BOOL); }
rational get_coeff(expr* a, unsigned index) const { return get_coeff(to_app(a)->get_decl(), index); }
rational get_coeff(func_decl* a, unsigned index) const;

6
src/ast/proof_checker/CMakeLists.txt Normal file
View file

@ -0,0 +1,6 @@
z3_add_component(proof_checker
SOURCES
proof_checker.cpp
COMPONENT_DEPENDENCIES
rewriter
)

41
src/ast/rewriter/CMakeLists.txt Normal file
View file

@ -0,0 +1,41 @@
z3_add_component(rewriter
SOURCES
arith_rewriter.cpp
array_rewriter.cpp
ast_counter.cpp
bool_rewriter.cpp
bv_bounds.cpp
bv_rewriter.cpp
datatype_rewriter.cpp
der.cpp
distribute_forall.cpp
dl_rewriter.cpp
enum2bv_rewriter.cpp
expr_replacer.cpp
expr_safe_replace.cpp
factor_rewriter.cpp
fpa_rewriter.cpp
label_rewriter.cpp
mk_simplified_app.cpp
pb_rewriter.cpp
pb2bv_rewriter.cpp
quant_hoist.cpp
rewriter.cpp
seq_rewriter.cpp
th_rewriter.cpp
var_subst.cpp
bv_trailing.cpp
mk_extract_proc.cpp
COMPONENT_DEPENDENCIES
ast
automata
polynomial
PYG_FILES
arith_rewriter_params.pyg
array_rewriter_params.pyg
bool_rewriter_params.pyg
bv_rewriter_params.pyg
fpa_rewriter_params.pyg
poly_rewriter_params.pyg
rewriter_params.pyg
)

2
src/ast/rewriter/arith_rewriter.cpp
View file

@ -1030,7 +1030,7 @@ br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & res
br_status arith_rewriter::mk_to_int_core(expr * arg, expr_ref & result) {
numeral a;
expr* x;
expr* x = 0;
if (m_util.is_numeral(arg, a)) {
result = m_util.mk_numeral(floor(a), true);
return BR_DONE;

8
src/ast/rewriter/bit_blaster/CMakeLists.txt Normal file
View file

@ -0,0 +1,8 @@
z3_add_component(bit_blaster
SOURCES
bit_blaster.cpp
bit_blaster_rewriter.cpp
COMPONENT_DEPENDENCIES
rewriter
simplifier
)

1
src/ast/rewriter/pb_rewriter.cpp
View file

@ -196,6 +196,7 @@ void pb_rewriter::dump_pb_rewrite(expr* fml) {
}
br_status pb_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
if (m_util.is_aux_bool(f)) return BR_FAILED;
ast_manager& m = result.get_manager();
rational sum(0), maxsum(0);
for (unsigned i = 0; i < num_args; ++i) {

29
src/ast/simplifier/CMakeLists.txt Normal file
View file

@ -0,0 +1,29 @@
z3_add_component(simplifier
SOURCES
arith_simplifier_params.cpp
arith_simplifier_plugin.cpp
array_simplifier_params.cpp
array_simplifier_plugin.cpp
basic_simplifier_plugin.cpp
bit2int.cpp
bv_elim.cpp
bv_simplifier_params.cpp
bv_simplifier_plugin.cpp
datatype_simplifier_plugin.cpp
elim_bounds.cpp
fpa_simplifier_plugin.cpp
inj_axiom.cpp
maximise_ac_sharing.cpp
poly_simplifier_plugin.cpp
pull_ite_tree.cpp
push_app_ite.cpp
seq_simplifier_plugin.cpp
simplifier.cpp
simplifier_plugin.cpp
COMPONENT_DEPENDENCIES
rewriter
PYG_FILES
arith_simplifier_params_helper.pyg
array_simplifier_params_helper.pyg
bv_simplifier_params_helper.pyg
)

10
src/ast/substitution/CMakeLists.txt Normal file
View file

@ -0,0 +1,10 @@
z3_add_component(substitution
SOURCES
matcher.cpp
substitution.cpp
substitution_tree.cpp
unifier.cpp
COMPONENT_DEPENDENCIES
ast
rewriter
)

4
src/ast/substitution/substitution.cpp
View file

@ -85,7 +85,7 @@ void substitution::apply(unsigned num_actual_offsets, unsigned const * deltas, e
m_state = APPLY;
unsigned j;
expr * e;
expr * e = 0;
unsigned off;
expr_offset n1;
bool visited;
@ -214,7 +214,7 @@ void substitution::apply(unsigned num_actual_offsets, unsigned const * deltas, e
}
}
SASSERT(m_apply_cache.contains(n));
m_apply_cache.find(n, e);
VERIFY(m_apply_cache.find(n, e));
m_new_exprs.push_back(e);
result = e;

23
src/cmd_context/CMakeLists.txt Normal file
View file

@ -0,0 +1,23 @@
z3_add_component(cmd_context
SOURCES
basic_cmds.cpp
check_logic.cpp
cmd_context.cpp
cmd_context_to_goal.cpp
cmd_util.cpp
context_params.cpp
echo_tactic.cpp
eval_cmd.cpp
interpolant_cmds.cpp
parametric_cmd.cpp
pdecl.cpp
simplify_cmd.cpp
tactic_cmds.cpp
tactic_manager.cpp
COMPONENT_DEPENDENCIES
interp
rewriter
solver
EXTRA_REGISTER_MODULE_HEADERS
context_params.h
)

121
src/cmd_context/basic_cmds.cpp
View file

@ -39,7 +39,7 @@ class help_cmd : public cmd {
ctx.regular_stream() << " (" << s;
if (usage)
ctx.regular_stream() << " " << escaped(usage, true) << ")\n";
else
else
ctx.regular_stream() << ")\n";
if (descr) {
ctx.regular_stream() << " " << escaped(descr, true, 4) << "\n";
@ -62,7 +62,7 @@ public:
}
m_cmds.push_back(s);
}
typedef std::pair<symbol, cmd*> named_cmd;
struct named_cmd_lt {
bool operator()(named_cmd const & c1, named_cmd const & c2) const { return c1.first.str() < c2.first.str(); }
@ -104,14 +104,14 @@ class get_model_cmd : public cmd {
unsigned m_index;
public:
get_model_cmd(): cmd("get-model"), m_index(0) {}
virtual char const * get_usage() const { return "[<index of box objective>]"; }
virtual char const * get_descr(cmd_context & ctx) const {
return "retrieve model for the last check-sat command.\nSupply optional index if retrieving a model corresponding to a box optimization objective";
virtual char const * get_usage() const { return "[<index of box objective>]"; }
virtual char const * get_descr(cmd_context & ctx) const {
return "retrieve model for the last check-sat command.\nSupply optional index if retrieving a model corresponding to a box optimization objective";
}
virtual unsigned get_arity() const { return VAR_ARITY; }
virtual unsigned get_arity() const { return VAR_ARITY; }
virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { return CPK_UINT; }
virtual void set_next_arg(cmd_context & ctx, unsigned index) { m_index = index; }
virtual void execute(cmd_context & ctx) {
virtual void set_next_arg(cmd_context & ctx, unsigned index) { m_index = index; }
virtual void execute(cmd_context & ctx) {
if (!ctx.is_model_available() || ctx.get_check_sat_result() == 0)
throw cmd_exception("model is not available");
model_ref m;
@ -122,7 +122,7 @@ public:
ctx.get_check_sat_result()->get_model(m);
}
ctx.display_model(m);
}
}
virtual void reset(cmd_context& ctx) {
m_index = 0;
}
@ -149,7 +149,14 @@ ATOMIC_CMD(get_assignment_cmd, "get-assignment", "retrieve assignment", {
first = false;
else
ctx.regular_stream() << " ";
ctx.regular_stream() << "(" << name << " " << (ctx.m().is_true(val) ? "true" : "false") << ")";
ctx.regular_stream() << "(";
if (is_smt2_quoted_symbol(name)) {
ctx.regular_stream() << mk_smt2_quoted_symbol(name);
}
else {
ctx.regular_stream() << name;
}
ctx.regular_stream() << " " << (ctx.m().is_true(val) ? "true" : "false") << ")";
}
}
}
@ -160,11 +167,11 @@ class cmd_is_declared : public ast_smt_pp::is_declared {
cmd_context& m_ctx;
public:
cmd_is_declared(cmd_context& ctx): m_ctx(ctx) {}
virtual bool operator()(func_decl* d) const {
virtual bool operator()(func_decl* d) const {
return m_ctx.is_func_decl(d->get_name());
}
virtual bool operator()(sort* s) const {
virtual bool operator()(sort* s) const {
return m_ctx.is_sort_decl(s->get_name());
}
};
@ -182,13 +189,13 @@ ATOMIC_CMD(get_proof_cmd, "get-proof", "retrieve proof", {
if (ctx.well_sorted_check_enabled() && !is_well_sorted(ctx.m(), pr)) {
throw cmd_exception("proof is not well sorted");
}
pp_params params;
if (params.pretty_proof()) {
ctx.regular_stream() << mk_pp(pr, ctx.m()) << std::endl;
}
else {
// TODO: reimplement a new SMT2 pretty printer
// TODO: reimplement a new SMT2 pretty printer
ast_smt_pp pp(ctx.m());
cmd_is_declared isd(ctx);
pp.set_is_declared(&isd);
@ -199,19 +206,19 @@ ATOMIC_CMD(get_proof_cmd, "get-proof", "retrieve proof", {
});
static void print_core(cmd_context& ctx) {
ptr_vector<expr> core;
ctx.get_check_sat_result()->get_unsat_core(core);
ctx.regular_stream() << "(";
ptr_vector<expr>::const_iterator it = core.begin();
ptr_vector<expr>::const_iterator end = core.end();
for (bool first = true; it != end; ++it) {
if (first)
first = false;
else
ctx.regular_stream() << " ";
ctx.regular_stream() << mk_ismt2_pp(*it, ctx.m());
}
ctx.regular_stream() << ")" << std::endl;
ptr_vector<expr> core;
ctx.get_check_sat_result()->get_unsat_core(core);
ctx.regular_stream() << "(";
ptr_vector<expr>::const_iterator it = core.begin();
ptr_vector<expr>::const_iterator end = core.end();
for (bool first = true; it != end; ++it) {
if (first)
first = false;
else
ctx.regular_stream() << " ";
ctx.regular_stream() << mk_ismt2_pp(*it, ctx.m());
}
ctx.regular_stream() << ")" << std::endl;
}
ATOMIC_CMD(get_unsat_core_cmd, "get-unsat-core", "retrieve unsat core", {
@ -251,9 +258,9 @@ ATOMIC_CMD(get_assertions_cmd, "get-assertions", "retrieve asserted terms when i
ATOMIC_CMD(reset_assertions_cmd, "reset-assertions", "reset all asserted formulas (but retain definitions and declarations)", ctx.reset_assertions(););
ATOMIC_CMD(reset_assertions_cmd, "reset-assertions", "reset all asserted formulas (but retain definitions and declarations)", ctx.reset_assertions(); ctx.print_success(););
UNARY_CMD(set_logic_cmd, "set-logic", "<symbol>", "set the background logic.", CPK_SYMBOL, symbol const &,
UNARY_CMD(set_logic_cmd, "set-logic", "<symbol>", "set the background logic.", CPK_SYMBOL, symbol const &,
if (ctx.set_logic(arg))
ctx.print_success();
else {
@ -262,12 +269,14 @@ UNARY_CMD(set_logic_cmd, "set-logic", "<symbol>", "set the background logic.", C
}
);
UNARY_CMD(pp_cmd, "display", "<term>", "display the given term.", CPK_EXPR, expr *, {
UNARY_CMD(pp_cmd, "display", "<term>", "display the given term.", CPK_EXPR, expr *, {
ctx.display(ctx.regular_stream(), arg);
ctx.regular_stream() << std::endl;
ctx.regular_stream() << std::endl;
});
UNARY_CMD(echo_cmd, "echo", "<string>", "display the given string", CPK_STRING, char const *, ctx.regular_stream() << "\"" << arg << "\"" << std::endl;);
UNARY_CMD(echo_cmd, "echo", "<string>", "display the given string", CPK_STRING, char const *,
bool smt2c = ctx.params().m_smtlib2_compliant;
ctx.regular_stream() << (smt2c ? "\"" : "") << arg << (smt2c ? "\"" : "") << std::endl;);
class set_get_option_cmd : public cmd {
@ -298,18 +307,18 @@ protected:
symbol m_reproducible_resource_limit;
bool is_builtin_option(symbol const & s) const {
return
s == m_print_success || s == m_print_warning || s == m_expand_definitions ||
return
s == m_print_success || s == m_print_warning || s == m_expand_definitions ||
s == m_interactive_mode || s == m_produce_proofs || s == m_produce_unsat_cores || s == m_produce_unsat_assumptions ||
s == m_produce_models || s == m_produce_assignments || s == m_produce_interpolants ||
s == m_regular_output_channel || s == m_diagnostic_output_channel ||
s == m_regular_output_channel || s == m_diagnostic_output_channel ||
s == m_random_seed || s == m_verbosity || s == m_global_decls || s == m_global_declarations ||
s == m_produce_assertions || s == m_reproducible_resource_limit;
}
public:
set_get_option_cmd(char const * name):
cmd(name),
cmd(name),
m_true("true"),
m_false("false"),
m_print_success(":print-success"),
@ -341,7 +350,7 @@ public:
class set_option_cmd : public set_get_option_cmd {
bool m_unsupported;
symbol m_option;
bool to_bool(symbol const & value) const {
if (value != m_true && value != m_false)
throw cmd_exception("invalid option value, true/false expected");
@ -362,7 +371,7 @@ class set_option_cmd : public set_get_option_cmd {
throw cmd_exception(msg);
}
}
void set_param(cmd_context & ctx, char const * value) {
try {
gparams::set(m_option, value);
@ -459,11 +468,11 @@ public:
virtual void prepare(cmd_context & ctx) { m_unsupported = false; m_option = symbol::null; }
virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const {
virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const {
return m_option == symbol::null ? CPK_KEYWORD : CPK_OPTION_VALUE;
}
virtual void set_next_arg(cmd_context & ctx, symbol const & opt) {
virtual void set_next_arg(cmd_context & ctx, symbol const & opt) {
if (m_option == symbol::null) {
m_option = opt;
}
@ -518,7 +527,7 @@ class get_option_cmd : public set_get_option_cmd {
static void print_bool(cmd_context & ctx, bool b) {
ctx.regular_stream() << (b ? "true" : "false") << std::endl;
}
static void print_unsigned(cmd_context & ctx, unsigned v) {
ctx.regular_stream() << v << std::endl;
}
@ -535,11 +544,11 @@ public:
virtual char const * get_descr(cmd_context & ctx) const { return "get configuration option."; }
virtual unsigned get_arity() const { return 1; }
virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { return CPK_KEYWORD; }
virtual void set_next_arg(cmd_context & ctx, symbol const & opt) {
virtual void set_next_arg(cmd_context & ctx, symbol const & opt) {
if (opt == m_print_success) {
print_bool(ctx, ctx.print_success_enabled());
print_bool(ctx, ctx.print_success_enabled());
}
// TODO:
// TODO:
// else if (opt == m_print_warning) {
// print_bool(ctx, );
// }
@ -629,7 +638,7 @@ public:
virtual char const * get_descr(cmd_context & ctx) const { return "get information."; }
virtual unsigned get_arity() const { return 1; }
virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { return CPK_KEYWORD; }
virtual void set_next_arg(cmd_context & ctx, symbol const & opt) {
virtual void set_next_arg(cmd_context & ctx, symbol const & opt) {
if (opt == m_error_behavior) {
if (ctx.exit_on_error())
ctx.regular_stream() << "(:error-behavior immediate-exit)" << std::endl;
@ -685,12 +694,12 @@ public:
virtual char const * get_descr(cmd_context & ctx) const { return "set information."; }
virtual unsigned get_arity() const { return 2; }
virtual void prepare(cmd_context & ctx) { m_info = symbol::null; }
virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const {
return m_info == symbol::null ? CPK_KEYWORD : CPK_OPTION_VALUE;
virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const {
return m_info == symbol::null ? CPK_KEYWORD : CPK_OPTION_VALUE;
}
virtual void set_next_arg(cmd_context & ctx, rational const & val) {}
virtual void set_next_arg(cmd_context & ctx, char const * val) {}
virtual void set_next_arg(cmd_context & ctx, symbol const & s) {
virtual void set_next_arg(cmd_context & ctx, symbol const & s) {
if (m_info == symbol::null) {
m_info = s;
}
@ -738,7 +747,7 @@ public:
virtual char const * get_descr(cmd_context & ctx) const { return "declare a new array map operator with name <symbol> using the given function declaration.\n<func-decl-ref> ::= <symbol>\n | (<symbol> (<sort>*) <sort>)\n | ((_ <symbol> <numeral>+) (<sort>*) <sort>)\nThe last two cases are used to disumbiguate between declarations with the same name and/or select (indexed) builtin declarations.\nFor more details about the the array map operator, see 'Generalized and Efficient Array Decision Procedures' (FMCAD 2009).\nExample: (declare-map set-union (Int) (or (Bool Bool) Bool))\nDeclares a new function (declare-fun set-union ((Array Int Bool) (Array Int Bool)) (Array Int Bool)).\nThe instance of the map axiom for this new declaration is:\n(forall ((a1 (Array Int Bool)) (a2 (Array Int Bool)) (i Int)) (= (select (set-union a1 a2) i) (or (select a1 i) (select a2 i))))"; }
virtual unsigned get_arity() const { return 3; }
virtual void prepare(cmd_context & ctx) { m_name = symbol::null; m_domain.reset(); }
virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const {
virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const {
if (m_name == symbol::null) return CPK_SYMBOL;
if (m_domain.empty()) return CPK_SORT_LIST;
return CPK_FUNC_DECL;
@ -749,10 +758,10 @@ public:
throw cmd_exception("invalid map declaration, empty sort list");
m_domain.append(num, slist);
}
virtual void set_next_arg(cmd_context & ctx, func_decl * f) {
m_f = f;
if (m_f->get_arity() == 0)
throw cmd_exception("invalid map declaration, function declaration must have arity > 0");
virtual void set_next_arg(cmd_context & ctx, func_decl * f) {
m_f = f;
if (m_f->get_arity() == 0)
throw cmd_exception("invalid map declaration, function declaration must have arity > 0");
}
virtual void reset(cmd_context & ctx) {
m_array_fid = null_family_id;
@ -791,7 +800,7 @@ public:
virtual char const * get_descr(cmd_context & ctx) const { return "retrieve consequences that fix values for supplied variables"; }
virtual unsigned get_arity() const { return 2; }
virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { return CPK_EXPR_LIST; }
virtual void set_next_arg(cmd_context & ctx, unsigned num, expr * const * tlist) {
virtual void set_next_arg(cmd_context & ctx, unsigned num, expr * const * tlist) {
if (m_count == 0) {
m_assumptions.append(num, tlist);
++m_count;
@ -851,7 +860,7 @@ void install_basic_cmds(cmd_context & ctx) {
ctx.insert(alloc(builtin_cmd, "declare-fun", "<symbol> (<sort>*) <sort>", "declare a new function/constant."));
ctx.insert(alloc(builtin_cmd, "declare-const", "<symbol> <sort>", "declare a new constant."));
ctx.insert(alloc(builtin_cmd, "declare-datatypes", "(<symbol>*) (<datatype-declaration>+)", "declare mutually recursive datatypes.\n<datatype-declaration> ::= (<symbol> <constructor-decl>+)\n<constructor-decl> ::= (<symbol> <accessor-decl>*)\n<accessor-decl> ::= (<symbol> <sort>)\nexample: (declare-datatypes (T) ((BinTree (leaf (value T)) (node (left BinTree) (right BinTree)))))"));
ctx.insert(alloc(builtin_cmd, "check-sat-asuming", "( hprop_literali* )", "check sat assuming a collection of literals"));
ctx.insert(alloc(builtin_cmd, "check-sat-assuming", "( hprop_literali* )", "check sat assuming a collection of literals"));
ctx.insert(alloc(get_unsat_assumptions_cmd));
ctx.insert(alloc(reset_assertions_cmd));

50
src/cmd_context/cmd_context.cpp
View file

@ -15,6 +15,7 @@ Author:
Notes:
--*/
#include<signal.h>
#include"tptr.h"
#include"cmd_context.h"
@ -71,14 +72,22 @@ void func_decls::finalize(ast_manager & m) {
m_decls = 0;
}
bool func_decls::signatures_collide(func_decl* f, func_decl* g) const {
return f == g;
}
bool func_decls::contains(func_decl * f) const {
if (GET_TAG(m_decls) == 0) {
return UNTAG(func_decl*, m_decls) == f;
func_decl* g = UNTAG(func_decl*, m_decls);
return g && signatures_collide(f, g);
}
else {
func_decl_set * fs = UNTAG(func_decl_set *, m_decls);
return fs->contains(f);
for (func_decl* g : *fs) {
if (signatures_collide(f, g)) return true;
}
}
return false;
}
bool func_decls::insert(ast_manager & m, func_decl * f) {
@ -249,6 +258,7 @@ protected:
array_util m_arutil;
fpa_util m_futil;
seq_util m_sutil;
datatype_util m_dtutil;
datalog::dl_decl_util m_dlutil;
@ -270,7 +280,7 @@ protected:
}
public:
pp_env(cmd_context & o):m_owner(o), m_autil(o.m()), m_bvutil(o.m()), m_arutil(o.m()), m_futil(o.m()), m_sutil(o.m()), m_dlutil(o.m()) {}
pp_env(cmd_context & o):m_owner(o), m_autil(o.m()), m_bvutil(o.m()), m_arutil(o.m()), m_futil(o.m()), m_sutil(o.m()), m_dtutil(o.m()), m_dlutil(o.m()) {}
virtual ~pp_env() {}
virtual ast_manager & get_manager() const { return m_owner.m(); }
virtual arith_util & get_autil() { return m_autil; }
@ -278,6 +288,7 @@ public:
virtual array_util & get_arutil() { return m_arutil; }
virtual fpa_util & get_futil() { return m_futil; }
virtual seq_util & get_sutil() { return m_sutil; }
virtual datatype_util & get_dtutil() { return m_dtutil; }
virtual datalog::dl_decl_util& get_dlutil() { return m_dlutil; }
virtual bool uses(symbol const & s) const {
@ -325,8 +336,8 @@ cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l):
m_status(UNKNOWN),
m_numeral_as_real(false),
m_ignore_check(false),
m_exit_on_error(false),
m_processing_pareto(false),
m_exit_on_error(false),
m_manager(m),
m_own_manager(m == 0),
m_manager_initialized(false),
@ -1209,6 +1220,7 @@ void cmd_context::push() {
scope & s = m_scopes.back();
s.m_func_decls_stack_lim = m_func_decls_stack.size();
s.m_psort_decls_stack_lim = m_psort_decls_stack.size();
s.m_psort_inst_stack_lim = m_psort_inst_stack.size();
s.m_macros_stack_lim = m_macros_stack.size();
s.m_aux_pdecls_lim = m_aux_pdecls.size();
s.m_assertions_lim = m_assertions.size();
@ -1223,7 +1235,7 @@ void cmd_context::push(unsigned n) {
push();
}
void cmd_context::restore_func_decls(unsigned old_sz) {
void cmd_context::restore_func_decls(unsigned old_sz) {
SASSERT(old_sz <= m_func_decls_stack.size());
svector<sf_pair>::iterator it = m_func_decls_stack.begin() + old_sz;
svector<sf_pair>::iterator end = m_func_decls_stack.end();
@ -1234,6 +1246,14 @@ void cmd_context::restore_func_decls(unsigned old_sz) {
m_func_decls_stack.resize(old_sz);
}
void cmd_context::restore_psort_inst(unsigned old_sz) {
for (unsigned i = old_sz; i < m_psort_inst_stack.size(); ++i) {
pdecl * s = m_psort_inst_stack[i];
s->reset_cache(*m_pmanager);
}
m_psort_inst_stack.resize(old_sz);
}
void cmd_context::restore_psort_decls(unsigned old_sz) {
SASSERT(old_sz <= m_psort_decls_stack.size());
svector<symbol>::iterator it = m_psort_decls_stack.begin() + old_sz;
@ -1241,9 +1261,7 @@ void cmd_context::restore_psort_decls(unsigned old_sz) {
for (; it != end; ++it) {
symbol const & s = *it;
psort_decl * d = 0;
if (!m_psort_decls.find(s, d)) {
UNREACHABLE();
}
VERIFY(m_psort_decls.find(s, d));
pm().dec_ref(d);
m_psort_decls.erase(s);
}
@ -1257,9 +1275,7 @@ void cmd_context::restore_macros(unsigned old_sz) {
for (; it != end; ++it) {
symbol const & s = *it;
macro _m;
if (!m_macros.find(s, _m)) {
UNREACHABLE();
}
VERIFY (m_macros.find(s, _m));
m().dec_ref(_m.second);
m_macros.erase(s);
}
@ -1322,7 +1338,9 @@ void cmd_context::pop(unsigned n) {
restore_macros(s.m_macros_stack_lim);
restore_aux_pdecls(s.m_aux_pdecls_lim);
restore_assertions(s.m_assertions_lim);
restore_psort_inst(s.m_psort_inst_stack_lim);
m_scopes.shrink(new_lvl);
}
void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions) {
@ -1359,7 +1377,6 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
throw ex;
}
catch (z3_exception & ex) {
get_opt()->display_assignment(regular_stream());
throw cmd_exception(ex.msg());
}
if (m_processing_pareto && r != l_true) {
@ -1397,7 +1414,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
}
validate_check_sat_result(r);
if (was_opt && r != l_false && !m_processing_pareto) {
get_opt()->display_assignment(regular_stream());
// get_opt()->display_assignment(regular_stream());
}
if (r == l_true && m_params.m_dump_models) {
@ -1802,7 +1819,7 @@ cmd_context::dt_eh::dt_eh(cmd_context & owner):
cmd_context::dt_eh::~dt_eh() {
}
void cmd_context::dt_eh::operator()(sort * dt) {
void cmd_context::dt_eh::operator()(sort * dt, pdecl* pd) {
TRACE("new_dt_eh", tout << "new datatype: "; m_owner.pm().display(tout, dt); tout << "\n";);
ptr_vector<func_decl> const * constructors = m_dt_util.get_datatype_constructors(dt);
unsigned num_constructors = constructors->size();
@ -1821,8 +1838,13 @@ void cmd_context::dt_eh::operator()(sort * dt) {
TRACE("new_dt_eh", tout << "new accessor: " << a->get_name() << "\n";);
}
}
if (m_owner.m_scopes.size() > 0) {
m_owner.m_psort_inst_stack.push_back(pd);
}
}
std::ostream & operator<<(std::ostream & out, cmd_context::status st) {
switch (st) {
case cmd_context::UNSAT: out << "unsat"; break;

9
src/cmd_context/cmd_context.h
View file

@ -42,6 +42,7 @@ Notes:
class func_decls {
func_decl * m_decls;
bool signatures_collide(func_decl* f, func_decl* g) const;
public:
func_decls():m_decls(0) {}
func_decls(ast_manager & m, func_decl * f);
@ -159,7 +160,7 @@ protected:
bool m_produce_assignments;
status m_status;
bool m_numeral_as_real;
bool m_ignore_check; // used by the API to disable check-sat() commands when parsing SMT 2.0 files.
bool m_ignore_check; // used by the API to disable check-sat() commands when parsing SMT 2.0 files.
bool m_processing_pareto; // used when re-entering check-sat for pareto front.
bool m_exit_on_error;
@ -189,6 +190,8 @@ protected:
svector<sf_pair> m_func_decls_stack;
svector<symbol> m_psort_decls_stack;
svector<symbol> m_macros_stack;
ptr_vector<pdecl> m_psort_inst_stack;
//
ptr_vector<pdecl> m_aux_pdecls;
ptr_vector<expr> m_assertions;
@ -200,6 +203,7 @@ protected:
unsigned m_psort_decls_stack_lim;
unsigned m_macros_stack_lim;
unsigned m_aux_pdecls_lim;
unsigned m_psort_inst_stack_lim;
// only m_assertions_lim is relevant when m_global_decls = true
unsigned m_assertions_lim;
};
@ -219,7 +223,7 @@ protected:
public:
dt_eh(cmd_context & owner);
virtual ~dt_eh();
virtual void operator()(sort * dt);
virtual void operator()(sort * dt, pdecl* pd);
};
friend class dt_eh;
@ -245,6 +249,7 @@ protected:
void restore_macros(unsigned old_sz);
void restore_aux_pdecls(unsigned old_sz);
void restore_assertions(unsigned old_sz);
void restore_psort_inst(unsigned old_sz);
void erase_func_decl_core(symbol const & s, func_decl * f);
void erase_psort_decl_core(symbol const & s);

10
src/cmd_context/extra_cmds/CMakeLists.txt Normal file
View file

@ -0,0 +1,10 @@
z3_add_component(extra_cmds
SOURCES
dbg_cmds.cpp
polynomial_cmds.cpp
subpaving_cmds.cpp
COMPONENT_DEPENDENCIES
arith_tactics
cmd_context
subpaving_tactic
)

12
src/cmd_context/interpolant_cmds.cpp
View file

@ -46,20 +46,14 @@ static void show_interpolant_and_maybe_check(cmd_context & ctx,
m_params.set_bool("flat", true);
th_rewriter s(ctx.m(), m_params);
ctx.regular_stream() << "(interpolants";
for(unsigned i = 0; i < interps.size(); i++){
expr_ref r(ctx.m());
proof_ref pr(ctx.m());
s(to_expr(interps[i]),r,pr);
ctx.regular_stream() << mk_pp(r.get(), ctx.m()) << std::endl;
#if 0
ast_smt_pp pp(ctx.m());
pp.set_logic(ctx.get_logic().str().c_str());
pp.display_smt2(ctx.regular_stream(), to_expr(interps[i]));
ctx.regular_stream() << std::endl;
#endif
ctx.regular_stream() << "\n " << r;
}
ctx.regular_stream() << ")\n";
s.cleanup();

54
src/cmd_context/pdecl.cpp
View file

@ -123,6 +123,10 @@ sort * psort::find(sort * const * s) const {
}
void psort::finalize(pdecl_manager & m) {
reset_cache(m);
}
void psort::reset_cache(pdecl_manager& m) {
m.del_inst_cache(m_inst_cache);
m_inst_cache = 0;
}
@ -171,10 +175,11 @@ public:
if (other->hcons_kind() != hcons_kind())
return false;
return get_num_params() == other->get_num_params() && m_idx == static_cast<psort_var const *>(other)->m_idx;
}
}
virtual void display(std::ostream & out) const {
out << "s_" << m_idx;
}
unsigned idx() const { return m_idx; }
};
class psort_app : public psort {
@ -268,6 +273,10 @@ psort_decl::psort_decl(unsigned id, unsigned num_params, pdecl_manager & m, symb
}
void psort_decl::finalize(pdecl_manager & m) {
reset_cache(m);
}
void psort_decl::reset_cache(pdecl_manager& m) {
m.del_inst_cache(m_inst_cache);
m_inst_cache = 0;
}
@ -284,6 +293,27 @@ sort * psort_decl::find(sort * const * s) {
return m_inst_cache->find(s);
}
#if 0
psort_dt_decl::psort_dt_decl(unsigned id, unsigned num_params, pdecl_manager& m, symbol const& n):
psort_decl(id, num_params, m, n) {
}
void psort_dt_decl::finalize(pdecl_manager& m) {
psort_decl::finalize(m);
}
sort * psort_dt_decl::instantiate(pdecl_manager & m, unsigned n, sort * const * s) {
UNREACHABLE();
return 0;
}
void psort_dt_decl::display(std::ostream & out) const {
out << get_name() << " " << get_num_params();
}
#endif
psort_user_decl::psort_user_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n, psort * p):
psort_decl(id, num_params, m, n),
m_def(p) {
@ -389,13 +419,15 @@ paccessor_decl::paccessor_decl(unsigned id, unsigned num_params, pdecl_manager &
pdecl(id, num_params),
m_name(n),
m_type(r) {
if (m_type.kind() == PTR_PSORT)
if (m_type.kind() == PTR_PSORT) {
m.inc_ref(r.get_psort());
}
}
void paccessor_decl::finalize(pdecl_manager & m) {
if (m_type.kind() == PTR_PSORT)
m.lazy_dec_ref(m_type.get_psort());
if (m_type.kind() == PTR_PSORT) {
m.lazy_dec_ref(m_type.get_psort());
}
}
bool paccessor_decl::has_missing_refs(symbol & missing) const {
@ -576,13 +608,13 @@ sort * pdatatype_decl::instantiate(pdecl_manager & m, unsigned n, sort * const *
dts.m_buffer.push_back(instantiate_decl(m, s));
datatype_decl * d_ptr = dts.m_buffer[0];
sort_ref_vector sorts(m.m());
bool is_ok = m.get_dt_plugin()->mk_datatypes(1, &d_ptr, sorts);
bool is_ok = m.get_dt_plugin()->mk_datatypes(1, &d_ptr, m_num_params, s, sorts);
TRACE("pdatatype_decl", tout << "instantiating " << m_name << " is_ok: " << is_ok << "\n";);
if (is_ok) {
r = sorts.get(0);
cache(m, s, r);
m.save_info(r, this, n, s);
m.notify_new_dt(r);
m.notify_new_dt(r, this);
return r;
}
}
@ -651,7 +683,7 @@ bool pdatatypes_decl::instantiate(pdecl_manager & m, sort * const * s) {
dts.m_buffer.push_back((*it)->instantiate_decl(m, s));
}
sort_ref_vector sorts(m.m());
bool is_ok = m.get_dt_plugin()->mk_datatypes(dts.m_buffer.size(), dts.m_buffer.c_ptr(), sorts);
bool is_ok = m.get_dt_plugin()->mk_datatypes(dts.m_buffer.size(), dts.m_buffer.c_ptr(), m_num_params, s, sorts);
if (!is_ok)
return false;
it = m_datatypes.begin();
@ -659,7 +691,7 @@ bool pdatatypes_decl::instantiate(pdecl_manager & m, sort * const * s) {
sort * new_dt = sorts.get(i);
(*it)->cache(m, s, new_dt);
m.save_info(new_dt, *it, m_num_params, s);
m.notify_new_dt(new_dt);
m.notify_new_dt(new_dt, *it);
}
return true;
}
@ -853,6 +885,11 @@ psort_decl * pdecl_manager::mk_psort_user_decl(unsigned num_params, symbol const
return new (a().allocate(sizeof(psort_user_decl))) psort_user_decl(m_id_gen.mk(), num_params, *this, n, def);
}
//psort_decl * pdecl_manager::mk_psort_dt_decl(unsigned num_params, symbol const & n) {
// return new (a().allocate(sizeof(psort_dt_decl))) psort_dt_decl(m_id_gen.mk(), num_params, *this, n);
//}
psort_decl * pdecl_manager::mk_psort_builtin_decl(symbol const & n, family_id fid, decl_kind k) {
return new (a().allocate(sizeof(psort_builtin_decl))) psort_builtin_decl(m_id_gen.mk(), *this, n, fid, k);
}
@ -862,6 +899,7 @@ sort * pdecl_manager::instantiate(psort * p, unsigned num, sort * const * args)
return p->instantiate(*this, args);
}
void pdecl_manager::del_decl_core(pdecl * p) {
TRACE("pdecl_manager",
tout << "del_decl_core:\n";

24
src/cmd_context/pdecl.h
View file

@ -46,6 +46,7 @@ public:
unsigned get_ref_count() const { return m_ref_count; }
unsigned hash() const { return m_id; }
virtual void display(std::ostream & out) const {}
virtual void reset_cache(pdecl_manager& m) {}
};
class psort_inst_cache;
@ -75,6 +76,7 @@ public:
virtual char const * hcons_kind() const = 0;
virtual unsigned hcons_hash() const = 0;
virtual bool hcons_eq(psort const * other) const = 0;
virtual void reset_cache(pdecl_manager& m);
};
// for hash consing
@ -102,6 +104,7 @@ public:
// Only builtin declarations can have a variable number of parameters.
bool has_var_params() const { return m_num_params == PSORT_DECL_VAR_PARAMS; }
symbol const & get_name() const { return m_name; }
virtual void reset_cache(pdecl_manager& m);
};
class psort_user_decl : public psort_decl {
@ -131,6 +134,20 @@ public:
virtual void display(std::ostream & out) const;
};
#if 0
class psort_dt_decl : public psort_decl {
protected:
friend class pdecl_manager;
psort_dt_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n);
virtual size_t obj_size() const { return sizeof(psort_dt_decl); }
virtual void finalize(pdecl_manager & m);
virtual ~psort_dt_decl() {}
public:
virtual sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s);
virtual void display(std::ostream & out) const;
};
#endif
class datatype_decl_plugin;
class datatype_decl;
class constructor_decl;
@ -246,7 +263,7 @@ public:
class new_datatype_eh {
public:
virtual ~new_datatype_eh() {}
virtual void operator()(sort * dt) = 0;
virtual void operator()(sort * dt, pdecl* pd) = 0;
};
class pdecl_manager {
@ -279,10 +296,11 @@ public:
small_object_allocator & a() const { return m_allocator; }
family_id get_datatype_fid() const { return m_datatype_fid; }
void set_new_datatype_eh(new_datatype_eh * eh) { m_new_dt_eh = eh; }
psort * mk_psort_cnst(sort * s);
psort * mk_psort_cnst(sort * s);
psort * mk_psort_var(unsigned num_params, unsigned vidx);
psort * mk_psort_app(unsigned num_params, psort_decl * d, unsigned num_args, psort * const * args);
psort * mk_psort_app(psort_decl * d);
// psort_decl * mk_psort_dt_decl(unsigned num_params, symbol const & n);
psort_decl * mk_psort_user_decl(unsigned num_params, symbol const & n, psort * def);
psort_decl * mk_psort_builtin_decl(symbol const & n, family_id fid, decl_kind k);
paccessor_decl * mk_paccessor_decl(unsigned num_params, symbol const & s, ptype const & p);
@ -304,7 +322,7 @@ public:
void dec_ref(unsigned num, T * const * ps) { lazy_dec_ref(num, ps); del_decls(); }
psort_inst_cache * mk_inst_cache(unsigned num_params);
void del_inst_cache(psort_inst_cache * c);
void notify_new_dt(sort * dt) { if (m_new_dt_eh) (*m_new_dt_eh)(dt); }
void notify_new_dt(sort * dt, pdecl* pd) { if (m_new_dt_eh) (*m_new_dt_eh)(dt, pd); }
datatype_decl_plugin * get_dt_plugin() const;
void save_info(sort * s, psort_decl * d, unsigned num_args, sort * const * args);

3
src/cmd_context/tactic_cmds.cpp
View file

@ -308,6 +308,9 @@ public:
}
virtual void execute(cmd_context & ctx) {
if (!m_tactic) {
throw cmd_exception("apply needs a tactic argument");
}
params_ref p = ctx.params().merge_default_params(ps());
tactic_ref tref = using_params(sexpr2tactic(ctx, m_tactic), p);
{

11
src/duality/CMakeLists.txt Normal file
View file

@ -0,0 +1,11 @@
z3_add_component(duality
SOURCES
duality_profiling.cpp
duality_rpfp.cpp
duality_solver.cpp
duality_wrapper.cpp
COMPONENT_DEPENDENCIES
interp
qe
smt
)

18
src/interp/CMakeLists.txt Normal file
View file

@ -0,0 +1,18 @@
z3_add_component(interp
SOURCES
iz3base.cpp
iz3checker.cpp
iz3interp.cpp
iz3mgr.cpp
iz3pp.cpp
iz3profiling.cpp
iz3proof.cpp
iz3proof_itp.cpp
iz3scopes.cpp
iz3translate.cpp
iz3translate_direct.cpp
COMPONENT_DEPENDENCIES
solver
PYG_FILES
interp_params.pyg
)

6
src/math/automata/CMakeLists.txt Normal file
View file

@ -0,0 +1,6 @@
z3_add_component(automata
SOURCES
automaton.cpp
COMPONENT_DEPENDENCIES
util
)

6
src/math/euclid/CMakeLists.txt Normal file
View file

@ -0,0 +1,6 @@
z3_add_component(euclid
SOURCES
euclidean_solver.cpp
COMPONENT_DEPENDENCIES
util
)

6
src/math/grobner/CMakeLists.txt Normal file
View file

@ -0,0 +1,6 @@
z3_add_component(grobner
SOURCES
grobner.cpp
COMPONENT_DEPENDENCIES
ast
)

6
src/math/hilbert/CMakeLists.txt Normal file
View file

@ -0,0 +1,6 @@
z3_add_component(hilbert
SOURCES
hilbert_basis.cpp
COMPONENT_DEPENDENCIES
util
)

6
src/math/interval/CMakeLists.txt Normal file
View file

@ -0,0 +1,6 @@
z3_add_component(interval
SOURCES
interval_mpq.cpp
COMPONENT_DEPENDENCIES
util
)

17
src/math/polynomial/CMakeLists.txt Normal file
View file

@ -0,0 +1,17 @@
z3_add_component(polynomial
SOURCES
algebraic_numbers.cpp
polynomial_cache.cpp
polynomial.cpp
rpolynomial.cpp
sexpr2upolynomial.cpp
upolynomial.cpp
upolynomial_factorization.cpp
COMPONENT_DEPENDENCIES
util
PYG_FILES
algebraic_params.pyg
EXTRA_REGISTER_MODULE_HEADERS
polynomial.h
)

9
src/math/realclosure/CMakeLists.txt Normal file
View file

@ -0,0 +1,9 @@
z3_add_component(realclosure
SOURCES
mpz_matrix.cpp
realclosure.cpp
COMPONENT_DEPENDENCIES
interval
PYG_FILES
rcf_params.pyg
)

7
src/math/simplex/CMakeLists.txt Normal file
View file

@ -0,0 +1,7 @@
z3_add_component(simplex
SOURCES
simplex.cpp
model_based_opt.cpp
COMPONENT_DEPENDENCIES
util
)

11
src/math/simplex/model_based_opt.cpp
View file

@ -18,8 +18,9 @@ Revision History:
--*/
#include "model_based_opt.h"
#include "uint_set.h"
#include "math/simplex/model_based_opt.h"
#include "util/uint_set.h"
#include "util/z3_exception.h"
std::ostream& operator<<(std::ostream& out, opt::ineq_type ie) {
switch (ie) {
@ -868,6 +869,9 @@ namespace opt {
for (unsigned i = 0; i < mod_rows.size(); ++i) {
D = lcm(D, m_rows[mod_rows[i]].m_mod);
}
if (D.is_zero()) {
throw default_exception("modulo 0 is not defined");
}
TRACE("opt", display(tout << "lcm: " << D << " tableau\n"););
rational val_x = m_var2value[x];
rational u = mod(val_x, D);
@ -954,7 +958,8 @@ namespace opt {
row& r1 = m_rows[row_id1];
vector<var> coeffs;
mk_coeffs_without(coeffs, r1.m_vars, x);
add_divides(coeffs, r1.m_coeff, abs(a));
rational c = r1.m_coeff;
add_divides(coeffs, c, abs(a));
}
unsigned_vector const& row_ids = m_var2row_ids[x];
uint_set visited;

11
src/math/subpaving/CMakeLists.txt Normal file
View file

@ -0,0 +1,11 @@
z3_add_component(subpaving
SOURCES
subpaving.cpp
subpaving_hwf.cpp
subpaving_mpf.cpp
subpaving_mpff.cpp
subpaving_mpfx.cpp
subpaving_mpq.cpp
COMPONENT_DEPENDENCIES
interval
)

10
src/math/subpaving/tactic/CMakeLists.txt Normal file
View file

@ -0,0 +1,10 @@
z3_add_component(subpaving_tactic
SOURCES
expr2subpaving.cpp
subpaving_tactic.cpp
COMPONENT_DEPENDENCIES
core_tactics
subpaving
TACTIC_HEADERS
subpaving_tactic.h
)

18
src/model/CMakeLists.txt Normal file
View file

@ -0,0 +1,18 @@
z3_add_component(model
SOURCES
func_interp.cpp
model2expr.cpp
model_core.cpp
model.cpp
model_evaluator.cpp
model_implicant.cpp
model_pp.cpp
model_smt2_pp.cpp
model_v2_pp.cpp
COMPONENT_DEPENDENCIES
rewriter
PYG_FILES
model_evaluator_params.pyg
model_params.pyg
)

61
src/model/model_evaluator.cpp
View file

@ -125,7 +125,6 @@ struct evaluator_cfg : public default_rewriter_cfg {
expr * val = m_model.get_const_interp(f);
if (val != 0) {
result = val;
expand_value(result);
return BR_DONE;
}
@ -202,8 +201,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
void expand_value(expr_ref& val) {
vector<expr_ref_vector> stores;
expr_ref else_case(m());
bool args_are_unique;
if (m_ar.is_array(val) && extract_array_func_interp(val, stores, else_case, args_are_unique)) {
bool _unused;
if (m_ar.is_array(val) && extract_array_func_interp(val, stores, else_case, _unused)) {
sort* srt = m().get_sort(val);
val = m_ar.mk_const_array(srt, else_case);
for (unsigned i = stores.size(); i > 0; ) {
@ -213,7 +212,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
args.append(stores[i].size(), stores[i].c_ptr());
val = m_ar.mk_store(args.size(), args.c_ptr());
}
}
}
}
bool get_macro(func_decl * f, expr * & def, quantifier * & q, proof * & def_pr) {
@ -274,7 +273,6 @@ struct evaluator_cfg : public default_rewriter_cfg {
return BR_FAILED;
}
// disabled until made more efficient
vector<expr_ref_vector> stores1, stores2;
bool args_are_unique1, args_are_unique2;
expr_ref else1(m()), else2(m());
@ -291,13 +289,13 @@ struct evaluator_cfg : public default_rewriter_cfg {
else {
conj.push_back(m().mk_eq(else1, else2));
}
args1.push_back(a);
args2.push_back(b);
if (args_are_unique1 && args_are_unique2 && !stores1.empty()) {
return mk_array_eq(stores1, else1, stores2, else2, conj, result);
return mk_array_eq_core(stores1, else1, stores2, else2, conj, result);
}
// TBD: this is too inefficient.
args1.push_back(a);
args2.push_back(b);
stores1.append(stores2);
for (unsigned i = 0; i < stores1.size(); ++i) {
args1.resize(1); args1.append(stores1[i].size() - 1, stores1[i].c_ptr());
@ -338,20 +336,22 @@ struct evaluator_cfg : public default_rewriter_cfg {
typedef hashtable<expr*const*, args_hash, args_eq> args_table;
br_status mk_array_eq(vector<expr_ref_vector> const& stores1, expr* else1,
vector<expr_ref_vector> const& stores2, expr* else2,
expr_ref_vector& conj, expr_ref& result) {
br_status mk_array_eq_core(vector<expr_ref_vector> const& stores1, expr* else1,
vector<expr_ref_vector> const& stores2, expr* else2,
expr_ref_vector& conj, expr_ref& result) {
unsigned arity = stores1[0].size()-1; // TBD: fix arity.
args_hash ah(arity);
args_eq ae(arity);
args_table table1(DEFAULT_HASHTABLE_INITIAL_CAPACITY, ah, ae);
args_table table2(DEFAULT_HASHTABLE_INITIAL_CAPACITY, ah, ae);
for (unsigned i = 0; i < stores1.size(); ++i) {
table1.insert(stores1[i].c_ptr());
}
for (unsigned i = stores2.size(); i > 0; ) {
// stores with smaller index take precedence
for (unsigned i = stores1.size(); i > 0; ) {
--i;
table1.insert(stores1[i].c_ptr());
}
for (unsigned i = 0, sz = stores2.size(); i < sz; ++i) {
if (table2.contains(stores2[i].c_ptr())) {
// first insertion takes precedence.
continue;
@ -361,7 +361,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
expr* val = stores2[i][arity];
if (table1.find(stores2[i].c_ptr(), args)) {
switch (compare(args[arity], val)) {
case l_true: table1.remove(stores2[i].c_ptr()); break;
case l_true: table1.remove(args); break;
case l_false: result = m().mk_false(); return BR_DONE;
default: conj.push_back(m().mk_eq(val, args[arity])); break;
}
@ -389,10 +389,10 @@ struct evaluator_cfg : public default_rewriter_cfg {
lbool compare(expr* a, expr* b) {
if (m().are_equal(a, b)) return l_true;
if (m().are_distinct(a, b)) return l_false;
return l_undef;
return l_undef;
}
bool args_are_values(expr_ref_vector const& store, bool& are_unique) {
bool are_values = true;
for (unsigned j = 0; are_values && j + 1 < store.size(); ++j) {
@ -402,7 +402,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
SASSERT(!are_unique || are_values);
return are_values;
}
bool extract_array_func_interp(expr* a, vector<expr_ref_vector>& stores, expr_ref& else_case, bool& are_unique) {
SASSERT(m_ar.is_array(a));
@ -417,14 +417,14 @@ struct evaluator_cfg : public default_rewriter_cfg {
stores.push_back(store);
a = to_app(a)->get_arg(0);
}
if (m_ar.is_const(a)) {
else_case = to_app(a)->get_arg(0);
return true;
}
if (!m_ar.is_as_array(a)) {
TRACE("model_evaluator", tout << "no translation: " << mk_pp(a, m()) << "\n";);
TRACE("model_evaluator", tout << "no translation: " << mk_pp(a, m()) << "\n";);
return false;
}
@ -432,6 +432,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
func_interp* g = m_model.get_func_interp(f);
unsigned sz = g->num_entries();
unsigned arity = f->get_arity();
unsigned base_sz = stores.size();
for (unsigned i = 0; i < sz; ++i) {
expr_ref_vector store(m());
func_entry const* fe = g->get_entry(i);
@ -444,7 +445,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
}
}
stores.push_back(store);
}
}
else_case = g->get_else();
if (!else_case) {
TRACE("model_evaluator", tout << "no else case " << mk_pp(a, m()) << "\n";
@ -456,7 +457,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
TRACE("model_evaluator", tout << "non-ground else case " << mk_pp(a, m()) << "\n" << else_case << "\n";);
return false;
}
for (unsigned i = stores.size(); are_values && i > 0; ) {
for (unsigned i = stores.size(); are_values && i > base_sz; ) {
--i;
if (m().are_equal(else_case, stores[i].back())) {
for (unsigned j = i + 1; j < stores.size(); ++j) {
@ -487,6 +488,10 @@ struct model_evaluator::imp : public rewriter_tpl<evaluator_cfg> {
m_cfg(md.get_manager(), md, p) {
set_cancel_check(false);
}
void expand_value (expr_ref &val) {
m_cfg.expand_value (val);
}
};
model_evaluator::model_evaluator(model_core & md, params_ref const & p) {
@ -524,7 +529,7 @@ unsigned model_evaluator::get_num_steps() const {
void model_evaluator::cleanup(params_ref const & p) {
model_core & md = m_imp->cfg().m_model;
dealloc(m_imp);
m_imp = alloc(imp, md, p);
m_imp = alloc(imp, md, p);
}
void model_evaluator::reset(params_ref const & p) {
@ -535,14 +540,12 @@ void model_evaluator::reset(params_ref const & p) {
void model_evaluator::operator()(expr * t, expr_ref & result) {
TRACE("model_evaluator", tout << mk_ismt2_pp(t, m()) << "\n";);
m_imp->operator()(t, result);
m_imp->expand_value(result);
}
expr_ref model_evaluator::operator()(expr * t) {
TRACE("model_evaluator", tout << mk_ismt2_pp(t, m()) << "\n";);
expr_ref result(m());
m_imp->operator()(t, result);
this->operator()(t, result);
return result;
}

23
src/muz/base/CMakeLists.txt Normal file
View file

@ -0,0 +1,23 @@
z3_add_component(muz
SOURCES
bind_variables.cpp
dl_boogie_proof.cpp
dl_context.cpp
dl_costs.cpp
dl_rule.cpp
dl_rule_set.cpp
dl_rule_subsumption_index.cpp
dl_rule_transformer.cpp
dl_util.cpp
hnf.cpp
proof_utils.cpp
rule_properties.cpp
COMPONENT_DEPENDENCIES
aig_tactic
qe
sat
smt
smt2parser
PYG_FILES
fixedpoint_params.pyg
)

3
src/muz/base/dl_rule.cpp
View file

@ -784,7 +784,7 @@ namespace datalog {
SASSERT(tail.size()==tail_neg.size());
rule_ref old_r = r;
r = mk(head, tail.size(), tail.c_ptr(), tail_neg.c_ptr());
r = mk(head, tail.size(), tail.c_ptr(), tail_neg.c_ptr(), old_r->name());
r->set_accounting_parent_object(m_ctx, old_r);
}
@ -1003,6 +1003,7 @@ namespace datalog {
void rule::display(context & ctx, std::ostream & out) const {
ast_manager & m = ctx.get_manager();
out << m_name.str () << ":\n";
//out << mk_pp(m_head, m);
output_predicate(ctx, m_head, out);
if (m_tail_size == 0) {

9
src/muz/base/dl_rule.h
View file

@ -298,7 +298,7 @@ namespace datalog {
static unsigned get_obj_size(unsigned n) { return sizeof(rule) + n * sizeof(app *); }
rule() : m_ref_cnt(0) {}
rule() : m_ref_cnt(0), m_name(symbol::null) {}
~rule() {}
void deallocate(ast_manager & m);
@ -355,7 +355,12 @@ namespace datalog {
void display(context & ctx, std::ostream & out) const;
symbol const& name() const { return m_name; }
/**
\brief Return the name(s) associated with this rule. Plural for preprocessed (e.g. obtained by inlining) rules.
This possibly returns a ";"-separated list of names.
*/
symbol const& name() const { return m_name; } ;
unsigned hash() const;

2
src/muz/base/dl_rule_set.cpp
View file

@ -668,7 +668,7 @@ namespace datalog {
T * el = it->m_key;
item_set * out_edges = it->m_value;
unsigned el_comp;
unsigned el_comp = 0;
VERIFY( m_component_nums.find(el, el_comp) );
item_set::iterator eit = out_edges->begin();

3
src/muz/base/rule_properties.cpp
View file

@ -51,7 +51,8 @@ void rule_properties::collect(rule_set const& rules) {
for (unsigned i = 0; m_inf_sort.empty() && i < r->get_decl()->get_arity(); ++i) {
sort* d = r->get_decl()->get_domain(i);
sort_size sz = d->get_num_elements();
if (!sz.is_finite()) {
if (!sz.is_finite() && !m_dl.is_rule_sort(d)) {
TRACE("dl", tout << "sort " << mk_pp(d, m) << " is not finite " << sz << "\n";);
m_inf_sort.push_back(m_rule);
}
}

7
src/muz/bmc/CMakeLists.txt Normal file
View file

@ -0,0 +1,7 @@
z3_add_component(bmc
SOURCES
dl_bmc_engine.cpp
COMPONENT_DEPENDENCIES
muz
transforms
)

4
src/muz/bmc/dl_bmc_engine.cpp
View file

@ -979,7 +979,7 @@ namespace datalog {
sort_ref_vector new_sorts(m);
family_id dfid = m.mk_family_id("datatype");
datatype_decl_plugin* dtp = static_cast<datatype_decl_plugin*>(m.get_plugin(dfid));
VERIFY (dtp->mk_datatypes(dts.size(), dts.c_ptr(), new_sorts));
VERIFY (dtp->mk_datatypes(dts.size(), dts.c_ptr(), 0, 0, new_sorts));
it = b.m_rules.begin_grouped_rules();
for (unsigned i = 0; it != end; ++it, ++i) {
@ -1021,7 +1021,7 @@ namespace datalog {
cnstrs.push_back(mk_constructor_decl(name, is_name, accs.size(), accs.c_ptr()));
}
dts.push_back(mk_datatype_decl(symbol("Path"), cnstrs.size(), cnstrs.c_ptr()));
VERIFY (dtp->mk_datatypes(dts.size(), dts.c_ptr(), new_sorts));
VERIFY (dtp->mk_datatypes(dts.size(), dts.c_ptr(), 0, 0, new_sorts));
m_path_sort = new_sorts[0].get();
}
}

7
src/muz/clp/CMakeLists.txt Normal file
View file

@ -0,0 +1,7 @@
z3_add_component(clp
SOURCES
clp_context.cpp
COMPONENT_DEPENDENCIES
muz
transforms
)

6
src/muz/dataflow/CMakeLists.txt Normal file
View file

@ -0,0 +1,6 @@
z3_add_component(dataflow
SOURCES
dataflow.cpp
COMPONENT_DEPENDENCIES
muz
)

8
src/muz/ddnf/CMakeLists.txt Normal file
View file

@ -0,0 +1,8 @@
z3_add_component(ddnf
SOURCES
ddnf.cpp
COMPONENT_DEPENDENCIES
muz
rel
transforms
)

8
src/muz/duality/CMakeLists.txt Normal file
View file

@ -0,0 +1,8 @@
z3_add_component(duality_intf
SOURCES
duality_dl_interface.cpp
COMPONENT_DEPENDENCIES
duality
muz
transforms
)

18
src/muz/fp/CMakeLists.txt Normal file
View file

@ -0,0 +1,18 @@
z3_add_component(fp
SOURCES
datalog_parser.cpp
dl_cmds.cpp
dl_register_engine.cpp
horn_tactic.cpp
COMPONENT_DEPENDENCIES
bmc
clp
ddnf
duality_intf
muz
pdr
rel
tab
TACTIC_HEADERS
horn_tactic.h
)

15
src/muz/fp/dl_cmds.cpp
View file

@ -374,12 +374,9 @@ class dl_declare_rel_cmd : public cmd {
unsigned m_arg_idx;
mutable unsigned m_query_arg_idx;
symbol m_rel_name;
scoped_ptr<sort_ref_vector> m_domain;
ptr_vector<sort> m_domain;
svector<symbol> m_kinds;
void ensure_domain(cmd_context& ctx) {
if (!m_domain) m_domain = alloc(sort_ref_vector, ctx.m());
}
public:
dl_declare_rel_cmd(dl_context * dl_ctx):
@ -395,7 +392,7 @@ public:
ctx.m(); // ensure manager is initialized.
m_arg_idx = 0;
m_query_arg_idx = 0;
m_domain = 0;
m_domain.reset();
m_kinds.reset();
}
virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const {
@ -406,8 +403,8 @@ public:
}
}
virtual void set_next_arg(cmd_context & ctx, unsigned num, sort * const * slist) {
ensure_domain(ctx);
m_domain->append(num, slist);
m_domain.reset();
m_domain.append(num, slist);
m_arg_idx++;
}
virtual void set_next_arg(cmd_context & ctx, symbol const & s) {
@ -424,14 +421,12 @@ public:
if(m_arg_idx<2) {
throw cmd_exception("at least 2 arguments expected");
}
ensure_domain(ctx);
ast_manager& m = ctx.m();
func_decl_ref pred(
m.mk_func_decl(m_rel_name, m_domain->size(), m_domain->c_ptr(), m.mk_bool_sort()), m);
m.mk_func_decl(m_rel_name, m_domain.size(), m_domain.c_ptr(), m.mk_bool_sort()), m);
ctx.insert(pred);
m_dl_ctx->register_predicate(pred, m_kinds.size(), m_kinds.c_ptr());
m_domain = 0;
}
};

20
src/muz/pdr/CMakeLists.txt Normal file
View file

@ -0,0 +1,20 @@
z3_add_component(pdr
SOURCES
pdr_closure.cpp
pdr_context.cpp
pdr_dl_interface.cpp
pdr_farkas_learner.cpp
pdr_generalizers.cpp
pdr_manager.cpp
pdr_prop_solver.cpp
pdr_reachable_cache.cpp
pdr_smt_context_manager.cpp
pdr_sym_mux.cpp
pdr_util.cpp
COMPONENT_DEPENDENCIES
arith_tactics
core_tactics
muz
smt_tactic
transforms
)

31
src/muz/rel/CMakeLists.txt Normal file
View file

@ -0,0 +1,31 @@
z3_add_component(rel
SOURCES
aig_exporter.cpp
check_relation.cpp
dl_base.cpp
dl_bound_relation.cpp
dl_check_table.cpp
dl_compiler.cpp
dl_external_relation.cpp
dl_finite_product_relation.cpp
dl_instruction.cpp
dl_interval_relation.cpp
dl_lazy_table.cpp
dl_mk_explanations.cpp
dl_mk_similarity_compressor.cpp
dl_mk_simple_joins.cpp
dl_product_relation.cpp
dl_relation_manager.cpp
dl_sieve_relation.cpp
dl_sparse_table.cpp
dl_table.cpp
dl_table_relation.cpp
doc.cpp
karr_relation.cpp
rel_context.cpp
tbv.cpp
udoc_relation.cpp
COMPONENT_DEPENDENCIES
muz
transforms
)

2
src/muz/rel/dl_mk_similarity_compressor.cpp
View file

@ -426,7 +426,7 @@ namespace datalog {
new_negs.push_back(false);
rule * new_rule = m_context.get_rule_manager().mk(new_head, new_tail.size(), new_tail.c_ptr(),
new_negs.c_ptr());
new_negs.c_ptr(), r->name());
m_result_rules.push_back(new_rule);
//TODO: allow for a rule to have multiple parent objects

2
src/muz/rel/dl_mk_simple_joins.cpp
View file

@ -726,7 +726,7 @@ namespace datalog {
}
rule * new_rule = m_context.get_rule_manager().mk(orig_r->get_head(), tail.size(), tail.c_ptr(),
negs.c_ptr());
negs.c_ptr(), orig_r->name());
new_rule->set_accounting_parent_object(m_context, orig_r);
m_context.get_rule_manager().mk_rule_rewrite_proof(*orig_r, *new_rule);

52
src/muz/rel/dl_relation_manager.cpp
View file

@ -36,13 +36,10 @@ namespace datalog {
void relation_manager::reset_relations() {
relation_map::iterator it=m_relations.begin();
relation_map::iterator end=m_relations.end();
for(;it!=end;++it) {
func_decl * pred = it->m_key;
for (auto const& kv : m_relations) {
func_decl * pred = kv.m_key;
get_context().get_manager().dec_ref(pred); //inc_ref in get_relation
relation_base * r=(*it).m_value;
r->deallocate();
kv.m_value->deallocate();
}
m_relations.reset();
}
@ -119,35 +116,25 @@ namespace datalog {
}
void relation_manager::collect_non_empty_predicates(decl_set & res) const {
relation_map::iterator it = m_relations.begin();
relation_map::iterator end = m_relations.end();
for(; it!=end; ++it) {
if(!it->m_value->fast_empty()) {
res.insert(it->m_key);
for (auto const& kv : m_relations) {
if (!kv.m_value->fast_empty()) {
res.insert(kv.m_key);
}
}
}
void relation_manager::restrict_predicates(const decl_set & preds) {
typedef ptr_vector<func_decl> fd_vector;
fd_vector to_remove;
ptr_vector<func_decl> to_remove;
relation_map::iterator rit = m_relations.begin();
relation_map::iterator rend = m_relations.end();
for(; rit!=rend; ++rit) {
func_decl * pred = rit->m_key;
for (auto const& kv : m_relations) {
func_decl* pred = kv.m_key;
if (!preds.contains(pred)) {
to_remove.insert(pred);
}
}
fd_vector::iterator pit = to_remove.begin();
fd_vector::iterator pend = to_remove.end();
for(; pit!=pend; ++pit) {
func_decl * pred = *pit;
relation_base * rel;
VERIFY( m_relations.find(pred, rel) );
rel->deallocate();
for (func_decl* pred : to_remove) {
m_relations.find(pred)->deallocate();
m_relations.remove(pred);
get_context().get_manager().dec_ref(pred);
}
@ -283,18 +270,16 @@ namespace datalog {
}
table_plugin * relation_manager::get_table_plugin(symbol const& k) {
table_plugin_vector::iterator tpit = m_table_plugins.begin();
table_plugin_vector::iterator tpend = m_table_plugins.end();
for(; tpit!=tpend; ++tpit) {
if((*tpit)->get_name()==k) {
return *tpit;
for (table_plugin * tp : m_table_plugins) {
if (tp->get_name()==k) {
return tp;
}
}
return 0;
}
table_relation_plugin & relation_manager::get_table_relation_plugin(table_plugin & tp) {
table_relation_plugin * res;
table_relation_plugin * res = 0;
VERIFY( m_table_relation_plugins.find(&tp, res) );
return *res;
}
@ -341,10 +326,9 @@ namespace datalog {
return res;
}
for (unsigned i = 0; i < m_relation_plugins.size(); ++i) {
p = m_relation_plugins[i];
if (p->can_handle_signature(s)) {
return p->mk_empty(s);
for (relation_plugin* p1 : m_relation_plugins) {
if (p1->can_handle_signature(s)) {
return p1->mk_empty(s);
}
}

7
src/muz/tab/CMakeLists.txt Normal file
View file

@ -0,0 +1,7 @@
z3_add_component(tab
SOURCES
tab_context.cpp
COMPONENT_DEPENDENCIES
muz
transforms
)

28
src/muz/transforms/CMakeLists.txt Normal file
View file

@ -0,0 +1,28 @@
z3_add_component(transforms
SOURCES
dl_mk_array_blast.cpp
dl_mk_backwards.cpp
dl_mk_bit_blast.cpp
dl_mk_coalesce.cpp
dl_mk_coi_filter.cpp
dl_mk_filter_rules.cpp
dl_mk_interp_tail_simplifier.cpp
dl_mk_karr_invariants.cpp
dl_mk_loop_counter.cpp
dl_mk_magic_sets.cpp
dl_mk_magic_symbolic.cpp
dl_mk_quantifier_abstraction.cpp
dl_mk_quantifier_instantiation.cpp
dl_mk_rule_inliner.cpp
dl_mk_scale.cpp
dl_mk_separate_negated_tails.cpp
dl_mk_slice.cpp
dl_mk_subsumption_checker.cpp
dl_mk_unbound_compressor.cpp
dl_mk_unfold.cpp
dl_transforms.cpp
COMPONENT_DEPENDENCIES
dataflow
hilbert
muz
)

2
src/muz/transforms/dl_mk_filter_rules.cpp
View file

@ -140,7 +140,7 @@ namespace datalog {
if (rule_modified) {
remove_duplicate_tails(new_tail, new_is_negated);
SASSERT(new_tail.size() == new_is_negated.size());
rule * new_rule = m_context.get_rule_manager().mk(new_head, new_tail.size(), new_tail.c_ptr(), new_is_negated.c_ptr());
rule * new_rule = m_context.get_rule_manager().mk(new_head, new_tail.size(), new_tail.c_ptr(), new_is_negated.c_ptr(), r->name());
new_rule->set_accounting_parent_object(m_context, m_current);
m_result->add_rule(new_rule);
m_context.get_rule_manager().mk_rule_rewrite_proof(*r, *new_rule);

17
src/muz/transforms/dl_mk_interp_tail_simplifier.cpp
View file

@ -84,7 +84,7 @@ namespace datalog {
mk_rule_inliner::remove_duplicate_tails(m_tail, m_neg);
SASSERT(m_tail.size() == m_neg.size());
res = m_context.get_rule_manager().mk(m_head, m_tail.size(), m_tail.c_ptr(), m_neg.c_ptr());
res = m_context.get_rule_manager().mk(m_head, m_tail.size(), m_tail.c_ptr(), m_neg.c_ptr(),m_rule->name());
res->set_accounting_parent_object(m_context, m_rule);
res->norm_vars(res.get_manager());
}
@ -250,7 +250,7 @@ namespace datalog {
bool detect_equivalences(expr_ref_vector& v, bool inside_disjunction)
{
bool have_pair = false;
unsigned prev_pair_idx;
unsigned prev_pair_idx = 0;
arg_pair ap;
unsigned read_idx = 0;
@ -296,21 +296,20 @@ namespace datalog {
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result,
proof_ref & result_pr)
{
if (m.is_not(f) && (m.is_and(args[0]) || m.is_or(args[0]))) {
SASSERT(num==1);
SASSERT(num == 1);
expr_ref tmp(m);
app* a = to_app(args[0]);
m_app_args.reset();
for (unsigned i = 0; i < a->get_num_args(); ++i) {
m_brwr.mk_not(a->get_arg(i), tmp);
for (expr* arg : *a) {
m_brwr.mk_not(arg, tmp);
m_app_args.push_back(tmp);
}
if (m.is_and(args[0])) {
result = m.mk_or(m_app_args.size(), m_app_args.c_ptr());
result = mk_or(m_app_args);
}
else {
result = m.mk_and(m_app_args.size(), m_app_args.c_ptr());
result = mk_and(m_app_args);
}
return BR_REWRITE2;
}
@ -557,7 +556,7 @@ namespace datalog {
}
SASSERT(m_tail.size() == m_tail_neg.size());
res = m_context.get_rule_manager().mk(head, m_tail.size(), m_tail.c_ptr(), m_tail_neg.c_ptr());
res = m_context.get_rule_manager().mk(head, m_tail.size(), m_tail.c_ptr(), m_tail_neg.c_ptr(), r->name());
res->set_accounting_parent_object(m_context, r);
}
else {

2
src/muz/transforms/dl_mk_magic_sets.cpp
View file

@ -280,7 +280,7 @@ namespace datalog {
new_tail.push_back(create_magic_literal(new_head));
negations.push_back(false);
rule * nr = m_context.get_rule_manager().mk(new_head, new_tail.size(), new_tail.c_ptr(), negations.c_ptr());
rule * nr = m_context.get_rule_manager().mk(new_head, new_tail.size(), new_tail.c_ptr(), negations.c_ptr(), r->name());
result.add_rule(nr);
nr->set_accounting_parent_object(m_context, r);
}

5
src/muz/transforms/dl_mk_quantifier_abstraction.cpp
View file

@ -142,7 +142,8 @@ namespace datalog {
m(ctx.get_manager()),
m_ctx(ctx),
a(m),
m_refs(m) {
m_refs(m),
m_mc(NULL){
}
mk_quantifier_abstraction::~mk_quantifier_abstraction() {
@ -341,7 +342,7 @@ namespace datalog {
head = mk_head(source, *result, r.get_head(), cnt);
fml = m.mk_implies(m.mk_and(tail.size(), tail.c_ptr()), head);
proof_ref pr(m);
rm.mk_rule(fml, pr, *result);
rm.mk_rule(fml, pr, *result, r.name());
TRACE("dl", result->last()->display(m_ctx, tout););
}

2
src/muz/transforms/dl_mk_quantifier_instantiation.cpp
View file

@ -232,7 +232,7 @@ namespace datalog {
rule_set added_rules(m_ctx);
proof_ref pr(m);
rm.mk_rule(fml, pr, added_rules);
rm.mk_rule(fml, pr, added_rules, r.name());
if (r.get_proof()) {
// use def-axiom to encode that new rule is a weakening of the original.
proof* p1 = r.get_proof();

Some files were not shown because too many files have changed in this diff Show more