mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity

fixes to handling signed operators

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-08-27 14:00:26 -07:00
parent b1f7965697
commit 677b5b4196
3 changed files with 28 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -636,6 +636,28 @@ namespace bv {
return sls_valuation::random_bits(m_rand);
}
bool sls_eval::is_uninterpreted(app* e) const {
if (is_uninterp(e))
return true;
if (e->get_family_id() != bv.get_family_id())
return false;
switch (e->get_decl_kind()) {
case OP_BSREM:
case OP_BSREM_I:
case OP_BSREM0:
case OP_BSMOD:
case OP_BSMOD_I:
case OP_BSMOD0:
case OP_BSDIV:
case OP_BSDIV_I:
case OP_BSDIV0:
return true;
default:
return false;
}
}
bool sls_eval::repair_down(app* e, unsigned i) {
if (e->get_family_id() == bv.get_family_id() && try_repair_bv(e, i)) {
commit_eval(to_app(e->get_arg(i)));
@ -807,6 +829,7 @@ namespace bv {
case OP_BSDIV:
case OP_BSDIV_I:
case OP_BSDIV0:
UNREACHABLE();
// these are currently compiled to udiv and urem.
// there is an equation that enforces equality between the semantics
// of these operators.
@ -1900,9 +1923,9 @@ namespace bv {
void sls_eval::commit_eval(app* e) {
if (!bv.is_bv(e))
return;
//verbose_stream() << mk_bounded_pp(e, m) << " " << wval(e) << "\n";
// verbose_stream() << mk_bounded_pp(e, m) << " " << wval(e) << "\n";
//
// SASSERT(wval(e).commit_eval());
SASSERT(wval(e).commit_eval());
VERIFY(wval(e).commit_eval());
}

2
src/ast/sls/bv_sls_eval.h
View file

@ -160,6 +160,8 @@ namespace bv {
bool eval_is_correct(app* e);
bool is_uninterpreted(app* e) const;
expr_ref get_value(app* e);
bool bval1(app* e) const;

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

@ -107,7 +107,7 @@ namespace sls {
bool bv_plugin::repair_down(app* e) {
unsigned n = e->get_num_args();
if (n == 0 || m_eval.eval_is_correct(e))
if (n == 0 || m_eval.is_uninterpreted(e) || m_eval.eval_is_correct(e))
return true;
if (n == 2) {