mirror of
https://github.com/Z3Prover/z3
synced 2025-08-20 18:20:22 +00:00
976e4c91b0
* std::cout debugging statements * comment out std::cout debugging as this is now a shared fork * convert std::cout to TRACE statements for seq_rewriter and seq_regex * add cases to min_length and max_length for regexes * bug fix * update min_length and max_length functions for REs * initial pass on simplifying derivative normal forms by eliminating redundant predicates locally * add seq_regex_brief trace statements * working on debugging ref count issue * fix ref count bug and convert trace statements to seq_regex_brief * add compact tracing for cache hits/misses * seq_regex fix cache hit/miss tracing and wrapper around is_nullable * minor * label and disable more experimental changes for testing * minor documentation / tracing * a few more @EXP annotations * dead state elimination skeleton code * progress on dead state elimination * more progress on dead state elimination * refactor dead state class to separate self-contained state_graph class * finish factoring state_graph to only work with unsigned values, and implement separate functionality for expr* logic * implement get_all_derivatives, add debug tracing * trace statements for debugging is_nullable loop bug * fix is_nullable loop bug * comment out local nullable change and mark experimental * pretty printing for state_graph * rewrite state graph to remove the fragile assumption that all edges from a state are added at a time * start of general cycle detection check + fix some comments * implement full cycle detection procedure * normalize derivative conditions to form 'ele <= a' * order derivative conditions by character code * fix confusing names m_to and m_from * assign increasing state IDs from 1 instead of using get_id on AST node * remove elim_condition call in get_dall_derivatives * use u_map instead of uint_map to avoid memory leak * remove unnecessary call to is_ground * debugging * small improvements to seq_regex_brief tracing * fix bug on evil2 example * save work * new propagate code * work in progress on using same seq sort for deriv calls * avoid re-computing derivatives: use same head var for every derivative call * use min_length on regexes to prune search * simple implementation of can_be_in_cycle using rank function idea * add a disabled experimental change * minor cleanup comments, etc. * seq_rewriter cleanup for PR * typo noticed by Nikolaj * move state graph to util/state_graph * re-add accidentally removed line * clean up seq_regex code removing obsolete functions and comments * a few more cleanup items * remove experimental functionality for integration * fix compilation * remove some tracing and TODOs * remove old comment * update copyright dates to 2020 * feedback from Nikolaj * use [] for map access * make state_graph methods constant * avoid recursion in mark_dead_recursive and mark_live_recursive * a possible bug fix in propagate_nonempty * write down list of invariants in state_graph * implement partial invariant check and insert CASSERT statements * expand on invariant check and tracing * finish state graph invariant check * minor tweaks * regex propagation: convert first two axioms to propagations * remove obsolete regex solver functionality Co-authored-by: calebstanford-msr <t-casta@microsoft.com>
74 lines
1.4 KiB
CMake
74 lines
1.4 KiB
CMake
if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/z3_version.h")
|
|
message(FATAL_ERROR "\"${CMAKE_CURRENT_SOURCE_DIR}/z3_version.h\""
|
|
${z3_polluted_tree_msg}
|
|
)
|
|
endif()
|
|
|
|
set(Z3_FULL_VERSION "\"${Z3_FULL_VERSION_STR}\"")
|
|
configure_file(z3_version.h.cmake.in ${CMAKE_CURRENT_BINARY_DIR}/z3_version.h)
|
|
|
|
|
|
z3_add_component(util
|
|
SOURCES
|
|
approx_nat.cpp
|
|
approx_set.cpp
|
|
bit_util.cpp
|
|
bit_vector.cpp
|
|
cmd_context_types.cpp
|
|
common_msgs.cpp
|
|
debug.cpp
|
|
env_params.cpp
|
|
fixed_bit_vector.cpp
|
|
gparams.cpp
|
|
hash.cpp
|
|
hwf.cpp
|
|
inf_int_rational.cpp
|
|
inf_rational.cpp
|
|
inf_s_integer.cpp
|
|
lbool.cpp
|
|
luby.cpp
|
|
memory_manager.cpp
|
|
min_cut.cpp
|
|
mpbq.cpp
|
|
mpf.cpp
|
|
mpff.cpp
|
|
mpfx.cpp
|
|
mpn.cpp
|
|
mpq.cpp
|
|
mpq_inf.cpp
|
|
mpz.cpp
|
|
page.cpp
|
|
params.cpp
|
|
permutation.cpp
|
|
prime_generator.cpp
|
|
rational.cpp
|
|
region.cpp
|
|
rlimit.cpp
|
|
scoped_ctrl_c.cpp
|
|
scoped_timer.cpp
|
|
sexpr.cpp
|
|
s_integer.cpp
|
|
small_object_allocator.cpp
|
|
smt2_util.cpp
|
|
stack.cpp
|
|
state_graph.cpp
|
|
statistics.cpp
|
|
symbol.cpp
|
|
timeit.cpp
|
|
timeout.cpp
|
|
trace.cpp
|
|
util.cpp
|
|
warning.cpp
|
|
z3_exception.cpp
|
|
EXTRA_REGISTER_MODULE_HEADERS
|
|
env_params.h
|
|
MEMORY_INIT_FINALIZER_HEADERS
|
|
debug.h
|
|
gparams.h
|
|
prime_generator.h
|
|
rational.h
|
|
rlimit.h
|
|
state_graph.h
|
|
symbol.h
|
|
trace.h
|
|
)
|