mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

patches to theory_str for theory_seq compat

Browse source
This commit is contained in:
Murphy Berzish 2017-03-01 22:18:18 -05:00
parent d00723e7ea
commit 9f79015ee6
4 changed files with 7 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/smt_setup.cpp
View file

@ -825,7 +825,9 @@ namespace smt {
}
void setup::setup_seq() {
m_context.register_plugin(alloc(theory_seq, m_manager));
// TODO proper negotiation of theory_str vs. theory_seq
//m_context.register_plugin(alloc(theory_seq, m_manager));
setup_str();
}
void setup::setup_card() {

4
src/smt/theory_str.cpp
View file

@ -31,7 +31,7 @@ Revision History:
namespace smt {
theory_str::theory_str(ast_manager & m, theory_str_params const & params):
theory(m.mk_family_id("str")),
theory(m.mk_family_id("seq")),
m_params(params),
/* Options */
opt_EagerStringConstantLengthAssertions(true),
@ -266,7 +266,7 @@ void theory_str::refresh_theory_var(expr * e) {
theory_var theory_str::mk_var(enode* n) {
TRACE("t_str_detail", tout << "mk_var for " << mk_pp(n->get_owner(), get_manager()) << std::endl;);
ast_manager & m = get_manager();
if (!(is_sort_of(m.get_sort(n->get_owner()), u.get_family_id(), _STRING_SORT))) {
if (!(m.get_sort(n->get_owner()) == u.str.mk_string_sort())) {
return null_theory_var;
}
if (is_attached_to_var(n)) {

2
src/smt/theory_str.h
View file

@ -603,7 +603,7 @@ namespace smt {
theory_str(ast_manager & m, theory_str_params const & params);
virtual ~theory_str();
virtual char const * get_name() const { return "strings"; }
virtual char const * get_name() const { return "seq"; }
virtual void display(std::ostream & out) const;
bool overlapping_variables_detected() const { return loopDetected; }