feat(library/compiler/csimp): add basic constant folding for nat operations
This commit is contained in:
Leonardo de Moura
parent
fa9d6b4ddf
commit
a40c526e48
5 changed files with 174 additions and 1 deletions
|
|
@ -51,6 +51,7 @@ public:
|
|||
explicit literal(unsigned v);
|
||||
explicit literal(mpz const & v);
|
||||
explicit literal(nat const & v);
|
||||
literal():literal(0u) {}
|
||||
literal(literal const & other):object_ref(other) {}
|
||||
literal(literal && other):object_ref(other) {}
|
||||
literal & operator=(literal const & other) { object_ref::operator=(other); return *this; }
|
||||
|
|
|
|||
|
|
@ -1095,6 +1095,109 @@ class csimp_fn {
|
|||
}
|
||||
}
|
||||
|
||||
bool get_unary_lit(expr const & e, literal & a) {
|
||||
if (get_app_num_args(e) != 1) return false;
|
||||
expr arg = find(app_arg(e));
|
||||
if (!is_lit(arg)) return false;
|
||||
a = lit_value(arg);
|
||||
return true;
|
||||
}
|
||||
|
||||
bool get_unary_nat_lit(expr const & e, nat & a) {
|
||||
literal l;
|
||||
if (!get_unary_lit(e, l)) return false;
|
||||
if (l.kind() != literal_kind::Nat) return false;
|
||||
a = l.get_nat();
|
||||
return true;
|
||||
}
|
||||
|
||||
bool get_binary_lits(expr const & e, literal & a, literal & b) {
|
||||
if (get_app_num_args(e) != 2) return false;
|
||||
expr arg2 = find(app_arg(e));
|
||||
if (!is_lit(arg2)) return false;
|
||||
expr arg1 = find(app_arg(app_fn(e)));
|
||||
if (!is_lit(arg1)) return false;
|
||||
a = lit_value(arg1);
|
||||
b = lit_value(arg2);
|
||||
return true;
|
||||
}
|
||||
|
||||
bool get_binary_nat_lits(expr const & e, nat & a, nat & b) {
|
||||
literal l1, l2;
|
||||
if (!get_binary_lits(e, l1, l2)) return false;
|
||||
if (l1.kind() != literal_kind::Nat) return false;
|
||||
if (l2.kind() != literal_kind::Nat) return false;
|
||||
a = l1.get_nat();
|
||||
b = l2.get_nat();
|
||||
return true;
|
||||
}
|
||||
|
||||
expr to_nat_expr(nat const & n) {
|
||||
return mk_lit(literal(n));
|
||||
}
|
||||
|
||||
expr visit_nat_succ(expr const & e) {
|
||||
nat a;
|
||||
if (!get_unary_nat_lit(e, a)) return e;
|
||||
return to_nat_expr(a+nat(1));
|
||||
}
|
||||
|
||||
expr visit_nat_add(expr const & e) {
|
||||
nat a, b;
|
||||
if (!get_binary_nat_lits(e, a, b)) return e;
|
||||
return to_nat_expr(a+b);
|
||||
}
|
||||
|
||||
expr visit_nat_mul(expr const & e) {
|
||||
nat a, b;
|
||||
if (!get_binary_nat_lits(e, a, b)) return e;
|
||||
return to_nat_expr(a*b);
|
||||
}
|
||||
|
||||
expr visit_nat_sub(expr const & e) {
|
||||
nat a, b;
|
||||
if (!get_binary_nat_lits(e, a, b)) return e;
|
||||
return to_nat_expr(a-b);
|
||||
}
|
||||
|
||||
expr to_bool_expr(bool b) {
|
||||
return b ? mk_bool_tt() : mk_bool_ff();
|
||||
}
|
||||
|
||||
expr visit_nat_beq(expr const & e) {
|
||||
nat a, b;
|
||||
if (!get_binary_nat_lits(e, a, b)) return e;
|
||||
return to_bool_expr(a == b);
|
||||
}
|
||||
|
||||
expr visit_nat_ble(expr const & e) {
|
||||
nat a, b;
|
||||
if (!get_binary_nat_lits(e, a, b)) return e;
|
||||
return to_bool_expr(a <= b);
|
||||
}
|
||||
|
||||
expr to_decidable_expr(bool b, expr const & p) {
|
||||
if (b) {
|
||||
return mk_app(mk_constant(get_decidable_is_true_name()), p, mk_app(mk_constant(get_lc_proof_name()), p));
|
||||
} else {
|
||||
return mk_app(mk_constant(get_decidable_is_false_name()), p, mk_app(mk_constant(get_lc_proof_name()), p));
|
||||
}
|
||||
}
|
||||
|
||||
expr visit_nat_dec_eq(expr const & e) {
|
||||
nat a, b;
|
||||
if (!get_binary_nat_lits(e, a, b)) return e;
|
||||
expr type = whnf_infer_type(e);
|
||||
return to_decidable_expr(a == b, app_arg(type));
|
||||
}
|
||||
|
||||
expr visit_nat_decidable_lt(expr const & e) {
|
||||
nat a, b;
|
||||
if (!get_binary_nat_lits(e, a, b)) return e;
|
||||
expr type = whnf_infer_type(e);
|
||||
return to_decidable_expr(a < b, app_arg(type));
|
||||
}
|
||||
|
||||
expr visit_app(expr const & e, bool is_let_val) {
|
||||
if (is_cases_on_app(env(), e)) {
|
||||
return visit_cases(e, is_let_val);
|
||||
|
|
@ -1119,7 +1222,28 @@ class csimp_fn {
|
|||
} else if (is_app(fn)) {
|
||||
return merge_app_app(fn, e, is_let_val);
|
||||
} else if (is_constant(fn)) {
|
||||
return try_inline(fn, e, is_let_val);
|
||||
name const & n = const_name(fn);
|
||||
if (n == get_nat_add_name()) {
|
||||
return visit_nat_add(e);
|
||||
} else if (n == get_nat_mul_name()) {
|
||||
return visit_nat_mul(e);
|
||||
} else if (n == get_nat_sub_name()) {
|
||||
return visit_nat_sub(e);
|
||||
} else if (n == get_nat_dec_eq_name()) {
|
||||
return visit_nat_dec_eq(e);
|
||||
} else if (n == get_nat_decidable_lt_name()) {
|
||||
return visit_nat_decidable_lt(e);
|
||||
} else if (n == get_nat_beq_name()) {
|
||||
return visit_nat_beq(e);
|
||||
} else if (n == get_nat_ble_name()) {
|
||||
return visit_nat_ble(e);
|
||||
} else if (n == get_nat_succ_name()) {
|
||||
return visit_nat_succ(e);
|
||||
} else if (n == get_nat_zero_name()) {
|
||||
return mk_lit(literal(nat(0)));
|
||||
} else {
|
||||
return try_inline(fn, e, is_let_val);
|
||||
}
|
||||
}
|
||||
return e;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -40,6 +40,8 @@ name const * g_congr_arg = nullptr;
|
|||
name const * g_congr_fun = nullptr;
|
||||
name const * g_decidable = nullptr;
|
||||
name const * g_decidable_to_bool = nullptr;
|
||||
name const * g_decidable_is_true = nullptr;
|
||||
name const * g_decidable_is_false = nullptr;
|
||||
name const * g_dite = nullptr;
|
||||
name const * g_empty = nullptr;
|
||||
name const * g_Exists = nullptr;
|
||||
|
|
@ -184,6 +186,12 @@ name const * g_nat_one_lt_bit0 = nullptr;
|
|||
name const * g_nat_one_lt_bit1 = nullptr;
|
||||
name const * g_nat_le_of_lt = nullptr;
|
||||
name const * g_nat_le_refl = nullptr;
|
||||
name const * g_nat_decidable_lt = nullptr;
|
||||
name const * g_nat_dec_eq = nullptr;
|
||||
name const * g_nat_mul = nullptr;
|
||||
name const * g_nat_sub = nullptr;
|
||||
name const * g_nat_beq = nullptr;
|
||||
name const * g_nat_ble = nullptr;
|
||||
name const * g_ne = nullptr;
|
||||
name const * g_neq_of_not_iff = nullptr;
|
||||
name const * g_not = nullptr;
|
||||
|
|
@ -305,6 +313,8 @@ void initialize_constants() {
|
|||
g_congr_fun = new name{"congr_fun"};
|
||||
g_decidable = new name{"decidable"};
|
||||
g_decidable_to_bool = new name{"decidable", "to_bool"};
|
||||
g_decidable_is_true = new name{"decidable", "is_true"};
|
||||
g_decidable_is_false = new name{"decidable", "is_false"};
|
||||
g_dite = new name{"dite"};
|
||||
g_empty = new name{"empty"};
|
||||
g_Exists = new name{"Exists"};
|
||||
|
|
@ -449,6 +459,12 @@ void initialize_constants() {
|
|||
g_nat_one_lt_bit1 = new name{"nat", "one_lt_bit1"};
|
||||
g_nat_le_of_lt = new name{"nat", "le_of_lt"};
|
||||
g_nat_le_refl = new name{"nat", "le_refl"};
|
||||
g_nat_decidable_lt = new name{"nat", "decidable_lt"};
|
||||
g_nat_dec_eq = new name{"nat", "dec_eq"};
|
||||
g_nat_mul = new name{"nat", "mul"};
|
||||
g_nat_sub = new name{"nat", "sub"};
|
||||
g_nat_beq = new name{"nat", "beq"};
|
||||
g_nat_ble = new name{"nat", "ble"};
|
||||
g_ne = new name{"ne"};
|
||||
g_neq_of_not_iff = new name{"neq_of_not_iff"};
|
||||
g_not = new name{"not"};
|
||||
|
|
@ -571,6 +587,8 @@ void finalize_constants() {
|
|||
delete g_congr_fun;
|
||||
delete g_decidable;
|
||||
delete g_decidable_to_bool;
|
||||
delete g_decidable_is_true;
|
||||
delete g_decidable_is_false;
|
||||
delete g_dite;
|
||||
delete g_empty;
|
||||
delete g_Exists;
|
||||
|
|
@ -715,6 +733,12 @@ void finalize_constants() {
|
|||
delete g_nat_one_lt_bit1;
|
||||
delete g_nat_le_of_lt;
|
||||
delete g_nat_le_refl;
|
||||
delete g_nat_decidable_lt;
|
||||
delete g_nat_dec_eq;
|
||||
delete g_nat_mul;
|
||||
delete g_nat_sub;
|
||||
delete g_nat_beq;
|
||||
delete g_nat_ble;
|
||||
delete g_ne;
|
||||
delete g_neq_of_not_iff;
|
||||
delete g_not;
|
||||
|
|
@ -836,6 +860,8 @@ name const & get_congr_arg_name() { return *g_congr_arg; }
|
|||
name const & get_congr_fun_name() { return *g_congr_fun; }
|
||||
name const & get_decidable_name() { return *g_decidable; }
|
||||
name const & get_decidable_to_bool_name() { return *g_decidable_to_bool; }
|
||||
name const & get_decidable_is_true_name() { return *g_decidable_is_true; }
|
||||
name const & get_decidable_is_false_name() { return *g_decidable_is_false; }
|
||||
name const & get_dite_name() { return *g_dite; }
|
||||
name const & get_empty_name() { return *g_empty; }
|
||||
name const & get_Exists_name() { return *g_Exists; }
|
||||
|
|
@ -980,6 +1006,12 @@ name const & get_nat_one_lt_bit0_name() { return *g_nat_one_lt_bit0; }
|
|||
name const & get_nat_one_lt_bit1_name() { return *g_nat_one_lt_bit1; }
|
||||
name const & get_nat_le_of_lt_name() { return *g_nat_le_of_lt; }
|
||||
name const & get_nat_le_refl_name() { return *g_nat_le_refl; }
|
||||
name const & get_nat_decidable_lt_name() { return *g_nat_decidable_lt; }
|
||||
name const & get_nat_dec_eq_name() { return *g_nat_dec_eq; }
|
||||
name const & get_nat_mul_name() { return *g_nat_mul; }
|
||||
name const & get_nat_sub_name() { return *g_nat_sub; }
|
||||
name const & get_nat_beq_name() { return *g_nat_beq; }
|
||||
name const & get_nat_ble_name() { return *g_nat_ble; }
|
||||
name const & get_ne_name() { return *g_ne; }
|
||||
name const & get_neq_of_not_iff_name() { return *g_neq_of_not_iff; }
|
||||
name const & get_not_name() { return *g_not; }
|
||||
|
|
|
|||
|
|
@ -42,6 +42,8 @@ name const & get_congr_arg_name();
|
|||
name const & get_congr_fun_name();
|
||||
name const & get_decidable_name();
|
||||
name const & get_decidable_to_bool_name();
|
||||
name const & get_decidable_is_true_name();
|
||||
name const & get_decidable_is_false_name();
|
||||
name const & get_dite_name();
|
||||
name const & get_empty_name();
|
||||
name const & get_Exists_name();
|
||||
|
|
@ -186,6 +188,12 @@ name const & get_nat_one_lt_bit0_name();
|
|||
name const & get_nat_one_lt_bit1_name();
|
||||
name const & get_nat_le_of_lt_name();
|
||||
name const & get_nat_le_refl_name();
|
||||
name const & get_nat_decidable_lt_name();
|
||||
name const & get_nat_dec_eq_name();
|
||||
name const & get_nat_mul_name();
|
||||
name const & get_nat_sub_name();
|
||||
name const & get_nat_beq_name();
|
||||
name const & get_nat_ble_name();
|
||||
name const & get_ne_name();
|
||||
name const & get_neq_of_not_iff_name();
|
||||
name const & get_not_name();
|
||||
|
|
|
|||
|
|
@ -35,6 +35,8 @@ congr_arg
|
|||
congr_fun
|
||||
decidable
|
||||
decidable.to_bool
|
||||
decidable.is_true
|
||||
decidable.is_false
|
||||
dite
|
||||
empty
|
||||
Exists
|
||||
|
|
@ -179,6 +181,12 @@ nat.one_lt_bit0
|
|||
nat.one_lt_bit1
|
||||
nat.le_of_lt
|
||||
nat.le_refl
|
||||
nat.decidable_lt
|
||||
nat.dec_eq
|
||||
nat.mul
|
||||
nat.sub
|
||||
nat.beq
|
||||
nat.ble
|
||||
ne
|
||||
neq_of_not_iff
|
||||
not
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue