mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-25 01:55:32 +00:00
Code Activity
18642 commits 24 branches 48 tags 158 MiB
Commit graph

823 commits

Author SHA1 Message Date
Jakob Rath
5704e8d154
fix intblast is_bounded (#7163) 2024-03-14 08:48:38 -07:00
Nikolaj Bjorner
361e04a18e port fixes to intblast 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-03-09 10:27:12 -08:00
Nikolaj Bjorner
5379fabf9d include thread 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-03-05 12:28:30 -08:00
Nikolaj Bjorner
b14499f230 prepare for sls experiment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-03-05 12:28:30 -08:00
Nikolaj Bjorner
cf72a916f8 bugfixes, adding plugin solver 2024-03-05 12:28:30 -08:00
Nikolaj Bjorner
7970e4fe51 add clause persistence to sat/smt solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-02-04 16:42:10 -08:00
Nikolaj Bjorner
5cac9b84e4 fix build warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-02-01 09:36:52 -08:00
Nikolaj Bjorner
bdb9106f99
Api (#7097) 
* rename ul_pair to column

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* t

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* simple test passed

* remove an assert

* relax an assertion

* remove an obsolete function

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* access a term by the term column

* remove the column index from colunm.h

* remove an unused method

* remove debug code

* fix the build of lp_tst

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

---------

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Co-authored-by: Lev Nachmanson <levnach@hotmail.com>
 2024-01-24 16:05:18 -08:00
Nikolaj Bjorner
8d4e7fac6b add diagnostics option to new arithmetic solver 2024-01-22 16:23:55 -08:00
Nikolaj Bjorner
7486e8724f track quantifier instantiation method in proof hint #7080 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-20 17:44:07 -08:00
Nikolaj Bjorner
2c55aa5466 remove unused code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-17 18:04:08 -08:00
Nikolaj Bjorner
955c80e98b import updates from poly branch 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-10 19:42:58 -08:00
Nikolaj Bjorner
ea44c110bb gc expressions in the scope of updates, not old expressions 2023-12-18 20:08:29 -08:00
Nikolaj Bjorner
5d4c18dde2 fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-18 16:57:00 -08:00
Nikolaj Bjorner
6d23847482 fix typos 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-18 09:33:40 -08:00
Nikolaj Bjorner
d008dbe50a port Jakob's update to bv_internalize 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-18 09:31:59 -08:00
Nikolaj Bjorner
085b5e2588 port Jakob's update to union_find from polysat branch 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-18 09:25:24 -08:00
Nikolaj Bjorner
2f2bf749b9 fixes to intblast encoding and more arithmetic rewriters 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-17 18:15:51 -08:00
Nikolaj Bjorner
bb99f44214 fix bugs in elim-unconstr2 and fix bugs in intblast_solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-17 17:42:55 -08:00
Nikolaj Bjorner
4867073290 remove windowsArm64 from nightly 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-17 10:04:49 -08:00
Nikolaj Bjorner
d0a59f3740 intblast with lazy expansion of shl, ashr, lshr 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-16 15:12:57 -08:00
Bruce Mitchener
50e0fd3ba6
Use noexcept more. (#7058) 2023-12-16 12:14:53 +00:00
Nikolaj Bjorner
9293923b8a Add intblast solver 2023-12-15 13:50:38 -08:00
Nikolaj Bjorner
f98b42ae42 install importlib-resources for ubuntu doc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-04 10:33:29 -08:00
Nikolaj Bjorner
f7415bb677 install importlib-resources for ubuntu doc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-04 10:32:02 -08:00
Nikolaj Bjorner
1b1ebaa3b0 minor simplification during internalization 2023-12-03 12:43:39 -08:00
Nikolaj Bjorner
36725383d3 minor simplification of terms during internalization. 2023-12-03 12:43:14 -08:00
Nikolaj Bjorner
9cc2ce42f7 #7027 
fix lossy function declaration inclusion functionality exposed when fixing a bug for incomplete model generation.
 2023-12-03 11:14:18 -08:00
Nikolaj Bjorner
965bee5801 fix build 2023-12-02 19:52:59 -08:00
Nikolaj Bjorner
1de25ed09c pending files 2023-12-02 19:43:51 -08:00
Nikolaj Bjorner
362d299a5c #7027 2023-12-02 19:34:36 -08:00
Nikolaj Bjorner
331507c4cd #7027 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-02 12:05:06 -08:00
Nikolaj Bjorner
99e2794a6d update output 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-11-30 17:20:43 -08:00
Nikolaj Bjorner
b52fd8d954 add EUF plugin framework. 
plugin setting allows adding equality saturation within the E-graph propagation without involving externalizing theory solver dispatch. It makes equality saturation independent of SAT integration.
Add a special relation operator to support ad-hoc AC symbols.
 2023-11-30 13:58:30 -08:00
Nikolaj Bjorner
faa2d8ac6c re-enable delayed literal propagation 2023-11-29 14:00:37 -08:00
Nikolaj Bjorner
2f01b5b567 re-enable delayed literal propagation 2023-11-29 14:00:17 -08:00
Nikolaj Bjorner
41a3196c89 fix #7024 2023-11-29 13:35:30 -08:00
Nikolaj Bjorner
8179f8b5d7 fix #7017 2023-11-28 14:32:56 -08:00
Nikolaj Bjorner
c2610cb37c #6523 
malformed models on giveup status
 2023-11-13 14:32:53 -08:00
Nikolaj Bjorner
8a4e857294 #6523 
regressions from changes inside math/lp/int_solver
 2023-11-13 14:28:03 -08:00
Nikolaj Bjorner
e86eae27e6 #6523 and other heap-use-after-free error 2023-11-07 19:57:49 +01:00
Nikolaj Bjorner
49a071988c remove temporary algebraic numbers from upper layers, move to owner module 2023-11-01 03:52:20 -07:00
Nikolaj Bjorner
ea915e5b37 #6971 
clear m_a1, m_a2 before calls that may affect model.
 2023-11-01 03:36:01 -07:00
Nikolaj Bjorner
bd8e5eee4b add simplification experiment (disabled) for tracking, some reshuffling of equation/fixed_equation structs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-10-29 10:21:31 -07:00
Nikolaj Bjorner
52d16a11f9 deal with non-termination in new arithmetic solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-10-27 16:15:36 -07:00
Nikolaj Bjorner
0859be5649 #6953 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-10-25 09:07:04 -07:00
Nikolaj Bjorner
4e21e126a8 update add_lemmas to use check-feasible 2023-10-21 19:58:07 -07:00
Nikolaj Bjorner
c9c5dbc347 #6523 2023-10-16 09:27:22 -07:00
Nikolaj Bjorner
cafe3acff1 delay detach 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-10-15 12:41:34 -07:00
Nikolaj Bjorner
891ab8bac5 #6523 
fixup looping
 2023-10-15 12:37:14 -07:00