mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-09 12:50:32 +00:00
Code Activity

add option in theory_str to assert string constant lengths more eagerly

Browse source 
now passes z3str/concat-025
This commit is contained in:
Murphy Berzish 2016-06-12 17:16:14 -04:00
parent fd968783a5
commit 08328c5614
2 changed files with 20 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/smt/theory_str.cpp
View file

@ -30,6 +30,7 @@ theory_str::theory_str(ast_manager & m):
/* Options */ /* Options */
opt_AggressiveLengthTesting(true), opt_AggressiveLengthTesting(true),
opt_AggressiveValueTesting(true), opt_AggressiveValueTesting(true),
opt_EagerStringConstantLengthAssertions(true),
/* Internal setup */ /* Internal setup */
search_started(false), search_started(false),
m_autil(m), m_autil(m),
@ -191,7 +192,9 @@ bool theory_str::internalize_term(app * term) {
//} //}
*/ */
// from theory_seq::internalize_term() // TODO do we still need to do instantiate_concat_axiom()?
// partially from theory_seq::internalize_term()
if (ctx.e_internalized(term)) { if (ctx.e_internalized(term)) {
enode* e = ctx.get_enode(term); enode* e = ctx.get_enode(term);
mk_var(e); mk_var(e);
@ -217,6 +220,12 @@ bool theory_str::internalize_term(app * term) {
else { else {
e = ctx.mk_enode(term, false, m.is_bool(term), true); e = ctx.mk_enode(term, false, m.is_bool(term), true);
} }
if (opt_EagerStringConstantLengthAssertions && m_strutil.is_string(term)) {
TRACE("t_str", tout << "eagerly asserting length of string term " << mk_pp(term, m) << std::endl;);
m_basicstr_axiom_todo.insert(e);
}
theory_var v = mk_var(e); theory_var v = mk_var(e);
TRACE("t_str_detail", tout << "term " << mk_ismt2_pp(term, get_manager()) << " = v#" << v << std::endl;); TRACE("t_str_detail", tout << "term " << mk_ismt2_pp(term, get_manager()) << " = v#" << v << std::endl;);

10
src/smt/theory_str.h
View file

@ -74,6 +74,15 @@ namespace smt {
*/ */
bool opt_AggressiveValueTesting; bool opt_AggressiveValueTesting;
/*
* Setting EagerStringConstantLengthAssertions to true allows some methods,
* in particular internalize_term(), to add
* length assertions about relevant string constants.
* Note that currently this should always be set to 'true', or else *no* length assertions
* will be made about string constants.
*/
bool opt_EagerStringConstantLengthAssertions;
bool search_started; bool search_started;
arith_util m_autil; arith_util m_autil;
str_util m_strutil; str_util m_strutil;
@ -87,6 +96,7 @@ namespace smt {
ptr_vector<enode> m_basicstr_axiom_todo; ptr_vector<enode> m_basicstr_axiom_todo;
svector<std::pair<enode*,enode*> > m_str_eq_todo; svector<std::pair<enode*,enode*> > m_str_eq_todo;
ptr_vector<enode> m_concat_axiom_todo; ptr_vector<enode> m_concat_axiom_todo;
ptr_vector<enode> m_string_constant_length_todo;
int tmpStringVarCount; int tmpStringVarCount;
int tmpXorVarCount; int tmpXorVarCount;