mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

ensure parameters are updated and ensure that global use of auto-config is not obscured by smt.auto-config scoping

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-10-07 11:00:45 -07:00
parent c7e27fb2d9
commit 4ea3ed7e27
5 changed files with 28 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

25
src/qe/qe.cpp
View file

@ -2238,8 +2238,7 @@ namespace qe {
m_params(p),
m_trail(m),
m_qe(0),
m_assumption(m.mk_true()),
m_use_new_qe(true)
m_assumption(m.mk_true())
{
}
@ -2261,12 +2260,6 @@ namespace qe {
}
void expr_quant_elim::updt_params(params_ref const& p) {
bool r = p.get_bool("use_neq_qe", m_use_new_qe);
if (r != m_use_new_qe) {
dealloc(m_qe);
m_qe = 0;
m_use_new_qe = r;
}
init_qe();
m_qe->updt_params(p);
}
@ -2274,7 +2267,6 @@ namespace qe {
void expr_quant_elim::collect_param_descrs(param_descrs& r) {
r.insert("eliminate_variables_as_block", CPK_BOOL,
"(default: true) eliminate variables as a block (true) or one at a time (false)");
// r.insert("use_new_qe", CPK_BOOL, "(default: true) invoke quantifier engine based on abstracted solver");
}
void expr_quant_elim::init_qe() {
@ -2504,7 +2496,7 @@ namespace qe {
class simplify_solver_context : public i_solver_context {
ast_manager& m;
smt_params m_fparams;
smt_params m_fparams;
app_ref_vector* m_vars;
expr_ref* m_fml;
ptr_vector<contains_app> m_contains;
@ -2520,6 +2512,10 @@ namespace qe {
add_plugin(mk_arith_plugin(*this, false, m_fparams));
}
void updt_params(params_ref const& p) {
m_fparams.updt_params(p);
}
virtual ~simplify_solver_context() { reset(); }
void solve(expr_ref& fml, app_ref_vector& vars) {
@ -2610,6 +2606,10 @@ namespace qe {
public:
impl(ast_manager& m) : m(m), m_ctx(m) {}
void updt_params(params_ref const& p) {
m_ctx.updt_params(p);
}
bool reduce_quantifier(
quantifier * old_q,
expr * new_body,
@ -2673,6 +2673,10 @@ namespace qe {
return imp->reduce_quantifier(old_q, new_body, new_patterns, new_no_patterns, result, result_pr);
}
void simplify_rewriter_cfg::updt_params(params_ref const& p) {
imp->updt_params(p);
}
bool simplify_rewriter_cfg::pre_visit(expr* e) {
if (!is_quantifier(e)) return true;
quantifier * q = to_quantifier(e);
@ -2680,7 +2684,6 @@ namespace qe {
}
void simplify_exists(app_ref_vector& vars, expr_ref& fml) {
smt_params params;
ast_manager& m = fml.get_manager();
simplify_solver_context ctx(m);
ctx.solve(fml, vars);