3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-05 09:04:07 +00:00

minimal addition to rewrite bit-vector to character conversion using constant folding.

This commit is contained in:
Nikolaj Bjorner 2022-03-10 17:31:17 -08:00
parent 8f2ea90db1
commit e839e18381
4 changed files with 122 additions and 0 deletions

View file

@ -9,6 +9,7 @@ z3_add_component(rewriter
bv_elim.cpp
bv_rewriter.cpp
cached_var_subst.cpp
char_rewriter.cpp
datatype_rewriter.cpp
der.cpp
distribute_forall.cpp

View file

@ -0,0 +1,62 @@
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
char_rewriter.cpp
Abstract:
Basic rewriting rules for character constraints
Author:
Nikolaj Bjorner (nbjorner) 2015-12-5
--*/
#include "util/debug.h"
#include "ast/rewriter/char_rewriter.h"
#include "ast/bv_decl_plugin.h"
char_rewriter::char_rewriter(ast_manager& m):
m(m) {
m_char = static_cast<char_decl_plugin*>(m.get_plugin(m.mk_family_id("char")));
}
family_id char_rewriter::get_fid() {
return m_char->get_family_id();
}
br_status char_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
SASSERT(f->get_family_id() == get_fid());
br_status st = BR_FAILED;
switch (f->get_decl_kind()) {
case OP_CHAR_CONST:
break;
case OP_CHAR_LE:
break;
case OP_CHAR_TO_INT:
break;
case OP_CHAR_TO_BV:
break;
case OP_CHAR_FROM_BV:
st = mk_char_from_bv(args[0], result);
break;
case OP_CHAR_IS_DIGIT:
break;
}
return st;
}
br_status char_rewriter::mk_char_from_bv(expr* e, expr_ref& result) {
bv_util bv(m);
rational n;
if (bv.is_numeral(e, n) && n.is_unsigned()) {
if (n > m_char->max_char())
return BR_FAILED;
result = m_char->mk_char(n.get_unsigned());
return BR_DONE;
}
return BR_FAILED;
}

View file

@ -0,0 +1,54 @@
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
char_rewriter.h
Abstract:
Basic rewriting rules for characters constraints.
Author:
Nikolaj Bjorner (nbjorner) 2022-03-10
Notes:
--*/
#pragma once
#include "ast/char_decl_plugin.h"
#include "ast/rewriter/rewriter_types.h"
#include "util/params.h"
#include "util/lbool.h"
/**
\brief Cheap rewrite rules for character constraints
*/
class char_rewriter {
ast_manager& m;
char_decl_plugin* m_char;
br_status mk_char_from_bv(expr* e, expr_ref& result);
public:
char_rewriter(ast_manager& m);
family_id get_fid();
br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
expr_ref mk_app(func_decl* f, expr_ref_vector const& args) { return mk_app(f, args.size(), args.data()); }
expr_ref mk_app(func_decl* f, unsigned n, expr* const* args) {
expr_ref result(m);
if (f->get_family_id() != get_fid() ||
BR_FAILED == mk_app_core(f, n, args, result))
result = m.mk_app(f, n, args);
return result;
}
};

View file

@ -21,6 +21,7 @@ Notes:
#include "ast/rewriter/bool_rewriter.h"
#include "ast/rewriter/arith_rewriter.h"
#include "ast/rewriter/bv_rewriter.h"
#include "ast/rewriter/char_rewriter.h"
#include "ast/rewriter/datatype_rewriter.h"
#include "ast/rewriter/array_rewriter.h"
#include "ast/rewriter/fpa_rewriter.h"
@ -48,6 +49,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
dl_rewriter m_dl_rw;
pb_rewriter m_pb_rw;
seq_rewriter m_seq_rw;
char_rewriter m_char_rw;
recfun_rewriter m_rec_rw;
arith_util m_a_util;
bv_util m_bv_util;
@ -247,6 +249,8 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
return m_pb_rw.mk_app_core(f, num, args, result);
if (fid == m_seq_rw.get_fid())
return m_seq_rw.mk_app_core(f, num, args, result);
if (fid == m_char_rw.get_fid())
return m_char_rw.mk_app_core(f, num, args, result);
if (fid == m_rec_rw.get_fid())
return m_rec_rw.mk_app_core(f, num, args, result);
return BR_FAILED;
@ -802,6 +806,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
m_dl_rw(m),
m_pb_rw(m),
m_seq_rw(m),
m_char_rw(m),
m_rec_rw(m),
m_a_util(m),
m_bv_util(m),