3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-20 17:14:43 +00:00
Commit graph

80 commits

Author SHA1 Message Date
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
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
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
Lev Nachmanson
8f066e1573 t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2026-01-14 07:45:13 -10:00
Lev Nachmanson
4ac0bf5007 define symbolic_interval
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2026-01-14 07:45:13 -10:00
Lev Nachmanson
0ca9c2eb93 more scaffolding
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2026-01-14 07:45:13 -10:00
Lev Nachmanson
3aba50f48d closer to the paper
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2026-01-14 07:45:13 -10:00
Lev Nachmanson
bbd304e1a5 scaffolding
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2026-01-14 07:45:13 -10:00
Lev Nachmanson
26ea9391a9 scaffoldin 2026-01-14 07:45:12 -10:00