mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

use abstract sort also for value slices

Browse source
This commit is contained in:
Jakob Rath 2023-07-17 18:31:17 +02:00
parent a2fdb03625
commit d1cb02b735
2 changed files with 23 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

21
src/math/polysat/slicing.cpp
View file

@ -94,6 +94,7 @@ namespace polysat {
slicing::slicing(solver& s):
m_solver(s),
m_slice_sort(m_ast),
m_embed_decls(m_ast),
m_concat_decls(m_ast),
m_egraph(m_ast)
{
@ -113,6 +114,15 @@ namespace polysat {
return i.is_slice() ? i : info(i.slice);
}
func_decl* slicing::get_embed_decl(unsigned bit_width) {
func_decl* decl = m_embed_decls.get(bit_width, nullptr);
if (!decl) {
decl = m_ast.mk_func_decl(symbol("embed"), m_bv->mk_sort(bit_width), m_slice_sort);
m_embed_decls.setx(bit_width, decl);
}
return decl;
}
func_decl* slicing::get_concat_decl(unsigned arity) {
SASSERT(arity >= 2);
func_decl* decl = m_concat_decls.get(arity, nullptr);
@ -122,7 +132,7 @@ namespace polysat {
domain.push_back(m_slice_sort);
SASSERT_EQ(arity, domain.size());
// TODO: mk_fresh_func_decl("concat", ...) if overload doesn't work
func_decl* decl = m_ast.mk_func_decl(symbol("slice-concat"), arity, domain.data(), m_slice_sort);
decl = m_ast.mk_func_decl(symbol("slice-concat"), arity, domain.data(), m_slice_sort);
m_concat_decls.setx(arity, decl);
}
return decl;
@ -185,8 +195,8 @@ namespace polysat {
}
slicing::enode* slicing::alloc_slice(unsigned width, pvar var) {
app* a = m_ast.mk_fresh_const("s", m_bv->mk_sort(width), false);
// app* a = m_ast.mk_fresh_const("s", m_slice_sort, false);
// app* a = m_ast.mk_fresh_const("s", m_bv->mk_sort(width), false);
app* a = m_ast.mk_fresh_const("s", m_slice_sort, false);
return alloc_enode(a, width, var);
}
@ -248,8 +258,11 @@ namespace polysat {
slicing::enode* slicing::mk_value_slice(rational const& val, unsigned bit_width) {
SASSERT(0 <= val && val < rational::power_of_two(bit_width));
app* a = m_bv->mk_numeral(val, bit_width);
a = m_ast.mk_app(get_embed_decl(bit_width), a); // adjust sort
enode* s = find_or_alloc_enode(a, bit_width, null_var);
s->mark_interpreted();
SASSERT(s->interpreted());
SASSERT_EQ(get_value(s), val);
return s;
}
@ -261,7 +274,7 @@ namespace polysat {
}
bool slicing::try_get_value(enode* s, rational& val) const {
return m_bv->is_numeral(s->get_expr(), val);
return m_bv->is_numeral(s->get_app()->get_arg(0), val);
}
bool slicing::merge_base(enode* s1, enode* s2, dep_t dep) {

14
src/math/polysat/slicing.h
View file

@ -70,6 +70,7 @@ namespace polysat {
ast_manager m_ast;
scoped_ptr<bv_util> m_bv;
sort_ref m_slice_sort;
func_decl_ref_vector m_embed_decls;
func_decl_ref_vector m_concat_decls;
euf::egraph m_egraph;
@ -80,6 +81,7 @@ namespace polysat {
func_decl* get_embed_decl(unsigned bit_width);
func_decl* get_concat_decl(unsigned arity);
static void* encode_dep(dep_t d);
@ -131,14 +133,6 @@ namespace polysat {
/// If output_base is false, return coarsest intermediate slices instead of only base slices.
void mk_slice(enode* src, unsigned hi, unsigned lo, enode_vector& out, bool output_full_src = false, bool output_base = true);
// Merge equivalence classes of two base slices.
// Returns true if merge succeeded without conflict.
[[nodiscard]] bool merge_base(enode* s1, enode* s2, dep_t dep);
// Merge equality s == val and propagate the value downward into sub-slices.
// Returns true if merge succeeded without conflict.
[[nodiscard]] bool merge_value(enode* s, rational val, dep_t dep);
void begin_explain();
void end_explain();
void push_dep(void* dp, dep_vector& out_deps);
@ -150,6 +144,10 @@ namespace polysat {
// (i.e., x and y have the same base, but are not necessarily in the same equivalence class)
void explain_equal(enode* x, enode* y, dep_vector& out_deps);
// Merge equivalence classes of two base slices.
// Returns true if merge succeeded without conflict.
[[nodiscard]] bool merge_base(enode* s1, enode* s2, dep_t dep);
// Merge equality x_1 ++ ... ++ x_n == y_1 ++ ... ++ y_k
//
// Precondition: