3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-12-31 16:29:52 +00:00
Commit graph

20247 commits

Author SHA1 Message Date
Lev Nachmanson
8ed693a2bc t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:26 -10:00
Lev Nachmanson
20938f569f remove a parameter
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:26 -10:00
Lev Nachmanson
ae171dfee2 t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:26 -10:00
Lev Nachmanson
79899e1b52 t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:26 -10:00
Lev Nachmanson
3cd49d0e54 introdure mk_prop
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:26 -10:00
Lev Nachmanson
a8226b04f2 t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:26 -10:00
Lev Nachmanson
73741fecfe got a section
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:26 -10:00
Lev Nachmanson
05d5669e21 t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:26 -10:00
Lev Nachmanson
d0e340afe4 t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:26 -10:00
Lev Nachmanson
282ee84223 t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:26 -10:00
Lev Nachmanson
014d02d180 t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:26 -10:00
Lev Nachmanson
1aab5cf37f t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:26 -10:00
Lev Nachmanson
52a76af764 t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:26 -10:00
Lev Nachmanson
415bd451c2 t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:26 -10:00
Lev Nachmanson
191a4f6e0f t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:26 -10:00
Lev Nachmanson
b55508ce95 ignore holds properties
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:26 -10:00
Lev Nachmanson
9c7b91a68e remove erase_from_Q
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:26 -10:00
Lev Nachmanson
605a24b169 simplify
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:26 -10:00
Lev Nachmanson
6daf2c26dd simplify
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:26 -10:00
Lev Nachmanson
13abcbaa4e t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:26 -10:00
Lev Nachmanson
516a906393 t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:26 -10:00
Lev Nachmanson
97692ac0b8 t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:26 -10:00
Lev Nachmanson
696cb57278 t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:26 -10:00
Lev Nachmanson
a2e05443f1 t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:26 -10:00
Lev Nachmanson
f51083fd99 t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:26 -10:00
Lev Nachmanson
ade559e762 add a display method
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:26 -10:00
Lev Nachmanson
3d6c3a6cb0 refactor and assert _irreducible
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:26 -10:00
Lev Nachmanson
668064c39e debug
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:26 -10:00
Lev Nachmanson
458fb58b50 simplify
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:26 -10:00
Lev Nachmanson
78c1b08c4c simplify
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:26 -10:00
Lev Nachmanson
e83e5d03ae t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:26 -10:00
Lev Nachmanson
2271c6d038 t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:26 -10:00
Lev Nachmanson
4dbd3725d1 t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:26 -10:00
Lev Nachmanson
6633eaf671 t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:26 -10:00
Lev Nachmanson
4ee6650d90 t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:26 -10:00
Lev Nachmanson
f443f7716b t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:26 -10:00
Lev Nachmanson
747e415110 t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:25 -10:00
Lev Nachmanson
2eaba91b99 t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:25 -10:00
Lev Nachmanson
d31380416f t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:25 -10:00
Lev Nachmanson
ff984670b9 t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:25 -10:00
Lev Nachmanson
97e35e1f31 move a comment
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:25 -10:00
Lev Nachmanson
0cdb1beca9 work on seed_properties
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:25 -10:00
Lev Nachmanson
6ffc120510 work on seed_properties
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:25 -10:00
Lev Nachmanson
45184762ab work on seed_properties
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:25 -10:00
Lev Nachmanson
ef310a671d rename
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:25 -10:00
Lev Nachmanson
5150a652cd renaming
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:25 -10:00
Lev Nachmanson
3ce4f89832 ttt
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:25 -10:00
Lev Nachmanson
3e4171ff96 preprocess the input of levelwise to drop a level
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:25 -10:00
Lev Nachmanson
2e810e3aaa rename explain::main_operator to compute_conflict_explanation 2025-12-03 11:16:25 -10:00
Lev Nachmanson
fbc7f6c77d trying to figure out right indices
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:25 -10:00