From a4ccb6390d69a2c9d2cd5f73a339e25079c0259c Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Fri, 27 Feb 2026 04:36:28 +0000 Subject: [PATCH] Integrate rw_table into th_rewriter_cfg and expand populate_rules() Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/ast/rewriter/rw_rule.cpp | 41 +++++++ src/ast/rewriter/th_rewriter.cpp | 10 ++ src/test/rw_rule.cpp | 188 +++++++++++++++++++++++++++++++ 3 files changed, 239 insertions(+) diff --git a/src/ast/rewriter/rw_rule.cpp b/src/ast/rewriter/rw_rule.cpp index 152b2f2df..cc9093c12 100644 --- a/src/ast/rewriter/rw_rule.cpp +++ b/src/ast/rewriter/rw_rule.cpp @@ -145,6 +145,25 @@ void rw_table::populate_rules() { add_rule(1, arith.mk_uminus(arith.mk_uminus(v0i)), v0i); // -(-x) -> x (Int) add_rule(1, arith.mk_uminus(arith.mk_uminus(v0r)), v0r); // -(-x) -> x (Real) + // Arithmetic: unary minus of zero -(0) -> 0 + add_rule(0, arith.mk_uminus(zero_i), zero_i); // -(0_i) -> 0 (Int) + add_rule(0, arith.mk_uminus(zero_r), zero_r); // -(0_r) -> 0 (Real) + + // Arithmetic: integer division by 1 x div 1 -> x + add_rule(1, arith.mk_idiv(v0i, one_i), v0i); // x div 1 -> x (Int) + + // Arithmetic: mod by 1 x mod 1 -> 0 + add_rule(1, arith.mk_mod(v0i, one_i), zero_i); // x mod 1 -> 0 (Int) + + // Arithmetic: rem by 1 x rem 1 -> 0 + add_rule(1, arith.mk_rem(v0i, one_i), zero_i); // x rem 1 -> 0 (Int) + + // Arithmetic: reflexive inequality x <= x -> true, x >= x -> true + add_rule(1, arith.mk_le(v0i, v0i), t_true); // x <= x -> true (Int) + add_rule(1, arith.mk_ge(v0i, v0i), t_true); // x >= x -> true (Int) + add_rule(1, arith.mk_le(v0r, v0r), t_true); // x <= x -> true (Real) + add_rule(1, arith.mk_ge(v0r, v0r), t_true); // x >= x -> true (Real) + // ------------------------------------------------------------------ // Boolean: and/or identities and annihilators // ------------------------------------------------------------------ @@ -158,6 +177,16 @@ void rw_table::populate_rules() { add_rule(1, m.mk_or(t_true, v0b), t_true); // true \/ x -> true add_rule(1, m.mk_or(v0b, t_true), t_true); // x \/ true -> true + // Boolean: idempotency x /\ x -> x, x \/ x -> x + add_rule(1, m.mk_and(v0b, v0b), v0b); // x /\ x -> x + add_rule(1, m.mk_or(v0b, v0b), v0b); // x \/ x -> x + + // Boolean: complementation x /\ not(x) -> false, x \/ not(x) -> true + add_rule(1, m.mk_and(v0b, m.mk_not(v0b)), t_false); // x /\ not(x) -> false + add_rule(1, m.mk_and(m.mk_not(v0b), v0b), t_false); // not(x) /\ x -> false + add_rule(1, m.mk_or(v0b, m.mk_not(v0b)), t_true); // x \/ not(x) -> true + add_rule(1, m.mk_or(m.mk_not(v0b), v0b), t_true); // not(x) \/ x -> true + // Boolean: double negation not(not(x)) -> x add_rule(1, m.mk_not(m.mk_not(v0b)), v0b); @@ -165,6 +194,14 @@ void rw_table::populate_rules() { add_rule(0, m.mk_not(m.mk_true()), m.mk_false()); // not(true) -> false add_rule(0, m.mk_not(m.mk_false()), m.mk_true()); // not(false) -> true + // Boolean: equality with true/false + // (= true x) -> x, (= x true) -> x + // (= false x) -> not(x), (= x false) -> not(x) + add_rule(1, m.mk_eq(t_true, v0b), v0b); // (= true x) -> x + add_rule(1, m.mk_eq(v0b, t_true), v0b); // (= x true) -> x + add_rule(1, m.mk_eq(t_false, v0b), m.mk_not(v0b)); // (= false x) -> not(x) + add_rule(1, m.mk_eq(v0b, t_false), m.mk_not(v0b)); // (= x false) -> not(x) + // ------------------------------------------------------------------ // ITE simplifications (Bool, Int, Real branches) // ------------------------------------------------------------------ @@ -183,6 +220,10 @@ void rw_table::populate_rules() { add_rule(2, m.mk_ite(v0b, v1i, v1i), v1i); // Int add_rule(2, m.mk_ite(v0b, v1r, v1r), v1r); // Real + // ite(c, true, false) -> c and ite(c, false, true) -> not(c) + add_rule(1, m.mk_ite(v0b, t_true, t_false), v0b); // Bool + add_rule(1, m.mk_ite(v0b, t_false, t_true), m.mk_not(v0b)); // Bool + // ------------------------------------------------------------------ // Equality: x = x -> true // ------------------------------------------------------------------ diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index f77bc1a68..29a3afd11 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -33,6 +33,7 @@ Notes: #include "ast/rewriter/finite_set_rewriter.h" #include "ast/rewriter/rewriter_def.h" #include "ast/rewriter/var_subst.h" +#include "ast/rewriter/rw_rule.h" #include "ast/rewriter/der.h" #include "ast/rewriter/expr_safe_replace.h" #include "ast/expr_substitution.h" @@ -57,6 +58,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { char_rewriter m_char_rw; recfun_rewriter m_rec_rw; finite_set_rewriter m_fs_rw; + rw_table m_rw_table; arith_util m_a_util; bv_util m_bv_util; der m_der; @@ -157,6 +159,12 @@ struct th_rewriter_cfg : public default_rewriter_cfg { } br_status reduce_app_core(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + // Try abstract machine rules first: catches simple Bool/arith identities cheaply. + { + br_status st = m_rw_table.apply(f, num, args, result); + if (st != BR_FAILED) + return st; + } family_id fid = f->get_family_id(); if (fid == null_family_id) return BR_FAILED; @@ -891,6 +899,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { m_char_rw(m), m_rec_rw(m), m_fs_rw(m), + m_rw_table(m), m_a_util(m), m_bv_util(m), m_der(m), @@ -899,6 +908,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { m_pinned(m), m_used_dependencies(m) { updt_local_params(p); + m_rw_table.populate_rules(); } void set_substitution(expr_substitution * s) { diff --git a/src/test/rw_rule.cpp b/src/test/rw_rule.cpp index 3b1de5820..ead6ecf97 100644 --- a/src/test/rw_rule.cpp +++ b/src/test/rw_rule.cpp @@ -352,6 +352,186 @@ static void test_compound() { check(m, "(0+x)+(1*x)", result, expected); } +// --------------------------------------------------------------------------- +// New rules: Bool idempotency, complementation, eq simplification, ITE Bool +// --------------------------------------------------------------------------- + +static void test_bool_idempotency() { + ast_manager m; + reg_decl_plugins(m); + + rw_evaluator ev(m); + expr_ref result(m); + + sort * bool_sort = m.mk_bool_sort(); + expr_ref bx(m.mk_const(symbol("bx"), bool_sort), m); + + // x /\ x -> x + ev(m.mk_and(bx, bx), result); + check(m, "x /\\ x", result, bx); + + // x \/ x -> x + ev(m.mk_or(bx, bx), result); + check(m, "x \\/ x", result, bx); +} + +static void test_bool_complementation() { + ast_manager m; + reg_decl_plugins(m); + + rw_evaluator ev(m); + expr_ref result(m); + + sort * bool_sort = m.mk_bool_sort(); + expr_ref bx(m.mk_const(symbol("bx"), bool_sort), m); + + // x /\ not(x) -> false + ev(m.mk_and(bx, m.mk_not(bx)), result); + check_false(m, "x /\\ not(x)", result); + + // not(x) /\ x -> false + ev(m.mk_and(m.mk_not(bx), bx), result); + check_false(m, "not(x) /\\ x", result); + + // x \/ not(x) -> true + ev(m.mk_or(bx, m.mk_not(bx)), result); + check_true(m, "x \\/ not(x)", result); + + // not(x) \/ x -> true + ev(m.mk_or(m.mk_not(bx), bx), result); + check_true(m, "not(x) \\/ x", result); +} + +static void test_bool_eq_simplification() { + ast_manager m; + reg_decl_plugins(m); + + rw_evaluator ev(m); + expr_ref result(m); + + sort * bool_sort = m.mk_bool_sort(); + expr_ref bx(m.mk_const(symbol("bx"), bool_sort), m); + + // (= true x) -> x + ev(m.mk_eq(m.mk_true(), bx), result); + check(m, "(= true bx)", result, bx); + + // (= x true) -> x + ev(m.mk_eq(bx, m.mk_true()), result); + check(m, "(= bx true)", result, bx); + + // (= false x) -> not(x) + ev(m.mk_eq(m.mk_false(), bx), result); + { + expr_ref not_bx(m.mk_not(bx), m); + check(m, "(= false bx)", result, not_bx); + } + + // (= x false) -> not(x) + ev(m.mk_eq(bx, m.mk_false()), result); + { + expr_ref not_bx(m.mk_not(bx), m); + check(m, "(= bx false)", result, not_bx); + } +} + +static void test_ite_bool_special() { + ast_manager m; + reg_decl_plugins(m); + + rw_evaluator ev(m); + expr_ref result(m); + + sort * bool_sort = m.mk_bool_sort(); + expr_ref c(m.mk_const(symbol("c"), bool_sort), m); + + // ite(c, true, false) -> c + ev(m.mk_ite(c, m.mk_true(), m.mk_false()), result); + check(m, "ite(c,true,false)", result, c); + + // ite(c, false, true) -> not(c) + ev(m.mk_ite(c, m.mk_false(), m.mk_true()), result); + { + expr_ref not_c(m.mk_not(c), m); + check(m, "ite(c,false,true)", result, not_c); + } +} + +static void test_arith_div_mod() { + ast_manager m; + reg_decl_plugins(m); + arith_util arith(m); + + rw_evaluator ev(m); + expr_ref result(m); + + sort * int_sort = arith.mk_int(); + expr_ref x(m.mk_const(symbol("x"), int_sort), m); + + // idiv(x, 1) -> x + ev(arith.mk_idiv(x, arith.mk_int(1)), result); + check(m, "x div 1", result, x); + + // mod(x, 1) -> 0 + ev(arith.mk_mod(x, arith.mk_int(1)), result); + ENSURE(arith.is_zero(result)); + std::cout << "x mod 1: " << mk_pp(result, m) << " [OK]\n"; + + // rem(x, 1) -> 0 + ev(arith.mk_rem(x, arith.mk_int(1)), result); + ENSURE(arith.is_zero(result)); + std::cout << "x rem 1: " << mk_pp(result, m) << " [OK]\n"; +} + +static void test_arith_uminus_zero() { + ast_manager m; + reg_decl_plugins(m); + arith_util arith(m); + + rw_evaluator ev(m); + expr_ref result(m); + + // -(0_i) -> 0_i + ev(arith.mk_uminus(arith.mk_int(0)), result); + ENSURE(arith.is_zero(result) && arith.is_int(result)); + std::cout << "-(0_i): " << mk_pp(result, m) << " [OK]\n"; + + // -(0_r) -> 0_r + ev(arith.mk_uminus(arith.mk_real(0)), result); + ENSURE(arith.is_zero(result) && !arith.is_int(result)); + std::cout << "-(0_r): " << mk_pp(result, m) << " [OK]\n"; +} + +static void test_arith_le_ge_reflexivity() { + ast_manager m; + reg_decl_plugins(m); + arith_util arith(m); + + rw_evaluator ev(m); + expr_ref result(m); + + sort * int_sort = arith.mk_int(); + sort * real_sort = arith.mk_real(); + expr_ref xi(m.mk_const(symbol("xi"), int_sort), m); + expr_ref xr(m.mk_const(symbol("xr"), real_sort), m); + + // xi <= xi -> true + ev(arith.mk_le(xi, xi), result); + check_true(m, "xi <= xi", result); + + // xi >= xi -> true + ev(arith.mk_ge(xi, xi), result); + check_true(m, "xi >= xi", result); + + // xr <= xr -> true + ev(arith.mk_le(xr, xr), result); + check_true(m, "xr <= xr", result); + + // xr >= xr -> true + ev(arith.mk_ge(xr, xr), result); + check_true(m, "xr >= xr", result); +} + // --------------------------------------------------------------------------- // Direct rw_table API test (no evaluator) // --------------------------------------------------------------------------- @@ -399,5 +579,13 @@ void tst_rw_rule() { test_eq_reflexivity(); test_compound(); test_table_direct(); + // new-rule tests + test_bool_idempotency(); + test_bool_complementation(); + test_bool_eq_simplification(); + test_ite_bool_special(); + test_arith_div_mod(); + test_arith_uminus_zero(); + test_arith_le_ge_reflexivity(); std::cout << "=== rw_rule: all tests passed ===\n"; }