mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-26 21:16:02 +00:00
Code Activity

Pr (#7654)

Browse source 
* 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>
This commit is contained in:
Nikolaj Bjorner 2025-05-19 03:24:45 -07:00 • committed by GitHub
parent 8d67feef9f
commit c2098b41d6
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 9 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/cmd_context/cmd_context.h
View file

@ -38,6 +38,7 @@ Notes:
#include "solver/solver.h"
#include "solver/check_logic.h"
#include "solver/progress_callback.h"
#include "solver/simplifier_solver.h"
#include "cmd_context/pdecl.h"
#include "cmd_context/tactic_manager.h"
#include "params/context_params.h"
@ -282,6 +283,7 @@ protected:
std::vector<std::string> m_assertion_strings;
ptr_vector<expr> m_assertion_names; // named assertions are represented using boolean variables.
scoped_ptr<var_subst> m_std_subst, m_rev_subst;
simplifier_factory m_simplifier_factory;
struct scope {
unsigned m_func_decls_stack_lim;
@ -429,6 +431,7 @@ public:
void set_initial_value(expr* var, expr* value);
void set_solver_factory(solver_factory * s);
void set_simplifier_factory(simplifier_factory& sf) { m_simplifier_factory = sf; }
void set_check_sat_result(check_sat_result * r) { m_check_sat_result = r; }
check_sat_result * get_check_sat_result() const { return m_check_sat_result.get(); }
check_sat_state cs_state() const;