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

gcm

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-08-29 15:10:35 -07:00
parent 43a5b3dde0
commit 5f9eb8917b
6 changed files with 117 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/ast/sls/bv_sls_eval.cpp
View file

@ -1001,8 +1001,7 @@ namespace bv {
if (a.try_set(m_tmp))
return true;
}
return a.set_random(m_rand);
return a.set_random(m_rand);
}
bool sls_eval::try_repair_sub(bvect const& e, bvval& a, bvval & b, unsigned i) {
@ -1269,7 +1268,7 @@ namespace bv {
}
bool sls_eval::try_repair_ule(bool e, bvval& a, bvval const& b) {
verbose_stream() << "try-repair-ule " << e << " " << a << " " << b << "\n";
//verbose_stream() << "try-repair-ule " << e << " " << a << " " << b << "\n";
if (e) {
// a <= t
return a.set_random_at_most(b.bits(), m_rand);
@ -1285,7 +1284,7 @@ namespace bv {
}
bool sls_eval::try_repair_uge(bool e, bvval& a, bvval const& b) {
verbose_stream() << "try-repair-uge " << e << " " << a << " " << b << "\n";
//verbose_stream() << "try-repair-uge " << e << " " << a << " " << b << "\n";
if (e) {
// a >= t
return a.set_random_at_least(b.bits(), m_rand);

37
src/ast/sls/bv_sls_fixed.cpp
View file

@ -312,29 +312,32 @@ namespace bv {
return;
switch (e->get_decl_kind()) {
case OP_BAND: {
SASSERT(e->get_num_args() == 2);
auto& a = ev.wval(e->get_arg(0));
auto& b = ev.wval(e->get_arg(1));
// (a.fixed & b.fixed) | (a.fixed & ~a.bits) | (b.fixed & ~b.bits)
for (unsigned i = 0; i < a.nw; ++i)
v.fixed[i] = (a.fixed[i] & b.fixed[i]) | (a.fixed[i] & ~a.bits(i)) | (b.fixed[i] & ~b.bits(i));
if (e->get_num_args() == 2) {
auto& a = ev.wval(e->get_arg(0));
auto& b = ev.wval(e->get_arg(1));
// (a.fixed & b.fixed) | (a.fixed & ~a.bits) | (b.fixed & ~b.bits)
for (unsigned i = 0; i < a.nw; ++i)
v.fixed[i] = (a.fixed[i] & b.fixed[i]) | (a.fixed[i] & ~a.bits(i)) | (b.fixed[i] & ~b.bits(i));
}
break;
}
case OP_BOR: {
SASSERT(e->get_num_args() == 2);
auto& a = ev.wval(e->get_arg(0));
auto& b = ev.wval(e->get_arg(1));
// (a.fixed & b.fixed) | (a.fixed & a.bits) | (b.fixed & b.bits)
for (unsigned i = 0; i < a.nw; ++i)
v.fixed[i] = (a.fixed[i] & b.fixed[i]) | (a.fixed[i] & a.bits(i)) | (b.fixed[i] & b.bits(i));
if (e->get_num_args() == 2) {
auto& a = ev.wval(e->get_arg(0));
auto& b = ev.wval(e->get_arg(1));
// (a.fixed & b.fixed) | (a.fixed & a.bits) | (b.fixed & b.bits)
for (unsigned i = 0; i < a.nw; ++i)
v.fixed[i] = (a.fixed[i] & b.fixed[i]) | (a.fixed[i] & a.bits(i)) | (b.fixed[i] & b.bits(i));
}
break;
}
case OP_BXOR: {
SASSERT(e->get_num_args() == 2);
auto& a = ev.wval(e->get_arg(0));
auto& b = ev.wval(e->get_arg(1));
for (unsigned i = 0; i < a.nw; ++i)
v.fixed[i] = a.fixed[i] & b.fixed[i];
if (e->get_num_args() == 2) {
auto& a = ev.wval(e->get_arg(0));
auto& b = ev.wval(e->get_arg(1));
for (unsigned i = 0; i < a.nw; ++i)
v.fixed[i] = a.fixed[i] & b.fixed[i];
}
break;
}
case OP_BNOT: {

2
src/ast/sls/sls_bv_plugin.cpp
View file

@ -91,7 +91,7 @@ namespace sls {
ctx.new_value_eh(t);
is_sat = false;
}
return true;
return is_sat;
}
std::ostream& bv_plugin::display(std::ostream& out) const {

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

@ -119,6 +119,7 @@ namespace sls {
TRACE("sls", tout << "repair down " << mk_bounded_pp(e, m) << "\n");
if (is_app(e)) {
auto p = m_plugins.get(get_fid(e), nullptr);
++m_stats.m_num_repair_down;
if (p && !p->repair_down(to_app(e)) && !m_repair_up.contains(e->get_id())) {
IF_VERBOSE(3, verbose_stream() << "revert repair: " << mk_bounded_pp(e, m) << "\n");
m_repair_up.insert(e->get_id());
@ -128,6 +129,7 @@ namespace sls {
while (!m_repair_up.empty() && !m_new_constraint && m.inc()) {
auto id = m_repair_up.erase_min();
expr* e = term(id);
++m_stats.m_num_repair_up;
TRACE("sls", tout << "repair up " << mk_bounded_pp(e, m) << "\n");
if (is_app(e)) {
auto p = m_plugins.get(get_fid(e), nullptr);
@ -531,11 +533,14 @@ namespace sls {
for (auto p : m_plugins)
if (p)
p->collect_statistics(st);
st.update("sls-repair-down", m_stats.m_num_repair_down);
st.update("sls-repair-up", m_stats.m_num_repair_up);
}
void context::reset_statistics() {
for (auto p : m_plugins)
if (p)
p->reset_statistics();
m_stats.reset();
}
}

7
src/ast/sls/sls_context.h
View file

@ -94,6 +94,12 @@ namespace sls {
}
};
struct stats {
unsigned m_num_repair_down = 0;
unsigned m_num_repair_up = 0;
void reset() { memset(this, 0, sizeof(*this)); }
};
ast_manager& m;
sat_solver_context& s;
scoped_ptr_vector<plugin> m_plugins;
@ -113,6 +119,7 @@ namespace sls {
less_depth m_ld;
heap<greater_depth> m_repair_down;
heap<less_depth> m_repair_up;
stats m_stats;
void register_plugin(plugin* p);