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

@@ -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

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:
+
+    <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 == !(x<y)
+            if (m_arith.is_ge(n1) && m.is_not(n2, t) && m_arith.is_lt(t)) {
+                n2 = to_app(t);
+            }
+            else if (m_arith.is_ge(n2) && m.is_not(n1, t) && m_arith.is_lt(t)) {
+                n1 = to_app(t);
+            }
+            // x+val1 matched to val2, where x is a variable, and
+            // val1, val2 are numerals
+            if (m_arith.is_numeral(n2, val2) && m_arith.is_add(n1, e1, e2) &&
+                m_arith.is_numeral(e2, val1) && is_var(e1)) {
+                val1 = val2 - val1;
+
+                expr_ref num1(m);
+                num1 = m_arith.mk_numeral (val1, val1.is_int());
+                m_pinned.push_back(num1);
+                if (!match_var (to_var(e1), num1)) {
+                    return false;
+                }
+
+                m_todo.pop_back();
+                continue;
+            }
+            else {
+                return false;
+            }
+        }
+
+        unsigned num_args1 = n1->get_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();
+}
+}

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 *, expr *> expr_pair;
+    typedef pair_hash<obj_ptr_hash<expr>, obj_ptr_hash<expr> > expr_pair_hash;
+    typedef hashtable<expr_pair, expr_pair_hash, default_eq<expr_pair> > cache;
+
+    ast_manager &m;
+    arith_util m_arith;
+    expr_ref_vector m_pinned;
+    substitution *        m_subst;
+    svector<expr_pair>    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_ */