Nikolaj Bjorner
45f088c89b
add user propagators to opt_solver
2025-10-10 15:36:49 -07:00
Nikolaj Bjorner
f5c217e15b
Add commands for forcing preferences during search
...
Add commands:
(prefer <formula>)
- will instruct case split queue to assign formula to true.
- prefer commands added within a scope are forgotten after leaving the scope.
(reset-preferences)
- resets asserted preferences. Has to be invoked at base level.
This provides functionality related to MathSAT and based on an ask by Tomáš Kolárik who is integrating the functionality with OpenSMT2
2025-10-10 15:36:49 -07:00
Nikolaj Bjorner
670df87460
update clang format
2025-10-10 15:36:43 -07:00
Nikolaj Bjorner
82b28202b2
fix #7952 - make auto-selector detect large bit-vectors so it does't use the datalog engine for hopelessly large tables
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-10-10 15:36:24 -07:00
Nikolaj Bjorner
4c69dc135c
update format
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-10-10 15:36:09 -07:00
Nikolaj Bjorner
d9b28cd485
fix #7956
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-10-10 15:35:39 -07:00
Ruijie Fang
7bece6e473
Correctly distinguish between Lambda and Quantifier in Z3 Java API ( #7955 )
...
* Distinguish between Quantifier and Lambda in AST.java
* Distinguish betwee Lambda and Quantifier in Expr.java
* Make things compile
2025-10-10 15:35:39 -07:00
Nikolaj Bjorner
a9a46f4ac9
add analysis
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-10-10 15:35:38 -07:00
Nikolaj Bjorner
151f007f23
add analysis
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-10-10 15:35:38 -07:00
Nikolaj Bjorner
5b7d30357f
add analysis
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-10-10 15:35:38 -07:00
Nikolaj Bjorner
27bcca72f1
fix #7948
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-10-10 15:35:37 -07:00
Nikolaj Bjorner
201731baf1
fix #7948
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-10-10 15:35:36 -07:00
Wael Boutglay
7fdc5ab682
Add missing ::z3::sdiv to z3++.h ( #7947 )
2025-10-10 15:35:36 -07:00
Nikolaj Bjorner
95ab02aa4f
propagate value initialization to atoms
2025-10-10 15:35:35 -07:00
Nikolaj Bjorner
10dce45d8b
remove stale comment
2025-10-10 15:35:35 -07:00
Arie Gurfinkel
599e9da8a9
optionally limit linearization
2025-10-06 16:40:06 -04:00
Nikolaj Bjorner
5846570012
gcd reduce and use c().val for sign constraints
2025-10-01 18:42:34 -07:00
Nikolaj Bjorner
538480b4f8
limit sos loop
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-09-30 13:51:05 -07:00
Nikolaj Bjorner
3b1ac52ff9
generate more proper proof format
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-09-30 07:42:27 -07:00
Nikolaj Bjorner
4162d89170
move to lex-leading resolvents
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-09-29 19:21:30 -07:00
Nikolaj Bjorner
fa2d7a1c57
fix introduced memory leak
2025-09-29 18:33:47 -07:00
Nikolaj Bjorner
c3281f08ef
wip
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-09-29 16:14:59 -07:00
Nikolaj Bjorner
69a9d9f0b0
move to global occurs list, throttle saturation lemmas based on monomial size
2025-09-29 08:57:49 -07:00
Nikolaj Bjorner
eff17a6252
notes
2025-09-29 04:52:51 -07:00
Nikolaj Bjorner
81cffee736
add factorization
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-09-29 04:29:54 -07:00
Nikolaj Bjorner
184fae6fcc
wip stellensatz
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-09-28 23:06:35 +03:00
Nikolaj Bjorner
72f5fe1f7f
logging and bug fixes
2025-09-28 18:16:23 +03:00
Nikolaj Bjorner
c621f59740
fix bug with saturation of monotonicity, and add more general case for downward saturation
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-09-28 14:36:53 +03:00
Nikolaj Bjorner
e684537b01
retrieve both bounds and explanations recursively
2025-09-28 13:46:22 +03:00
Nikolaj Bjorner
360de4af03
add basic linearization as pre-processing and refinement
2025-09-28 12:27:13 +03:00
Nikolaj Bjorner
a12f4b9686
prepare for enforcing cheap incremental linearization axioms
2025-09-27 20:33:53 +03:00
Nikolaj Bjorner
ad11e4626e
household
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-09-27 16:59:22 +03:00
Nikolaj Bjorner
88844a84aa
mul-saturation wip
...
fixup conflict explanations in mul_saturation, add parameter to enable it, add statistics
2025-09-27 12:17:40 +03:00
Nikolaj Bjorner
ad2c97a4df
remove debug
2025-09-26 23:05:21 +03:00
Nikolaj Bjorner
ef27e38d5f
v0.1 of nla saturation
2025-09-26 23:05:02 +03:00
Nikolaj Bjorner
6adb234673
outline for adding monomials
2025-09-26 12:03:26 +03:00
Nikolaj Bjorner
a6ea667776
fix access to k'th emon
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-09-23 11:31:23 +03:00
Nikolaj Bjorner
08ef4de4a6
introduce shuffle
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-09-23 11:24:50 +03:00
Nikolaj Bjorner
3c9ab28731
remove secondary random traversal
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-09-23 11:16:16 +03:00
Nikolaj Bjorner
18d7231c4c
latent bug found with relevancy filtering
2025-09-23 10:46:33 +03:00
Nikolaj Bjorner
0ed37be40f
missing update
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-09-22 15:30:32 +03:00
Nikolaj Bjorner
9579064671
setup
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-09-22 15:19:40 +03:00
Nikolaj Bjorner
b02b0cf31f
fix build
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-09-22 14:44:50 +03:00
Nikolaj Bjorner
db5a991257
more imp notes and relevancy experiment
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-09-22 12:44:50 +03:00
Nikolaj Bjorner
0a0e925f27
updates
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-09-22 11:26:48 +03:00
Nikolaj Bjorner
fae67b79b7
outline
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-09-22 10:55:08 +03:00
Nikolaj Bjorner
f5c28a0b76
household cleanup
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-09-22 03:58:04 +03:00
Nikolaj Bjorner
e26f7b900c
fix unsound axiom for lower-bounding
2025-09-21 19:24:13 +03:00
Nikolaj Bjorner
dcdae5a61c
add smt debug output for nla_core
2025-09-21 19:24:13 +03:00
Nikolaj Bjorner
ce53e06e29
Par ( #7945 )
...
* port parallel
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* updates
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* update smt-parallel
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* cleanup
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* neat
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* configuration parameter renaming
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* config parameters
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---------
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-09-21 10:11:04 +03:00
