From 922f49e1870025da659706aeb5c6c818ee52f7fe Mon Sep 17 00:00:00 2001 From: Hari Govind V K Date: Wed, 3 Jun 2026 15:23:21 +0100 Subject: [PATCH] Fix MBP QEL soundness bug in datatype accessor elimination (#9571) (#9692) Two fixes for mbp_dt_tg::apply() when encountering an accessor whose argument has a different constructor in the model: 1. Don't call rm_accessor (which would assert a contradictory recognizer, making the formula false). This prevents the original bug where QEL returned 'false' for satisfiable formulas. 2. Branch on the model-assigned constructor for the accessor's argument. The correct output should include the literal introduced in (2). However, this fix does not produce it. Spacer is sound with this over-approximation, as long as the counter example does not depend on value of mismatched accessors (e.g. (tl nil)). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/qe/mbp/mbp_dt_tg.cpp | 18 +++ src/test/CMakeLists.txt | 1 + src/test/main.cpp | 1 + src/test/mbp_qel.cpp | 250 +++++++++++++++++++++++++++++++++++++++ 4 files changed, 270 insertions(+) create mode 100644 src/test/mbp_qel.cpp diff --git a/src/qe/mbp/mbp_dt_tg.cpp b/src/qe/mbp/mbp_dt_tg.cpp index aee54c459..b844843cd 100644 --- a/src/qe/mbp/mbp_dt_tg.cpp +++ b/src/qe/mbp/mbp_dt_tg.cpp @@ -163,6 +163,24 @@ struct mbp_dt_tg::impl { if (is_app(term) && m_dt_util.is_accessor(to_app(term)->get_decl()) && has_var(to_app(term)->get_arg(0))) { + // Only apply rm_accessor if the model confirms the argument + // has the constructor that this accessor belongs to. + // Otherwise we introduce a contradictory is-cons literal. + func_decl *cons = + m_dt_util.get_accessor_constructor(to_app(term)->get_decl()); + func_decl *rec = m_dt_util.get_constructor_recognizer(cons); + expr_ref is_rec(m.mk_app(rec, to_app(term)->get_arg(0)), m); + if (!m_mdl.is_true(is_rec)) { + // Ground the argument so the accessor term becomes + // constructively ground. This preserves any enclosing + // literal (e.g., (not (is-nil (tl nil)))) as a guard in + // the output, preventing an over-approximation. + expr_ref is(m.mk_not(is_rec), m); + m_tg.add_lit(is); + mark_seen(term); + progress = true; + continue; + } mark_seen(term); progress = true; rm_accessor(term); diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt index c79a0696f..39050620a 100644 --- a/src/test/CMakeLists.txt +++ b/src/test/CMakeLists.txt @@ -115,6 +115,7 @@ add_executable(test-z3 prime_generator.cpp proof_checker.cpp qe_arith.cpp + mbp_qel.cpp quant_elim.cpp quant_solve.cpp random.cpp diff --git a/src/test/main.cpp b/src/test/main.cpp index 802512f89..1727cb9dc 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -163,6 +163,7 @@ X(rcf) \ X(polynorm) \ X(qe_arith) \ + X(mbp_qel) \ X(expr_substitution) \ X(sorting_network) \ X(theory_pb) \ diff --git a/src/test/mbp_qel.cpp b/src/test/mbp_qel.cpp new file mode 100644 index 000000000..1ff262785 --- /dev/null +++ b/src/test/mbp_qel.cpp @@ -0,0 +1,250 @@ + +/*++ +Copyright (c) 2025 Microsoft Corporation + +Module Name: + + mbp_qel.cpp + +Abstract: + + Unit tests for model-based projection with QEL (term-graph based) + +Author: + + Hari Govind V K (hgvk94) 2025-05-25 + +--*/ + +#include "qe/qe_mbp.h" +#include "ast/reg_decl_plugins.h" +#include "ast/datatype_decl_plugin.h" +#include "ast/arith_decl_plugin.h" +#include "ast/ast_pp.h" +#include "smt/smt_context.h" +#include "params/smt_params.h" +#include + +// Test that MBP with QEL does not return false for a satisfiable formula +// involving datatype accessors applied past the end of a list. +// +// Formula: (and ((_ is cons) x) ((_ is nil) (tl x)) (= nil (tl (tl x))) (< 8 n)) +// Project: x +// Expected: result should imply n >= 9 (and model should satisfy it) +// Bug: QEL was returning false because rm_accessor unconditionally +// assumed (tl x) has constructor cons when eliminating (tl (tl x)), +// contradicting the ((_ is nil) (tl x)) literal. +static void test_dt_accessor_past_end() { + std::cout << "test_dt_accessor_past_end\n"; + ast_manager m; + reg_decl_plugins(m); + datatype_util dt(m); + arith_util a(m); + + // Create list datatype: (declare-datatypes ((L 0)) (((cons (hd Int) (tl L)) (nil)))) + sort_ref int_sort(a.mk_int(), m); + func_decl_ref cons(m), is_cons(m), head(m), tail(m), nil(m), is_nil(m); + sort_ref L = dt.mk_list_datatype(int_sort, symbol("L"), + cons, is_cons, head, tail, nil, is_nil); + + // Declare variables + app_ref x(m.mk_const("x", L), m); + app_ref n(m.mk_const("n", int_sort), m); + + // Build formula: (and ((_ is cons) x) ((_ is nil) (tl x)) (= nil (tl (tl x))) (< 8 n)) + expr_ref tl_x(m.mk_app(tail, x.get()), m); + expr_ref tl_tl_x(m.mk_app(tail, tl_x.get()), m); + expr_ref nil_val(m.mk_const(nil), m); + + expr_ref is_cons_x(m.mk_app(is_cons, x.get()), m); + expr_ref is_nil_tl_x(m.mk_app(is_nil, tl_x.get()), m); + expr_ref eq_nil_tl_tl_x(m.mk_eq(nil_val, tl_tl_x), m); + expr_ref lt_8_n(a.mk_lt(a.mk_int(8), n), m); + + expr_ref_vector conjs(m); + conjs.push_back(is_cons_x).push_back(is_nil_tl_x).push_back(eq_nil_tl_tl_x).push_back(lt_8_n); + expr_ref fml(m.mk_and(conjs), m); + + std::cout << " formula:\n " << mk_pp(fml, m, 5) << "\n"; + + // Get a model + smt_params params; + params.m_model = true; + model_ref mdl; + { + smt::context ctx(m, params); + ctx.assert_expr(fml); + lbool result = ctx.check(); + VERIFY(result == l_true); + ctx.get_model(mdl); + } + + std::cout << " model: x = " << mk_pp((*mdl)(x), m) + << ", n = " << mk_pp((*mdl)(n), m) << "\n"; + + // Call MBP with QEL enabled + app_ref_vector vars(m); + vars.push_back(x); + + params_ref p; + p.set_bool("qsat_use_qel", true); + qe::mbproj mbp(m, p); + expr_ref projected(fml, m); + mbp.spacer(vars, *mdl.get(), projected); + + std::cout << " projected (qel=true):\n " << mk_pp(projected, m, 5) << "\n"; + + // The result must not be false + VERIFY(!m.is_false(projected)); + + // The model should satisfy the projected formula + VERIFY(mdl->is_true(projected)); + + // x should have been eliminated + VERIFY(vars.empty()); + + std::cout << " PASS\n\n"; +} + +// Same test but with a deeper list structure: +// x is a 2-element list with a past-end accessor constraint +// Formula: (and ((_ is cons) x) ((_ is cons) (tl x)) ((_ is nil) (tl (tl x))) +// (= nil (tl (tl (tl x)))) (< 8 n)) +static void test_dt_accessor_past_end_depth2() { + std::cout << "test_dt_accessor_past_end_depth2\n"; + ast_manager m; + reg_decl_plugins(m); + datatype_util dt(m); + arith_util a(m); + + sort_ref int_sort(a.mk_int(), m); + func_decl_ref cons(m), is_cons(m), head(m), tail(m), nil(m), is_nil(m); + sort_ref L = dt.mk_list_datatype(int_sort, symbol("L"), + cons, is_cons, head, tail, nil, is_nil); + + app_ref x(m.mk_const("x", L), m); + app_ref n(m.mk_const("n", int_sort), m); + + // Build: (and (is-cons x) (is-cons (tl x)) (is-nil (tl (tl x))) + // (= nil (tl (tl (tl x)))) (< 8 n)) + expr_ref tl_x(m.mk_app(tail, x.get()), m); + expr_ref tl_tl_x(m.mk_app(tail, tl_x.get()), m); + expr_ref tl_tl_tl_x(m.mk_app(tail, tl_tl_x.get()), m); + expr_ref nil_val(m.mk_const(nil), m); + + expr_ref is_cons_x(m.mk_app(is_cons, x.get()), m); + expr_ref is_cons_tl_x(m.mk_app(is_cons, tl_x.get()), m); + expr_ref is_nil_tl_tl_x(m.mk_app(is_nil, tl_tl_x.get()), m); + expr_ref eq_nil_tl3(m.mk_eq(nil_val, tl_tl_tl_x), m); + expr_ref lt_8_n(a.mk_lt(a.mk_int(8), n), m); + + expr_ref_vector conjs(m); + conjs.push_back(is_cons_x).push_back(is_cons_tl_x).push_back(is_nil_tl_tl_x).push_back(eq_nil_tl3).push_back(lt_8_n); + expr_ref fml(m.mk_and(conjs), m); + + std::cout << " formula:\n " << mk_pp(fml, m, 5) << "\n"; + + smt_params sparams; + sparams.m_model = true; + model_ref mdl; + { + smt::context ctx(m, sparams); + ctx.assert_expr(fml); + lbool result = ctx.check(); + VERIFY(result == l_true); + ctx.get_model(mdl); + } + + std::cout << " model: x = " << mk_pp((*mdl)(x), m) + << ", n = " << mk_pp((*mdl)(n), m) << "\n"; + + app_ref_vector vars(m); + vars.push_back(x); + + params_ref p; + p.set_bool("qsat_use_qel", true); + qe::mbproj mbp(m, p); + expr_ref projected(fml, m); + mbp.spacer(vars, *mdl.get(), projected); + + std::cout << " projected (qel=true):\n " << mk_pp(projected, m, 5) << "\n"; + + VERIFY(!m.is_false(projected)); + VERIFY(mdl->is_true(projected)); + VERIFY(vars.empty()); + + std::cout << " PASS\n\n"; +} + +// Test with multiple DT variables projected simultaneously +// Formula: (and (= nil (tl (tl (tl x)))) ((_ is nil) (tl (tl x))) +// ((_ is cons) y) ((_ is nil) (tl y)) (< 8 n)) +// Project: x, y +static void test_dt_multiple_vars() { + std::cout << "test_dt_multiple_vars\n"; + ast_manager m; + reg_decl_plugins(m); + datatype_util dt(m); + arith_util a(m); + + sort_ref int_sort(a.mk_int(), m); + func_decl_ref cons(m), is_cons(m), head(m), tail(m), nil(m), is_nil(m); + sort_ref L = dt.mk_list_datatype(int_sort, symbol("L"), + cons, is_cons, head, tail, nil, is_nil); + + app_ref x(m.mk_const("x", L), m); + app_ref y(m.mk_const("y", L), m); + app_ref n(m.mk_const("n", int_sort), m); + + expr_ref tl_x(m.mk_app(tail, x.get()), m); + expr_ref tl_tl_x(m.mk_app(tail, tl_x.get()), m); + expr_ref tl_tl_tl_x(m.mk_app(tail, tl_tl_x.get()), m); + expr_ref tl_y(m.mk_app(tail, y.get()), m); + expr_ref nil_val(m.mk_const(nil), m); + + expr_ref eq_nil_tl3x(m.mk_eq(nil_val, tl_tl_tl_x), m); + expr_ref is_nil_tl2x(m.mk_app(is_nil, tl_tl_x.get()), m); + expr_ref is_cons_y(m.mk_app(is_cons, y.get()), m); + expr_ref is_nil_tl_y(m.mk_app(is_nil, tl_y.get()), m); + expr_ref lt_8_n(a.mk_lt(a.mk_int(8), n), m); + + expr_ref_vector conjs(m); + conjs.push_back(eq_nil_tl3x).push_back(is_nil_tl2x).push_back(is_cons_y).push_back(is_nil_tl_y).push_back(lt_8_n); + expr_ref fml(m.mk_and(conjs), m); + + std::cout << " formula:\n " << mk_pp(fml, m, 5) << "\n"; + + smt_params sparams; + sparams.m_model = true; + model_ref mdl; + { + smt::context ctx(m, sparams); + ctx.assert_expr(fml); + lbool result = ctx.check(); + VERIFY(result == l_true); + ctx.get_model(mdl); + } + + app_ref_vector vars(m); + vars.push_back(x); + vars.push_back(y); + + params_ref p; + p.set_bool("qsat_use_qel", true); + qe::mbproj mbp(m, p); + expr_ref projected(fml, m); + mbp.spacer(vars, *mdl.get(), projected); + + std::cout << " projected (qel=true):\n " << mk_pp(projected, m, 5) << "\n"; + + VERIFY(!m.is_false(projected)); + VERIFY(mdl->is_true(projected)); + + std::cout << " PASS\n\n"; +} + +void tst_mbp_qel() { + test_dt_accessor_past_end(); + test_dt_accessor_past_end_depth2(); + test_dt_multiple_vars(); +}