mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-09 01:11:55 +00:00
Code Activity
20027 commits 29 branches 52 tags 173 MiB
Commit graph

1952 commits

Author SHA1 Message Date
Nikolaj Bjorner
bba10c7a88 dampen order lemmas 2025-06-12 11:31:55 -07:00
Nikolaj Bjorner
c387b20ac6 move smt params to params directory, update release.yml 2025-06-09 10:47:22 -07:00
Nikolaj Bjorner
16452fec43 pretty printing for lp 2025-06-06 11:34:28 +02:00
Nikolaj Bjorner
ef284cca5d for Arie 2025-06-04 14:24:01 +02:00
Nikolaj Bjorner
7f5427b839 disable assertion that checks nl lemmas if using nra core 2025-05-30 14:47:31 +01:00
LeeYoungJoon
0a93ff515d
Centralize and document TRACE tags using X-macros (#7657) 
* Introduce X-macro-based trace tag definition
- Created trace_tags.def to centralize TRACE tag definitions
- Each tag includes a symbolic name and description
- Set up enum class TraceTag for type-safe usage in TRACE macros

* Add script to generate Markdown documentation from trace_tags.def
- Python script parses trace_tags.def and outputs trace_tags.md

* Refactor TRACE_NEW to prepend TraceTag and pass enum to is_trace_enabled

* trace: improve trace tag handling system with hierarchical tagging

- Introduce hierarchical tag-class structure: enabling a tag class activates all child tags
- Unify TRACE, STRACE, SCTRACE, and CTRACE under enum TraceTag
- Implement initial version of trace_tag.def using X(tag, tag_class, description)
  (class names and descriptions to be refined in a future update)

* trace: replace all string-based TRACE tags with enum TraceTag
- Migrated all TRACE, STRACE, SCTRACE, and CTRACE macros to use enum TraceTag values instead of raw string literals

* trace : add cstring header

* trace : Add Markdown documentation generation from trace_tags.def via mk_api_doc.py

* trace : rename macro parameter 'class' to 'tag_class' and remove Unicode comment in trace_tags.h.

* trace : Add TODO comment for future implementation of tag_class activation

* trace : Disable code related to tag_class until implementation is ready (#7663).
 2025-05-28 14:31:25 +01:00
Lev Nachmanson
f680242620 adjust the frequency of dio calls 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-05-14 08:17:39 -07:00
Lev Nachmanson
15a3818fce cleanup in dioph_eq.cpp 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-05-13 14:57:21 -07:00
Lev Nachmanson
6b32aaed10 remove slack heuristic 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-05-12 14:02:17 -07:00
Lev Nachmanson
a5e5d4dbd3 testing 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-05-12 14:02:17 -07:00
Lev Nachmanson
bbaec0bf95 trying randomly shuffle the indices in the slack utilization 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-05-12 14:02:17 -07:00
Lev Nachmanson
52241b6474 some refactoring of lar_solver.h 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-05-12 14:02:17 -07:00
Lev Nachmanson
fef954c028 shring lar_solver.h 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-05-12 14:02:17 -07:00
Lev Nachmanson
4abd9843a0 fix the build 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-05-12 14:02:17 -07:00
Lev Nachmanson
e3f5e8c8a6 restore lar_solver::add_named_var 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-05-12 14:02:17 -07:00
Lev Nachmanson
b375faa77c continue PIMPL refactor in lar_solver 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-05-12 14:02:17 -07:00
Lev Nachmanson
b7ffcb7e61 implement imp of lar_solver as lar_solver::imp 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-05-12 14:02:17 -07:00
Lev Nachmanson
39955f1d04 remove a function from lar_solver 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-05-12 14:02:17 -07:00
Lev Nachmanson
4e56834b76 test 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-05-12 14:02:17 -07:00
Lev Nachmanson
a527667fc0 shuffle more functionality from lar_solver.h to lar_solver::imp 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-05-12 14:02:17 -07:00
Lev Nachmanson
c81eb74c93 apply the slack idea in a loop 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-05-12 14:02:17 -07:00
Lev Nachmanson
e041fe95bc slack 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-05-12 14:02:17 -07:00
Nikolaj Bjorner
792ffeeda7 fix latent sign bug 2025-04-23 17:22:57 -07:00
Nikolaj Bjorner
fe1fff3b7e add scaffolding for experiments with slack 2025-04-23 17:07:50 -07:00
Nikolaj Bjorner
12ccf59ab9 rename fields to compile on c++ platforms 2025-04-23 17:06:15 -07:00
Nikolaj Bjorner
e41acd7b50 convert m_r_upper and m_r_lower bounds to plain vectors 
manage backtracking state together with backtracking of column data.
 2025-04-23 16:33:38 -07:00
Nikolaj Bjorner
fae60946bf consolidate some bounds references 2025-04-23 15:45:44 -07:00
Nikolaj Bjorner
7641393f8a use inlined functions 2025-04-23 14:28:31 -07:00
Nikolaj Bjorner
5cc57b8958 coalesce updates to bounds 2025-04-23 14:05:17 -07:00
Nikolaj Bjorner
d73d104ded remove overwriting x,y,rval 2025-04-23 09:17:22 -07:00
Nikolaj Bjorner
ff920ba51b handle root expressions, and checking exponentiation with nlsat 
this one is for you @matthai
 2025-04-22 13:47:47 -07:00
Lev Nachmanson
a1673f2bdd fallback to Gomory cuts and gcd conflicts if dio fails 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-04-21 17:10:32 -07:00
Lev Nachmanson
ab9f3307d6 change the default of running dio to true, and running gcd to false, remove branching in dio 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-04-18 18:24:50 -07:00
Lev Nachmanson
dbde713eb3 remove testing code in is_big_term_on_no_term 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-04-18 18:24:50 -07:00
Lev Nachmanson
1131d5294d fix a bug in tracking the changes in dio 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-04-18 18:24:50 -07:00
Lev Nachmanson
d289495ca4 allow gcd when dio ignores some terms 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-04-18 18:24:50 -07:00
Lev Nachmanson
17af18fe31 make gcd call in dio optional 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-04-18 18:24:50 -07:00
Lev Nachmanson
436eefbce2 always remove the tightened term 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-04-18 18:24:50 -07:00
Lev Nachmanson
dc7185d0a4 change the name of m_changed_columns to m_changed_f_columns 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-04-18 18:24:50 -07:00
Lev Nachmanson
32e77d8214 typo 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-04-18 18:24:50 -07:00
Lev Nachmanson
cb1818f4b8 reject more terms with big numbers 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-04-18 18:24:50 -07:00
Lev Nachmanson
1cde40bddb dio_calls_period=4 2025-04-18 18:24:50 -07:00
Lev Nachmanson
87e2ce8948 Update lp_settings.h - m_dio_calls_period = 4 2025-04-18 18:24:50 -07:00
Lev Nachmanson
59edb81f86 Update lp_settings.cpp 
white space change
 2025-04-18 18:24:50 -07:00
Lev Nachmanson
8db9f52386 add parameter m_dio_calls_period 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-04-18 18:24:50 -07:00
Lev Nachmanson
ae97ee09d9 throttle dio 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-04-18 18:24:50 -07:00
Lev Nachmanson
972f80188a throttle dio for big numbers 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-04-18 18:24:50 -07:00
Lev Nachmanson
3e49d9fcfe reuse dio branch 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-04-18 18:24:50 -07:00
Nikolaj Bjorner
8035edbe65 remove lp_assert 2025-04-14 11:10:26 -07:00
Nikolaj Bjorner
a39efbb008 fix #7607 2025-04-05 11:58:47 -07:00