mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-03 16:19:57 +00:00
Code Activity

Merge shared parts from polysat branch (#7063)

Browse source 
* sat_literal: make constants constexpr

* dlist: rename elem -> list

* tbv: use get_bit

* additional pdd and rational tests

* egraph: callback setters take functions by value

This allows to set callbacks without defining a separate variable for
the callback lambda.

(previous usage does one copy of the function, exactly as before)

* cmake: enable compiler error when non-void function does not return value
This commit is contained in:
Jakob Rath 2023-12-28 20:11:53 +01:00 committed by GitHub
parent 53c95e3627
commit ec2b8eb4ca
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
7 changed files with 101 additions and 43 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
cmake/compiler_warnings.cmake
View file

@ -30,6 +30,8 @@ set(MSVC_WARNINGS "/W3")
set(GCC_AND_CLANG_WARNINGS_AS_ERRORS
# https://clang.llvm.org/docs/DiagnosticsReference.html#wodr
"-Werror=odr"
# https://clang.llvm.org/docs/DiagnosticsReference.html#wreturn-type
"-Werror=return-type"
)
set(GCC_WARNINGS_AS_ERRORS
""

29
src/ast/euf/euf_egraph.h
View file

@ -192,8 +192,8 @@ namespace euf {
enode_vector m_empty_enodes;
unsigned m_num_scopes = 0;
bool m_inconsistent = false;
enode *m_n1 = nullptr;
enode *m_n2 = nullptr;
enode* m_n1 = nullptr;
enode* m_n2 = nullptr;
justification m_justification;
unsigned m_new_th_eqs_qhead = 0;
svector<th_eq> m_new_th_eqs;
@ -205,11 +205,11 @@ namespace euf {
uint64_t m_congruence_timestamp = 0;
std::vector<std::function<void(enode*,enode*)>> m_on_merge;
std::function<void(enode*, enode*)> m_on_propagate_literal;
std::function<void(enode*)> m_on_make;
std::function<void(expr*,expr*,expr*)> m_used_eq;
std::function<void(app*,app*)> m_used_cc;
std::function<void(std::ostream&, void*)> m_display_justification;
std::function<void(enode*,enode*)> m_on_propagate_literal;
std::function<void(enode*)> m_on_make;
std::function<void(expr*,expr*,expr*)> m_used_eq;
std::function<void(app*,app*)> m_used_cc;
std::function<void(std::ostream&,void*)> m_display_justification;
void push_eq(enode* r1, enode* n1, unsigned r2_num_parents) {
m_updates.push_back(update_record(r1, n1, r2_num_parents));
@ -279,7 +279,6 @@ namespace euf {
void merge(enode* n1, enode* n2, void* reason) { merge(n1, n2, justification::external(reason)); }
void new_diseq(enode* n);
/**
\brief propagate set of merges.
This call may detect an inconsistency. Then inconsistent() is true.
@ -326,13 +325,13 @@ namespace euf {
void set_relevant(enode* n);
void set_default_relevant(bool b) { m_default_relevant = b; }
void set_on_merge(std::function<void(enode* root,enode* other)>& on_merge) { m_on_merge.push_back(on_merge); }
void set_on_propagate(std::function<void(enode* lit,enode* ante)>& on_propagate) { m_on_propagate_literal = on_propagate; }
void set_on_make(std::function<void(enode* n)>& on_make) { m_on_make = on_make; }
void set_used_eq(std::function<void(expr*,expr*,expr*)>& used_eq) { m_used_eq = used_eq; }
void set_used_cc(std::function<void(app*,app*)>& used_cc) { m_used_cc = used_cc; }
void set_display_justification(std::function<void (std::ostream&, void*)> & d) { m_display_justification = d; }
void set_on_merge(std::function<void(enode* root,enode* other)> on_merge) { m_on_merge.push_back(std::move(on_merge)); }
void set_on_propagate(std::function<void(enode* lit,enode* ante)> on_propagate) { m_on_propagate_literal = std::move(on_propagate); }
void set_on_make(std::function<void(enode* n)> on_make) { m_on_make = std::move(on_make); }
void set_used_eq(std::function<void(expr*,expr*,expr*)> used_eq) { m_used_eq = std::move(used_eq); }
void set_used_cc(std::function<void(app*,app*)> used_cc) { m_used_cc = std::move(used_cc); }
void set_display_justification(std::function<void(std::ostream&, void*)> d) { m_display_justification = std::move(d); }
void begin_explain();
void end_explain();
bool uses_congruence() const { return m_uses_congruence; }

48
src/test/pdd.cpp
View file

@ -153,12 +153,49 @@ public:
pdd b = m.mk_var(1);
pdd c = m.mk_var(2);
pdd d = m.mk_var(3);
pdd p = (a + b)*(c + 3*d) + 2;
std::cout << p << "\n";
for (auto const& m : p) {
std::cout << m << "\n";
}
auto const check = [](unsigned const expected_num_monomials, pdd const& p) {
unsigned count = 0;
std::cout << p << "\n";
for (auto const& m : p) {
std::cout << " " << m << "\n";
++count;
}
VERIFY_EQ(expected_num_monomials, count);
};
check(9, (a + b + 2)*(c + 3*d + 5) + 2);
check(5, (a + b)*(c + 3*d) + 2);
check(1, a);
check(2, a + 5);
check(1, m.mk_val(5));
check(0, m.mk_val(0));
}
static void linear_iterator() {
std::cout << "test linear iterator\n";
pdd_manager m(4);
pdd a = m.mk_var(0);
pdd b = m.mk_var(1);
pdd c = m.mk_var(2);
pdd d = m.mk_var(3);
pdd p = (a + b + 2)*(c + 3*d + 5) + 2;
std::cout << p << "\n";
for (auto const& m : p.linear_monomials())
std::cout << " " << m << "\n";
std::cout << a << "\n";
for (auto const& m : a.linear_monomials())
std::cout << " " << m << "\n";
pdd one = m.mk_val(5);
std::cout << one << "\n";
for (auto const& m : one.linear_monomials())
std::cout << " " << m << "\n";
pdd zero = m.mk_val(0);
std::cout << zero << "\n";
for (auto const& m : zero.linear_monomials())
std::cout << " " << m << "\n";
}
static void order() {
std::cout << "order\n";
pdd_manager m(4);
@ -693,6 +730,7 @@ void tst_pdd() {
dd::test::canonize();
dd::test::reset();
dd::test::iterator();
dd::test::linear_iterator();
dd::test::order();
dd::test::order_lm();
dd::test::mod4_operations();

23
src/test/rational.cpp
View file

@ -466,6 +466,28 @@ static void tst12() {
std::cout << i << ": " << r.get_bit(i) << "\n";
}
static void tst13() {
std::cout << "test13\n";
rational const step = rational(1) / rational(3);
for (rational r; r < 5000; r += step) {
{
unsigned k = r.prev_power_of_two();
if (r >= 1) {
VERIFY(rational::power_of_two(k) <= r);
VERIFY(r < rational::power_of_two(k + 1));
}
else {
VERIFY_EQ(k, 0);
}
}
{
unsigned k = r.next_power_of_two();
VERIFY(r <= rational::power_of_two(k));
VERIFY(k == 0 || rational::power_of_two(k - 1) < r);
}
}
}
void tst_rational() {
TRACE("rational", tout << "starting rational test...\n";);
@ -492,4 +514,5 @@ void tst_rational() {
tst10(true);
tst10(false);
tst12();
tst13();
}

19
src/util/dlist.h
View file

@ -188,14 +188,14 @@ class dll_iterator {
dll_iterator(T const* elem, bool first): m_elem(elem), m_first(first) { }
public:
static dll_iterator mk_begin(T const* elem) {
// Setting first==(bool)elem makes this also work for elem==nullptr;
static dll_iterator mk_begin(T const* list) {
// Setting first==(bool)list makes this also work for list==nullptr;
// but we can't implement top-level begin/end for pointers because it clashes with the definition for arrays.
return {elem, (bool)elem};
return {list, (bool)list};
}
static dll_iterator mk_end(T const* elem) {
return {elem, false};
static dll_iterator mk_end(T const* list) {
return {list, false};
}
using value_type = T;
@ -232,18 +232,17 @@ public:
dll_iterator<T> end() const { return dll_iterator<T>::mk_end(m_list); }
};
template < typename T
, typename U = std::enable_if_t<std::is_base_of_v<dll_base<T>, T>> // should only match if T actually inherits from dll_base<T>
>
dll_iterator<T> begin(T const& elem) {
return dll_iterator<T>::mk_begin(&elem);
dll_iterator<T> begin(T const& list) {
return dll_iterator<T>::mk_begin(&list);
}
template < typename T
, typename U = std::enable_if_t<std::is_base_of_v<dll_base<T>, T>> // should only match if T actually inherits from dll_base<T>
>
dll_iterator<T> end(T const& elem)
dll_iterator<T> end(T const& list)
{
return dll_iterator<T>::mk_end(&elem);
return dll_iterator<T>::mk_end(&list);
}

15
src/util/sat_literal.h
View file

@ -30,7 +30,7 @@ namespace sat {
typedef svector<bool_var> bool_var_vector;
const bool_var null_bool_var = UINT_MAX >> 1;
inline constexpr bool_var null_bool_var = UINT_MAX >> 1;
/**
\brief The literal b is represented by the value 2*b, and
@ -39,9 +39,7 @@ namespace sat {
class literal {
unsigned m_val;
public:
literal():m_val(null_bool_var << 1) {
SASSERT(var() == null_bool_var && !sign());
}
constexpr literal(): m_val(null_bool_var << 1) { }
explicit literal(bool_var v, bool _sign = false):
m_val((v << 1) + static_cast<unsigned>(_sign)) {
@ -49,11 +47,11 @@ namespace sat {
SASSERT(sign() == _sign);
}
bool_var var() const {
constexpr bool_var var() const {
return m_val >> 1;
}
bool sign() const {
constexpr bool sign() const {
return m_val & 1ul;
}
@ -86,7 +84,10 @@ namespace sat {
friend bool operator!=(literal const & l1, literal const & l2);
};
const literal null_literal;
inline constexpr literal null_literal;
static_assert(null_literal.var() == null_bool_var);
static_assert(!null_literal.sign());
using literal_hash = obj_hash<literal>;
inline literal to_literal(unsigned x) { literal l; l.m_val = x; return l; }

8
src/util/tbv.cpp
View file

@ -142,12 +142,8 @@ void tbv_manager::set(tbv& dst, rational const& r, unsigned hi, unsigned lo) {
set(dst, r.get_uint64(), hi, lo);
return;
}
for (unsigned i = 0; i < hi - lo + 1; ++i) {
if (bitwise_and(r, rational::power_of_two(i)).is_zero())
set(dst, lo + i, BIT_0);
else
set(dst, lo + i, BIT_1);
}
for (unsigned i = 0; i < hi - lo + 1; ++i)
set(dst, lo + i, r.get_bit(i) ? BIT_1 : BIT_0);
}
void tbv_manager::set(tbv& dst, tbv const& other, unsigned hi, unsigned lo) {