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
Lev Nachmanson
1035c95234
t0
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 11:16:25 -10:00
Lev Nachmanson
52949f2d79
fix the build
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-12-03 06:49:00 -10:00
Copilot
595513611e
Disable C++98 compatibility warnings for Clang builds ( #8060 )
...
* Initial plan
* Disable C++98 compatibility warnings for Clang to fix vcpkg build freeze
Add -Wno-c++98-compat and -Wno-c++98-compat-pedantic flags to prevent
excessive warning output when building with clang-cl or when -Weverything
is enabled. These warnings are not useful for Z3 since it requires C++20.
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>
2025-12-03 08:27:25 -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
a5488cf6e7
fix #8054
...
inherit denominators when evaluating polynomials
2025-11-30 07:51:06 -08:00
Nikolaj Bjorner
3712d1e0f1
fix #8055
2025-11-29 15:39:50 -08:00
Nikolaj Bjorner
ab227c83b2
remove deprecated set_has_size
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-11-27 15:11:59 -08:00
Nikolaj Bjorner
8ba77dfc6b
remove deprecated set_has_size
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-11-27 15:10:20 -08:00
Nikolaj Bjorner
682865df24
remove deprecated set_has_size
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-11-27 15:07:27 -08:00
Nikolaj Bjorner
449ce1a012
remove deprecated set_has_size
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-11-27 15:04:40 -08:00
Josh Berdine
aecf10b3ac
Fix _in vs _out def_API param for Z3_solver_get_levels ( #8050 )
...
Signed-off-by: Josh Berdine <josh@berdine.net>
2025-11-27 15:00:38 -08:00
Nikolaj Bjorner
f98fd2a137
refine givup conditions
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-11-27 14:59:48 -08:00
Nikolaj Bjorner
482fa7dadf
insert theory only once
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-11-27 10:34:01 -08:00
