mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-19 23:14:40 +00:00
Code Activity
z3/src/smt
History
Ilana Shapiro 34a40c7747 Search tree core resolution optimization (#8066) 
* Add cube tree optimization about resolving cores recursively up the path, to prune. Also integrate asms into the tree so they're not tracked separately (#7960)

* draft attempt at optimizing cube tree with resolvents. have not tested/ran yet

* adding comments

* fix bug about needing to bubble resolvent upwards to highest ancestor

* fix bug where we need to cover the whole resolvent in the path when bubbling up

* clean up comments

* close entire tree when sibling resolvent is empty

* integrate asms directly into cube tree, remove separate tracking

* try to fix bug about redundant resolutions, merging close and try_resolve_upwards into once function

* separate the logic again to avoid mutual recursion

* Refactor search tree closure and resolution logic

Refactor close_with_core to simplify logic and remove unnecessary parameters. Update sibling resolvent computation and try_resolve_upwards for clarity.

* apply formatting

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* Refactor close_with_core to use current node in lambda

* Fix formatting issues in search_tree.h

* fix build issues

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* Update smt_parallel.cpp

* Change loop variable type in unsat core processing

* Change method to retrieve unsat core from root

---------

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2026-02-18 20:56:58 -08:00
..
proto_model move smt params to params directory, update release.yml 2025-06-09 10:47:22 -07:00
tactic add an option to register callback on quantifier instantiation 2025-08-06 21:11:55 -07:00
arith_eq_adapter.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
arith_eq_adapter.h
arith_eq_solver.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
arith_eq_solver.h
CMakeLists.txt remove set cardinality operators from array theory. Make final-check use priority levels 2026-02-18 20:56:51 -08:00
database.h Make sure all headers do #pragma once. (#6188) 2022-07-23 10:41:14 -07:00
database.smt
diff_logic.h Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
dyn_ack.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
dyn_ack.h move smt params to params directory, update release.yml 2025-06-09 10:47:22 -07:00
expr_context_simplifier.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
expr_context_simplifier.h move smt params to params directory, update release.yml 2025-06-09 10:47:22 -07:00
fingerprints.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
fingerprints.h remove a few default constructors 2024-09-23 08:17:58 +01:00
mam.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
mam.h Use = default for virtual constructors. 2022-08-05 18:11:46 +03:00
old_interval.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
old_interval.h Use noexcept more. (#7058) 2023-12-16 12:14:53 +00:00
qi_queue.cpp add an option to register callback on quantifier instantiation 2025-08-06 21:11:55 -07:00
qi_queue.h add an option to register callback on quantifier instantiation 2025-08-06 21:11:55 -07: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 debug under defined calls 2025-08-07 08:33:04 -07:00
seq_ne_solver.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
seq_offset_eq.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
seq_offset_eq.h fix misspelled \brief for doxygen (#5632) 2021-10-29 15:34:28 +02:00
seq_regex.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
seq_regex.h fix co-factoring' 2021-12-14 10:12:38 -08:00
smt2_extra_cmds.cpp
smt2_extra_cmds.h
smt_almost_cg_table.cpp
smt_almost_cg_table.h
smt_arith_value.cpp remove set cardinality operators from array theory. Make final-check use priority levels 2026-02-18 20:56:51 -08:00
smt_arith_value.h remove set cardinality operators from array theory. Make final-check use priority levels 2026-02-18 20:56:51 -08:00
smt_b_justification.h
smt_bool_var_data.h
smt_case_split_queue.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
smt_case_split_queue.h move smt params to params directory, update release.yml 2025-06-09 10:47:22 -07:00
smt_cg_table.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
smt_cg_table.h
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
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 fixup proof log annotations of rules 2025-10-19 10:04:18 +02:00
smt_clause_proof.h fixup proof log annotations of rules 2025-10-19 10:04:18 +02:00
smt_conflict_resolution.cpp fixup proof log annotations of rules 2025-10-19 10:04:18 +02:00
smt_conflict_resolution.h move smt params to params directory, update release.yml 2025-06-09 10:47:22 -07:00
smt_consequences.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
smt_context.cpp refine givup conditions 2026-02-18 20:56:56 -08:00
smt_context.h fix build 2025-10-18 13:30:46 +02:00
smt_context_inv.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
smt_context_pp.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +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 Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
smt_enode.h remove unneeded iterator functions 2024-09-23 12:59:04 +01:00
smt_eq_justification.h
smt_failure.h fix crash reported by Nikhil on F* due to unhandled exception while using the rewriter during search 2025-01-28 16:27:28 -08:00
smt_farkas_util.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
smt_farkas_util.h
smt_for_each_relevant_expr.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
smt_for_each_relevant_expr.h Use = default for virtual constructors. 2022-08-05 18:11:46 +03:00
smt_implied_equalities.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
smt_implied_equalities.h
smt_induction.cpp.disabled Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
smt_induction.h.disabled remove dependencies on stale component 2021-08-16 17:52:36 -07:00
smt_internalizer.cpp revise axiom instantiation scheme for finite-sets 2025-10-18 12:08:39 +02:00
smt_justification.cpp adding proof hint output 2025-10-18 19:26:19 +02:00
smt_justification.h add options for logging learned lemmas and theory axioms 2022-08-08 11:18:56 +03:00
smt_kernel.cpp add an option to register callback on quantifier instantiation 2025-08-06 21:11:55 -07:00
smt_kernel.h add an option to register callback on quantifier instantiation 2025-08-06 21:11:55 -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 disable pre-processing during cubing 2025-07-31 20:58:58 -07:00
smt_lookahead.h Revert "Parallel solving (#7775)" (#7777) 2025-08-14 18:16:35 -07:00
smt_model_checker.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
smt_model_checker.h move smt params to params directory, update release.yml 2025-06-09 10:47:22 -07:00
smt_model_finder.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
smt_model_finder.h
smt_model_generator.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
smt_model_generator.h fix #7584 2025-03-15 13:33:08 -07:00
smt_parallel.cpp Search tree core resolution optimization (#8066) 2026-02-18 20:56:58 -08:00
smt_parallel.h Search tree core resolution optimization (#8066) 2026-02-18 20:56:58 -08:00
smt_quantifier.cpp add an option to register callback on quantifier instantiation 2025-08-06 21:11:55 -07:00
smt_quantifier.h add an option to register callback on quantifier instantiation 2025-08-06 21:11:55 -07:00
smt_quantifier_instances.h
smt_quick_checker.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
smt_quick_checker.h
smt_relevancy.cpp fix build warnings 2026-02-18 20:56:02 -08:00
smt_relevancy.h allow for internalize implies 2025-07-31 20:48:15 -07:00
smt_setup.cpp add finite_set to quantifieed theories in smt_setup, fix type signature for map-inverse axioms 2025-10-27 20:34:13 +01:00
smt_setup.h Complete theory_finite_set.h header and implement finite set theory solver (#7976) 2025-10-15 14:55:08 +02:00
smt_solver.cpp display assumptions used 2025-09-11 10:20:55 -07:00
smt_solver.h
smt_statistics.cpp
smt_statistics.h remove '#include <iostream>' from headers and from unneeded places 2022-06-17 14:10:19 +01:00
smt_theory.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
smt_theory.h remove set cardinality operators from array theory. Make final-check use priority levels 2026-02-18 20:56:51 -08:00
smt_types.h signed 2021-05-21 15:51:27 -07:00
smt_value_sort.cpp
smt_value_sort.h
spanning_tree.h
spanning_tree_base.h
spanning_tree_def.h Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
theory_arith.cpp
theory_arith.h remove set cardinality operators from array theory. Make final-check use priority levels 2026-02-18 20:56:51 -08:00
theory_arith_aux.h Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
theory_arith_core.h remove set cardinality operators from array theory. Make final-check use priority levels 2026-02-18 20:56:51 -08:00
theory_arith_def.h
theory_arith_eq.h Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
theory_arith_int.h Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
theory_arith_inv.h Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
theory_arith_nl.h Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
theory_arith_pp.h fix #7053 2023-12-13 19:25:18 -08:00
theory_array.cpp remove set cardinality operators from array theory. Make final-check use priority levels 2026-02-18 20:56:51 -08:00
theory_array.h remove set cardinality operators from array theory. Make final-check use priority levels 2026-02-18 20:56:51 -08:00
theory_array_base.cpp remove set cardinality operators from array theory. Make final-check use priority levels 2026-02-18 20:56:51 -08:00
theory_array_base.h remove set cardinality operators from array theory. Make final-check use priority levels 2026-02-18 20:56:51 -08:00
theory_array_full.cpp remove set cardinality operators from array theory. Make final-check use priority levels 2026-02-18 20:56:51 -08:00
theory_array_full.h remove some uneeded constructors 2024-12-22 15:06:58 +00:00
theory_bv.cpp remove set cardinality operators from array theory. Make final-check use priority levels 2026-02-18 20:56:51 -08:00
theory_bv.h remove set cardinality operators from array theory. Make final-check use priority levels 2026-02-18 20:56:51 -08:00
theory_char.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
theory_char.h remove set cardinality operators from array theory. Make final-check use priority levels 2026-02-18 20:56:51 -08:00
theory_datatype.cpp remove set cardinality operators from array theory. Make final-check use priority levels 2026-02-18 20:56:51 -08:00
theory_datatype.h remove set cardinality operators from array theory. Make final-check use priority levels 2026-02-18 20:56:51 -08:00
theory_dense_diff_logic.cpp
theory_dense_diff_logic.h remove set cardinality operators from array theory. Make final-check use priority levels 2026-02-18 20:56:51 -08:00
theory_dense_diff_logic_def.h remove set cardinality operators from array theory. Make final-check use priority levels 2026-02-18 20:56:51 -08:00
theory_diff_logic.cpp
theory_diff_logic.h remove set cardinality operators from array theory. Make final-check use priority levels 2026-02-18 20:56:51 -08:00
theory_diff_logic_def.h remove set cardinality operators from array theory. Make final-check use priority levels 2026-02-18 20:56:51 -08:00
theory_dl.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
theory_dl.h
theory_dummy.cpp remove set cardinality operators from array theory. Make final-check use priority levels 2026-02-18 20:56:51 -08:00
theory_dummy.h remove set cardinality operators from array theory. Make final-check use priority levels 2026-02-18 20:56:51 -08:00
theory_finite_set.cpp Add smt.finite_set.lattice_refutation parameter to control lattice refutation code path (#8247) 2026-01-20 17:20:52 -08:00
theory_finite_set.h Lattice based refutation (#8211) 2026-01-18 17:42:40 -08:00
theory_finite_set_lattice_refutation.cpp nits 2026-01-21 11:44:18 -08:00
theory_finite_set_lattice_refutation.h nits 2026-01-21 11:44:18 -08:00
theory_finite_set_size.cpp add functions that create unique sets for model construction based on solving cardinality constraints 2025-12-29 11:57:48 -08:00
theory_finite_set_size.h add functions that create unique sets for model construction based on solving cardinality constraints 2025-12-29 11:57:48 -08:00
theory_fpa.cpp remove set cardinality operators from array theory. Make final-check use priority levels 2026-02-18 20:56:51 -08:00
theory_fpa.h remove set cardinality operators from array theory. Make final-check use priority levels 2026-02-18 20:56:51 -08:00
theory_intblast.cpp remove set cardinality operators from array theory. Make final-check use priority levels 2026-02-18 20:56:51 -08:00
theory_intblast.h remove set cardinality operators from array theory. Make final-check use priority levels 2026-02-18 20:56:51 -08:00
theory_lra.cpp remove set cardinality operators from array theory. Make final-check use priority levels 2026-02-18 20:56:51 -08:00
theory_lra.h remove set cardinality operators from array theory. Make final-check use priority levels 2026-02-18 20:56:51 -08:00
theory_opt.cpp
theory_opt.h Add and fix a few general compiler warnings. (#5628) 2021-10-29 15:42:32 +02:00
theory_pb.cpp remove set cardinality operators from array theory. Make final-check use priority levels 2026-02-18 20:56:51 -08:00
theory_pb.h remove set cardinality operators from array theory. Make final-check use priority levels 2026-02-18 20:56:51 -08:00
theory_polymorphism.h remove set cardinality operators from array theory. Make final-check use priority levels 2026-02-18 20:56:51 -08:00
theory_recfun.cpp remove set cardinality operators from array theory. Make final-check use priority levels 2026-02-18 20:56:51 -08:00
theory_recfun.h remove set cardinality operators from array theory. Make final-check use priority levels 2026-02-18 20:56:51 -08:00
theory_seq.cpp remove set cardinality operators from array theory. Make final-check use priority levels 2026-02-18 20:56:51 -08:00
theory_seq.h remove set cardinality operators from array theory. Make final-check use priority levels 2026-02-18 20:56:51 -08:00
theory_seq_empty.h remove set cardinality operators from array theory. Make final-check use priority levels 2026-02-18 20:56:51 -08:00
theory_sls.cpp remove set cardinality operators from array theory. Make final-check use priority levels 2026-02-18 20:56:51 -08:00
theory_sls.h remove set cardinality operators from array theory. Make final-check use priority levels 2026-02-18 20:56:51 -08:00
theory_special_relations.cpp remove set cardinality operators from array theory. Make final-check use priority levels 2026-02-18 20:56:51 -08:00
theory_special_relations.h remove set cardinality operators from array theory. Make final-check use priority levels 2026-02-18 20:56:51 -08:00
theory_user_propagator.cpp remove set cardinality operators from array theory. Make final-check use priority levels 2026-02-18 20:56:51 -08:00
theory_user_propagator.h remove set cardinality operators from array theory. Make final-check use priority levels 2026-02-18 20:56:51 -08:00
theory_utvpi.cpp Fix some typos. (#7115) 2024-02-07 23:06:43 -08:00
theory_utvpi.h remove set cardinality operators from array theory. Make final-check use priority levels 2026-02-18 20:56:51 -08:00
theory_utvpi_def.h remove set cardinality operators from array theory. Make final-check use priority levels 2026-02-18 20:56:51 -08:00
theory_wmaxsat.cpp remove set cardinality operators from array theory. Make final-check use priority levels 2026-02-18 20:56:51 -08:00
theory_wmaxsat.h remove set cardinality operators from array theory. Make final-check use priority levels 2026-02-18 20:56:51 -08:00
uses_theory.cpp
uses_theory.h
watch_list.cpp
watch_list.h