Nikolaj Bjorner
2708635b94
remove experiment from pr
2025-05-19 03:24:14 -07:00
Nikolaj Bjorner
d14bffc5ac
allows setting simplifier factory independently of whether solver has been allocated.
...
Instances, such as #7484 can be solved faster by either having authors rewrite benchmarks or by using incremental pre-processing. You can add incremental pre-processing to the SMT solver by using the command
```
(set-simplifier (then simplify propagate-values solve-eqs elim-unconstrained simplify))
```
This command can be invoked any time prior to push or adding assertions.
The effect of the command is that it adds an incremental pre-processing pass to check-sat invocations that is potentially more powerful than the default pre-processing. The default pre-processing functionality is not touched mainly to avoid instability against functionality that is already built around its behavior.
2025-05-19 03:22:00 -07:00
Nikolaj Bjorner
75fe46b8c0
Update prd.yml
2025-05-18 16:08:54 -07:00
Nikolaj Bjorner
17e50c6f5a
Merge branch 'master' into pr
2025-05-17 17:33:27 -07:00
Nikolaj Bjorner
a7fbddd049
Update prd.yml
2025-05-17 17:24:14 -07:00
Nikolaj Bjorner
fd8f5d296a
fix
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-05-17 17:19:43 -07:00
Nikolaj Bjorner
610e3b5b17
missing text
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-05-17 17:19:43 -07:00
Nikolaj Bjorner
b009ed38c8
Create prd.yml
2025-05-17 17:19:43 -07:00
Nikolaj Bjorner
33732f839f
initial stab at randomizer
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-05-17 17:15:40 -07:00
Nikolaj Bjorner
ad02d18e63
add prd ( #7649 )
...
* add prd
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* missing text
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix #7647
* fix #7647 - with respect to scope level
---------
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-05-17 17:07:03 -07:00
Nikolaj Bjorner
b0c8a5cf21
fix #7647 - with respect to scope level
2025-05-16 21:22:08 -07:00
Nikolaj Bjorner
3fac441f3d
fix #7647
2025-05-16 21:17:06 -07:00
Nikolaj Bjorner
33812201cb
Create prd.yml
2025-05-16 14:15:52 -07:00
Nikolaj Bjorner
9988a93f7f
fix
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-05-16 14:11:58 -07:00
Nikolaj Bjorner
73bf37398d
missing text
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-05-16 14:09:28 -07:00
Nikolaj Bjorner
8e6a650c7a
add prd
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-05-16 14:02:26 -07:00
Nikolaj Bjorner
47c12f9a18
refactoring to use for-range
2025-05-15 10:57:46 -07:00
Nikolaj Bjorner
7ebe7c46b9
remove stale API #7648
2025-05-15 10:57:46 -07:00
Steffen Smolka
0b26f7e0ee
Add support for building Z3 using Bazel. ( #7646 )
...
Signed-off-by: Steffen Smolka <smolkaj@google.com>
2025-05-15 08:47:29 -07:00
Lev Nachmanson
f680242620
adjust the frequency of dio calls
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-05-14 08:17:39 -07:00
Lev Nachmanson
15a3818fce
cleanup in dioph_eq.cpp
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-05-13 14:57:21 -07:00
Nikolaj Bjorner
1109139359
move to readme-cmake
2025-05-13 14:36:20 -07:00
Nikolaj Bjorner
ce1535119d
include some build cheat sheet
2025-05-13 14:34:47 -07:00
Nikolaj Bjorner
a5a2a13d34
update version number
2025-05-13 14:32:35 -07:00
Nikolaj Bjorner
0d3c29a250
handle larger buffers
2025-05-13 14:11:59 -07:00
Lev Nachmanson
6b32aaed10
remove slack heuristic
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-05-12 14:02:17 -07:00
Lev Nachmanson
a5e5d4dbd3
testing
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-05-12 14:02:17 -07:00
Lev Nachmanson
bbaec0bf95
trying randomly shuffle the indices in the slack utilization
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-05-12 14:02:17 -07:00
Lev Nachmanson
52241b6474
some refactoring of lar_solver.h
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-05-12 14:02:17 -07:00
Lev Nachmanson
fef954c028
shring lar_solver.h
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-05-12 14:02:17 -07:00
Lev Nachmanson
4abd9843a0
fix the build
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-05-12 14:02:17 -07:00
Lev Nachmanson
e3f5e8c8a6
restore lar_solver::add_named_var
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-05-12 14:02:17 -07:00
Lev Nachmanson
b375faa77c
continue PIMPL refactor in lar_solver
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-05-12 14:02:17 -07:00
Lev Nachmanson
b7ffcb7e61
implement imp of lar_solver as lar_solver::imp
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-05-12 14:02:17 -07:00
Lev Nachmanson
39955f1d04
remove a function from lar_solver
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-05-12 14:02:17 -07:00
Lev Nachmanson
4e56834b76
test
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-05-12 14:02:17 -07:00
Lev Nachmanson
a527667fc0
shuffle more functionality from lar_solver.h to lar_solver::imp
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-05-12 14:02:17 -07:00
Lev Nachmanson
c81eb74c93
apply the slack idea in a loop
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-05-12 14:02:17 -07:00
Lev Nachmanson
e041fe95bc
slack
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-05-12 14:02:17 -07:00
Nikolaj Bjorner
7ca94e8fef
add E-matching to EUF completion
2025-05-10 16:15:04 -07:00
Nikolaj Bjorner
9232ef579c
remove copy of LICENSE.txt - pypi doesn't take it
2025-05-09 16:53:45 -07:00
Nikolaj Bjorner
49dffaed39
enable pypi
2025-05-09 15:37:19 -07:00
Nikolaj Bjorner
b54ed38cea
enable pypi
2025-05-09 13:15:42 -07:00
Nikolaj Bjorner
59a7e007a4
disable pypi
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-05-09 08:26:38 -07:00
Nikolaj Bjorner
d4b622e239
update version number
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-05-09 08:25:40 -07:00
Nikolaj Bjorner
a51239c641
update namespace, hoist exported functions outside of embedded namespace
2025-05-07 15:57:47 -07:00
Nikolaj Bjorner
644118660f
list euf dependency in api cmakefile
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-05-07 15:47:03 -07:00
Nikolaj Bjorner
eca5cd1841
mark virtual methods as override
2025-05-07 15:24:20 -07:00
Nikolaj Bjorner
9a299eb9ff
move mam to euf
2025-05-07 14:38:59 -07:00
Nikolaj Bjorner
0e4c033e30
fix #7639
2025-05-03 11:06:25 -07:00
