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

remove bit-vector dependencies in theory_str_mc. See discussion #4939

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-01-23 13:03:06 -08:00
parent e4cec19f03
commit 47cb1d1207
3 changed files with 19 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/ast/seq_decl_plugin.cpp
View file

@ -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);

6
src/ast/seq_decl_plugin.h
View file

@ -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); }

27
src/smt/theory_str_mc.cpp
View file

@ -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)'?');
}