mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity
19604 commits 23 branches 48 tags 157 MiB
Commit graph

4347 commits

Author SHA1 Message Date
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
Nikolaj Bjorner
beb9d2e553 update restart next 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-22 21:40:35 -08:00
Nikolaj Bjorner
ec3915218d modify backoff mechanisms and theory exchange 2025-01-22 20:32:30 -08:00
Nikolaj Bjorner
a941f5ae84 reset m_conflict indicator on sls model 2025-01-15 20:56:44 -08:00
Nikolaj Bjorner
557c01a0e5 fix #7499 - add another way to avoid adding user-defined functions to models if user don't want it 
- you can already do model.user_functions=false
- now you can also specify smtlib2_compliant (globally) and get smtlib2 behavior
 2025-01-15 19:52:04 -08:00
Nikolaj Bjorner
158dea575b add case for ite 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-15 19:07:18 -08:00
Nikolaj Bjorner
eed3fa6d49 add case for ite 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-15 18:54:50 -08:00
Nikolaj Bjorner
f422e26b3c add case for ite 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-15 18:53:26 -08:00
Nikolaj Bjorner
5365952796 fix #7510 2025-01-15 13:12:20 -08:00
Nikolaj Bjorner
878fd48819 fix compiler warning 2025-01-14 16:38:22 -08:00
Nikolaj Bjorner
31d4ba0009 re-introduce option to dump arithmetic lemmas to std-out 2025-01-14 13:54:56 -08:00
Nikolaj Bjorner
8c5abdf818 Can's fix to relevancy propagation 2025-01-14 08:14:53 -08:00
Nikolaj Bjorner
c01336553e move fixed variable propagation to nla_core/monomial_bounds 2025-01-13 18:18:53 -08:00
Nikolaj Bjorner
85356c5548 enable propagation when there are changed columns 
- to fix bug reported by Nikhil Swamy/F*
- deal with some compiler warnings by adding annotations
 2025-01-12 13:30:31 -08:00
Nikolaj Bjorner
9a237d55ca fix misc build warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-11 17:41:24 -08:00
Nikolaj Bjorner
f9ce41bd2b Update theory_lra.cpp 2025-01-08 15:41:08 -08:00
Nikolaj Bjorner
270c127407 sketch fixed variable callback mechanism 2025-01-08 12:50:46 -08:00
Nikolaj Bjorner
5a5570ef4e remove type check in insert_update 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-06 11:12:08 -08:00
Nikolaj Bjorner
23c4728d68 remove some platform specific behavior 2024-12-23 16:28:10 -08:00
Nikolaj Bjorner
554191885e remove platform dependent print 2024-12-23 16:13:36 -08:00
Nuno Lopes
97c70ba501 remove some uneeded constructors 2024-12-22 15:06:58 +00:00
Nikolaj Bjorner
fb5bbb8074 read laziness parameter modulo relvancy to avoid race conditions with setting relevancy = 0 2024-12-22 14:07:29 +01:00
Nikolaj Bjorner
78ce6c1c6c revert relevancy override 2024-12-21 18:10:10 +01:00
Nikolaj Bjorner
07b1ee5dcc mask regression on fpa by not auto-setting relevancy=0 2024-12-21 12:41:04 +01:00
Nikolaj Bjorner
da6a5facca revert change to setup_context that delays it until there are assertions 2024-12-21 11:53:46 +01:00