QEL: Fast Approximated Quantifier Elimination

src/ast/CMakeLists.txt

@@ -3,6 +3,7 @@ z3_add_component(ast
     act_cache.cpp
     arith_decl_plugin.cpp
     array_decl_plugin.cpp
+    array_peq.cpp
     ast.cpp
     ast_ll_pp.cpp
     ast_lt.cpp

src/ast/array_peq.cpp

@@ -0,0 +1,88 @@
+#include "ast/array_peq.h"
+
+#define PARTIAL_EQ "!partial_eq"
+bool is_partial_eq(const func_decl *f) {
+    SASSERT(f);
+    return f->get_name() == PARTIAL_EQ;
+}
+
+bool is_partial_eq(const app *a) {
+    SASSERT(a);
+    return is_partial_eq(a->get_decl());
+}
+
+app_ref mk_peq(expr *e0, expr *e1, vector<expr_ref_vector> const &indices,
+               ast_manager &m) {
+    peq p(e0, e1, indices, m);
+    return p.mk_peq();
+}
+
+app_ref peq::mk_eq(app_ref_vector &aux_consts, bool stores_on_rhs) {
+    if (!m_eq) {
+        expr_ref lhs(m_lhs, m), rhs(m_rhs, m);
+        if (!stores_on_rhs) { std::swap(lhs, rhs); }
+        // lhs = (...(store (store rhs i0 v0) i1 v1)...)
+        sort *val_sort = get_array_range(lhs->get_sort());
+        for (expr_ref_vector const &diff : m_diff_indices) {
+            ptr_vector<expr> store_args;
+            store_args.push_back(rhs);
+            store_args.append(diff.size(), diff.data());
+            app_ref val(m.mk_fresh_const("diff", val_sort), m);
+            store_args.push_back(val);
+            aux_consts.push_back(val);
+            rhs = m_arr_u.mk_store(store_args);
+        }
+        m_eq = m.mk_eq(lhs, rhs);
+    }
+    return m_eq;
+}
+
+app_ref peq::mk_peq() {
+    if (!m_peq) {
+        ptr_vector<expr> args;
+        args.push_back(m_lhs);
+        args.push_back(m_rhs);
+        for (auto const &v : m_diff_indices) {
+            args.append(v.size(), v.data());
+        }
+        m_peq = m.mk_app(m_decl, args.size(), args.data());
+    }
+    return m_peq;
+}
+
+peq::peq(expr *lhs, expr *rhs, vector<expr_ref_vector> const &diff_indices,
+         ast_manager &m)
+    : m(m), m_lhs(lhs, m), m_rhs(rhs, m), m_diff_indices(diff_indices),
+      m_decl(m), m_peq(m), m_eq(m), m_arr_u(m) {
+    SASSERT(m_arr_u.is_array(lhs));
+    SASSERT(m_arr_u.is_array(rhs));
+    SASSERT(lhs->get_sort() == rhs->get_sort());
+    ptr_vector<sort> sorts;
+    sorts.push_back(m_lhs->get_sort());
+    sorts.push_back(m_rhs->get_sort());
+
+    for (auto const &v : diff_indices) {
+        SASSERT(v.size() == get_array_arity(m_lhs->get_sort()));
+        for (expr *e : v) sorts.push_back(e->get_sort());
+    }
+    m_decl = m.mk_func_decl(symbol(PARTIAL_EQ), sorts.size(), sorts.data(),
+                            m.mk_bool_sort());
+}
+
+peq::peq(app *p, ast_manager &m)
+    : m(m), m_lhs(p->get_arg(0), m), m_rhs(p->get_arg(1), m),
+      m_decl(p->get_decl(), m), m_peq(p, m), m_eq(m), m_arr_u(m),
+      m_name(symbol(PARTIAL_EQ)) {
+    SASSERT(is_partial_eq(p));
+
+    SASSERT(m_arr_u.is_array(m_lhs));
+    SASSERT(m_arr_u.is_array(m_rhs));
+    SASSERT(m_lhs->get_sort() == m_rhs->get_sort());
+    unsigned arity = get_array_arity(m_lhs->get_sort());
+    for (unsigned i = 2; i < p->get_num_args(); i += arity) {
+        SASSERT(arity + i <= p->get_num_args());
+        expr_ref_vector vec(m);
+        vec.append(arity, p->get_args() + i);
+        m_diff_indices.push_back(std::move(vec));
+    }
+}

src/ast/array_peq.h

@@ -0,0 +1,91 @@
+/*++
+Copyright (c) 2023 Microsoft Corporation
+
+Module Name:
+
+    array_peq.h
+
+Abstract:
+
+  Partial equality for arrays
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2015-06-13
+    Hari Govind V K
+
+Revision History:
+
+--*/
+#pragma once
+
+#include "ast/array_decl_plugin.h"
+#include "ast/ast.h"
+
+/**
+ * \brief utility class for partial equalities
+ *
+ * A partial equality (a ==I b), for two arrays a, b and a finite set of indices
+ * I holds iff (forall i :: i \not\in I => a[i] == b[i]). In other words, peq is
+ * a restricted form of the extensionality axiom
+ *
+ * Using this class, we denote (a =I b) as f(a,b,i0,i1,...),
+ * where f is an uninterpreted predicate with the name PARTIAL_EQ and
+ * I = {i0,i1,...}
+ */
+
+class peq {
+    ast_manager &m;
+    expr_ref m_lhs;
+    expr_ref m_rhs;
+    vector<expr_ref_vector> m_diff_indices;
+    func_decl_ref m_decl; // the partial equality declaration
+    app_ref m_peq;        // partial equality application
+    app_ref m_eq;         // equivalent std equality using def. of partial eq
+    array_util m_arr_u;
+    symbol m_name;
+
+  public:
+    peq(app *p, ast_manager &m);
+
+    peq(expr *lhs, expr *rhs, vector<expr_ref_vector> const &diff_indices,
+        ast_manager &m);
+
+    expr_ref lhs() { return m_lhs; }
+
+    expr_ref rhs() { return m_rhs; }
+
+    void get_diff_indices(vector<expr_ref_vector> &result) {
+        result.append(m_diff_indices);
+    }
+
+    /** Convert peq into a peq expression */
+    app_ref mk_peq();
+
+    /** Convert peq into an equality
+
+        For peq of the form (a =I b) returns (a = b[i0 := v0, i1 := v1, ...])
+        where i0, i1 \in I, and v0, v1 are fresh skolem constants
+
+        Skolems are returned in aux_consts
+
+        The left and right hand arguments are reversed when stores_on_rhs is
+       false
+     */
+    app_ref mk_eq(app_ref_vector &aux_consts, bool stores_on_rhs = true);
+};
+
+/**
+ * mk (e0 ==indices e1)
+ *
+ * result has stores if either e0 or e1 or an index term has stores
+ */
+app_ref mk_peq(expr *e0, expr *e1, vector<expr_ref_vector> const &indices,
+               ast_manager &m);
+
+bool is_partial_eq(const func_decl *f);
+
+bool is_partial_eq(const app *a);
+
+inline bool is_peq(const func_decl *f) { return is_partial_eq(f); }
+inline bool is_peq(const app *a) { return is_partial_eq(a); }

src/ast/rewriter/array_rewriter.cpp

@@ -24,6 +24,7 @@ Module Name:
 #include "ast/rewriter/var_subst.h"
 #include "params/array_rewriter_params.hpp"
 #include "util/util.h"
+#include "ast/array_peq.h"
 
 void array_rewriter::updt_params(params_ref const & _p) {
     array_rewriter_params p(_p);
@@ -40,8 +41,48 @@ void array_rewriter::get_param_descrs(param_descrs & r) {
 }
 
 br_status array_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
+    br_status st = BR_FAILED;
+
+    // BEGIN: rewrite rules for PEQs
+    if (is_partial_eq(f)) {
+        SASSERT(num_args >= 2);
+        expr *e0, *e1;
+        e0 = args[0];
+        e1 = args[1];
+
+        expr_ref a(m()), val(m());
+        expr_ref_vector vindex(m());
+
+        if (e0 == e1) {
+            // t peq t --> true
+            result = m().mk_true();
+            st = BR_DONE;
+        }
+        else if (m_util.is_store_ext(e0, a, vindex, val)) {
+            if (num_args == 2 && a == e1) {
+                // (a[i := x] peq_{\emptyset} a) ---> a[i] == x
+                mk_select(vindex.size(), vindex.data(), result);
+                result = m().mk_eq(result, val);
+                st = BR_REWRITE_FULL;
+            }
+            else if (a == e1 && vindex.size() == num_args + 2) {
+                // a [i: = x] peq_{i} a -- > true
+                bool all_eq = true;
+                for (unsigned i = 0, sz = vindex.size(); all_eq && i < sz;
+                     ++i) {
+                    all_eq &= vindex.get(i) == args[2+i];
+                }
+                if (all_eq) {
+                    result = m().mk_true();
+                    st = BR_DONE;
+                }
+            }
+        }
+        return st;
+    }
+    // END: rewrite rules for PEQs
+
     SASSERT(f->get_family_id() == get_fid());
-    br_status st;
     switch (f->get_decl_kind()) {
     case OP_SELECT:
         st = mk_select_core(num_args, args, result);

src/ast/rewriter/datatype_rewriter.cpp

@@ -21,7 +21,33 @@ Module Name:
 br_status datatype_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
     SASSERT(f->get_family_id() == get_fid());
     switch(f->get_decl_kind()) {
-    case OP_DT_CONSTRUCTOR: return BR_FAILED;
+    case OP_DT_CONSTRUCTOR: {
+        // cons(head(x), tail(x)) --> x
+        ptr_vector<func_decl> const *accessors =
+            m_util.get_constructor_accessors(f);
+
+        SASSERT(num_args == accessors->size());
+        // -- all accessors must have exactly one argument
+        if (any_of(*accessors, [&](const func_decl* acc) { return acc->get_arity() != 1; })) {
+            return BR_FAILED;
+        }
+
+        if (num_args >= 1 && is_app(args[0]) && to_app(args[0])->get_decl() == accessors->get(0) ) {
+            bool is_all = true;
+            expr* t = to_app(args[0])->get_arg(0);
+            for(unsigned i = 1; i < num_args && is_all; ++i) {
+                is_all &= (is_app(args[i]) &&
+                           to_app(args[i])->get_decl() == accessors->get(i) &&
+                           to_app(args[i])->get_arg(0) == t);
+            }
+            if (is_all) {
+                result = t;
+                return BR_DONE;
+            }
+            return BR_FAILED;
+        }
+        return BR_FAILED;
+    }
     case OP_DT_RECOGNISER:
         SASSERT(num_args == 1);
         result = m_util.mk_is(m_util.get_recognizer_constructor(f), args[0]);

src/ast/rewriter/th_rewriter.cpp

@@ -39,6 +39,7 @@ Module Name:
 #include "ast/ast_util.h"
 #include "ast/well_sorted.h"
 #include "ast/for_each_expr.h"
+#include "ast/array_peq.h"
 
 namespace {
 struct th_rewriter_cfg : public default_rewriter_cfg {
@@ -644,6 +645,10 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
             else
                 st = pull_ite(result);
         }
+        if (st == BR_FAILED && f->get_family_id() == null_family_id && is_partial_eq(f)) {
+            st = m_ar_rw.mk_app_core(f,  num, args, result);
+        }
+
         CTRACE("th_rewriter_step", st != BR_FAILED,
                tout << f->get_name() << "\n";
                for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << "\n";