mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-28 14:08:55 +00:00
Code Activity
z3/src/sat/smt
History
Exact
Nikolaj Bjorner b33f444545 add an option to register callback on quantifier instantiation 
Suppose a user propagator encodes axioms using quantifiers and uses E-matching for instantiation. If it wants to implement a custom priority scheme or drop some instances based on internal checks it can register a callback with quantifier instantiation
2025-08-06 21:11:55 -07:00
..
arith_axioms.cpp revamp ac plugin and plugin propagation 2025-07-21 07:35:06 -07:00
arith_diagnostics.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
arith_internalize.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
arith_solver.cpp revamp ac plugin and plugin propagation 2025-07-21 07:35:06 -07:00
arith_solver.h add power axioms to arith_solver 2025-04-23 10:48:29 -07:00
arith_theory_checker.h update format and checker for implied-eq 2023-07-27 13:21:45 -07:00
arith_value.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
arith_value.h Add intblast solver 2023-12-15 13:50:38 -08:00
array_axioms.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
array_diagnostics.cpp remove '#include <iostream>' from headers and from unneeded places 2022-06-17 14:10:19 +01:00
array_internalize.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
array_model.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
array_solver.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
array_solver.h remove default destructors & some default constructors 2024-09-04 22:30:23 +01:00
atom2bool_var.cpp improve pre-processing 2022-04-15 12:55:26 +02:00
atom2bool_var.h mbp (#4741) 2020-10-21 15:48:40 -07:00
ba_xor.h arrays (#4684) 2020-09-13 19:29:59 -07:00
bv_ackerman.cpp Sls (#7439) 2024-11-02 12:32:48 -07:00
bv_ackerman.h don't have bv-ackerman influence simplification 2022-08-21 15:25:18 -07:00
bv_delay_internalize.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
bv_internalize.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
bv_invariant.cpp remove '#include <iostream>' from headers and from unneeded places 2022-06-17 14:10:19 +01:00
bv_solver.cpp revamp ac plugin and plugin propagation 2025-07-21 07:35:06 -07:00
bv_solver.h fixes to #7250 2024-06-12 08:50:24 -07:00
bv_theory_checker.cpp remove once pragma from cpp file 2022-10-18 14:57:49 -07:00
bv_theory_checker.h wip - add bit-vector validator plugins and logging 2022-10-18 14:50:21 -07:00
CMakeLists.txt move smt params to params directory, update release.yml 2025-06-09 10:47:22 -07:00
distinct_theory_checker.h wip - features and bug-fixes to proof logging 2022-10-18 07:54:49 -07:00
dt_solver.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
dt_solver.h fix typos 2023-12-18 09:33:40 -08:00
euf_ackerman.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
euf_ackerman.h wip - updates to proof logging and self-checking 2022-10-16 23:33:30 +02:00
euf_internalize.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
euf_invariant.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
euf_model.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
euf_proof.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
euf_proof_checker.cpp Sls (#7439) 2024-11-02 12:32:48 -07:00
euf_proof_checker.h remove default destructors 2024-10-02 22:20:12 +01:00
euf_relevancy.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
euf_relevancy.h more fixes on relevancy 2022-01-04 22:02:28 -08:00
euf_solver.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
euf_solver.h add an option to register callback on quantifier instantiation 2025-08-06 21:11:55 -07:00
fpa_solver.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
fpa_solver.h #6364 - remove option of redundant clauses from internalization 2022-10-24 00:38:31 -07:00
intblast_solver.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
intblast_solver.h Sls (#7439) 2024-11-02 12:32:48 -07:00
pb_card.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
pb_card.h Use noexcept more. (#7058) 2023-12-16 12:14:53 +00:00
pb_constraint.cpp streamline pb solver interface and naming after removal of xor 2021-02-28 12:32:04 -08:00
pb_constraint.h remove unneeded iterator functions 2024-09-23 12:59:04 +01:00
pb_internalize.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
pb_pb.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
pb_pb.h Use noexcept more. (#7058) 2023-12-16 12:14:53 +00:00
pb_solver.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
pb_solver.h update gcm script 2024-12-20 17:27:21 +01:00
pb_solver_interface.h Add and fix a few general compiler warnings. (#5628) 2021-10-29 15:42:32 +02:00
q_clause.cpp fixes to sat.euf ematching #5573 2021-10-16 15:52:37 -07:00
q_clause.h log also quantifier generation (besides binding) 2022-10-20 17:49:15 -07:00
q_ematch.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
q_ematch.h update namespace, hoist exported functions outside of embedded namespace 2025-05-07 15:57:47 -07:00
q_eval.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
q_eval.h #5753 2022-01-15 09:35:25 -08:00
q_mbi.cpp handle build warnings 2025-06-06 15:13:31 +02:00
q_mbi.h track quantifier instantiation method in proof hint #7080 2024-01-20 17:44:07 -08:00
q_model_fixer.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
q_model_fixer.h Use = default for virtual constructors. 2022-08-05 18:11:46 +03:00
q_queue.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
q_queue.h redo bindings/fingerprints 2021-10-05 10:15:56 -07:00
q_solver.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
q_solver.h track quantifier instantiation method in proof hint #7080 2024-01-20 17:44:07 -08:00
q_theory_checker.cpp #6364 2022-10-20 16:39:43 -07:00
q_theory_checker.h wip - updates to proof logging and self-checking 2022-10-16 23:33:30 +02:00
recfun_solver.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
recfun_solver.h #6364 - remove option of redundant clauses from internalization 2022-10-24 00:38:31 -07:00
sat_internalizer.h fix #6623 2023-04-09 21:10:24 -07:00
sat_smt.h CNF conversion refactoring (#5547) 2021-09-20 08:53:10 -07:00
sat_th.cpp fixes to #7250 2024-06-12 08:50:24 -07:00
sat_th.h move smt params to params directory, update release.yml 2025-06-09 10:47:22 -07:00
sls_solver.cpp throttle value smt -> sls 2025-01-26 14:16:43 -08:00
sls_solver.h build fixes 2024-11-14 21:55:44 -08:00
specrel_solver.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
specrel_solver.h remove default destructors 2024-10-02 22:20:12 +01:00
tseitin_theory_checker.cpp strengthen Tseitin checker to take true/false constants into account 2023-07-28 16:54:33 -07:00
tseitin_theory_checker.h wip - proof checking, add support for distinct, other fixes 2022-10-17 17:51:10 -07:00
user_solver.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
user_solver.h fix bugs with tracking premises in user propagator in sat/smt 2024-05-31 11:25:09 +04:00
xor_solver.cpp wip - remove stale skaffolding for retrieving sub-hints. 2022-10-16 17:18:08 -07:00
xor_solver.d Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
xor_solver.h fix build 2022-10-24 10:23:50 +01:00