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

20236 commits

Author SHA1 Message Date
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
Lev Nachmanson
bcd0d2d099 refactor lws
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:25 -10:00
Lev Nachmanson
056b83e770 refact lws
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:25 -10:00
Lev Nachmanson
963a9085a6 refact lws
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:25 -10:00
Lev Nachmanson
4d6461310f define indexed root expression
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:25 -10:00
Lev Nachmanson
841775ffdd refactor
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:25 -10:00
Lev Nachmanson
3cff4d3410 refactor
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:25 -10:00
Lev Nachmanson
f46cc6814a add trace tag for levelwise
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:25 -10:00
Lev Nachmanson
1066f3ea3b pass nlsat::solver to levelwise
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:25 -10:00
Lev Nachmanson
9a11697167 use new display functions 2025-12-03 11:16:25 -10:00
Lev Nachmanson
b4dcf0afd7 create free function display functions 2025-12-03 11:16:25 -10:00
Lev Nachmanson
2c35dae2e2 pass pmanager
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:25 -10:00