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

option to control array_der in qe_lite

Browse source
This commit is contained in:
Arie Gurfinkel 2017-07-31 14:19:16 -04:00
parent 7670b49ada
commit 331eec8a05
2 changed files with 13 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/qe/qe_lite.cpp
View file

@ -2342,6 +2342,7 @@ private:
elim_star m_elim_star; elim_star m_elim_star;
th_rewriter m_rewriter; th_rewriter m_rewriter;
bool m_use_array_der;
bool has_unique_non_ground(expr_ref_vector const& fmls, unsigned& index) { bool has_unique_non_ground(expr_ref_vector const& fmls, unsigned& index) {
index = fmls.size(); index = fmls.size();
if (index <= 1) { if (index <= 1) {
@ -2359,13 +2360,14 @@ private:
} }
public: public:
impl(ast_manager & m, params_ref const & p): impl(ast_manager & m, params_ref const & p, bool use_array_der):
m(m), m(m),
m_der(m, p), m_der(m, p),
m_fm(m), m_fm(m),
m_array_der(m), m_array_der(m),
m_elim_star(*this), m_elim_star(*this),
m_rewriter(m) {} m_rewriter(m),
m_use_array_der(use_array_der) {}
void operator()(app_ref_vector& vars, expr_ref& fml) { void operator()(app_ref_vector& vars, expr_ref& fml) {
if (vars.empty()) { if (vars.empty()) {
@ -2445,14 +2447,15 @@ public:
m_array_der.set_is_variable_proc(is_var); m_array_der.set_is_variable_proc(is_var);
m_der(fmls); m_der(fmls);
m_fm(fmls); m_fm(fmls);
m_array_der(fmls); // AG: disalble m_array_der() since it interferes with other array handling
if (m_use_array_der) m_array_der(fmls);
TRACE("qe_lite", for (unsigned i = 0; i < fmls.size(); ++i) tout << mk_pp(fmls[i].get(), m) << "\n";); TRACE("qe_lite", for (unsigned i = 0; i < fmls.size(); ++i) tout << mk_pp(fmls[i].get(), m) << "\n";);
} }
}; };
qe_lite::qe_lite(ast_manager & m, params_ref const & p) { qe_lite::qe_lite(ast_manager & m, params_ref const & p, bool use_array_der) {
m_impl = alloc(impl, m, p); m_impl = alloc(impl, m, p, use_array_der);
} }
qe_lite::~qe_lite() { qe_lite::~qe_lite() {
@ -2484,7 +2487,7 @@ class qe_lite_tactic : public tactic {
imp(ast_manager& m, params_ref const & p): imp(ast_manager& m, params_ref const & p):
m(m), m(m),
m_qe(m, p) m_qe(m, p, true)
{} {}
void checkpoint() { void checkpoint() {

5
src/qe/qe_lite.h
View file

@ -31,7 +31,10 @@ class qe_lite {
class impl; class impl;
impl * m_impl; impl * m_impl;
public: public:
qe_lite(ast_manager & m, params_ref const & p); /**
use_array_der controls whether equalities over array reads are simplified
*/
qe_lite(ast_manager& m, params_ref const & p, bool use_array_der = true);
~qe_lite(); ~qe_lite();