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
Nikolaj Bjorner
62b3668beb
remove set cardinality operators from array theory. Make final-check use priority levels
...
Issue #7502 shows that running nlsat eagerly during final check can block quantifier instantiation.
To give space for quantifier instances we introduce two levels for final check such that nlsat is only applied in the second and final level.
2025-11-26 15:35:19 -08:00
Nikolaj Bjorner
28dc71c75e
fix second byref to bool
2025-11-26 14:40:11 -08:00
Nikolaj Bjorner
ed8b92411e
remove references to set_has_size
2025-11-26 13:57:24 -08:00
Nikolaj Bjorner
fab414a7ab
use c_bool instead of c_int for sign
2025-11-26 13:55:06 -08:00
