mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-28 14:08:55 +00:00
Code Activity

set up test for slicing

Browse source
This commit is contained in:
Jakob Rath 2023-06-15 11:43:14 +02:00
parent 71ef78fb25
commit 136e819cb9
5 changed files with 24 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -198,6 +198,7 @@ namespace polysat {
xs.push_back(x);
}
}
SASSERT(ys.empty());
}
void slicing::find_base(slice src, slice_vector& out_base) const {

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

@ -32,6 +32,8 @@ namespace polysat {
class slicing final {
friend class test_slicing;
// solver& m_solver;
#if 0
@ -111,16 +113,16 @@ namespace polysat {
// Retrieve (or create) base slices s_1,...,s_n such that src[hi:lo] == s_1 ++ ... ++ s_n
void mk_slice(slice src, unsigned hi, unsigned lo, slice_vector& out_base);
// find representative
// Find representative
slice_idx find(slice_idx i) const;
// merge equivalence classes of two base slices
// Merge equivalence classes of two base slices
void merge(slice_idx s1, slice_idx s2);
// Equality x_1 ++ ... ++ x_n == y_1 ++ ... ++ y_k
// Merge equality x_1 ++ ... ++ x_n == y_1 ++ ... ++ y_k
//
// Precondition:
// - sequence of base slices without holes (TODO: condition on holes probably not necessary? total widths have to match of course)
// - sequence of base slices (equal total width)
// - ordered from msb to lsb
// - slices have the same reference point
void merge(slice_vector& xs, slice_vector& ys);