mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2014-10-08 10:56:20 +01:00
parent 7fc95aff3c 4ea3ed7e27
commit 4370d40dd8
5 changed files with 28 additions and 17 deletions
Show stats 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);

7
src/qe/qe.h
View file

@ -275,13 +275,12 @@ namespace qe {
class expr_quant_elim {
ast_manager& m;
smt_params const& m_fparams;
smt_params const& m_fparams;
params_ref m_params;
expr_ref_vector m_trail;
obj_map<expr,expr*> m_visited;
quant_elim* m_qe;
expr* m_assumption;
bool m_use_new_qe;
public:
expr_quant_elim(ast_manager& m, smt_params const& fp, params_ref const& p = params_ref());
~expr_quant_elim();
@ -372,6 +371,8 @@ namespace qe {
bool pre_visit(expr* e);
void updt_params(params_ref const& p);
};
class simplify_rewriter_star : public rewriter_tpl<simplify_rewriter_cfg> {
@ -380,6 +381,8 @@ namespace qe {
simplify_rewriter_star(ast_manager& m):
rewriter_tpl<simplify_rewriter_cfg>(m, false, m_cfg),
m_cfg(m) {}
void updt_params(params_ref const& p) { m_cfg.updt_params(p); }
};
};

9
src/qe/qe_sat_tactic.cpp
View file

@ -74,6 +74,7 @@ namespace qe {
is_relevant_default m_is_relevant;
mk_atom_default m_mk_atom;
th_rewriter m_rewriter;
simplify_rewriter_star m_qe_rw;
expr_strong_context_simplifier m_ctx_rewriter;
class solver_context : public i_solver_context {
@ -218,6 +219,7 @@ namespace qe {
m_Ms(m),
m_assignments(m),
m_rewriter(m),
m_qe_rw(m),
m_ctx_rewriter(m_fparams, m) {
m_fparams.m_model = true;
}
@ -256,10 +258,9 @@ namespace qe {
ptr_vector<expr> fmls;
goal->get_formulas(fmls);
m_fml = m.mk_and(fmls.size(), fmls.c_ptr());
TRACE("qe", tout << "input: " << mk_pp(m_fml,m) << "\n";);
simplify_rewriter_star rw(m);
TRACE("qe", tout << "input: " << mk_pp(m_fml,m) << "\n";);
expr_ref tmp(m);
rw(m_fml, tmp);
m_qe_rw(m_fml, tmp);
m_fml = tmp;
TRACE("qe", tout << "reduced: " << mk_pp(m_fml,m) << "\n";);
skolemize_existential_prefix();
@ -305,6 +306,8 @@ namespace qe {
m_projection_mode_param = p.get_bool("projection_mode", m_projection_mode_param);
m_strong_context_simplify_param = p.get_bool("strong_context_simplify", m_strong_context_simplify_param);
m_ctx_simplify_local_param = p.get_bool("strong_context_simplify_local", m_ctx_simplify_local_param);
m_fparams.updt_params(p);
m_qe_rw.updt_params(p);
}
virtual void collect_param_descrs(param_descrs & r) {

1
src/qe/qe_tactic.cpp
View file

@ -36,6 +36,7 @@ class qe_tactic : public tactic {
}
void updt_params(params_ref const & p) {
m_fparams.updt_params(p);
m_fparams.m_nlquant_elim = p.get_bool("qe_nonlinear", false);
m_qe.updt_params(p);
}

3
src/smt/params/smt_params.cpp
View file

@ -19,10 +19,11 @@ Revision History:
#include"smt_params.h"
#include"smt_params_helper.hpp"
#include"model_params.hpp"
#include"gparams.h"
void smt_params::updt_local_params(params_ref const & _p) {
smt_params_helper p(_p);
m_auto_config = p.auto_config();
m_auto_config = p.auto_config() && gparams::get_value("auto_config") == "true"; // auto-config is not scoped by smt in gparams.
m_random_seed = p.random_seed();
m_relevancy_lvl = p.relevancy();
m_ematching = p.ematching();