From a1efb88318ec7182b0845db5be465d1856af39c9 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Wed, 27 Dec 2017 12:54:35 -0500 Subject: [PATCH] Semantic matcher Extends matcher with rewrites based on semantics of arithmetic operations Like matcher, but uses arithmetic and logic rewrites to try to get a semantic match. --- src/muz/spacer/CMakeLists.txt | 2 + src/muz/spacer/spacer_sem_matcher.cpp | 147 ++++++++++++++++++++++++++ src/muz/spacer/spacer_sem_matcher.h | 69 ++++++++++++ 3 files changed, 218 insertions(+) create mode 100644 src/muz/spacer/spacer_sem_matcher.cpp create mode 100644 src/muz/spacer/spacer_sem_matcher.h diff --git a/src/muz/spacer/CMakeLists.txt b/src/muz/spacer/CMakeLists.txt index f27f6e726..16ce3e4f9 100644 --- a/src/muz/spacer/CMakeLists.txt +++ b/src/muz/spacer/CMakeLists.txt @@ -21,6 +21,8 @@ z3_add_component(spacer spacer_mev_array.cpp spacer_qe_project.cpp spacer_term_graph.cpp + spacer_sem_matcher.cpp + spacer_quant_generalizer.cpp COMPONENT_DEPENDENCIES arith_tactics core_tactics diff --git a/src/muz/spacer/spacer_sem_matcher.cpp b/src/muz/spacer/spacer_sem_matcher.cpp new file mode 100644 index 000000000..f3c2af8a9 --- /dev/null +++ b/src/muz/spacer/spacer_sem_matcher.cpp @@ -0,0 +1,147 @@ +/*++ +Copyright (c) 2006 Microsoft Corporation and Arie Gurfinkel + +Module Name: + + sem_matcher.cpp + +Abstract: + + + +Author: + + Leonardo de Moura (leonardo) 2008-02-02. + Arie Gurfinkel + +Revision History: + +--*/ +#include "muz/spacer/spacer_sem_matcher.h" + +namespace spacer { + +sem_matcher::sem_matcher(ast_manager &man) : m(man), m_arith(m), m_pinned(m) {} + +bool sem_matcher::match_var (var *v, expr *e) { + expr_offset r; + if (m_subst->find(v, 0, r)) { + if (!m.are_equal(r.get_expr(), e)) { + return false; + } + } + else { + m_subst->insert(v, 0, expr_offset(e, 1)); + } + return true; +} +bool sem_matcher::operator()(expr * e1, expr * e2, substitution & s, bool &pos) { + reset(); + m_subst = &s; + m_todo.push_back(expr_pair(e1, e2)); + + // true on the first run through the loop + bool top = true; + pos = true; + while (!m_todo.empty()) { + expr_pair const & p = m_todo.back(); + + if (is_var(p.first)) { + if (!match_var(to_var(p.first), p.second)) { + return false; + } + m_todo.pop_back(); + top = false; + continue; + } + + + if (is_var(p.second)) + return false; + if (!is_app(p.first)) + return false; + if (!is_app(p.second)) + return false; + + app * n1 = to_app(p.first); + app * n2 = to_app(p.second); + + expr *t = nullptr; + + // strip negation + if (top && n1->get_decl() != n2->get_decl()) { + if (m.is_not(n1, t) && !m.is_not(n2) && is_app(t) && + to_app(t)->get_decl() == n2->get_decl()) { + pos = false; + n1 = to_app(e1); + } + else if (!m.is_not(n1) && m.is_not(n2, t) && is_app(t) && + to_app(t)->get_decl() == n1->get_decl()) { + pos = false; + n2 = to_app(t); + } + } + top = false; + + if (n1->get_decl() != n2->get_decl()) { + expr *e1 = nullptr, *e2 = nullptr; + rational val1, val2; + + // x<=y == !(x>y) + if (m_arith.is_le(n1) && m.is_not(n2, t) && m_arith.is_gt(t)) { + n2 = to_app(t); + } + else if (m_arith.is_le(n2) && m.is_not(n1, t) && m_arith.is_gt(t)) { + n1 = to_app(t); + } + // x>=y == !(xget_num_args(); + if (num_args1 != n2->get_num_args()) + return false; + + m_todo.pop_back(); + + if (num_args1 == 0) + continue; + + unsigned j = num_args1; + while (j > 0) { + --j; + m_todo.push_back(expr_pair(n1->get_arg(j), n2->get_arg(j))); + } + } + return true; +} + +void sem_matcher::reset() { + m_todo.reset(); + m_pinned.reset(); +} +} diff --git a/src/muz/spacer/spacer_sem_matcher.h b/src/muz/spacer/spacer_sem_matcher.h new file mode 100644 index 000000000..7d169166e --- /dev/null +++ b/src/muz/spacer/spacer_sem_matcher.h @@ -0,0 +1,69 @@ +/*++ +Copyright (c) 2006 Microsoft Corporation and Arie Gurfinkel + +Module Name: + + sem_matcher.h + +Abstract: + + Semantic matcher + +Author: + + Leonardo de Moura (leonardo) 2008-02-02. + Arie Gurfinkel + +Revision History: + +--*/ +#ifndef SPACER_SEM_MATCHER_H_ +#define SPACER_SEM_MATCHER_H_ + +#include "ast/substitution/substitution.h" +#include "ast/arith_decl_plugin.h" +#include "util/hashtable.h" + +namespace spacer { +/** + \brief Functor for matching expressions. +*/ +class sem_matcher { + typedef std::pair expr_pair; + typedef pair_hash, obj_ptr_hash > expr_pair_hash; + typedef hashtable > cache; + + ast_manager &m; + arith_util m_arith; + expr_ref_vector m_pinned; + substitution * m_subst; + svector m_todo; + + void reset(); + + bool match_var(var *v, expr *e); +public: + sem_matcher(ast_manager &man); + + /** + \brief Return true if e2 is an instance of e1. + In case of success (result is true), it will store the substitution that makes e1 equals to e2 into s. + Sets pos to true if the match is positive and to false if it is negative (i.e., e1 equals !e2) + + For example: + 1) e1 = f(g(x), x), e2 = f(g(h(a)), h(a)) + The result is true, and s will contain x -> h(a) + + 2) e1 = f(a, x) e2 = f(x, a) + The result is false. + + 3) e1 = f(x, x) e2 = f(y, a) + The result is false + + 4) e1 = f(x, y) e2 = f(h(z), a) + The result is true, and s contains x->h(z) and y->a + */ + bool operator()(expr * e1, expr * e2, substitution & s, bool &pos); +}; +} +#endif /* SPACER_SEM_MATCHER_H_ */