mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-04 13:21:22 +00:00
Code Activity

axiomatize dt

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-10-16 19:01:20 -07:00
parent 180614330a
commit 0755b2b5f7
2 changed files with 8 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/ast/sls/sls_bv_eval.cpp
View file

@ -735,6 +735,7 @@ namespace sls {
a.set_mul(out, out, c.bits()); a.set_mul(out, out, c.bits());
}; };
fold_oper(m_mul_tmp, e, i, f); fold_oper(m_mul_tmp, e, i, f);
m_mul_tmp.set_bw(a.bw);
return try_repair_mul(assign_value(e), wval(e, i), m_mul_tmp); return try_repair_mul(assign_value(e), wval(e, i), m_mul_tmp);
} }
case OP_BNOT: case OP_BNOT:
@ -907,7 +908,7 @@ namespace sls {
auto& v = wval(e); auto& v = wval(e);
v.get_variant(m_tmp, m_rand); v.get_variant(m_tmp, m_rand);
auto d = lookahead(e, m_tmp); auto d = lookahead(e, m_tmp);
verbose_stream() << mk_bounded_pp(e, m) << " " << d << "\n"; //verbose_stream() << mk_bounded_pp(e, m) << " " << d << "\n";
} }
return false; return false;
} }
@ -1105,7 +1106,7 @@ namespace sls {
* 8*e = a*(2b), then a = 4e*b^-1 * 8*e = a*(2b), then a = 4e*b^-1
*/ */
bool bv_eval::try_repair_mul(bvect const& e, bvval& a, bvect const& b) { bool bv_eval::try_repair_mul(bvect const& e, bvval& a, bvect const& b) {
//verbose_stream() << e << " := " << a << " * " << b << "\n"; // verbose_stream() << e << " := " << a << " * " << b << "\n";
unsigned parity_e = a.parity(e); unsigned parity_e = a.parity(e);
unsigned parity_b = a.parity(b); unsigned parity_b = a.parity(b);

8
src/ast/sls/sls_datatype_plugin.cpp
View file

@ -17,12 +17,14 @@ Notes:
Eager reduction to EUF: Eager reduction to EUF:
is-c(c(t)) for each c(t) in T is-c(c(t)) for each c(t) in T
f_i(c(t_i)) = t_i for each c(..t_i..) in T acc_i(c(t_i)) = t_i for each c(..t_i..) in T
is-c(t) => t = c(...acc_j(t)..) for each acc_j(t) in T is-c(t) => t = c(...acc_j(t)..) for each acc_j(t) in T
sum_i is-c_i(t) = 1 sum_i is-c_i(t) = 1
is-c(t) <=> c = t for each 0-ary constructor c is-c(t) <=> c = t for each 0-ary constructor c
is-c(t) <=> t = c(acc_1(t)..acc_n(t))
s = acc(...(acc(t)) => s != t if t is recursive s = acc(...(acc(t)) => s != t if t is recursive
or_i t = t_i if t is a finite sort with terms t_i or_i t = t_i if t is a finite sort with terms t_i
@ -238,7 +240,7 @@ namespace sls {
expr_ref_vector args(m); expr_ref_vector args(m);
for (auto a : acc) for (auto a : acc)
args.push_back(m.mk_app(a, t)); args.push_back(m.mk_app(a, t));
m_axioms.push_back(m.mk_implies(m.mk_app(r, t), m.mk_eq(t, m.mk_app(c, args)))); m_axioms.push_back(m.mk_iff(m.mk_app(r, t), m.mk_eq(t, m.mk_app(c, args))));
} }
// //
@ -456,7 +458,7 @@ namespace sls {
idx = todo.size() - 1; idx = todo.size() - 1;
if (con) if (con)
for (auto child : euf::enode_args(con)) for (auto child : euf::enode_args(con))
if (color.get(child->get_root_id(), white) == white && dt.is_datatype(child->get_expr())) if (color.get(child->get_root_id(), black) != black && dt.is_datatype(child->get_expr()))
todo.push_back({ depth + 1, child, idx }); todo.push_back({ depth + 1, child, idx });
break; break;
} }