mirror of
https://github.com/Z3Prover/z3
synced 2026-03-06 21:34:53 +00:00
Integrate rw_table into th_rewriter_cfg and expand populate_rules()
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot]
parent
57c9987d25
commit
a4ccb6390d
3 changed files with 239 additions and 0 deletions
|
|
@ -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
|
||||
// ------------------------------------------------------------------
|
||||
|
|
|
|||
|
|
@ -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) {
|
||||
|
|
|
|||
|
|
@ -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";
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue