mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-21 09:34:43 +00:00
Code Activity
20382 commits 32 branches 53 tags 159 MiB
Commit graph

20382 commits

This branch
This branch
All branches
Author SHA1 Message Date
Lev Nachmanson
8193f67b84 ignore holds properties 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
4e4e24fbe1 remove erase_from_Q 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
76b7acaf2b simplify 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
30b3a156b8 simplify 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
6e10b93952 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
6e8dea6023 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
cf1bea1d59 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
402680f340 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
533f568775 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
97535c5a7c t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
48ceea699d add a display method 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
70d54ef175 refactor and assert _irreducible 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
9d6dd07f33 debug 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
fbd9ba73f9 simplify 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
3d1a4bbb32 simplify 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
f3a2de12bd t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
ad143d4bac t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
59645d1055 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
5819ceb184 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
55c986c2fe t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
55086950e2 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
a33820aa71 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
037f4b82b0 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
bb4cefd1e1 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
fd41daf6ef t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
205b17d0f3 move a comment 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
e2b62f97a0 work on seed_properties 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
01da01edf8 work on seed_properties 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
1b65129fdd work on seed_properties 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
538cc7abe5 rename 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
d40ccc9be5 renaming 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
13ef5a660c ttt 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
1aa282437d preprocess the input of levelwise to drop a level 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
4f56a98586 rename explain::main_operator to compute_conflict_explanation 2026-01-14 07:45:13 -10:00
Lev Nachmanson
ba62a55cc0 trying to figure out right indices 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
7fc072984a refactor lws 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
94a2583af8 refact lws 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
7098863435 refact lws 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
ac7299b425 define indexed root expression 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
e4f609715f refactor 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
dfa87e68dc refactor 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
ed5d9364d7 add trace tag for levelwise 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
a6a02ee0b1 pass nlsat::solver to levelwise 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
ae6ae57f5f use new display functions 2026-01-14 07:45:13 -10:00
Lev Nachmanson
d8917ffe12 create free function display functions 2026-01-14 07:45:13 -10:00
Lev Nachmanson
e7193501d4 pass pmanager 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
cdc5272040 pass anum_manager to levelwise, crash on sign 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
7fca133f6f t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
23328e8226 more accurate init of the relation between polynomial properties 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
e5b9643b01 use std::map instead of std::unordered_map 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00