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 |
|
Lev Nachmanson
|
a79c0a7901
|
pass anum_manager to levelwise, crash on sign
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:25 -10:00 |
|
Lev Nachmanson
|
856c71acb2
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:25 -10:00 |
|
Lev Nachmanson
|
2216825f43
|
more accurate init of the relation between polynomial properties
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:25 -10:00 |
|
Lev Nachmanson
|
5e1572d610
|
use std::map instead of std::unordered_map
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:25 -10:00 |
|
Lev Nachmanson
|
2c5a7c965f
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:25 -10:00 |
|
Lev Nachmanson
|
0d8d77277f
|
define symbolic_interval
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:25 -10:00 |
|
Lev Nachmanson
|
6ef4743015
|
more scaffolding
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:25 -10:00 |
|
Lev Nachmanson
|
80f2a8b17c
|
closer to the paper
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:25 -10:00 |
|
Lev Nachmanson
|
7cd68fee7b
|
scaffolding
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:25 -10:00 |
|
Lev Nachmanson
|
b64ce02dc2
|
scaffoldin
|
2025-12-03 11:16:25 -10:00 |
|
Lev Nachmanson
|
cdbc89964f
|
t2
|
2025-12-03 11:16:25 -10:00 |
|
Lev Nachmanson
|
d3a576411f
|
t1
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-03 11:16:25 -10:00 |
|