From ac6ca4d334ae957759c911cacb5eeb37b0100309 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Tue, 20 Jun 2017 21:34:49 -0400 Subject: [PATCH 1/3] factored out is_variable_proc to a header file --- src/qe/qe_lite.cpp | 39 +--------------------------- src/qe/qe_vartest.h | 63 +++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 64 insertions(+), 38 deletions(-) create mode 100644 src/qe/qe_vartest.h diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp index 0e7db9971..62f6c41a6 100644 --- a/src/qe/qe_lite.cpp +++ b/src/qe/qe_lite.cpp @@ -36,44 +36,7 @@ Revision History: #include "cooperate.h" #include "datatype_decl_plugin.h" -class is_variable_proc { -public: - virtual bool operator()(expr* e) const = 0; -}; - -class is_variable_test : public is_variable_proc { - enum is_var_kind { BY_VAR_SET, BY_VAR_SET_COMPLEMENT, BY_NUM_DECLS }; - uint_set m_var_set; - unsigned m_num_decls; - is_var_kind m_var_kind; -public: - is_variable_test(uint_set const& vars, bool index_of_bound) : - m_var_set(vars), - m_num_decls(0), - m_var_kind(index_of_bound?BY_VAR_SET:BY_VAR_SET_COMPLEMENT) {} - - is_variable_test(unsigned num_decls) : - m_num_decls(num_decls), - m_var_kind(BY_NUM_DECLS) {} - - virtual bool operator()(expr* e) const { - if (!is_var(e)) { - return false; - } - unsigned idx = to_var(e)->get_idx(); - switch(m_var_kind) { - case BY_VAR_SET: - return m_var_set.contains(idx); - case BY_VAR_SET_COMPLEMENT: - return !m_var_set.contains(idx); - case BY_NUM_DECLS: - return idx < m_num_decls; - } - UNREACHABLE(); - return false; - } -}; - +#include "qe_vartest.h" namespace eq { class der { diff --git a/src/qe/qe_vartest.h b/src/qe/qe_vartest.h new file mode 100644 index 000000000..b2b4be649 --- /dev/null +++ b/src/qe/qe_vartest.h @@ -0,0 +1,63 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + qe_vartest.h + +Abstract: + + Utilities for quantifiers. + +Author: + + Nikolaj Bjorner (nbjorner) 2013-08-28 + +Revision History: + +--*/ +#ifndef QE_VARTEST_H_ +#define QE_VARTEST_H_ + +#include "ast.h" +#include "uint_set.h" + +class is_variable_proc { +public: + virtual bool operator()(expr* e) const = 0; +}; + +class is_variable_test : public is_variable_proc { + enum is_var_kind { BY_VAR_SET, BY_VAR_SET_COMPLEMENT, BY_NUM_DECLS }; + uint_set m_var_set; + unsigned m_num_decls; + is_var_kind m_var_kind; +public: + is_variable_test(uint_set const& vars, bool index_of_bound) : + m_var_set(vars), + m_num_decls(0), + m_var_kind(index_of_bound?BY_VAR_SET:BY_VAR_SET_COMPLEMENT) {} + + is_variable_test(unsigned num_decls) : + m_num_decls(num_decls), + m_var_kind(BY_NUM_DECLS) {} + + virtual bool operator()(expr* e) const { + if (!is_var(e)) { + return false; + } + unsigned idx = to_var(e)->get_idx(); + switch(m_var_kind) { + case BY_VAR_SET: + return m_var_set.contains(idx); + case BY_VAR_SET_COMPLEMENT: + return !m_var_set.contains(idx); + case BY_NUM_DECLS: + return idx < m_num_decls; + } + UNREACHABLE(); + return false; + } +}; + +#endif From 9f73359a86c634fc31a60db2c0a2c997063df47d Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Tue, 20 Jun 2017 21:50:35 -0400 Subject: [PATCH 2/3] improve comments --- src/qe/qe_lite.cpp | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp index 62f6c41a6..e84ab5cb8 100644 --- a/src/qe/qe_lite.cpp +++ b/src/qe/qe_lite.cpp @@ -788,12 +788,13 @@ namespace ar { } /** - Ex A. A[x] = t & Phi where x \not\in A, t. A \not\in t, x + Ex A. A[x] = t & Phi[A] where x \not\in A, t. A \not\in t, x => Ex A. Phi[store(A,x,t)] + (Not implemented) Perhaps also: - Ex A. store(A,y,z)[x] = t & Phi where x \not\in A, t, y, z, A \not\in y z, t + Ex A. store(A,y,z)[x] = t & Phi[A] where x \not\in A, t, y, z, A \not\in y z, t => Ex A, v . (x = y => z = t) & Phi[store(store(A,x,t),y,v)] @@ -822,7 +823,8 @@ namespace ar { expr_safe_replace rep(m); rep.insert(A, B); expr_ref tmp(m); - std::cout << mk_pp(e1, m) << " = " << mk_pp(e2, m) << "\n"; + TRACE("qe_lite", + tout << mk_pp(e1, m) << " = " << mk_pp(e2, m) << "\n";); for (unsigned j = 0; j < conjs.size(); ++j) { if (i == j) { conjs[j] = m.mk_true(); From ef62621f50eb71a13b9485280a5115e0aa0e3575 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Tue, 20 Jun 2017 21:51:08 -0400 Subject: [PATCH 3/3] make qe_lite prefer simpler definitions --- src/qe/qe_lite.cpp | 40 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 40 insertions(+) diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp index e84ab5cb8..ce182a97b 100644 --- a/src/qe/qe_lite.cpp +++ b/src/qe/qe_lite.cpp @@ -49,6 +49,7 @@ namespace eq { ptr_vector m_map; int_vector m_pos2var; + int_vector m_var2pos; ptr_vector m_inx2var; unsigned_vector m_order; expr_ref_vector m_subst_map; @@ -541,6 +542,7 @@ namespace eq { largest_vinx = 0; m_map.reset(); m_pos2var.reset(); + m_var2pos.reset(); m_inx2var.reset(); m_pos2var.reserve(num_args, -1); @@ -560,10 +562,48 @@ namespace eq { m_map[idx] = t; m_inx2var[idx] = v; m_pos2var[i] = idx; + m_var2pos.reserve(idx + 1, -1); + m_var2pos[idx] = i; def_count++; largest_vinx = std::max(idx, largest_vinx); m_new_exprs.push_back(t); } + else if (!m.is_value(m_map[idx])) { + // check if the new definition is simpler + expr *old_def = m_map[idx]; + + // -- prefer values + if (m.is_value(t)) { + m_pos2var[m_var2pos[idx]] = -1; + m_pos2var[i] = idx; + m_var2pos[idx] = i; + m_map[idx] = t; + m_new_exprs.push_back(t); + } + // -- prefer ground + else if (is_app(t) && to_app(t)->is_ground() && + (!is_app(old_def) || + !to_app(old_def)->is_ground())) { + m_pos2var[m_var2pos[idx]] = -1; + m_pos2var[i] = idx; + m_var2pos[idx] = i; + m_map[idx] = t; + m_new_exprs.push_back(t); + } + // -- prefer constants + else if (is_uninterp_const(t) + /* && !is_uninterp_const(old_def) */){ + m_pos2var[m_var2pos[idx]] = -1; + m_pos2var[i] = idx; + m_var2pos[idx] = i; + m_map[idx] = t; + m_new_exprs.push_back(t); + } + TRACE ("qe_def", + tout << "Replacing definition of VAR " << idx << " from " + << mk_pp(old_def, m) << " to " << mk_pp(t, m) + << " inferred from: " << mk_pp(args[i], m) << "\n";); + } } } }