mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity
z3/src/smt
History
Nikolaj Bjorner 81ebd52f61 #7207 
the utility that computes case analysis is brittle when the body of a function contains ite expressions that are not relevant to recursive unfolding.
The fold-rec occurrences that get inserted to harness large case splits work against throttling case generation: they get treated as recursive functions that have to be guarded.
2024-06-16 15:04:42 -07:00
..
params enable logging nla lemmas 2024-04-25 10:29:34 -04:00
proto_model update model validate to include arithmetic 2023-08-03 15:51:29 -07:00
tactic fix bug in new core not detecting conflict, fix #6525, add tactic doc 2023-01-14 17:20:43 -05:00
arith_eq_adapter.cpp make destructors virtual 2023-08-20 15:30:57 -07:00
arith_eq_adapter.h booyah 2020-07-04 15:56:30 -07:00
arith_eq_solver.cpp call it data instead of c_ptr for approaching C++11 std::vector convention. 2021-04-13 18:17:35 -07:00
arith_eq_solver.h booyah 2020-07-04 15:56:30 -07:00
CMakeLists.txt rename files to theory_user_propagator 2021-11-29 19:44:58 -08:00
database.h Make sure all headers do #pragma once. (#6188) 2022-07-23 10:41:14 -07:00
database.smt Tabs, whitespace 2017-09-17 18:10:06 +01:00
diff_logic.h call it data instead of c_ptr for approaching C++11 std::vector convention. 2021-04-13 18:17:35 -07:00
dyn_ack.cpp Remove empty leaf destructors. (#6211) 2022-07-30 10:07:03 +01:00
dyn_ack.h arrays (#4684) 2020-09-13 19:29:59 -07:00
expr_context_simplifier.cpp call it data instead of c_ptr for approaching C++11 std::vector convention. 2021-04-13 18:17:35 -07:00
expr_context_simplifier.h booyah 2020-07-04 15:56:30 -07:00
fingerprints.cpp call it data instead of c_ptr for approaching C++11 std::vector convention. 2021-04-13 18:17:35 -07:00
fingerprints.h use assignment 2024-01-22 15:48:45 -08:00
mam.cpp Regressions reported by Guido 2023-12-01 13:32:13 -08:00
mam.h Use = default for virtual constructors. 2022-08-05 18:11:46 +03:00
old_interval.cpp Use noexcept more. (#7058) 2023-12-16 12:14:53 +00:00
old_interval.h Use noexcept more. (#7058) 2023-12-16 12:14:53 +00:00
qi_queue.cpp revert log addition 2023-07-07 09:29:38 -07:00
qi_queue.h add priority queue to instantiation 2021-01-31 16:17:52 -08:00
seq_axioms.cpp add options for logging learned lemmas and theory axioms 2022-08-08 11:18:56 +03:00
seq_axioms.h na 2022-01-01 17:59:31 -08:00
seq_eq_solver.cpp remove assertion - literals could be assigned but propagation incomplete 2022-01-21 03:10:41 +01:00
seq_ne_solver.cpp call it data instead of c_ptr for approaching C++11 std::vector convention. 2021-04-13 18:17:35 -07:00
seq_offset_eq.cpp streamline pb solver interface and naming after removal of xor 2021-02-28 12:32:04 -08:00
seq_offset_eq.h fix misspelled \brief for doxygen (#5632) 2021-10-29 15:34:28 +02:00
seq_regex.cpp remove dead code 2021-12-14 13:42:52 -08:00
seq_regex.h fix co-factoring' 2021-12-14 10:12:38 -08:00
smt2_extra_cmds.cpp merge with Z3Prover/master 2018-06-25 19:44:46 +08:00
smt2_extra_cmds.h booyah 2020-07-04 15:56:30 -07:00
smt_almost_cg_table.cpp streamline pb solver interface and naming after removal of xor 2021-02-28 12:32:04 -08:00
smt_almost_cg_table.h booyah 2020-07-04 15:56:30 -07:00
smt_arith_value.cpp streamline pb solver interface and naming after removal of xor 2021-02-28 12:32:04 -08:00
smt_arith_value.h enable ranges for bit-vectors 2020-08-13 10:53:37 -07:00
smt_b_justification.h remove unneeded constructors (last round) 2020-07-12 17:41:57 +01:00
smt_bool_var_data.h booyah 2020-07-04 15:56:30 -07:00
smt_case_split_queue.cpp extract multi-patterns when pattern can be decomposed 2023-03-31 12:45:51 -07:00
smt_case_split_queue.h Use = default for virtual constructors. 2022-08-05 18:11:46 +03:00
smt_cg_table.cpp streamline pb solver interface and naming after removal of xor 2021-02-28 12:32:04 -08:00
smt_cg_table.h booyah 2020-07-04 15:56:30 -07:00
smt_checker.cpp call it data instead of c_ptr for approaching C++11 std::vector convention. 2021-04-13 18:17:35 -07:00
smt_checker.h booyah 2020-07-04 15:56:30 -07:00
smt_clause.cpp consolidate literals 2021-05-20 12:58:27 -07:00
smt_clause.h Use = default for virtual constructors. 2022-08-05 18:11:46 +03:00
smt_clause_proof.cpp remove unused variables 2023-10-10 13:42:21 -07:00
smt_clause_proof.h merging master to unit_prop_on_monomials 2023-10-02 16:42:59 -07:00
smt_conflict_resolution.cpp minor code simplification 2023-10-11 01:38:03 +01:00
smt_conflict_resolution.h call it data instead of c_ptr for approaching C++11 std::vector convention. 2021-04-13 18:17:35 -07:00
smt_consequences.cpp fix #6956 2023-10-19 10:34:31 -07:00
smt_context.cpp fix #7107 2024-01-31 15:38:10 -08:00
smt_context.h expose enode pp convenciences 2023-11-18 09:53:20 -08:00
smt_context_inv.cpp more useful diagnostics 2021-09-01 20:50:35 -07:00
smt_context_pp.cpp fix assertion failure when printing stats 2024-05-18 16:30:26 +01:00
smt_context_stat.cpp remove '#include <iostream>' from headers and from unneeded places 2022-06-17 14:10:19 +01:00
smt_enode.cpp revert smt_enode 2023-12-20 14:03:27 -10:00
smt_enode.h revert smt_enode 2023-12-20 14:03:27 -10:00
smt_eq_justification.h booyah 2020-07-04 15:56:30 -07:00
smt_failure.h flag incomplete on lambdas #5803 2022-01-31 11:54:06 -08:00
smt_farkas_util.cpp call it data instead of c_ptr for approaching C++11 std::vector convention. 2021-04-13 18:17:35 -07:00
smt_farkas_util.h booyah 2020-07-04 15:56:30 -07:00
smt_for_each_relevant_expr.cpp make include paths uniformly use path relative to src. #534 2017-07-31 13:24:11 -07:00
smt_for_each_relevant_expr.h Use = default for virtual constructors. 2022-08-05 18:11:46 +03:00
smt_implied_equalities.cpp call it data instead of c_ptr for approaching C++11 std::vector convention. 2021-04-13 18:17:35 -07:00
smt_implied_equalities.h booyah 2020-07-04 15:56:30 -07:00
smt_induction.cpp.disabled remove dependencies on stale component 2021-08-16 17:52:36 -07:00
smt_induction.h.disabled remove dependencies on stale component 2021-08-16 17:52:36 -07:00
smt_internalizer.cpp Fix some typos. (#7115) 2024-02-07 23:06:43 -08:00
smt_justification.cpp added API to monitor clause inferences 2022-10-19 08:34:55 -07:00
smt_justification.h add options for logging learned lemmas and theory axioms 2022-08-08 11:18:56 +03:00
smt_kernel.cpp allow copy within a user scope #6827 2023-07-31 19:46:08 -07:00
smt_kernel.h fix #7245 2024-06-15 02:29:32 -07:00
smt_literal.cpp consolidate literals 2021-05-20 12:58:27 -07:00
smt_literal.h consolidate literals 2021-05-20 12:58:27 -07:00
smt_lookahead.cpp Add support of the SunOS platform (Solaris, OpenSolaris, OpenIndiana) (#4757) 2020-10-27 11:39:21 -07:00
smt_lookahead.h handle better cancellation for parallel, switch between cube mode and base level mode in smt.threads, expose parameters to control theory_bv and phase caching 2020-08-16 23:29:24 -07:00
smt_model_checker.cpp fix #6662 2023-04-08 17:14:39 -07:00
smt_model_checker.h fix #6662 2023-04-08 17:14:39 -07:00
smt_model_finder.cpp fix #6914 2023-09-23 11:22:25 -07:00
smt_model_finder.h fix compiler warnings #4727 2020-10-18 11:31:21 +01:00
smt_model_generator.cpp fix mbqi value caching issue raised by Clemens and Martin 2023-01-15 22:47:34 -05:00
smt_model_generator.h Use = default for virtual constructors. 2022-08-05 18:11:46 +03:00
smt_parallel.cpp use some suggestions from #5615 2021-10-22 12:39:55 -04:00
smt_parallel.h fix build 2020-01-31 22:20:25 -08:00
smt_quantifier.cpp Remove empty leaf destructors. (#6211) 2022-07-30 10:07:03 +01:00
smt_quantifier.h Use = default for virtual constructors. 2022-08-05 18:11:46 +03:00
smt_quantifier_instances.h booyah 2020-07-04 15:56:30 -07:00
smt_quick_checker.cpp call it data instead of c_ptr for approaching C++11 std::vector convention. 2021-04-13 18:17:35 -07:00
smt_quick_checker.h booyah 2020-07-04 15:56:30 -07:00
smt_relevancy.cpp optimize ~relevancy_propagator_imp() so it just dec refs the exprs in the trail 2023-08-20 10:07:56 +01:00
smt_relevancy.h make destructors virtual 2023-08-20 15:30:57 -07:00
smt_setup.cpp wip - alpha support for polymorphism 2023-07-12 18:09:02 -07:00
smt_setup.h wip - alpha support for polymorphism 2023-07-12 18:09:02 -07:00
smt_solver.cpp allow copy within a user scope #6827 2023-07-31 19:46:08 -07:00
smt_solver.h booyah 2020-07-04 15:56:30 -07:00
smt_statistics.cpp make include paths uniformly use path relative to src. #534 2017-07-31 13:24:11 -07:00
smt_statistics.h remove '#include <iostream>' from headers and from unneeded places 2022-06-17 14:10:19 +01:00
smt_theory.cpp fix regression from today, see #5676 2021-12-01 14:29:53 -08:00
smt_theory.h update model validate to include arithmetic 2023-08-03 15:51:29 -07:00
smt_types.h signed 2021-05-21 15:51:27 -07:00
smt_value_sort.cpp refactor get_sort 2021-02-02 04:45:54 -08:00
smt_value_sort.h booyah 2020-07-04 15:56:30 -07:00
spanning_tree.h booyah 2020-07-04 15:56:30 -07:00
spanning_tree_base.h booyah 2020-07-04 15:56:30 -07:00
spanning_tree_def.h booyah 2020-07-04 15:56:30 -07:00
theory_arith.cpp make include paths uniformly use path relative to src. #534 2017-07-31 13:24:11 -07:00
theory_arith.h household chores in legacy arithmetic solver 2023-11-18 09:56:06 -08:00
theory_arith_aux.h household chores in legacy arithmetic solver 2023-11-18 09:56:06 -08:00
theory_arith_core.h household chores in legacy arithmetic solver 2023-11-18 09:56:06 -08:00
theory_arith_def.h booyah 2020-07-04 15:56:30 -07:00
theory_arith_eq.h household chores in legacy arithmetic solver 2023-11-18 09:56:06 -08:00
theory_arith_int.h Fix some typos in identifiers. (#7118) 2024-02-14 09:25:32 +07:00
theory_arith_inv.h booyah 2020-07-04 15:56:30 -07:00
theory_arith_nl.h merging master to unit_prop_on_monomials 2023-10-02 16:42:59 -07:00
theory_arith_pp.h fix #7053 2023-12-13 19:25:18 -08:00
theory_array.cpp fix #6410 2022-10-18 12:34:45 -07:00
theory_array.h fix #5812 2022-02-04 13:08:52 -08:00
theory_array_bapa.cpp Remove empty leaf destructors. (#6211) 2022-07-30 10:07:03 +01:00
theory_array_bapa.h booyah 2020-07-04 15:56:30 -07:00
theory_array_base.cpp fix #6749 2023-06-07 16:09:50 -07:00
theory_array_base.h add option to select with folding 2022-08-04 16:59:26 +03:00
theory_array_full.cpp array theory: use expr_ref for mk_default() so it doesnt leak if internalize throws 2023-08-20 22:28:57 +01:00
theory_array_full.h fix #6591 2023-02-19 11:09:52 -08:00
theory_bv.cpp fix #6808 2023-07-13 10:47:55 -07:00
theory_bv.h Fix UP's decide callback (#6707) 2023-06-02 09:52:54 +02:00
theory_char.cpp add options for logging learned lemmas and theory axioms 2022-08-08 11:18:56 +03:00
theory_char.h bv2char and char2bv with Clemens 2021-09-13 16:09:03 +02:00
theory_datatype.cpp Add intblast solver 2023-12-15 13:50:38 -08:00
theory_datatype.h fix unsoundness in explanation handling for nested datatypes and sequences 2022-07-03 17:00:39 -07:00
theory_dense_diff_logic.cpp make include paths uniformly use path relative to src. #534 2017-07-31 13:24:11 -07:00
theory_dense_diff_logic.h add options for logging learned lemmas and theory axioms 2022-08-08 11:18:56 +03:00
theory_dense_diff_logic_def.h Fix some warnings about unused stuff. (#6290) 2022-08-21 12:39:30 -07:00
theory_diff_logic.cpp make include paths uniformly use path relative to src. #534 2017-07-31 13:24:11 -07:00
theory_diff_logic.h add options for logging learned lemmas and theory axioms 2022-08-08 11:18:56 +03:00
theory_diff_logic_def.h add options for logging learned lemmas and theory axioms 2022-08-08 11:18:56 +03:00
theory_dl.cpp streamline pb solver interface and naming after removal of xor 2021-02-28 12:32:04 -08:00
theory_dl.h booyah 2020-07-04 15:56:30 -07:00
theory_dummy.cpp remove template Context dependency in every trail object 2021-02-08 15:41:57 -08:00
theory_dummy.h Remove empty leaf destructors. (#6211) 2022-07-30 10:07:03 +01:00
theory_fpa.cpp Revert unsound NaN constraints in theory_fpa (#6993) 2023-11-14 14:28:30 -08:00
theory_fpa.h Revert unsound NaN constraints in theory_fpa (#6993) 2023-11-14 14:28:30 -08:00
theory_lra.cpp Api (#7097) 2024-01-24 16:05:18 -08:00
theory_lra.h update model validate to include arithmetic 2023-08-03 15:51:29 -07:00
theory_opt.cpp make include paths uniformly use path relative to src. #534 2017-07-31 13:24:11 -07:00
theory_opt.h Add and fix a few general compiler warnings. (#5628) 2021-10-29 15:42:32 +02:00
theory_pb.cpp fix #7098 2024-01-30 20:38:01 -08:00
theory_pb.h Make sure all headers do #pragma once. (#6188) 2022-07-23 10:41:14 -07:00
theory_polymorphism.h wip - alpha support for polymorphism 2023-07-12 18:09:02 -07:00
theory_recfun.cpp #7207 2024-06-16 15:04:42 -07:00
theory_recfun.h Treat arguments to recursive functions as beta redexes 2022-06-14 09:51:06 -07:00
theory_seq.cpp fix build warnings 2024-02-01 09:36:52 -08:00
theory_seq.h update model validate to include arithmetic 2023-08-03 15:51:29 -07:00
theory_seq_empty.h remove template Context dependency in every trail object 2021-02-08 15:41:57 -08:00
theory_special_relations.cpp fix #7103 2024-01-27 17:46:23 -08:00
theory_special_relations.h handle ac-op in legacy special relations procedure by adding warning 2023-12-03 12:55:37 -08:00
theory_str.cpp unused variables 2022-10-20 09:09:06 -07:00
theory_str.h Remove empty leaf destructors. (#6211) 2022-07-30 10:07:03 +01:00
theory_str_mc.cpp remove symbol -> zstring -> symbol round-trips 2021-05-22 13:12:49 -07:00
theory_str_regex.cpp fix re.range symbolic argument bug in z3str3 (#6189) 2022-07-27 04:24:20 +02:00
theory_user_propagator.cpp add m_replay_qhead to the trail 2024-05-31 11:54:50 +04:00
theory_user_propagator.h add option to persist clauses #7109 2024-02-04 11:15:59 -08:00
theory_utvpi.cpp Fix some typos. (#7115) 2024-02-07 23:06:43 -08:00
theory_utvpi.h remove a hundred implicit constructors/destructors 2021-05-23 14:25:01 +01:00
theory_utvpi_def.h add options for logging learned lemmas and theory axioms 2022-08-08 11:18:56 +03:00
theory_wmaxsat.cpp add options for logging learned lemmas and theory axioms 2022-08-08 11:18:56 +03:00
theory_wmaxsat.h move model and proof converters to self-contained module 2022-11-03 05:23:01 -07:00
uses_theory.cpp remove unused file & hide a few symbols 2020-01-31 17:13:28 +00:00
uses_theory.h booyah 2020-07-04 15:56:30 -07:00
watch_list.cpp fix #4856 2020-12-06 14:06:08 -08:00
watch_list.h enable ranges for bit-vectors 2020-08-13 10:53:37 -07:00