3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-18 22:59:02 +00:00
z3/src/util
Nikolaj Bjorner 4d8860c0bc wip - adding context equation solver
the solve_eqs_tactic is to be replaced by a re-implementation that uses solve_eqs in the simplifiers directory.
The re-implementation should address efficiency issues with the previous code.
At this point it punts on low level proofs. The plan is to use coarser
dependency tracking instead of low level proofs for pre-processing. Dependencies can be converted into a proof hint representation that can be checked using a stronger checker.
2022-11-05 10:34:57 -07:00
..
approx_nat.cpp make include paths uniformly use path relative to src. #534 2017-07-31 13:24:11 -07:00
approx_nat.h remove '#include <iostream>' from headers and from unneeded places 2022-06-17 14:10:19 +01:00
approx_set.cpp make include paths uniformly use path relative to src. #534 2017-07-31 13:24:11 -07:00
approx_set.h remove '#include <iostream>' from headers and from unneeded places 2022-06-17 14:10:19 +01:00
array.h Use = delete to delete special methods. 2022-08-02 09:23:14 +03:00
array_map.h remove unneeded constructors (last round) 2020-07-12 17:41:57 +01:00
backtrackable_set.h booyah 2020-07-04 15:56:30 -07:00
basic_interval.h remove a hundred implicit constructors/destructors 2021-05-23 14:25:01 +01:00
bit_util.cpp Fix some spelling errors (mostly in comments). 2018-10-20 17:07:41 +02:00
bit_util.h booyah 2020-07-04 15:56:30 -07:00
bit_vector.cpp fix #1762, #1764, #1768 2018-07-26 20:29:26 +01:00
bit_vector.h add rec decl/def to ML #4563 2020-07-04 15:38:32 -07:00
buffer.h typo 2021-05-23 14:28:42 +01:00
cancel_eh.h booyah 2020-07-04 15:56:30 -07:00
chashtable.h booyah 2020-07-04 15:56:30 -07:00
checked_int64.h buffer: require a move constructor to avoid copies 2020-06-03 11:57:49 +01:00
CMakeLists.txt Move tbv to util 2022-08-01 18:37:11 +03:00
cmd_context_types.cpp remove '#include <iostream>' from headers and from unneeded places 2022-06-17 14:10:19 +01:00
cmd_context_types.h Use = default for virtual constructors. 2022-08-05 18:11:46 +03:00
common_msgs.cpp make include paths uniformly use path relative to src. #534 2017-07-31 13:24:11 -07:00
common_msgs.h booyah 2020-07-04 15:56:30 -07:00
container_util.h call it data instead of c_ptr for approaching C++11 std::vector convention. 2021-04-13 18:17:35 -07:00
debug.cpp replace remaining volatiles with atomic<> 2020-10-24 11:47:45 +01:00
debug.h Add SASSERT_EQ and VERIFY_EQ 2022-08-01 18:37:11 +03:00
dec_ref_util.h booyah 2020-07-04 15:56:30 -07:00
dependency.h booyah 2020-07-04 15:56:30 -07:00
dictionary.h remove a hundred implicit constructors/destructors 2021-05-23 14:25:01 +01:00
dlist.h dlist::insert_before/after 2022-08-01 18:37:11 +03:00
double_manager.h booyah 2020-07-04 15:56:30 -07:00
ema.h booyah 2020-07-04 15:56:30 -07:00
env_params.cpp redo #6242 2022-08-08 11:26:18 +03:00
env_params.h booyah 2020-07-04 15:56:30 -07:00
error_codes.h booyah 2020-07-04 15:56:30 -07:00
event_handler.h Use = default for virtual constructors. 2022-08-05 18:11:46 +03:00
ext_gcd.h booyah 2020-07-04 15:56:30 -07:00
ext_numeral.h remove '#include <iostream>' from headers and from unneeded places 2022-06-17 14:10:19 +01:00
f2n.h booyah 2020-07-04 15:56:30 -07:00
file_path.h booyah 2020-07-04 15:56:30 -07:00
fixed_bit_vector.cpp clear memory on allocation to avoid msan warnings 2019-11-29 15:50:49 -08:00
fixed_bit_vector.h booyah 2020-07-04 15:56:30 -07:00
gparams.cpp include global parameters and fixup for HTML meta-characters 2022-08-22 14:25:18 -07:00
gparams.h add parameter descriptions 2022-08-16 08:26:53 -07:00
hash.cpp make include paths uniformly use path relative to src. #534 2017-07-31 13:24:11 -07:00
hash.h call it data instead of c_ptr for approaching C++11 std::vector convention. 2021-04-13 18:17:35 -07:00
hashtable.h remove a hundred implicit constructors/destructors 2021-05-23 14:25:01 +01:00
heap.h prepare for std::vector 2021-04-20 09:24:24 -07:00
hwf.cpp Remove remainder workaround for pre-MSVC2013. (#6204) 2022-07-29 11:50:31 +02:00
hwf.h remove unneeded constructors (last round) 2020-07-12 17:41:57 +01:00
id_gen.h booyah 2020-07-04 15:56:30 -07:00
id_var_list.h na 2020-09-01 07:15:13 -07:00
inf_eps_rational.h remove unneeded constructors (last round) 2020-07-12 17:41:57 +01:00
inf_int_rational.cpp make include paths uniformly use path relative to src. #534 2017-07-31 13:24:11 -07:00
inf_int_rational.h remove unneeded constructors (last round) 2020-07-12 17:41:57 +01:00
inf_rational.cpp make include paths uniformly use path relative to src. #534 2017-07-31 13:24:11 -07:00
inf_rational.h remove unneeded constructors (last round) 2020-07-12 17:41:57 +01:00
inf_s_integer.cpp make include paths uniformly use path relative to src. #534 2017-07-31 13:24:11 -07:00
inf_s_integer.h remove a few more copy constructors, though still not enough to enable the assertion in vector 2020-06-03 20:32:13 +01:00
lbool.cpp make include paths uniformly use path relative to src. #534 2017-07-31 13:24:11 -07:00
lbool.h booyah 2020-07-04 15:56:30 -07:00
lim_vector.h remove a hundred implicit constructors/destructors 2021-05-23 14:25:01 +01:00
list.h booyah 2020-07-04 15:56:30 -07:00
luby.cpp
luby.h booyah 2020-07-04 15:56:30 -07:00
machine.h booyah 2020-07-04 15:56:30 -07:00
map.h booyah 2020-07-04 15:56:30 -07:00
max_cliques.h Make sure all headers do #pragma once. (#6188) 2022-07-23 10:41:14 -07:00
memory_manager.cpp memory_manager: add support for MacOS & Windows to the new size tracking system 2022-10-24 10:09:56 +01:00
memory_manager.h cleanup thread pool of scoped_timer on memory finalize 2020-10-24 12:46:50 +01:00
min_cut.cpp remove ast.h reference 2017-10-25 09:49:53 -07:00
min_cut.h booyah 2020-07-04 15:56:30 -07:00
mpbq.cpp patch for Sturm sequence bug #4961 2021-01-24 12:58:25 -08:00
mpbq.h patch for Sturm sequence bug #4961 2021-01-24 12:58:25 -08:00
mpbqi.h booyah 2020-07-04 15:56:30 -07:00
mpf.cpp fix compiler warnings 2022-10-12 09:43:50 +01:00
mpf.h fix compiler warnings 2022-10-12 09:43:50 +01:00
mpff.cpp fix compiler warnings 2022-10-12 09:43:50 +01:00
mpff.h prepare for std::vector 2021-04-20 09:24:24 -07:00
mpfx.cpp prepare for std::vector 2021-04-20 09:24:24 -07:00
mpfx.h prepare for std::vector 2021-04-20 09:24:24 -07:00
mpn.cpp wip - adding context equation solver 2022-11-05 10:34:57 -07:00
mpn.h fix compiler warnings 2022-10-12 09:43:50 +01:00
mpq.cpp minor code simplifications 2022-08-20 12:56:45 +01:00
mpq.h delete dead code 2022-10-02 21:44:08 +01:00
mpq_inf.cpp remove remaining _NO_OMP_ 2019-06-05 10:07:16 +01:00
mpq_inf.h fix build 2020-07-05 11:44:12 +01:00
mpz.cpp fix compiler warnings 2022-10-12 09:43:50 +01:00
mpz.h Remove remnants of _MP_MSBIGNUM checks. 2022-08-02 09:28:57 +03:00
mpzzp.h booyah 2020-07-04 15:56:30 -07:00
mutex.h logging cleanup 2021-08-29 12:24:19 +01:00
nat_set.h working on mam 2021-01-25 17:54:53 -08:00
numeral_buffer.h call it data instead of c_ptr for approaching C++11 std::vector convention. 2021-04-13 18:17:35 -07:00
obj_hashtable.h remove a hundred implicit constructors/destructors 2021-05-23 14:25:01 +01:00
obj_mark.h booyah 2020-07-04 15:56:30 -07:00
obj_pair_hashtable.h remove a hundred implicit constructors/destructors 2021-05-23 14:25:01 +01:00
obj_pair_set.h remove a hundred implicit constructors/destructors 2021-05-23 14:25:01 +01:00
obj_ref.h remove unneeded constructors (last round) 2020-07-12 17:41:57 +01:00
obj_ref_hashtable.h booyah 2020-07-04 15:56:30 -07:00
obj_triple_hashtable.h remove a hundred implicit constructors/destructors 2021-05-23 14:25:01 +01:00
object_allocator.h booyah 2020-07-04 15:56:30 -07:00
optional.h remove unneeded constructors (last round) 2020-07-12 17:41:57 +01:00
page.cpp merge with Z3Prover/master 2018-06-25 19:44:46 +08:00
page.h booyah 2020-07-04 15:56:30 -07:00
params.cpp include global parameters and fixup for HTML meta-characters 2022-08-22 14:25:18 -07:00
params.h add parameter descriptions 2022-08-16 08:26:53 -07:00
parray.h remove dependency on pragma 2022-07-19 09:36:22 -07:00
permutation.cpp make include paths uniformly use path relative to src. #534 2017-07-31 13:24:11 -07:00
permutation.h remove '#include <iostream>' from headers and from unneeded places 2022-06-17 14:10:19 +01:00
plugin_manager.h booyah 2020-07-04 15:56:30 -07:00
pool.h booyah 2020-07-04 15:56:30 -07:00
prime_generator.cpp fix mutexes hanging due to access to free'd memory 2019-09-03 20:02:21 +01:00
prime_generator.h booyah 2020-07-04 15:56:30 -07:00
ptr_scoped_buffer.h booyah 2020-07-04 15:56:30 -07:00
queue.h booyah 2020-07-04 15:56:30 -07:00
rational.cpp numeral helper functions 2022-08-01 18:37:11 +03:00
rational.h minor code simplifications 2022-08-20 12:56:45 +01:00
ref.h ref/ref_vector minor convenience changes (#5322) 2021-05-31 10:27:46 -07:00
ref_buffer.h call it data instead of c_ptr for approaching C++11 std::vector convention. 2021-04-13 18:17:35 -07:00
ref_pair_vector.h call it data instead of c_ptr for approaching C++11 std::vector convention. 2021-04-13 18:17:35 -07:00
ref_util.h booyah 2020-07-04 15:56:30 -07:00
ref_vector.h ref/ref_vector minor convenience changes (#5322) 2021-05-31 10:27:46 -07:00
region.cpp mbqi 2020-10-26 11:06:40 -07:00
region.h remove '#include <iostream>' from headers and from unneeded places 2022-06-17 14:10:19 +01:00
rlimit.cpp fix rlimit for clang-10 (#4658) 2020-08-21 10:34:10 -07:00
rlimit.h replace remaining volatiles with atomic<> 2020-10-24 11:47:45 +01:00
s_integer.cpp merge with Z3Prover/master 2018-06-25 19:44:46 +08:00
s_integer.h remove unneeded constructors (last round) 2020-07-12 17:41:57 +01:00
sat_literal.h don't rename uint_set but keep the original name 2022-09-18 17:22:59 -07:00
scoped_ctrl_c.cpp remove '#include <iostream>' from headers and from unneeded places 2022-06-17 14:10:19 +01:00
scoped_ctrl_c.h booyah 2020-07-04 15:56:30 -07:00
scoped_limit_trail.h add variable replay, remove MacOS from Travis (#4681) 2020-09-08 05:57:07 -07:00
scoped_numeral.h numeral helper functions 2022-08-01 18:37:11 +03:00
scoped_numeral_buffer.h Use = delete to delete special methods. 2022-08-02 09:23:14 +03:00
scoped_numeral_vector.h prepare for std::vector 2021-04-20 09:24:24 -07:00
scoped_ptr_vector.h scoped_ptr_vector usability 2022-08-01 18:37:11 +03:00
scoped_timer.cpp fix for spurious wakeups in scoped_timer (#6102) 2022-06-22 10:50:19 +01:00
scoped_timer.h fix for spurious wakeups in scoped_timer (#6102) 2022-06-22 10:50:19 +01:00
scoped_vector.h simplify some constructors/destructors 2021-05-23 12:39:49 +01:00
sexpr.cpp #5445 2021-08-03 11:17:23 -07:00
sexpr.h arrays (#4684) 2020-09-13 19:29:59 -07:00
sign.h move out sign 2020-01-20 16:22:38 -06:00
small_object_allocator.cpp fix debug build 2022-06-17 14:35:33 +01:00
small_object_allocator.h support threading for TRACE mode 2021-10-25 13:35:32 +02:00
smt2_util.cpp merge with Z3Prover/master 2018-06-25 19:44:46 +08:00
smt2_util.h booyah 2020-07-04 15:56:30 -07:00
sorting_network.h call it data instead of c_ptr for approaching C++11 std::vector convention. 2021-04-13 18:17:35 -07:00
sstream.h merge with Z3Prover/master 2018-06-25 19:44:46 +08:00
stack.cpp merge with Z3Prover/master 2018-06-25 19:44:46 +08:00
stack.h booyah 2020-07-04 15:56:30 -07:00
stacked_value.h update pretty printer for recursive function filtering 2022-05-15 11:59:41 -07:00
state_graph.cpp State graph dgml update and fixes in condition simplifier (#5721) 2021-12-19 11:09:55 -08:00
state_graph.h fixing issue #4651 (#4666) 2020-09-08 04:13:18 -07:00
statistics.cpp call it data instead of c_ptr for approaching C++11 std::vector convention. 2021-04-13 18:17:35 -07:00
statistics.h remove '#include <iostream>' from headers and from unneeded places 2022-06-17 14:10:19 +01:00
stats.h booyah 2020-07-04 15:56:30 -07:00
stopwatch.h remove '#include <iostream>' from headers and from unneeded places 2022-06-17 14:10:19 +01:00
str_hashtable.h booyah 2020-07-04 15:56:30 -07:00
stream_buffer.h remove '#include <iostream>' from headers and from unneeded places 2022-06-17 14:10:19 +01:00
string_buffer.h fix a couple hundred deref-after-free bugs due to .c_str() on a temporary string 2020-07-11 20:24:45 +01:00
symbol.cpp optimize symbol table for single-threaded mode 2021-05-23 16:35:44 +01:00
symbol.h add stub for finalize 2020-10-22 11:07:05 -07:00
symbol_table.h booyah 2020-07-04 15:56:30 -07:00
tbv.cpp Move tbv to util 2022-08-01 18:37:11 +03:00
tbv.h Move tbv to util 2022-08-01 18:37:11 +03:00
timeit.cpp remove '#include <iostream>' from headers and from unneeded places 2022-06-17 14:10:19 +01:00
timeit.h remove '#include <iostream>' from headers and from unneeded places 2022-06-17 14:10:19 +01:00
timeout.cpp fix #4763: shell not finishing before hard timeout 2020-10-30 10:01:09 +00:00
timeout.h fix #4763: shell not finishing before hard timeout 2020-10-30 10:01:09 +00:00
timer.h booyah 2020-07-04 15:56:30 -07:00
top_sort.h fix regression in top-sort fix #6060 2022-06-14 09:51:06 -07:00
total_order.h booyah 2020-07-04 15:56:30 -07:00
tptr.h booyah 2020-07-04 15:56:30 -07:00
trace.cpp support threading for TRACE mode 2021-10-25 13:35:32 +02:00
trace.h support threading for TRACE mode 2021-10-25 13:35:32 +02:00
trail.h Use = default for virtual constructors. 2022-08-05 18:11:46 +03:00
uint_map.h booyah 2020-07-04 15:56:30 -07:00
uint_set.h union_find::reserve 2022-08-01 18:37:11 +03:00
union_find.h union_find::reserve 2022-08-01 18:37:11 +03:00
util.cpp remove '#include <iostream>' from headers and from unneeded places 2022-06-17 14:10:19 +01:00
util.h wip - adding context equation solver 2022-11-05 10:34:57 -07:00
var_queue.h var_queue display 2022-08-01 18:37:11 +03:00
vector.h import goodies from ps 2021-09-21 11:13:03 -07:00
visit_helper.h make visited_helper independent of literals 2022-11-03 03:54:39 -07:00
warning.cpp add redirect for warnings 2022-08-23 15:55:55 -07:00
warning.h add redirect for warnings 2022-08-23 15:55:55 -07:00
z3_exception.cpp Improve UX for unreachable/unimplemented errors (#4094) 2020-04-28 19:54:31 -07:00
z3_exception.h Use = default for virtual constructors. 2022-08-05 18:11:46 +03:00
z3_version.h.cmake.in rename version.h to z3_version.h to differentiate name in install include directory. Add support for z3_version.h in python build system. #1833 2018-09-21 20:13:58 -07:00
z3_version.h.in rename version.h to z3_version.h to differentiate name in install include directory. Add support for z3_version.h in python build system. #1833 2018-09-21 20:13:58 -07:00
zstring.cpp fir #5856 2022-02-20 15:32:41 +02:00
zstring.h expose propagate created 2021-12-17 16:12:47 -08:00