1 /*++ 2 Module Name: 3 4 theory_str.h 5 6 Abstract: 7 8 String Theory Plugin 9 10 Author: 11 12 Murphy Berzish and Yunhui Zheng 13 14 Revision History: 15 16 --*/ 17 #pragma once 18 19 #include "util/trail.h" 20 #include "util/union_find.h" 21 #include "util/scoped_ptr_vector.h" 22 #include "util/hashtable.h" 23 #include "ast/ast_pp.h" 24 #include "ast/arith_decl_plugin.h" 25 #include "ast/rewriter/th_rewriter.h" 26 #include "ast/rewriter/seq_rewriter.h" 27 #include "ast/seq_decl_plugin.h" 28 #include "model/value_factory.h" 29 #include "smt/smt_theory.h" 30 #include "smt/params/theory_str_params.h" 31 #include "smt/smt_model_generator.h" 32 #include "smt/smt_arith_value.h" 33 #include "smt/smt_kernel.h" 34 #include<set> 35 #include<stack> 36 #include<vector> 37 #include<map> 38 #include<functional> 39 40 namespace smt { 41 42 typedef hashtable<symbol, symbol_hash_proc, symbol_eq_proc> symbol_set; 43 typedef int_hashtable<int_hash, default_eq<int> > integer_set; 44 45 class str_value_factory : public value_factory { 46 seq_util u; 47 symbol_set m_strings; 48 std::string delim; 49 unsigned m_next; 50 public: str_value_factory(ast_manager & m,family_id fid)51 str_value_factory(ast_manager & m, family_id fid) : 52 value_factory(m, fid), 53 u(m), delim("!"), m_next(0) {} ~str_value_factory()54 ~str_value_factory() override {} get_some_value(sort * s)55 expr * get_some_value(sort * s) override { 56 return u.str.mk_string("some value"); 57 } get_some_values(sort * s,expr_ref & v1,expr_ref & v2)58 bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2) override { 59 v1 = u.str.mk_string("value 1"); 60 v2 = u.str.mk_string("value 2"); 61 return true; 62 } get_fresh_value(sort * s)63 expr * get_fresh_value(sort * s) override { 64 if (u.is_string(s)) { 65 while (true) { 66 std::ostringstream strm; 67 strm << delim << std::hex << (m_next++) << std::dec << delim; 68 std::string s(strm.str()); 69 symbol sym(s); 70 if (m_strings.contains(sym)) continue; 71 m_strings.insert(sym); 72 return u.str.mk_string(s); 73 } 74 } 75 sort* seq = nullptr; 76 if (u.is_re(s, seq)) { 77 expr* v0 = get_fresh_value(seq); 78 return u.re.mk_to_re(v0); 79 } 80 TRACE("t_str", tout << "unexpected sort in get_fresh_value(): " << mk_pp(s, m_manager) << std::endl;); 81 UNREACHABLE(); return nullptr; 82 } register_value(expr * n)83 void register_value(expr * n) override { /* Ignore */ } 84 }; 85 86 // NSB: added operator[] and contains to obj_pair_hashtable 87 class theory_str_contain_pair_bool_map_t : public obj_pair_map<expr, expr, expr*> {}; 88 89 template<typename Ctx> 90 class binary_search_trail : public trail { 91 obj_map<expr, ptr_vector<expr> > & target; 92 expr * entry; 93 public: binary_search_trail(obj_map<expr,ptr_vector<expr>> & target,expr * entry)94 binary_search_trail(obj_map<expr, ptr_vector<expr> > & target, expr * entry) : 95 target(target), entry(entry) {} ~binary_search_trail()96 ~binary_search_trail() override {} undo()97 void undo() override { 98 TRACE("t_str_binary_search", tout << "in binary_search_trail::undo()" << std::endl;); 99 if (target.contains(entry)) { 100 if (!target[entry].empty()) { 101 target[entry].pop_back(); 102 } else { 103 TRACE("t_str_binary_search", tout << "WARNING: attempt to remove length tester from an empty stack" << std::endl;); 104 } 105 } else { 106 TRACE("t_str_binary_search", tout << "WARNING: attempt to access length tester map via invalid key" << std::endl;); 107 } 108 } 109 }; 110 111 class regex_automaton_under_assumptions { 112 protected: 113 expr * re_term; 114 eautomaton * aut; 115 bool polarity; 116 117 bool assume_lower_bound; 118 rational lower_bound; 119 120 bool assume_upper_bound; 121 rational upper_bound; 122 public: regex_automaton_under_assumptions()123 regex_automaton_under_assumptions() : 124 re_term(nullptr), aut(nullptr), polarity(false), 125 assume_lower_bound(false), assume_upper_bound(false) {} 126 regex_automaton_under_assumptions(expr * re_term,eautomaton * aut,bool polarity)127 regex_automaton_under_assumptions(expr * re_term, eautomaton * aut, bool polarity) : 128 re_term(re_term), aut(aut), polarity(polarity), 129 assume_lower_bound(false), assume_upper_bound(false) {} 130 set_lower_bound(rational & lb)131 void set_lower_bound(rational & lb) { 132 lower_bound = lb; 133 assume_lower_bound = true; 134 } unset_lower_bound()135 void unset_lower_bound() { 136 assume_lower_bound = false; 137 } 138 set_upper_bound(rational & ub)139 void set_upper_bound(rational & ub) { 140 upper_bound = ub; 141 assume_upper_bound = true; 142 } unset_upper_bound()143 void unset_upper_bound() { 144 assume_upper_bound = false; 145 } 146 get_lower_bound(rational & lb)147 bool get_lower_bound(rational & lb) const { 148 if (assume_lower_bound) { 149 lb = lower_bound; 150 return true; 151 } else { 152 return false; 153 } 154 } 155 get_upper_bound(rational & ub)156 bool get_upper_bound(rational & ub) const { 157 if (assume_upper_bound) { 158 ub = upper_bound; 159 return true; 160 } else { 161 return false; 162 } 163 } 164 get_automaton()165 eautomaton * get_automaton() const { return aut; } get_regex_term()166 expr * get_regex_term() const { return re_term; } get_polarity()167 bool get_polarity() const { return polarity; } 168 }; 169 170 class char_union_find { 171 unsigned_vector m_find; 172 unsigned_vector m_size; 173 unsigned_vector m_next; 174 175 integer_set char_const_set; 176 177 u_map<svector<expr*> > m_justification; // representative -> list of formulas justifying EQC 178 ensure_size(unsigned v)179 void ensure_size(unsigned v) { 180 while (v >= get_num_vars()) { 181 mk_var(); 182 } 183 } 184 public: mk_var()185 unsigned mk_var() { 186 unsigned r = m_find.size(); 187 m_find.push_back(r); 188 m_size.push_back(1); 189 m_next.push_back(r); 190 return r; 191 } get_num_vars()192 unsigned get_num_vars() const { return m_find.size(); } mark_as_char_const(unsigned r)193 void mark_as_char_const(unsigned r) { 194 char_const_set.insert((int)r); 195 } is_char_const(unsigned r)196 bool is_char_const(unsigned r) { 197 return char_const_set.contains((int)r); 198 } 199 find(unsigned v)200 unsigned find(unsigned v) const { 201 if (v >= get_num_vars()) { 202 return v; 203 } 204 while (true) { 205 unsigned new_v = m_find[v]; 206 if (new_v == v) 207 return v; 208 v = new_v; 209 } 210 } 211 next(unsigned v)212 unsigned next(unsigned v) const { 213 if (v >= get_num_vars()) { 214 return v; 215 } 216 return m_next[v]; 217 } 218 is_root(unsigned v)219 bool is_root(unsigned v) const { 220 return v >= get_num_vars() || m_find[v] == v; 221 } 222 get_justification(unsigned v)223 svector<expr*> get_justification(unsigned v) { 224 unsigned r = find(v); 225 svector<expr*> retval; 226 if (m_justification.find(r, retval)) { 227 return retval; 228 } else { 229 return svector<expr*>(); 230 } 231 } 232 merge(unsigned v1,unsigned v2,expr * justification)233 void merge(unsigned v1, unsigned v2, expr * justification) { 234 unsigned r1 = find(v1); 235 unsigned r2 = find(v2); 236 if (r1 == r2) 237 return; 238 ensure_size(v1); 239 ensure_size(v2); 240 // swap r1 and r2 if: 241 // 1. EQC of r1 is bigger than EQC of r2 242 // 2. r1 is a character constant and r2 is not. 243 // this maintains the invariant that if a character constant is in an eqc then it is the root of that eqc 244 if (m_size[r1] > m_size[r2] || (is_char_const(r1) && !is_char_const(r2))) { 245 std::swap(r1, r2); 246 } 247 m_find[r1] = r2; 248 m_size[r2] += m_size[r1]; 249 std::swap(m_next[r1], m_next[r2]); 250 251 if (m_justification.contains(r1)) { 252 // add r1's justifications to r2 253 if (!m_justification.contains(r2)) { 254 m_justification.insert(r2, m_justification[r1]); 255 } else { 256 m_justification[r2].append(m_justification[r1]); 257 } 258 m_justification.remove(r1); 259 } 260 if (justification != nullptr) { 261 if (!m_justification.contains(r2)) { 262 m_justification.insert(r2, svector<expr*>()); 263 } 264 m_justification[r2].push_back(justification); 265 } 266 } 267 reset()268 void reset() { 269 m_find.reset(); 270 m_next.reset(); 271 m_size.reset(); 272 char_const_set.reset(); 273 m_justification.reset(); 274 } 275 }; 276 277 class theory_str : public theory { 278 struct T_cut 279 { 280 int level; 281 obj_map<expr, int> vars; 282 T_cutT_cut283 T_cut() { 284 level = -100; 285 } 286 }; 287 288 typedef union_find<theory_str> th_union_find; 289 290 typedef map<rational, expr*, obj_hash<rational>, default_eq<rational> > rational_map; 291 struct zstring_hash_proc { operatorzstring_hash_proc292 unsigned operator()(zstring const & s) const { 293 auto str = s.encode(); 294 return string_hash(str.c_str(), static_cast<unsigned>(s.length()), 17); 295 } 296 }; 297 typedef map<zstring, expr*, zstring_hash_proc, default_eq<zstring> > string_map; 298 299 struct stats { statsstats300 stats() { reset(); } resetstats301 void reset() { memset(this, 0, sizeof(stats)); } 302 unsigned m_refine_eq; 303 unsigned m_refine_neq; 304 unsigned m_refine_f; 305 unsigned m_refine_nf; 306 unsigned m_solved_by; 307 unsigned m_fixed_length_iterations; 308 }; 309 310 protected: 311 theory_str_params const & m_params; 312 313 /* 314 * Setting EagerStringConstantLengthAssertions to true allows some methods, 315 * in particular internalize_term(), to add 316 * length assertions about relevant string constants. 317 * Note that currently this should always be set to 'true', or else *no* length assertions 318 * will be made about string constants. 319 */ 320 bool opt_EagerStringConstantLengthAssertions; 321 322 /* 323 * If VerifyFinalCheckProgress is set to true, continuing after final check is invoked 324 * without asserting any new axioms is considered a bug and will throw an exception. 325 */ 326 bool opt_VerifyFinalCheckProgress; 327 328 /* 329 * This constant controls how eagerly we expand unrolls in unbounded regex membership tests. 330 */ 331 int opt_LCMUnrollStep; 332 333 /* 334 * If NoQuickReturn_IntegerTheory is set to true, 335 * integer theory integration checks that assert axioms 336 * will not return from the function after asserting their axioms. 337 * The default behaviour of Z3str2 is to set this to 'false'. This may be incorrect. 338 */ 339 bool opt_NoQuickReturn_IntegerTheory; 340 341 /* 342 * If DisableIntegerTheoryIntegration is set to true, 343 * ALL calls to the integer theory integration methods 344 * (get_arith_value, get_len_value, lower_bound, upper_bound) 345 * will ignore what the arithmetic solver believes about length terms, 346 * and will return no information. 347 * 348 * This reduces performance significantly, but can be useful to enable 349 * if it is suspected that string-integer integration, or the arithmetic solver itself, 350 * might have a bug. 351 * 352 * The default behaviour of Z3str2 is to set this to 'false'. 353 */ 354 bool opt_DisableIntegerTheoryIntegration; 355 356 /* 357 * If DeferEQCConsistencyCheck is set to true, 358 * expensive calls to new_eq_check() will be deferred until final check, 359 * at which time the consistency of *all* string equivalence classes will be validated. 360 */ 361 bool opt_DeferEQCConsistencyCheck; 362 363 /* 364 * If CheckVariableScope is set to true, 365 * pop_scope_eh() and final_check_eh() will run extra checks 366 * to determine whether the current assignment 367 * contains references to any internal variables that are no longer in scope. 368 */ 369 bool opt_CheckVariableScope; 370 371 /* 372 * If ConcatOverlapAvoid is set to true, 373 * the check to simplify Concat = Concat in handle_equality() will 374 * avoid simplifying wrt. pairs of Concat terms that will immediately 375 * result in an overlap. (false = Z3str2 behaviour) 376 */ 377 bool opt_ConcatOverlapAvoid; 378 379 bool search_started; 380 arith_util m_autil; 381 seq_util u; 382 int sLevel; 383 384 bool finalCheckProgressIndicator; 385 386 expr_ref_vector m_trail; // trail for generated terms 387 388 str_value_factory * m_factory; 389 390 re2automaton m_mk_aut; 391 392 // Unique identifier appended to unused variables to ensure that model construction 393 // does not introduce equalities when they weren't enforced. 394 unsigned m_unused_id; 395 396 // terms we couldn't go through set_up_axioms() with because they weren't internalized 397 expr_ref_vector m_delayed_axiom_setup_terms; 398 399 ptr_vector<enode> m_basicstr_axiom_todo; 400 ptr_vector<enode> m_concat_axiom_todo; 401 ptr_vector<enode> m_string_constant_length_todo; 402 ptr_vector<enode> m_concat_eval_todo; 403 expr_ref_vector m_delayed_assertions_todo; 404 405 // enode lists for library-aware/high-level string terms (e.g. substr, contains) 406 ptr_vector<enode> m_library_aware_axiom_todo; 407 408 // list of axioms that are re-asserted every time the scope is popped 409 expr_ref_vector m_persisted_axioms; 410 expr_ref_vector m_persisted_axiom_todo; 411 412 // hashtable of all exprs for which we've already set up term-specific axioms -- 413 // this prevents infinite recursive descent with respect to axioms that 414 // include an occurrence of the term for which axioms are being generated 415 obj_hashtable<expr> axiomatized_terms; 416 417 // hashtable of all top-level exprs for which set_up_axioms() has been called 418 obj_hashtable<expr> existing_toplevel_exprs; 419 420 int tmpStringVarCount; 421 int tmpXorVarCount; 422 // obj_pair_map<expr, expr, std::map<int, expr*> > varForBreakConcat; 423 std::map<std::pair<expr*,expr*>, std::map<int, expr*> > varForBreakConcat; 424 bool avoidLoopCut; 425 bool loopDetected; 426 obj_map<expr, std::stack<T_cut*> > cut_var_map; 427 scoped_ptr_vector<T_cut> m_cut_allocs; 428 expr_ref m_theoryStrOverlapAssumption_term; 429 430 obj_hashtable<expr> variable_set; 431 obj_hashtable<expr> internal_variable_set; 432 std::map<int, obj_hashtable<expr> > internal_variable_scope_levels; 433 434 expr_ref_vector contains_map; 435 436 theory_str_contain_pair_bool_map_t contain_pair_bool_map; 437 obj_map<expr, std::set<std::pair<expr*, expr*> > > contain_pair_idx_map; 438 439 // regex automata 440 scoped_ptr_vector<eautomaton> m_automata; 441 ptr_vector<eautomaton> regex_automata; 442 obj_hashtable<expr> regex_terms; 443 obj_map<expr, ptr_vector<expr> > regex_terms_by_string; // S --> [ (str.in.re S *) ] 444 obj_map<expr, svector<regex_automaton_under_assumptions> > regex_automaton_assumptions; // RegEx --> [ aut+assumptions ] 445 obj_hashtable<expr> regex_terms_with_path_constraints; // set of string terms which have had path constraints asserted in the current scope 446 obj_hashtable<expr> regex_terms_with_length_constraints; // set of regex terms which had had length constraints asserted in the current scope 447 obj_map<expr, expr*> regex_term_to_length_constraint; // (str.in.re S R) -> (length constraint over S wrt. R) 448 obj_map<expr, ptr_vector<expr> > regex_term_to_extra_length_vars; // extra length vars used in regex_term_to_length_constraint entries 449 450 // keep track of the last lower/upper bound we saw for each string term 451 // so we don't perform duplicate work 452 obj_map<expr, rational> regex_last_lower_bound; 453 obj_map<expr, rational> regex_last_upper_bound; 454 455 // each counter maps a (str.in.re) expression to an integer. 456 // use helper functions regex_inc_counter() and regex_get_counter() to access 457 obj_map<expr, unsigned> regex_length_attempt_count; 458 obj_map<expr, unsigned> regex_fail_count; 459 obj_map<expr, unsigned> regex_intersection_fail_count; 460 461 obj_map<expr, ptr_vector<expr> > string_chars; // S --> [S_0, S_1, ...] for character terms S_i 462 463 obj_pair_map<expr, expr, expr*> concat_astNode_map; 464 465 // all (str.to-int) and (int.to-str) terms 466 expr_ref_vector string_int_conversion_terms; 467 obj_hashtable<expr> string_int_axioms; 468 469 string_map stringConstantCache; 470 unsigned long totalCacheAccessCount; 471 unsigned long cacheHitCount; 472 unsigned long cacheMissCount; 473 474 unsigned m_fresh_id; 475 476 // cache mapping each string S to Length(S) 477 obj_map<expr, app*> length_ast_map; 478 479 trail_stack m_trail_stack; 480 trail_stack m_library_aware_trail_stack; 481 th_union_find m_find; 482 theory_var get_var(expr * n) const; 483 expr * get_eqc_next(expr * n); 484 app * get_ast(theory_var i); 485 486 // fixed length model construction 487 expr_ref_vector fixed_length_subterm_trail; // trail for subterms generated *in the subsolver* 488 expr_ref_vector fixed_length_assumptions; // cache of boolean terms to assert *into the subsolver*, unsat core is a subset of these 489 obj_map<expr, rational> fixed_length_used_len_terms; // constraints used in generating fixed length model 490 obj_map<expr, expr_ref_vector* > var_to_char_subterm_map; // maps a var to a list of character terms *in the subsolver* 491 obj_map<expr, expr_ref_vector* > uninterpreted_to_char_subterm_map; // maps an "uninterpreted" string term to a list of character terms *in the subsolver* 492 obj_map<expr, std::tuple<rational, expr*, expr*>> fixed_length_lesson; //keep track of information for the lesson 493 unsigned preprocessing_iteration_count; // number of attempts we've made to solve by preprocessing length information 494 obj_map<expr, zstring> candidate_model; 495 496 stats m_stats; 497 498 protected: 499 void reset_internal_data_structures(); 500 501 void assert_axiom(expr * e); 502 void assert_implication(expr * premise, expr * conclusion); 503 expr * rewrite_implication(expr * premise, expr * conclusion); 504 // Use the rewriter to simplify an axiom, then assert it. 505 void assert_axiom_rw(expr * e); 506 507 expr * mk_string(zstring const& str); 508 expr * mk_string(const char * str); 509 510 app * mk_strlen(expr * e); 511 expr * mk_concat(expr * n1, expr * n2); 512 expr * mk_concat_const_str(expr * n1, expr * n2); 513 app * mk_contains(expr * haystack, expr * needle); 514 app * mk_indexof(expr * haystack, expr * needle); 515 app * mk_fresh_const(char const* name, sort* s); 516 517 literal mk_literal(expr* _e); 518 app * mk_int(int n); 519 app * mk_int(rational & q); 520 521 void check_and_init_cut_var(expr * node); 522 void add_cut_info_one_node(expr * baseNode, int slevel, expr * node); 523 void add_cut_info_merge(expr * destNode, int slevel, expr * srcNode); 524 bool has_self_cut(expr * n1, expr * n2); 525 526 // for ConcatOverlapAvoid 527 bool will_result_in_overlap(expr * lhs, expr * rhs); 528 529 void track_variable_scope(expr * var); 530 app * mk_str_var(std::string name); 531 app * mk_int_var(std::string name); 532 app_ref mk_nonempty_str_var(); 533 app * mk_internal_xor_var(); 534 void add_nonempty_constraint(expr * s); 535 536 void instantiate_concat_axiom(enode * cat); 537 void try_eval_concat(enode * cat); 538 void instantiate_basic_string_axioms(enode * str); 539 void instantiate_str_eq_length_axiom(enode * lhs, enode * rhs); 540 541 // for count abstraction and refinement 542 expr* refine(expr* lhs, expr* rhs, rational offset); 543 expr* refine_eq(expr* lhs, expr* rhs, unsigned offset); 544 expr* refine_dis(expr* lhs, expr* rhs); 545 expr* refine_function(expr* f); 546 bool flatten(expr* ex, expr_ref_vector & flat); 547 rational get_refine_length(expr* ex, expr_ref_vector& extra_deps); 548 549 void instantiate_axiom_CharAt(enode * e); 550 void instantiate_axiom_prefixof(enode * e); 551 void instantiate_axiom_suffixof(enode * e); 552 void instantiate_axiom_Contains(enode * e); 553 void instantiate_axiom_Indexof(enode * e); 554 void instantiate_axiom_Indexof_extended(enode * e); 555 void instantiate_axiom_LastIndexof(enode * e); 556 void instantiate_axiom_Substr(enode * e); 557 void instantiate_axiom_Replace(enode * e); 558 void instantiate_axiom_str_to_int(enode * e); 559 void instantiate_axiom_int_to_str(enode * e); 560 void instantiate_axiom_is_digit(enode * e); 561 void instantiate_axiom_str_to_code(enode * e); 562 void instantiate_axiom_str_from_code(enode * e); 563 564 void add_persisted_axiom(expr * a); 565 566 expr * mk_RegexIn(expr * str, expr * regexp); 567 void instantiate_axiom_RegexIn(enode * e); 568 569 // regex automata and length-aware regex 570 bool solve_regex_automata(); 571 unsigned estimate_regex_complexity(expr * re); 572 unsigned estimate_regex_complexity_under_complement(expr * re); 573 unsigned estimate_automata_intersection_difficulty(eautomaton * aut1, eautomaton * aut2); 574 bool check_regex_length_linearity(expr * re); 575 bool check_regex_length_linearity_helper(expr * re, bool already_star); 576 expr_ref infer_all_regex_lengths(expr * lenVar, expr * re, expr_ref_vector & freeVariables); 577 void check_subterm_lengths(expr * re, integer_set & lens); 578 void find_automaton_initial_bounds(expr * str_in_re, eautomaton * aut); 579 bool refine_automaton_lower_bound(eautomaton * aut, rational current_lower_bound, rational & refined_lower_bound); 580 bool refine_automaton_upper_bound(eautomaton * aut, rational current_upper_bound, rational & refined_upper_bound); 581 expr_ref generate_regex_path_constraints(expr * stringTerm, eautomaton * aut, rational lenVal, expr_ref & characterConstraints); 582 void aut_path_add_next(u_map<expr*>& next, expr_ref_vector& trail, unsigned idx, expr* cond); 583 expr_ref aut_path_rewrite_constraint(expr * cond, expr * ch_var); 584 void regex_inc_counter(obj_map<expr, unsigned> & counter_map, expr * key); 585 unsigned regex_get_counter(obj_map<expr, unsigned> & counter_map, expr * key); 586 587 void set_up_axioms(expr * ex); 588 void handle_equality(expr * lhs, expr * rhs); 589 590 app * mk_value_helper(app * n); 591 expr * get_eqc_value(expr * n, bool & hasEqcValue); 592 bool get_string_constant_eqc(expr * n, zstring & stringVal); 593 expr * z3str2_get_eqc_value(expr * n , bool & hasEqcValue); 594 bool in_same_eqc(expr * n1, expr * n2); 595 expr * collect_eq_nodes(expr * n, expr_ref_vector & eqcSet); 596 bool is_var(expr * e) const; 597 598 bool get_arith_value(expr* e, rational& val) const; 599 bool get_len_value(expr* e, rational& val); 600 bool lower_bound(expr* _e, rational& lo); 601 bool upper_bound(expr* _e, rational& hi); 602 603 bool can_two_nodes_eq(expr * n1, expr * n2); 604 bool can_concat_eq_str(expr * concat, zstring& str); 605 bool can_concat_eq_concat(expr * concat1, expr * concat2); 606 bool check_concat_len_in_eqc(expr * concat); 607 void check_eqc_empty_string(expr * lhs, expr * rhs); 608 void check_eqc_concat_concat(std::set<expr*> & eqc_concat_lhs, std::set<expr*> & eqc_concat_rhs); 609 bool check_length_consistency(expr * n1, expr * n2); 610 bool check_length_const_string(expr * n1, expr * constStr); 611 bool check_length_eq_var_concat(expr * n1, expr * n2); 612 bool check_length_concat_concat(expr * n1, expr * n2); 613 bool check_length_concat_var(expr * concat, expr * var); 614 bool check_length_var_var(expr * var1, expr * var2); 615 void check_contain_in_new_eq(expr * n1, expr * n2); 616 void check_contain_by_eqc_val(expr * varNode, expr * constNode); 617 void check_contain_by_substr(expr * varNode, expr_ref_vector & willEqClass); 618 void check_contain_by_eq_nodes(expr * n1, expr * n2); 619 bool in_contain_idx_map(expr * n); 620 void compute_contains(std::map<expr*, expr*> & varAliasMap, 621 std::map<expr*, expr*> & concatAliasMap, std::map<expr*, expr *> & varConstMap, 622 std::map<expr*, expr*> & concatConstMap, std::map<expr*, std::map<expr*, int> > & varEqConcatMap); 623 expr * dealias_node(expr * node, std::map<expr*, expr*> & varAliasMap, std::map<expr*, expr*> & concatAliasMap); 624 void get_grounded_concats(unsigned depth, 625 expr* node, std::map<expr*, expr*> & varAliasMap, 626 std::map<expr*, expr*> & concatAliasMap, std::map<expr*, expr*> & varConstMap, 627 std::map<expr*, expr*> & concatConstMap, std::map<expr*, std::map<expr*, int> > & varEqConcatMap, 628 std::map<expr*, std::map<std::vector<expr*>, std::set<expr*> > > & groundedMap); 629 void print_grounded_concat(expr * node, std::map<expr*, std::map<std::vector<expr*>, std::set<expr*> > > & groundedMap); 630 void check_subsequence(expr* str, expr* strDeAlias, expr* subStr, expr* subStrDeAlias, expr* boolVar, 631 std::map<expr*, std::map<std::vector<expr*>, std::set<expr*> > > & groundedMap); 632 bool is_partial_in_grounded_concat(const std::vector<expr*> & strVec, const std::vector<expr*> & subStrVec); 633 634 void get_nodes_in_concat(expr * node, ptr_vector<expr> & nodeList); 635 expr * simplify_concat(expr * node); 636 637 void simplify_parent(expr * nn, expr * eq_str); 638 639 void simplify_concat_equality(expr * lhs, expr * rhs); 640 void solve_concat_eq_str(expr * concat, expr * str); 641 642 void infer_len_concat_equality(expr * nn1, expr * nn2); 643 bool infer_len_concat(expr * n, rational & nLen); 644 void infer_len_concat_arg(expr * n, rational len); 645 646 bool is_concat_eq_type1(expr * concatAst1, expr * concatAst2); 647 bool is_concat_eq_type2(expr * concatAst1, expr * concatAst2); 648 bool is_concat_eq_type3(expr * concatAst1, expr * concatAst2); 649 bool is_concat_eq_type4(expr * concatAst1, expr * concatAst2); 650 bool is_concat_eq_type5(expr * concatAst1, expr * concatAst2); 651 bool is_concat_eq_type6(expr * concatAst1, expr * concatAst2); 652 653 void process_concat_eq_type1(expr * concatAst1, expr * concatAst2); 654 void process_concat_eq_type2(expr * concatAst1, expr * concatAst2); 655 void process_concat_eq_type3(expr * concatAst1, expr * concatAst2); 656 void process_concat_eq_type4(expr * concatAst1, expr * concatAst2); 657 void process_concat_eq_type5(expr * concatAst1, expr * concatAst2); 658 void process_concat_eq_type6(expr * concatAst1, expr * concatAst2); 659 660 void print_cut_var(expr * node, std::ofstream & xout); 661 662 void generate_mutual_exclusion(expr_ref_vector & exprs); 663 void add_theory_aware_branching_info(expr * term, double priority, lbool phase); 664 665 bool new_eq_check(expr * lhs, expr * rhs); 666 void group_terms_by_eqc(expr * n, std::set<expr*> & concats, std::set<expr*> & vars, std::set<expr*> & consts); 667 668 void check_consistency_prefix(expr * e, bool is_true); 669 void check_consistency_suffix(expr * e, bool is_true); 670 void check_consistency_contains(expr * e, bool is_true); 671 672 int ctx_dep_analysis(std::map<expr*, int> & strVarMap, std::map<expr*, int> & freeVarMap, 673 std::map<expr*, std::map<expr*, int> > & var_eq_concat_map); 674 void trace_ctx_dep(std::ofstream & tout, 675 std::map<expr*, expr*> & aliasIndexMap, 676 std::map<expr*, expr*> & var_eq_constStr_map, 677 std::map<expr*, std::map<expr*, int> > & var_eq_concat_map, 678 std::map<expr*, std::map<expr*, int> > & var_eq_unroll_map, 679 std::map<expr*, expr*> & concat_eq_constStr_map, 680 std::map<expr*, std::map<expr*, int> > & concat_eq_concat_map); 681 682 bool term_appears_as_subterm(expr * needle, expr * haystack); 683 void classify_ast_by_type(expr * node, std::map<expr*, int> & varMap, 684 std::map<expr*, int> & concatMap, std::map<expr*, int> & unrollMap); 685 void classify_ast_by_type_in_positive_context(std::map<expr*, int> & varMap, 686 std::map<expr*, int> & concatMap, std::map<expr*, int> & unrollMap); 687 688 expr * get_alias_index_ast(std::map<expr*, expr*> & aliasIndexMap, expr * node); 689 expr * getMostLeftNodeInConcat(expr * node); 690 expr * getMostRightNodeInConcat(expr * node); 691 void get_var_in_eqc(expr * n, std::set<expr*> & varSet); 692 void get_concats_in_eqc(expr * n, std::set<expr*> & concats); 693 void get_const_str_asts_in_node(expr * node, expr_ref_vector & constList); 694 expr * eval_concat(expr * n1, expr * n2); 695 696 bool finalcheck_str2int(app * a); 697 bool finalcheck_int2str(app * a); 698 bool string_integer_conversion_valid(zstring str, rational& converted) const; 699 700 lbool fixed_length_model_construction(expr_ref_vector formulas, expr_ref_vector &precondition, 701 expr_ref_vector& free_variables, 702 obj_map<expr, zstring> &model, expr_ref_vector &cex); 703 bool fixed_length_reduce_string_term(smt::kernel & subsolver, expr * term, expr_ref_vector & term_chars, expr_ref & cex); 704 bool fixed_length_get_len_value(expr * e, rational & val); 705 bool fixed_length_reduce_eq(smt::kernel & subsolver, expr_ref lhs, expr_ref rhs, expr_ref & cex); 706 bool fixed_length_reduce_diseq(smt::kernel & subsolver, expr_ref lhs, expr_ref rhs, expr_ref & cex); 707 bool fixed_length_reduce_contains(smt::kernel & subsolver, expr_ref f, expr_ref & cex); 708 bool fixed_length_reduce_negative_contains(smt::kernel & subsolver, expr_ref f, expr_ref & cex); 709 bool fixed_length_reduce_prefix(smt::kernel & subsolver, expr_ref f, expr_ref & cex); 710 bool fixed_length_reduce_negative_prefix(smt::kernel & subsolver, expr_ref f, expr_ref & cex); 711 bool fixed_length_reduce_suffix(smt::kernel & subsolver, expr_ref f, expr_ref & cex); 712 bool fixed_length_reduce_negative_suffix(smt::kernel & subsolver, expr_ref f, expr_ref & cex); 713 bool fixed_length_reduce_regex_membership(smt::kernel & subsolver, expr_ref f, expr_ref & cex, bool polarity); 714 715 void dump_assignments(); 716 717 void check_variable_scope(); 718 void recursive_check_variable_scope(expr * ex); 719 720 void collect_var_concat(expr * node, std::set<expr*> & varSet, std::set<expr*> & concatSet); 721 bool propagate_length(std::set<expr*> & varSet, std::set<expr*> & concatSet, std::map<expr*, int> & exprLenMap); 722 void get_unique_non_concat_nodes(expr * node, std::set<expr*> & argSet); 723 bool propagate_length_within_eqc(expr * var); 724 725 726 const rational NEQ = rational(-1); // negative word equation lesson 727 const rational PFUN = rational(-2); // positive function lesson 728 const rational NFUN = rational(-3); // negative function lesson 729 730 // TESTING 731 void refresh_theory_var(expr * e); 732 733 public: 734 theory_str(context& ctx, ast_manager & m, theory_str_params const & params); 735 ~theory_str() override; 736 get_name()737 char const * get_name() const override { return "seq"; } 738 void init() override; 739 void display(std::ostream & out) const override; 740 741 void collect_statistics(::statistics & st) const override; 742 overlapping_variables_detected()743 bool overlapping_variables_detected() const { return loopDetected; } 744 get_trail_stack()745 trail_stack& get_trail_stack() { return m_trail_stack; } merge_eh(theory_var,theory_var,theory_var v1,theory_var v2)746 void merge_eh(theory_var, theory_var, theory_var v1, theory_var v2) {} after_merge_eh(theory_var r1,theory_var r2,theory_var v1,theory_var v2)747 void after_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) { } unmerge_eh(theory_var v1,theory_var v2)748 void unmerge_eh(theory_var v1, theory_var v2) {} 749 protected: 750 bool internalize_atom(app * atom, bool gate_ctx) override; 751 bool internalize_term(app * term) override; 752 virtual enode* ensure_enode(expr* e); 753 theory_var mk_var(enode * n) override; 754 755 void new_eq_eh(theory_var, theory_var) override; 756 void new_diseq_eh(theory_var, theory_var) override; 757 mk_fresh(context * c)758 theory* mk_fresh(context* c) override { return alloc(theory_str, *c, c->get_manager(), m_params); } 759 void init_search_eh() override; 760 void add_theory_assumptions(expr_ref_vector & assumptions) override; 761 lbool validate_unsat_core(expr_ref_vector & unsat_core) override; 762 void relevant_eh(app * n) override; 763 void assign_eh(bool_var v, bool is_true) override; 764 void push_scope_eh() override; 765 void pop_scope_eh(unsigned num_scopes) override; 766 void reset_eh() override; 767 768 bool can_propagate() override; 769 void propagate() override; 770 771 final_check_status final_check_eh() override; 772 virtual void attach_new_th_var(enode * n); 773 774 void init_model(model_generator & m) override; 775 model_value_proc * mk_value(enode * n, model_generator & mg) override; 776 void finalize_model(model_generator & mg) override; 777 }; 778 779 }; 780 781