mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

allow range comparison for bit-vectors and int/real

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-03-10 17:08:49 -08:00
parent 1d224d1bcd
commit 081c62d006
2 changed files with 11 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/ast/char_decl_plugin.cpp
View file

@ -16,6 +16,7 @@ Author:
--*/
#include "util/gparams.h"
#include "ast/bv_decl_plugin.h"
#include "ast/char_decl_plugin.h"
#include "ast/arith_decl_plugin.h"
#include "ast/ast_pp.h"
@ -164,6 +165,14 @@ app* char_decl_plugin::mk_le(expr* a, expr* b) {
unsigned v1 = 0, v2 = 0;
if (a == b)
return m_manager->mk_true();
bv_util bv(*m_manager);
if (bv.is_bv(a))
return bv.mk_ule(a, b);
arith_util arith(*m_manager);
if (arith.is_int_real(a))
return arith.mk_le(a, b);
if (a->get_sort() != char_sort())
throw default_exception("range comparison is only supported for bit-vectors, int, real and characters");
bool c1 = is_const_char(a, v1);
bool c2 = is_const_char(b, v2);
if (c1 && c2)

4
src/ast/rewriter/seq_rewriter.cpp
View file

@ -3128,8 +3128,8 @@ void seq_rewriter::mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref
expr_ref range(m());
expr_ref psi(m().mk_false(), m());
if (str().is_unit_string(r1, c1) && str().is_unit_string(r2, c2)) {
SASSERT(u().is_char(c1));
SASSERT(u().is_char(c2));
// SASSERT(u().is_char(c1));
// SASSERT(u().is_char(c2));
// case: c1 <= e <= c2
range = simplify_path(e, m().mk_and(u().mk_le(c1, e), u().mk_le(e, c2)));
psi = simplify_path(e, m().mk_and(path, range));