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

use LRA instead of LIA in strings setup, so that the theory_seq integer value code works

Browse source
This commit is contained in:
Murphy Berzish 2016-06-01 16:34:48 -04:00
parent ecb069b701
commit f8f7014a18
3 changed files with 43 additions and 30 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/smt_setup.cpp
View file

@ -700,7 +700,7 @@ namespace smt {
} }
void setup::setup_QF_S() { void setup::setup_QF_S() {
setup_QF_LIA(); setup_QF_LRA();
m_context.register_plugin(alloc(smt::theory_str, m_manager)); m_context.register_plugin(alloc(smt::theory_str, m_manager));
} }

68
src/smt/theory_str.cpp
View file

@ -21,6 +21,7 @@ Revision History:
#include"ast_pp.h" #include"ast_pp.h"
#include"ast_ll_pp.h" #include"ast_ll_pp.h"
#include<list> #include<list>
#include"theory_arith.h"
namespace smt { namespace smt {
@ -1440,13 +1441,14 @@ void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) {
expr * m = to_app(concatAst2)->get_arg(0); expr * m = to_app(concatAst2)->get_arg(0);
expr * n = to_app(concatAst2)->get_arg(1); expr * n = to_app(concatAst2)->get_arg(1);
rational x_len = get_len_value(x); rational x_len, y_len, m_len, n_len;
rational y_len = get_len_value(y); bool x_len_exists = get_len_value(x, x_len);
rational m_len = get_len_value(m); bool y_len_exists = get_len_value(y, y_len);
rational n_len = get_len_value(n); bool m_len_exists = get_len_value(m, m_len);
bool n_len_exists = get_len_value(n, n_len);
int splitType = -1; int splitType = -1;
if (x_len != rational(-1) && m_len != rational(-1)) { if (x_len_exists && m_len_exists) {
if (x_len < m_len) { if (x_len < m_len) {
splitType = 0; splitType = 0;
} else if (x_len == m_len) { } else if (x_len == m_len) {
@ -1456,7 +1458,7 @@ void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) {
} }
} }
if (splitType == -1 && y_len != rational(-1) && n_len != rational(-1)) { if (splitType == -1 && y_len_exists && n_len_exists) {
if (y_len > n_len) { if (y_len > n_len) {
splitType = 0; splitType = 0;
} else if (y_len == n_len) { } else if (y_len == n_len) {
@ -2367,7 +2369,6 @@ expr * theory_str::get_eqc_value(expr * n, bool & hasEqcValue) {
// from Z3: theory_seq.cpp // from Z3: theory_seq.cpp
/*
static theory_mi_arith* get_th_arith(context& ctx, theory_id afid, expr* e) { static theory_mi_arith* get_th_arith(context& ctx, theory_id afid, expr* e) {
theory* th = ctx.get_theory(afid); theory* th = ctx.get_theory(afid);
if (th && ctx.e_internalized(e)) { if (th && ctx.e_internalized(e)) {
@ -2378,15 +2379,18 @@ static theory_mi_arith* get_th_arith(context& ctx, theory_id afid, expr* e) {
} }
} }
bool theory_seq::get_value(expr* e, rational& val) const { bool theory_str::get_value(expr* e, rational& val) const {
context& ctx = get_context(); context& ctx = get_context();
ast_manager & m = get_manager();
theory_mi_arith* tha = get_th_arith(ctx, m_autil.get_family_id(), e); theory_mi_arith* tha = get_th_arith(ctx, m_autil.get_family_id(), e);
expr_ref _val(m); expr_ref _val(m);
if (!tha || !tha->get_value(ctx.get_enode(e), _val)) return false; if (!tha || !tha->get_value(ctx.get_enode(e), _val)) return false;
return m_autil.is_numeral(_val, val) && val.is_int(); return m_autil.is_numeral(_val, val) && val.is_int();
} }
bool theory_seq::lower_bound(expr* _e, rational& lo) const { // TODO bring these in as well
/*
bool theory_str::lower_bound(expr* _e, rational& lo) const {
context& ctx = get_context(); context& ctx = get_context();
expr_ref e(m_util.str.mk_length(_e), m); expr_ref e(m_util.str.mk_length(_e), m);
theory_mi_arith* tha = get_th_arith(ctx, m_autil.get_family_id(), e); theory_mi_arith* tha = get_th_arith(ctx, m_autil.get_family_id(), e);
@ -2395,7 +2399,7 @@ bool theory_seq::lower_bound(expr* _e, rational& lo) const {
return m_autil.is_numeral(_lo, lo) && lo.is_int(); return m_autil.is_numeral(_lo, lo) && lo.is_int();
} }
bool theory_seq::upper_bound(expr* _e, rational& hi) const { bool theory_str::upper_bound(expr* _e, rational& hi) const {
context& ctx = get_context(); context& ctx = get_context();
expr_ref e(m_util.str.mk_length(_e), m); expr_ref e(m_util.str.mk_length(_e), m);
theory_mi_arith* tha = get_th_arith(ctx, m_autil.get_family_id(), e); theory_mi_arith* tha = get_th_arith(ctx, m_autil.get_family_id(), e);
@ -2403,54 +2407,60 @@ bool theory_seq::upper_bound(expr* _e, rational& hi) const {
if (!tha || !tha->get_upper(ctx.get_enode(e), _hi)) return false; if (!tha || !tha->get_upper(ctx.get_enode(e), _hi)) return false;
return m_autil.is_numeral(_hi, hi) && hi.is_int(); return m_autil.is_numeral(_hi, hi) && hi.is_int();
} }
*/
bool theory_seq::get_length(expr* e, rational& val) const { bool theory_str::get_len_value(expr* e, rational& val) {
context& ctx = get_context(); context& ctx = get_context();
ast_manager & m = get_manager();
theory* th = ctx.get_theory(m_autil.get_family_id()); theory* th = ctx.get_theory(m_autil.get_family_id());
if (!th) return false; if (!th) {
TRACE("t_str_int", tout << "oops, can't get m_autil's theory" << std::endl;);
return false;
}
theory_mi_arith* tha = dynamic_cast<theory_mi_arith*>(th); theory_mi_arith* tha = dynamic_cast<theory_mi_arith*>(th);
if (!tha) return false; if (!tha) {
TRACE("t_str_int", tout << "oops, can't cast to theory_mi_arith" << std::endl;);
return false;
}
TRACE("t_str_int", tout << "checking len value of " << mk_ismt2_pp(e, m) << std::endl;);
rational val1; rational val1;
expr_ref len(m), len_val(m); expr_ref len(m), len_val(m);
expr* e1, *e2; expr* e1, *e2;
ptr_vector<expr> todo; ptr_vector<expr> todo;
todo.push_back(e); todo.push_back(e);
val.reset(); val.reset();
zstring s;
while (!todo.empty()) { while (!todo.empty()) {
expr* c = todo.back(); expr* c = todo.back();
todo.pop_back(); todo.pop_back();
if (m_util.str.is_concat(c, e1, e2)) { if (is_concat(to_app(c))) {
e1 = to_app(c)->get_arg(0);
e2 = to_app(c)->get_arg(1);
todo.push_back(e1); todo.push_back(e1);
todo.push_back(e2); todo.push_back(e2);
} }
else if (m_util.str.is_unit(c)) { else if (is_string(to_app(c))) {
val += rational(1); int sl = m_strutil.get_string_constant_value(c).length();
} val += rational(sl);
else if (m_util.str.is_empty(c)) {
continue;
}
else if (m_util.str.is_string(c, s)) {
val += rational(s.length());
}
else if (!has_length(c)) {
return false;
} }
else { else {
len = m_util.str.mk_length(c); len = mk_strlen(c);
if (ctx.e_internalized(len) && if (ctx.e_internalized(len) &&
tha->get_value(ctx.get_enode(len), len_val) && tha->get_value(ctx.get_enode(len), len_val) &&
m_autil.is_numeral(len_val, val1)) { m_autil.is_numeral(len_val, val1)) {
val += val1; val += val1;
TRACE("t_str_int", tout << "subexpression " << mk_ismt2_pp(len, m) << " has length " << val1 << std::endl;);
} }
else { else {
TRACE("t_str_int", tout << "subexpression " << mk_ismt2_pp(len, m) << " has no length assignment; bailing out" << std::endl;);
return false; return false;
} }
} }
} }
TRACE("t_str_int", tout << "length of " << mk_ismt2_pp(e, m) << " is " << val << std::endl;);
return val.is_int(); return val.is_int();
} }
*/
/* /*
* Look through the equivalence class of n to find an integer constant. * Look through the equivalence class of n to find an integer constant.
@ -2459,6 +2469,7 @@ bool theory_seq::get_length(expr* e, rational& val) const {
* string length cannot be negative. * string length cannot be negative.
*/ */
/*
rational theory_str::get_len_value(expr * x) { rational theory_str::get_len_value(expr * x) {
ast_manager & m = get_manager(); ast_manager & m = get_manager();
context & ctx = get_context(); context & ctx = get_context();
@ -2488,6 +2499,7 @@ rational theory_str::get_len_value(expr * x) {
TRACE("t_str_detail", tout << "eqc contains no integer constants" << std::endl;); TRACE("t_str_detail", tout << "eqc contains no integer constants" << std::endl;);
return rational(-1); return rational(-1);
} }
*/
/* /*
* Decide whether n1 and n2 are already in the same equivalence class. * Decide whether n1 and n2 are already in the same equivalence class.

3
src/smt/theory_str.h
View file

@ -146,7 +146,8 @@ namespace smt {
expr * get_eqc_value(expr * n, bool & hasEqcValue); expr * get_eqc_value(expr * n, bool & hasEqcValue);
bool in_same_eqc(expr * n1, expr * n2); bool in_same_eqc(expr * n1, expr * n2);
rational get_len_value(expr * x); bool get_value(expr* e, rational& val) const;
bool get_len_value(expr* e, rational& val);
bool can_two_nodes_eq(expr * n1, expr * n2); bool can_two_nodes_eq(expr * n1, expr * n2);
bool can_concat_eq_str(expr * concat, std::string str); bool can_concat_eq_str(expr * concat, std::string str);