mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-19 15:16:29 +00:00
Code Activity
z3/src/smt
History
Lev Nachmanson f508854fe5
Lcube (#9858) 
Implemented the largest cube heuristic from Bromberger and Weidenbach's
paper on cubes. Also fixes an overflow bug in mzp.
Use vswhere to find the visual studio version on windows in the build's ymls.
---------

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
2026-06-14 16:25:21 -07:00
..
proto_model Remove copies (#8583) 2026-02-18 21:02:22 -08:00
tactic connect parallel tactical2 as side load 2026-05-13 14:59:05 -07:00
arith_eq_adapter.cpp use expr based access to enodes to allow for storing first-class lambas 2026-05-30 15:13:08 -07:00
arith_eq_adapter.h use expr based access to enodes to allow for storing first-class lambas 2026-05-30 15:13:08 -07:00
arith_eq_solver.cpp Fix static analysis issues: null dereferences, unsafe casts, branch clones, uninitialized members (#9424) 2026-04-29 13:37:11 -07:00
arith_eq_solver.h Remove redundant non-virtual destructors with = default (#8462) 2026-02-18 20:58:01 -08:00
CMakeLists.txt remove lattice component 2026-02-19 15:49:45 -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 Replace fall-through comments with Z3_fallthrough macro (#8219) 2026-02-18 20:57:31 -08:00
dyn_ack.cpp use expr based access to enodes to allow for storing first-class lambas 2026-05-30 15:13:08 -07:00
dyn_ack.h use expr based access to enodes to allow for storing first-class lambas 2026-05-30 15:13:08 -07:00
expr_context_simplifier.cpp Fix static analysis issues: null dereferences, unsafe casts, branch clones, uninitialized members (#9424) 2026-04-29 13:37:11 -07:00
expr_context_simplifier.h move smt params to params directory, update release.yml 2025-06-09 10:47:22 -07:00
fingerprints.cpp Remove unused defined_names artifacts and simplify fingerprint_set::contains (#9702) 2026-06-03 08:16:46 -07:00
fingerprints.h remove side definitions 2026-06-02 21:43:55 -07:00
mam.cpp Update used_enodes properly (#9695) 2026-06-03 13:36:37 -07: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 remove side definitions 2026-06-02 21:43: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 Refactor SMT core: use structured bindings for enode_pair access (#8427) 2026-02-18 20:57:59 -08:00
seq_ne_solver.cpp Adopt C++17 structured bindings for map/pair iteration (#8159) 2026-02-18 20:57:09 -08:00
seq_offset_eq.cpp Refactor seq_offset_eq::find to use std::optional (#8300) 2026-02-18 20:57:53 -08:00
seq_offset_eq.h Refactor seq_offset_eq::find to use std::optional (#8300) 2026-02-18 20:57:53 -08:00
seq_regex.cpp Add OP_RE_XOR and union-find bisimulation for ground regex equivalence (#9804) 2026-06-10 14:58:20 -07: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 use expr based access to enodes to allow for storing first-class lambas 2026-05-30 15:13:08 -07:00
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 Merge branch 'master' into finite-sets 2026-02-18 21:11:44 -08:00
smt_b_justification.h
smt_bool_var_data.h
smt_case_split_queue.cpp Update generation number of already-internalized enodes (#9628) 2026-05-26 15:08:11 -07: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 Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
smt_cg_table.h
smt_checker.cpp control recursion depth for check function 2026-05-27 14:29:53 -07:00
smt_checker.h control recursion depth for check function 2026-05-27 14:29:53 -07:00
smt_clause.cpp Refactor mk_and/mk_or call sites to use vector overloads (#8286) 2026-02-18 20:57:52 -08: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 prepare for enodes over lambdas 2026-06-01 13:00:35 -07:00
smt_conflict_resolution.h Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
smt_consequences.cpp fix crash 2026-02-18 21:02:17 -08:00
smt_context.cpp remove side definitions 2026-06-02 21:43:55 -07:00
smt_context.h remove side definitions 2026-06-02 21:43:55 -07:00
smt_context_inv.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
smt_context_pp.cpp use expr based access to enodes to allow for storing first-class lambas 2026-05-30 15:13:08 -07:00
smt_context_stat.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
smt_enode.cpp disable test in tptp, move to native lambdas 2026-06-02 10:38:51 -07:00
smt_enode.h disable test in tptp, move to native lambdas 2026-06-02 10:38:51 -07: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 Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
smt_for_each_relevant_expr.h Use = default for virtual constructors. 2022-08-05 18:11:46 +03:00
smt_implied_equalities.cpp Refactor mk_and/mk_or call sites to use vector overloads (#8286) 2026-02-18 20:57:52 -08: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 disable test in tptp, move to native lambdas 2026-06-02 10:38:51 -07:00
smt_justification.cpp fix build 2026-02-18 20:58:00 -08:00
smt_justification.h add options for logging learned lemmas and theory axioms 2022-08-08 11:18:56 +03:00
smt_kernel.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
smt_kernel.h add an option to register callback on quantifier instantiation 2025-08-06 21:11:55 -07:00
smt_literal.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08: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 Remove unused defined_names artifacts and simplify fingerprint_set::contains (#9702) 2026-06-03 08:16:46 -07:00
smt_model_checker.h Remove unused defined_names artifacts and simplify fingerprint_set::contains (#9702) 2026-06-03 08:16:46 -07:00
smt_model_finder.cpp disable test in tptp, move to native lambdas 2026-06-02 10:38:51 -07:00
smt_model_finder.h
smt_model_generator.cpp disable test in tptp, move to native lambdas 2026-06-02 10:38:51 -07:00
smt_model_generator.h fix #7584 2025-03-15 13:33:08 -07:00
smt_parallel.cpp Simplify parallel SMT code: clean comments and deduplicate stat computation (#9507) 2026-05-12 14:41:20 -04:00
smt_parallel.h Final version of parallel architecture for FMCAD26 submission (#9476) 2026-05-11 18:08:23 -04:00
smt_quantifier.cpp remove side definitions 2026-06-02 21:43:55 -07:00
smt_quantifier.h remove side definitions 2026-06-02 21:43:55 -07:00
smt_quantifier_instances.h
smt_quick_checker.cpp remove side definitions 2026-06-02 21:43:55 -07:00
smt_quick_checker.h
smt_relevancy.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
smt_relevancy.h allow for internalize implies 2025-07-31 20:48:15 -07:00
smt_setup.cpp fix indentation 2026-02-18 20:57:01 -08: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 refactor solver to include settable stats 2026-06-07 14:17:38 -07:00
smt_solver.h
smt_statistics.cpp
smt_statistics.h Add global backbones to parallel architecture (#9343) 2026-04-20 18:22:07 +02:00
smt_theory.cpp prepare for enodes over lambdas 2026-06-01 13:00:35 -07:00
smt_theory.h prepare for enodes over lambdas 2026-06-01 13:00:35 -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
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 use expr based access to enodes to allow for storing first-class lambas 2026-05-30 15:13:08 -07:00
theory_arith_aux.h prepare for enodes over lambdas 2026-06-01 13:00:35 -07:00
theory_arith_core.h use expr based access to enodes to allow for storing first-class lambas 2026-05-30 15:13:08 -07: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 use expr based access to enodes to allow for storing first-class lambas 2026-05-30 15:13:08 -07:00
theory_arith_inv.h Standardize for-loop increments to prefix form (++i) (#8199) 2026-02-18 20:57:29 -08:00
theory_arith_nl.h use expr based access to enodes to allow for storing first-class lambas 2026-05-30 15:13:08 -07:00
theory_arith_pp.h use expr based access to enodes to allow for storing first-class lambas 2026-05-30 15:13:08 -07:00
theory_array.cpp disable test in tptp, move to native lambdas 2026-06-02 10:38:51 -07:00
theory_array.h use expr based access to enodes to allow for storing first-class lambas 2026-05-30 15:13:08 -07:00
theory_array_base.cpp disable test in tptp, move to native lambdas 2026-06-02 10:38:51 -07:00
theory_array_base.h disable test in tptp, move to native lambdas 2026-06-02 10:38:51 -07:00
theory_array_full.cpp disable test in tptp, move to native lambdas 2026-06-02 10:38:51 -07:00
theory_array_full.h move closure conversion to solver internalization 2026-05-30 18:41:37 -07:00
theory_bv.cpp prepare for enodes over lambdas 2026-06-01 13:00:35 -07:00
theory_bv.h prepare for enodes over lambdas 2026-06-01 13:00:35 -07:00
theory_char.cpp Refactor theory_char::get_char_value to use std::optional (#8302) 2026-02-18 20:57:53 -08:00
theory_char.h Refactor theory_char::get_char_value to use std::optional (#8302) 2026-02-18 20:57:53 -08:00
theory_datatype.cpp prepare for enodes over lambdas 2026-06-01 13:00:35 -07:00
theory_datatype.h use expr based access to enodes to allow for storing first-class lambas 2026-05-30 15:13:08 -07: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 use expr based access to enodes to allow for storing first-class lambas 2026-05-30 15:13:08 -07:00
theory_diff_logic.cpp
theory_diff_logic.h use expr based access to enodes to allow for storing first-class lambas 2026-05-30 15:13:08 -07:00
theory_diff_logic_def.h prepare for enodes over lambdas 2026-06-01 13:00:35 -07:00
theory_dl.cpp prepare for enodes over lambdas 2026-06-01 13:00:35 -07: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 use expr based access to enodes to allow for storing first-class lambas 2026-05-30 15:13:08 -07:00
theory_finite_set.h use expr based access to enodes to allow for storing first-class lambas 2026-05-30 15:13:08 -07:00
theory_finite_set_size.cpp build warnings 2026-05-29 10:17:46 -07: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 Fix FPA incremental soundness for fp.to_* terms (#9022) (#9787) 2026-06-09 10:22:03 -07:00
theory_fpa.h use expr based access to enodes to allow for storing first-class lambas 2026-05-30 15:13:08 -07:00
theory_intblast.cpp use expr based access to enodes to allow for storing first-class lambas 2026-05-30 15:13:08 -07:00
theory_intblast.h Fix intblast ubv_to_int bug: add bv2int axioms for compound expressions 2026-02-25 00:46:13 +00:00
theory_lra.cpp Lcube (#9858) 2026-06-14 16:25:21 -07:00
theory_lra.h use expr based access to enodes to allow for storing first-class lambas 2026-05-30 15:13:08 -07: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 prepare for enodes over lambdas 2026-06-01 13:00:35 -07:00
theory_pb.h Remove redundant default constructors when they're the only constructor (#8461) 2026-02-18 20:58:01 -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 use expr based access to enodes to allow for storing first-class lambas 2026-05-30 15:13:08 -07:00
theory_recfun.h use expr based access to enodes to allow for storing first-class lambas 2026-05-30 15:13:08 -07:00
theory_seq.cpp use expr based access to enodes to allow for storing first-class lambas 2026-05-30 15:13:08 -07:00
theory_seq.h use expr based access to enodes to allow for storing first-class lambas 2026-05-30 15:13:08 -07: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 redundant overridden default destructors (#8191) 2026-02-18 20:57:13 -08:00
theory_special_relations.cpp use expr based access to enodes to allow for storing first-class lambas 2026-05-30 15:13:08 -07: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 use expr based access to enodes to allow for storing first-class lambas 2026-05-30 15:13:08 -07:00
theory_utvpi_def.h use expr based access to enodes to allow for storing first-class lambas 2026-05-30 15:13:08 -07:00
theory_wmaxsat.cpp Refactor mk_and/mk_or call sites to use vector overloads (#8286) 2026-02-18 20:57:52 -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 AIX compat (#8113) 2026-02-18 20:57:04 -08:00
uses_theory.h
watch_list.cpp fix #4856 2020-12-06 14:06:08 -08:00
watch_list.h