* 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
* initial stab at randomizer
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* Create prd.yml
* missing text
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* Update prd.yml
* 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.
* remove experiment from pr
---------
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Add the ability to customize incremental pre-processing simplification for the SMTLIB2 front-end. The main new capability is to use pre-processing tactics in incremental mode that were previously not available. The main new capabilities are
- solve-eqs
- reduce-args
- elim-unconstrained
There are several more. Documentation and exposed simplifiers are populated incrementally. The current set of supported simplifiers can be inspected by using z3 with the --simplifiers flag or referring to https://microsoft.github.io/z3guide/docs/strategies/simplifiers
Some pending features are:
- add the ability to update parameters to simplifiers similar to how tactics can be controlled using parameters.
- expose simplification solvers over the binary API.
