From e839e18381b83c1171e34fa0955d6770564f379d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 10 Mar 2022 17:31:17 -0800
Subject: [PATCH] minimal addition to rewrite bit-vector to character
conversion using constant folding.
---
src/ast/rewriter/CMakeLists.txt | 1 +
src/ast/rewriter/char_rewriter.cpp | 62 ++++++++++++++++++++++++++++++
src/ast/rewriter/char_rewriter.h | 54 ++++++++++++++++++++++++++
src/ast/rewriter/th_rewriter.cpp | 5 +++
4 files changed, 122 insertions(+)
create mode 100644 src/ast/rewriter/char_rewriter.cpp
create mode 100644 src/ast/rewriter/char_rewriter.h
diff --git a/src/ast/rewriter/CMakeLists.txt b/src/ast/rewriter/CMakeLists.txt
index d2b80ea9c..4bd6d07c4 100644
--- a/src/ast/rewriter/CMakeLists.txt
+++ b/src/ast/rewriter/CMakeLists.txt
@@ -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
diff --git a/src/ast/rewriter/char_rewriter.cpp b/src/ast/rewriter/char_rewriter.cpp
new file mode 100644
index 000000000..5d730d7c6
--- /dev/null
+++ b/src/ast/rewriter/char_rewriter.cpp
@@ -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;
+}
diff --git a/src/ast/rewriter/char_rewriter.h b/src/ast/rewriter/char_rewriter.h
new file mode 100644
index 000000000..f8e3b909e
--- /dev/null
+++ b/src/ast/rewriter/char_rewriter.h
@@ -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;
+ }
+
+};
+
diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp
index 3bc9c4ce1..22d6a83b7 100644
--- a/src/ast/rewriter/th_rewriter.cpp
+++ b/src/ast/rewriter/th_rewriter.cpp
@@ -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),