From 47cb1d1207dfa65faabc6d4b19b9ca84977f9b26 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 23 Jan 2021 13:03:06 -0800
Subject: [PATCH] remove bit-vector dependencies in theory_str_mc. See
discussion #4939
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/ast/seq_decl_plugin.cpp | 5 +++--
src/ast/seq_decl_plugin.h | 6 ++++++
src/smt/theory_str_mc.cpp | 27 ++++++++++-----------------
3 files changed, 19 insertions(+), 19 deletions(-)
diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index a2a0e1da0..41f3a6b50 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -1037,8 +1037,8 @@ app* seq_decl_plugin::mk_char(unsigned u) {
return m_manager->mk_const(f);
}
else {
- UNREACHABLE();
- return nullptr;
+ bv_util bv(*m_manager);
+ return bv.mk_numeral(rational(u), 8);
}
}
@@ -1124,6 +1124,7 @@ expr* seq_decl_plugin::get_some_value(sort* s) {
return nullptr;
}
+
app* seq_util::mk_skolem(symbol const& name, unsigned n, expr* const* args, sort* range) {
SASSERT(range);
parameter param(name);
diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h
index 39fbb1fc6..5729b4ab9 100644
--- a/src/ast/seq_decl_plugin.h
+++ b/src/ast/seq_decl_plugin.h
@@ -238,6 +238,9 @@ public:
bool has_seq() const { return m_has_seq; }
bool is_considered_uninterpreted(func_decl * f) override;
+
+ sort* char_sort() const { return m_char; }
+ sort* string_sort() const { return m_string; }
};
class seq_util {
@@ -254,6 +257,9 @@ public:
ast_manager& get_manager() const { return m; }
+ sort* mk_char_sort() const { return seq.char_sort(); }
+ sort* mk_string_sort() const { return seq.string_sort(); }
+
bool is_char(sort* s) const { return seq.is_char(s); }
bool is_string(sort* s) const { return is_seq(s) && seq.is_char(s->get_parameter(0).get_ast()); }
bool is_seq(sort* s) const { return is_sort_of(s, m_fid, SEQ_SORT); }
diff --git a/src/smt/theory_str_mc.cpp b/src/smt/theory_str_mc.cpp
index c8a6f3dcb..afb134d38 100644
--- a/src/smt/theory_str_mc.cpp
+++ b/src/smt/theory_str_mc.cpp
@@ -619,9 +619,6 @@ namespace smt {
ast_manager & sub_m = subsolver.m();
- bv_util bv(m);
- sort * bv8_sort = bv.mk_sort(8);
-
expr * arg0;
expr * arg1;
expr * arg2;
@@ -646,7 +643,7 @@ namespace smt {
ptr_vector<expr> new_chars;
for (rational i = rational::zero(); i < varLen_value; ++i) {
// TODO we can probably name these better for the sake of debugging
- expr_ref ch(mk_fresh_const("char", bv8_sort), m);
+ expr_ref ch(mk_fresh_const("char", u.mk_char_sort()), m);
new_chars.push_back(ch);
fixed_length_subterm_trail.push_back(ch);
}
@@ -791,7 +788,7 @@ namespace smt {
TRACE("str_fl", tout << "creating character terms for uninterpreted function " << mk_pp(term, m) << ", length = " << ufLen_value << std::endl;);
ptr_vector<expr> new_chars;
for (rational i = rational::zero(); i < ufLen_value; ++i) {
- expr_ref ch(mk_fresh_const("char", bv8_sort), m);
+ expr_ref ch(mk_fresh_const("char", u.mk_char_sort()), m);
new_chars.push_back(ch);
fixed_length_subterm_trail.push_back(ch);
}
@@ -888,11 +885,8 @@ namespace smt {
ast_manager & m = get_manager();
if (bitvector_character_constants.empty()) {
- bv_util bv(m);
- sort * bv8_sort = bv.mk_sort(8);
- for (unsigned i = 0; i < 256; ++i) {
- rational ch(i);
- expr_ref chTerm(bv.mk_numeral(ch, bv8_sort), m);
+ for (unsigned i = 0; i <= u.max_char(); ++i) {
+ expr_ref chTerm(u.mk_char(i), m);
bitvector_character_constants.push_back(chTerm);
fixed_length_subterm_trail.push_back(chTerm);
}
@@ -1232,7 +1226,6 @@ namespace smt {
lbool subproblem_status = subsolver.check(fixed_length_assumptions);
if (subproblem_status == l_true) {
- bv_util bv(m);
TRACE("str_fl", tout << "subsolver found SAT; reconstructing model" << std::endl;);
model_ref subModel;
subsolver.get_model(subModel);
@@ -1246,9 +1239,9 @@ namespace smt {
ptr_vector<expr> char_subterms(entry.m_value);
for (expr * chExpr : char_subterms) {
expr_ref chAssignment(subModel->get_const_interp(to_app(chExpr)->get_decl()), m);
- rational n;
- if (chAssignment != nullptr && bv.is_numeral(chAssignment, n) && n.is_unsigned()) {
- assignment.push_back(n.get_unsigned());
+ unsigned n = 0;
+ if (chAssignment != nullptr && u.is_const_char(chAssignment, n)) {
+ assignment.push_back(n);
} else {
assignment.push_back((unsigned)'?');
}
@@ -1268,9 +1261,9 @@ namespace smt {
ptr_vector<expr> char_subterms(entry.m_value);
for (expr * chExpr : char_subterms) {
expr_ref chAssignment(subModel->get_const_interp(to_app(chExpr)->get_decl()), m);
- rational n;
- if (chAssignment != nullptr && bv.is_numeral(chAssignment, n) && n.is_unsigned()) {
- assignment.push_back(n.get_unsigned());
+ unsigned n = 0;
+ if (chAssignment != nullptr && u.is_const_char(chAssignment, n)) {
+ assignment.push_back(n);
} else {
assignment.push_back((unsigned)'?');
}