Lev Nachmanson
|
efb8e49234
|
refact lws
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:41 -10:00 |
|
Lev Nachmanson
|
e6aeb027ca
|
define indexed root expression
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:41 -10:00 |
|
Lev Nachmanson
|
51778e3ef7
|
refactor
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:41 -10:00 |
|
Lev Nachmanson
|
8cb7373c21
|
refactor
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:41 -10:00 |
|
Lev Nachmanson
|
2581c1ce38
|
add trace tag for levelwise
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:41 -10:00 |
|
Lev Nachmanson
|
ef6e3e21a8
|
pass nlsat::solver to levelwise
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:41 -10:00 |
|
Lev Nachmanson
|
0ccdbf96e5
|
use new display functions
|
2026-01-31 15:56:41 -10:00 |
|
Lev Nachmanson
|
1923bc80e1
|
create free function display functions
|
2026-01-31 15:56:41 -10:00 |
|
Lev Nachmanson
|
738084c651
|
pass pmanager
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:41 -10:00 |
|
Lev Nachmanson
|
0ae7394362
|
pass anum_manager to levelwise, crash on sign
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:41 -10:00 |
|
Lev Nachmanson
|
53edb0211f
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:41 -10:00 |
|
Lev Nachmanson
|
c22b9416ff
|
more accurate init of the relation between polynomial properties
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:41 -10:00 |
|
Lev Nachmanson
|
b77bf3c97e
|
use std::map instead of std::unordered_map
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:41 -10:00 |
|
Lev Nachmanson
|
7030832273
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:40 -10:00 |
|
Lev Nachmanson
|
0800dd9bc7
|
define symbolic_interval
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:40 -10:00 |
|
Lev Nachmanson
|
9d5295fa97
|
more scaffolding
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:40 -10:00 |
|
Lev Nachmanson
|
d41ba603c8
|
closer to the paper
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:40 -10:00 |
|
Lev Nachmanson
|
0fdbd2cba1
|
scaffolding
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:40 -10:00 |
|
Lev Nachmanson
|
2ea22b5972
|
scaffoldin
|
2026-01-31 15:56:40 -10:00 |
|
Lev Nachmanson
|
66a7eb24f7
|
t2
|
2026-01-31 15:56:40 -10:00 |
|
Lev Nachmanson
|
b53317bb9a
|
t1
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:40 -10:00 |
|
Lev Nachmanson
|
9e51f34475
|
t0
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-31 15:56:40 -10:00 |
|
Copilot
|
0b1d30e86f
|
[WIP] Refactor NLSAT solver to use structured bindings for variable bounds (#8425)
* Initial plan
* Refactor NLSAT solver to use structured bindings for variable bounds
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
|
2026-01-28 19:42:40 -08:00 |
|
Lev Nachmanson
|
2ac78b6def
|
revive nlsat check_lemma()
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2026-01-25 11:38:25 -10:00 |
|
Copilot
|
2436943794
|
Standardize for-loop increments to prefix form (++i) (#8199)
* Initial plan
* Convert postfix to prefix increment in for loops
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Fix member variable increment conversion bug
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Update API generator to produce prefix increments
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
|
2026-01-14 19:55:31 -08:00 |
|
Lev Nachmanson
|
7de648ff81
|
remove unused *_signed_project() methods
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-12-02 18:46:16 -10:00 |
|
Nikolaj Bjorner
|
233184944c
|
fix build warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2025-11-26 09:43:52 -08:00 |
|
Lev Nachmanson
|
4b5fb2607f
|
try reordering before analyzing bounds
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-11-24 13:08:52 -10:00 |
|
Lev Nachmanson
|
9529275e2f
|
parameter correct order experiment
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-11-24 13:08:52 -10:00 |
|
Lev Nachmanson
|
97f7e6fac4
|
remove the debug print
|
2025-11-24 07:54:06 -10:00 |
|
Lev Nachmanson
|
cc3328be8d
|
disable add_zero_disc(disc) by default
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-11-24 06:41:06 -10:00 |
|
Lev Nachmanson
|
784ea42521
|
optionally call add_zero_assumption on a vanishing discriminant
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-11-24 06:41:06 -10:00 |
|
Lev Nachmanson
|
ac58f53703
|
restart projection when found a non-trivial nullified polynomial, and remove is_square_free
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-11-24 06:41:06 -10:00 |
|
Lev Nachmanson
|
82f0cfb7cc
|
refactoring
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-11-24 06:41:06 -10:00 |
|
Lev Nachmanson
|
26a472fb3c
|
remove unused code
|
2025-11-24 06:41:06 -10:00 |
|
Lev Nachmanson
|
0886513de1
|
remve add_zero_assumption from pcs()
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-11-24 06:41:06 -10:00 |
|
Lev Nachmanson
|
fe6b777638
|
improve logging
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-11-24 06:41:06 -10:00 |
|
Lev Nachmanson
|
ebecfb8e6f
|
handle the case with no roots in add_zero_assumption
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-11-24 06:41:06 -10:00 |
|
Lev Nachmanson
|
2768962aa8
|
improve log_lemma
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-11-24 06:41:06 -10:00 |
|
Lev Nachmanson
|
0ee272a9d1
|
log for smtrat
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-11-24 06:41:06 -10:00 |
|
Lev Nachmanson
|
6856a61a83
|
use indexed root expressions id add_zero_assumption
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-11-24 06:41:06 -10:00 |
|
Lev Nachmanson
|
eeb83d48dc
|
add coefficients from the elim_vanishing to m_todo
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-11-24 06:41:06 -10:00 |
|
Lev Nachmanson
|
573ab2bbbf
|
remove unused method
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-11-24 06:41:06 -10:00 |
|
Lev Nachmanson
|
c6eb9d7eb7
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-11-24 06:41:06 -10:00 |
|
Lev Nachmanson
|
8e4557647f
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-11-24 06:41:06 -10:00 |
|
Lev Nachmanson
|
847f471015
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-11-24 06:41:06 -10:00 |
|
Lev Nachmanson
|
36c711d95b
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-11-24 06:41:06 -10:00 |
|
Lev Nachmanson
|
c8959dc67a
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-11-24 06:41:06 -10:00 |
|
Lev Nachmanson
|
7eb18771c2
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-11-24 06:41:06 -10:00 |
|
Lev Nachmanson
|
bce477530a
|
t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2025-11-24 06:41:06 -10:00 |
|