mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-26 21:16:02 +00:00
Code Activity
19851 commits 64 branches 52 tags 178 MiB
Commit graph

4371 commits

Author SHA1 Message Date
Lev Nachmanson
f5016b4433 remove a printout 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-08-07 08:33:04 -07:00
Lev Nachmanson
3eda3867d3 precalc parameters to define the eval order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-08-07 08:33:04 -07:00
Lev Nachmanson
eeb1c18aa4 more untangle params 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-08-07 08:33:04 -07:00
Lev Nachmanson
efa63db691 debug under defined calls 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-08-07 08:33:04 -07:00
Lev Nachmanson
d218e87f76 add python file 
Signed-off-by: Lev Nachmanson <levnach@Levs-MacBook-Pro.local>
 2025-08-07 08:33:04 -07:00
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
Nikolaj Bjorner
d66fabe462 Update smt_parallel.cpp 
Drop non-relevant units from shared structures.
 2025-08-03 14:17:00 -07:00
Nikolaj Bjorner
89cc9bd333 disable pre-processing during cubing 2025-07-31 20:58:58 -07:00
Nikolaj Bjorner
2d876d5af1 allow for internalize implies 2025-07-31 20:48:15 -07:00
Nikolaj Bjorner
0528c86905 fix #7745 
axioms for len(substr(...)) escaped due to nested rewriting
 2025-07-26 12:30:42 -07:00
Nikolaj Bjorner
3ccf7a695b make concurrent collect_statistics in a timeout thread safe 2025-07-04 18:58:29 -07:00
Lev Nachmanson
20fb830682 filter out empty lemmas from nla_solver on consumption 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-06-26 16:33:16 -07:00
Nikolaj Bjorner
8d1e954709 introduce notion of auxiliary constraints created by nla_solver lemmas 
notes: auxiliary constraints could extend to Gomory and B&B.
 2025-06-12 20:37:51 -07:00
Nikolaj Bjorner
c387b20ac6 move smt params to params directory, update release.yml 2025-06-09 10:47:22 -07:00
Nikolaj Bjorner
ef284cca5d for Arie 2025-06-04 14:24:01 +02:00
Nikolaj Bjorner
e2e54527db remove trace that accesses stale data #7668 2025-06-02 08:58:35 +02: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
Can Cebeci
b44c897a59
Fix setup_relevancy for relevancy-dependent case split strategies (#7662) 2025-05-27 16:52:35 +01:00
Nikolaj Bjorner
85e7243108 update add-term to avoid duplicating fresh aux-expr 2025-05-20 14:22:03 -07:00
Nikolaj Bjorner
47c12f9a18 refactoring to use for-range 2025-05-15 10:57:46 -07:00
Nikolaj Bjorner
f6fbeda9d7 fix #7629 2025-04-23 15:22:44 -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
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
3e49d9fcfe reuse dio branch 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-04-18 18:24:50 -07:00
Nikolaj Bjorner
e41090df83 fix #7602 
add missing relevancy propagation so that relationship between rel and TC(rel) are not lost to the theory solver.
 2025-04-14 15:38:22 -07:00
Nikolaj Bjorner
26ab0de8fc rename function 2025-04-04 18:40:15 -07:00
Lev Nachmanson
6f7b749ff9 improved dio handler 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-03-24 07:44:13 -10:00
Nikolaj Bjorner
2ecf6dc53c add code for free bounds axiom, but keep it disabled 2025-03-19 08:57:31 -10:00
Nikolaj Bjorner
0e881e7abb fix #7584 2025-03-15 13:33:08 -07:00
Nikolaj Bjorner
80f00f191a fix #7572 and fix #7574 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-07 10:46:29 -08:00
Nikolaj Bjorner
f977b48161 adjust solve_for to handle rationals 2025-02-17 13:59:23 -08:00
Nikolaj Bjorner
b27a2aa7fc remove calls to removed def constructor 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-02-16 10:13:00 -08:00
Lev Nachmanson
e920291393 fixing the default parameters of dio and rename m_gomory_cuts to m_cuts 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson
957b177c64 set arith.lp.dio_cuts_enable_gomory to False by default 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson
79e3f8ab39 disabling dio handler by default, and fix a print out 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson
134bed826a throttle the branching in dio 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson
a19e10912f make dio less aggressive, allow other cuts 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson
71c433908c work on incremental version 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson
2ebb957cc8 enable cuts from proofs 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson
a1a01b9da6 move some functionality from int_solver to int_solver::imp 2025-02-11 12:23:00 -10:00
Lev Nachmanson
097a25ebfe add parameter to control calling diophantine equations 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Clemens Eisenhofer
acd48b6a30
Fixing #7465 (#7551) 
* Fixed bug in UP

* Put decrement at the right position

* Fixed replaying in UP

* Set UP persist clauses to false
 2025-02-11 09:20:25 -08:00
Can Cebeci
af270da785
Fix complete_partial_func for finite domains (#7547) 2025-02-05 16:14:55 -08:00
Nikolaj Bjorner
17d47ca8c7 fix #7493 2025-02-02 15:00:31 -08:00
Nikolaj Bjorner
fd2a8a554d disable small clause generation for propagation 2025-02-01 20:04:29 -08:00
Nikolaj Bjorner
fa605454fb 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
Jonáš Fiala
2050fc3b35
Preserve fingerprint in trace (#7534) 2025-01-27 13:09:48 -08:00
Can Cebeci
2d8f024680
Mark fixed_eq literals as relevant (#7533) 2025-01-27 11:10:46 -08:00
Nikolaj Bjorner
0e8969ce60 deal with compiler warnings and include value exchange prior to final check. 2025-01-24 09:40:33 -08:00
Nikolaj Bjorner
4d33f442b9 enable value import in parallel mode 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-22 22:45:01 -08:00