1 /*++ 2 Copyright (c) 2011 Microsoft Corporation 3 4 Module Name: 5 6 theory_seq.h 7 8 Abstract: 9 10 Native theory solver for sequences. 11 12 Author: 13 14 Nikolaj Bjorner (nbjorner) 2015-6-12 15 16 Revision History: 17 18 --*/ 19 #pragma once 20 21 #include "ast/seq_decl_plugin.h" 22 #include "ast/rewriter/th_rewriter.h" 23 #include "ast/rewriter/seq_skolem.h" 24 #include "ast/rewriter/seq_eq_solver.h" 25 #include "ast/ast_trail.h" 26 #include "util/scoped_vector.h" 27 #include "util/scoped_ptr_vector.h" 28 #include "ast/rewriter/seq_rewriter.h" 29 #include "util/union_find.h" 30 #include "util/obj_ref_hashtable.h" 31 #include "smt/smt_theory.h" 32 #include "smt/smt_arith_value.h" 33 #include "smt/theory_seq_empty.h" 34 #include "smt/seq_axioms.h" 35 #include "smt/seq_regex.h" 36 #include "smt/seq_offset_eq.h" 37 38 namespace smt { 39 40 class theory_seq : public theory, public seq::eq_solver_context { 41 friend class seq_regex; 42 43 struct assumption { 44 enode* n1, *n2; 45 literal lit; assumptionassumption46 assumption(enode* n1, enode* n2): n1(n1), n2(n2), lit(null_literal) {} assumptionassumption47 assumption(literal lit): n1(nullptr), n2(nullptr), lit(lit) {} 48 }; 49 typedef scoped_dependency_manager<assumption> dependency_manager; 50 typedef dependency_manager::dependency dependency; 51 52 struct expr_dep { 53 expr* v; 54 expr* e; 55 dependency* d; expr_depexpr_dep56 expr_dep(expr* v, expr* e, dependency* d): v(v), e(e), d(d) {} expr_depexpr_dep57 expr_dep():v(nullptr), e(nullptr), d(nullptr) {} 58 }; 59 typedef svector<expr_dep> eqdep_map_t; 60 typedef union_find<theory_seq> th_union_find; 61 62 class seq_value_proc; 63 struct validate_model_proc; 64 struct compare_depth; 65 66 // cache to track evaluations under equalities 67 class eval_cache { 68 eqdep_map_t m_map; 69 expr_ref_vector m_trail; 70 public: eval_cache(ast_manager & m)71 eval_cache(ast_manager& m): m_trail(m) {} find(expr * v,expr_dep & r)72 bool find(expr* v, expr_dep& r) const { 73 return v->get_id() < m_map.size() && m_map[v->get_id()].e && (r = m_map[v->get_id()], true); 74 } insert(expr_dep const & r)75 void insert(expr_dep const& r) { 76 m_trail.push_back(r.v); 77 m_trail.push_back(r.e); 78 m_map.reserve(2*r.v->get_id() + 1); 79 m_map[r.v->get_id()] = r; 80 } reset()81 void reset() { m_map.reset(); m_trail.reset(); } 82 }; 83 84 // map from variables to representatives 85 // + a cache for normalization. 86 class solution_map { 87 enum map_update { INS, DEL }; 88 ast_manager& m; 89 dependency_manager& m_dm; 90 eqdep_map_t m_map; 91 eval_cache m_cache; 92 expr_ref_vector m_lhs, m_rhs; 93 ptr_vector<dependency> m_deps; 94 svector<map_update> m_updates; 95 unsigned_vector m_limit; 96 find(expr * v,expr_dep & r)97 bool find(expr* v, expr_dep& r) const { 98 return v->get_id() < m_map.size() && m_map[v->get_id()].e && (r = m_map[v->get_id()], true); 99 } insert(expr_dep const & r)100 void insert(expr_dep const& r) { 101 m_map.reserve(2*r.v->get_id() + 1); 102 m_map[r.v->get_id()] = r; 103 } 104 void add_trail(map_update op, expr* l, expr* r, dependency* d); 105 public: solution_map(ast_manager & m,dependency_manager & dm)106 solution_map(ast_manager& m, dependency_manager& dm): 107 m(m), m_dm(dm), m_cache(m), m_lhs(m), m_rhs(m) {} empty()108 bool empty() const { return m_map.empty(); } 109 void update(expr* e, expr* r, dependency* d); add_cache(expr_dep & r)110 void add_cache(expr_dep& r) { m_cache.insert(r); } find_cache(expr * v,expr_dep & r)111 bool find_cache(expr* v, expr_dep& r) { return m_cache.find(v, r); } 112 expr* find(expr* e, dependency*& d); 113 expr* find(expr* e); 114 bool find1(expr* a, expr*& b, dependency*& dep); 115 void find_rec(expr* e, svector<expr_dep>& finds); 116 bool is_root(expr* e) const; 117 void cache(expr* e, expr* r, dependency* d); reset_cache()118 void reset_cache() { m_cache.reset(); } push_scope()119 void push_scope() { m_limit.push_back(m_updates.size()); } 120 void pop_scope(unsigned num_scopes); 121 void display(std::ostream& out) const; begin()122 eqdep_map_t::iterator begin() { return m_map.begin(); } end()123 eqdep_map_t::iterator end() { return m_map.end(); } 124 }; 125 126 // Table of current disequalities 127 class exclusion_table { 128 public: 129 typedef obj_pair_hashtable<expr, expr> table_t; 130 protected: 131 ast_manager& m; 132 table_t m_table; 133 expr_ref_vector m_lhs, m_rhs; 134 unsigned_vector m_limit; 135 public: exclusion_table(ast_manager & m)136 exclusion_table(ast_manager& m): m(m), m_lhs(m), m_rhs(m) {} ~exclusion_table()137 ~exclusion_table() { } empty()138 bool empty() const { return m_table.empty(); } 139 void update(expr* e, expr* r); 140 bool contains(expr* e, expr* r) const; push_scope()141 void push_scope() { m_limit.push_back(m_lhs.size()); } 142 void pop_scope(unsigned num_scopes); 143 void display(std::ostream& out) const; begin()144 table_t::iterator begin() const { return m_table.begin(); } end()145 table_t::iterator end() const { return m_table.end(); } 146 }; 147 148 // Asserted or derived equality with dependencies 149 class depeq : public seq::eq { 150 unsigned m_id; 151 dependency* m_dep; 152 public: depeq(unsigned id,expr_ref_vector & l,expr_ref_vector & r,dependency * d)153 depeq(unsigned id, expr_ref_vector& l, expr_ref_vector& r, dependency* d): 154 eq(l, r), m_id(id), m_dep(d) {} dep()155 dependency* dep() const { return m_dep; } id()156 unsigned id() const { return m_id; } 157 }; 158 mk_eqdep(expr * l,expr * r,dependency * dep)159 depeq mk_eqdep(expr* l, expr* r, dependency* dep) { 160 expr_ref_vector ls(m), rs(m); 161 m_util.str.get_concat_units(l, ls); 162 m_util.str.get_concat_units(r, rs); 163 return depeq(m_eq_id++, ls, rs, dep); 164 } 165 mk_eqdep(expr_ref_vector const & l,expr_ref_vector const & r,dependency * dep)166 depeq mk_eqdep(expr_ref_vector const& l, expr_ref_vector const& r, dependency* dep) { 167 expr_ref_vector ls(m), rs(m); 168 for (expr* e : l) 169 m_util.str.get_concat_units(e, ls); 170 for (expr* e : r) 171 m_util.str.get_concat_units(e, rs); 172 return depeq(m_eq_id++, ls, rs, dep); 173 } 174 175 // equalities that are decomposed by conacatenations 176 typedef std::pair<expr_ref_vector, expr_ref_vector> decomposed_eq; 177 178 class ne { 179 expr_ref m_l, m_r; 180 vector<decomposed_eq> m_eqs; 181 literal_vector m_lits; 182 dependency* m_dep; 183 public: ne(expr_ref const & l,expr_ref const & r,dependency * dep)184 ne(expr_ref const& l, expr_ref const& r, dependency* dep): 185 m_l(l), m_r(r), m_dep(dep) { 186 expr_ref_vector ls(l.get_manager()); ls.push_back(l); 187 expr_ref_vector rs(r.get_manager()); rs.push_back(r); 188 m_eqs.push_back(std::make_pair(ls, rs)); 189 } 190 ne(expr_ref const & _l,expr_ref const & _r,vector<decomposed_eq> const & eqs,literal_vector const & lits,dependency * dep)191 ne(expr_ref const& _l, expr_ref const& _r, vector<decomposed_eq> const& eqs, literal_vector const& lits, dependency* dep): 192 m_l(_l), m_r(_r), 193 m_eqs(eqs), 194 m_lits(lits), 195 m_dep(dep) { 196 } 197 eqs()198 vector<decomposed_eq> const& eqs() const { return m_eqs; } 199 decomposed_eq const& operator[](unsigned i) const { return m_eqs[i]; } 200 lits()201 literal_vector const& lits() const { return m_lits; } lits(unsigned i)202 literal lits(unsigned i) const { return m_lits[i]; } dep()203 dependency* dep() const { return m_dep; } l()204 expr_ref const& l() const { return m_l; } r()205 expr_ref const& r() const { return m_r; } 206 }; 207 208 class nc { 209 expr_ref m_contains; 210 literal m_len_gt; 211 dependency* m_dep; 212 public: nc(expr_ref const & c,literal len_gt,dependency * dep)213 nc(expr_ref const& c, literal len_gt, dependency* dep): 214 m_contains(c), 215 m_len_gt(len_gt), 216 m_dep(dep) {} 217 deps()218 dependency* deps() const { return m_dep; } contains()219 expr_ref const& contains() const { return m_contains; } len_gt()220 literal len_gt() const { return m_len_gt; } 221 }; 222 223 class apply { 224 public: ~apply()225 virtual ~apply() {} 226 virtual void operator()(theory_seq& th) = 0; 227 }; 228 229 class replay_length_coherence : public apply { 230 expr_ref m_e; 231 public: replay_length_coherence(ast_manager & m,expr * e)232 replay_length_coherence(ast_manager& m, expr* e) : m_e(e, m) {} ~replay_length_coherence()233 ~replay_length_coherence() override {} operator()234 void operator()(theory_seq& th) override { 235 th.check_length_coherence(m_e); 236 m_e.reset(); 237 } 238 }; 239 240 class replay_fixed_length : public apply { 241 expr_ref m_e; 242 public: replay_fixed_length(ast_manager & m,expr * e)243 replay_fixed_length(ast_manager& m, expr* e) : m_e(e, m) {} ~replay_fixed_length()244 ~replay_fixed_length() override {} operator()245 void operator()(theory_seq& th) override { 246 th.fixed_length(m_e); 247 m_e.reset(); 248 } 249 }; 250 251 class replay_axiom : public apply { 252 expr_ref m_e; 253 public: replay_axiom(ast_manager & m,expr * e)254 replay_axiom(ast_manager& m, expr* e) : m_e(e, m) {} ~replay_axiom()255 ~replay_axiom() override {} operator()256 void operator()(theory_seq& th) override { 257 th.enque_axiom(m_e); 258 m_e.reset(); 259 } 260 }; 261 262 class replay_unit_literal : public apply { 263 expr_ref m_e; 264 bool m_sign; 265 public: replay_unit_literal(ast_manager & m,expr * e,bool sign)266 replay_unit_literal(ast_manager& m, expr* e, bool sign) : m_e(e, m), m_sign(sign) {} ~replay_unit_literal()267 ~replay_unit_literal() override {} operator()268 void operator()(theory_seq& th) override { 269 literal lit = th.mk_literal(m_e); 270 if (m_sign) lit.neg(); 271 th.add_axiom(lit); 272 m_e.reset(); 273 } 274 275 }; 276 277 class replay_is_axiom : public apply { 278 expr_ref m_e; 279 public: replay_is_axiom(ast_manager & m,expr * e)280 replay_is_axiom(ast_manager& m, expr* e) : m_e(e, m) {} ~replay_is_axiom()281 ~replay_is_axiom() override {} operator()282 void operator()(theory_seq& th) override { 283 th.check_int_string(m_e); 284 m_e.reset(); 285 } 286 }; 287 288 class push_replay : public trail { 289 theory_seq& th; 290 apply* m_apply; 291 public: push_replay(theory_seq & th,apply * app)292 push_replay(theory_seq& th, apply* app): th(th), m_apply(app) {} undo()293 void undo() override { 294 th.m_replay.push_back(m_apply); 295 } 296 }; 297 298 class pop_branch : public trail { 299 theory_seq& th; 300 unsigned k; 301 public: pop_branch(theory_seq & th,unsigned k)302 pop_branch(theory_seq& th, unsigned k): th(th), k(k) {} undo()303 void undo() override { 304 th.m_branch_start.erase(k); 305 } 306 }; 307 308 309 void erase_index(unsigned idx, unsigned i); 310 311 struct stats { statsstats312 stats() { reset(); } resetstats313 void reset() { memset(this, 0, sizeof(stats)); } 314 unsigned m_num_splits; 315 unsigned m_num_reductions; 316 unsigned m_check_length_coherence; 317 unsigned m_branch_variable; 318 unsigned m_branch_nqs; 319 unsigned m_solve_nqs; 320 unsigned m_solve_eqs; 321 unsigned m_add_axiom; 322 unsigned m_extensionality; 323 unsigned m_fixed_length; 324 unsigned m_propagate_contains; 325 unsigned m_int_string; 326 unsigned m_ubv_string; 327 }; 328 typedef hashtable<rational, rational::hash_proc, rational::eq_proc> rational_set; 329 330 dependency_manager m_dm; 331 solution_map m_rep; // unification representative. 332 scoped_vector<depeq> m_eqs; // set of current equations. 333 scoped_vector<ne> m_nqs; // set of current disequalities. 334 scoped_vector<nc> m_ncs; // set of non-contains constraints. 335 scoped_vector<expr*> m_lts; // set of asserted str.<, str.<= literals 336 bool m_lts_checked; 337 unsigned m_eq_id; 338 th_union_find m_find; 339 seq_offset_eq m_offset_eq; 340 341 obj_ref_map<ast_manager, expr, bool> m_overlap_lhs; 342 obj_ref_map<ast_manager, expr, bool> m_overlap_rhs; 343 344 345 seq_factory* m_factory; // value factory 346 exclusion_table m_exclude; // set of asserted disequalities. 347 expr_ref_vector m_axioms; // list of axioms to add. 348 obj_hashtable<expr> m_axiom_set; 349 unsigned m_axioms_head; // index of first axiom to add. 350 bool m_incomplete; // is the solver (clearly) incomplete for the fragment. 351 expr_ref_vector m_int_string; 352 expr_ref_vector m_ubv_string; // list all occurrences of str.from_ubv that have been seen 353 obj_hashtable<expr> m_has_ubv_axiom; // keep track of ubv that have been axiomatized within scope. 354 obj_hashtable<expr> m_has_length; // is length applied 355 expr_ref_vector m_length; // length applications themselves 356 obj_map<expr, unsigned> m_length_limit_map; // sequences that have length limit predicates 357 expr_ref_vector m_length_limit; // length limit predicates 358 scoped_ptr_vector<apply> m_replay; // set of actions to replay 359 model_generator* m_mg; 360 th_rewriter m_rewrite; // rewriter that converts strings to character concats 361 th_rewriter m_str_rewrite; // rewriter that coonverts character concats to strings 362 seq_rewriter m_seq_rewrite; 363 seq_util m_util; 364 arith_util m_autil; 365 seq::skolem m_sk; 366 seq_axioms m_ax; 367 seq::eq_solver m_eq; 368 seq_regex m_regex; 369 arith_value m_arith_value; 370 trail_stack m_trail_stack; 371 stats m_stats; 372 ptr_vector<expr> m_todo, m_concat; 373 expr_ref_vector m_ls, m_rs, m_lhs, m_rhs; 374 expr_ref_pair_vector m_new_eqs; 375 376 unsigned m_max_unfolding_depth; 377 literal m_max_unfolding_lit; 378 379 expr* m_unhandled_expr; 380 bool m_has_seq; 381 bool m_new_solution; // new solution added 382 bool m_new_propagation; // new propagation to core 383 384 obj_hashtable<expr> m_fixed; // string variables that are fixed length. 385 obj_hashtable<expr> m_is_digit; // expressions that have been constrained to be digits 386 387 final_check_status final_check_eh() override; 388 bool internalize_atom(app* atom, bool) override; 389 bool internalize_term(app*) override; 390 void internalize_eq_eh(app * atom, bool_var v) override; 391 void new_eq_eh(theory_var, theory_var) override; 392 void new_diseq_eh(theory_var, theory_var) override; 393 void assign_eh(bool_var v, bool is_true) override; 394 bool can_propagate() override; 395 void propagate() override; 396 void push_scope_eh() override; 397 void pop_scope_eh(unsigned num_scopes) override; 398 void restart_eh() override; 399 void relevant_eh(app* n) override; 400 bool should_research(expr_ref_vector &) override; 401 void add_theory_assumptions(expr_ref_vector & assumptions) override; mk_fresh(context * new_ctx)402 theory* mk_fresh(context* new_ctx) override { return alloc(theory_seq, *new_ctx); } get_name()403 char const * get_name() const override { return "seq"; } include_func_interp(func_decl * f)404 bool include_func_interp(func_decl* f) override { return m_util.str.is_nth_u(f); } 405 bool is_safe_to_copy(bool_var v) const override; 406 theory_var mk_var(enode* n) override; 407 void apply_sort_cnstr(enode* n, sort* s) override; 408 void display(std::ostream & out) const override; 409 void collect_statistics(::statistics & st) const override; 410 model_value_proc * mk_value(enode * n, model_generator & mg) override; 411 void init_model(model_generator & mg) override; 412 void finalize_model(model_generator & mg) override; 413 void init_search_eh() override; 414 void validate_model(model& mdl) override; 415 416 void init_model(expr_ref_vector const& es); 417 app* get_ite_value(expr* a); 418 void get_ite_concat(ptr_vector<expr>& head, ptr_vector<expr>& tail); 419 420 int find_fst_non_empty_idx(expr_ref_vector const& x); 421 expr* find_fst_non_empty_var(expr_ref_vector const& x); 422 bool has_len_offset(expr_ref_vector const& ls, expr_ref_vector const& rs, int & diff); 423 424 // final check 425 bool simplify_and_solve_eqs(); // solve unitary equalities 426 bool reduce_length_eq(); 427 bool branch_unit_variable(); // branch on XYZ = abcdef 428 bool branch_binary_variable(); // branch on abcX = Ydefg 429 bool branch_variable(); // branch on 430 bool branch_ternary_variable(); // branch on XabcY = Zdefg 431 bool branch_quat_variable(); // branch on XabcY = ZdefgT 432 bool len_based_split(); // split based on len offset 433 bool branch_variable_mb(); // branch on a variable, model based on length 434 bool branch_variable_eq(); // branch on a variable, by an alignment among variable boundaries. 435 bool is_solved(); 436 bool check_length_coherence(); 437 bool check_length_coherence0(expr* e); 438 bool check_length_coherence(expr* e); 439 bool fixed_length(bool is_zero = false); 440 bool fixed_length(expr* e, bool is_zero); 441 bool branch_variable_eq(depeq const& e); 442 bool branch_binary_variable(depeq const& e); 443 bool can_align_from_lhs(expr_ref_vector const& ls, expr_ref_vector const& rs); 444 bool can_align_from_rhs(expr_ref_vector const& ls, expr_ref_vector const& rs); 445 bool branch_ternary_variable_rhs(depeq const& e); 446 bool branch_ternary_variable_lhs(depeq const& e); 447 literal mk_alignment(expr* e1, expr* e2); 448 bool branch_quat_variable(depeq const& e); 449 bool len_based_split(depeq const& e); 450 bool is_unit_eq(expr_ref_vector const& ls, expr_ref_vector const& rs); 451 bool propagate_length_coherence(expr* e); 452 bool split_lengths(dependency* dep, 453 expr_ref_vector const& ls, expr_ref_vector const& rs, 454 vector<rational> const& ll, vector<rational> const& rl); 455 bool set_empty(expr* x); 456 bool is_complex(depeq const& e); 457 lbool regex_are_equal(expr* r1, expr* r2); 458 void add_unhandled_expr(expr* e); 459 460 bool check_extensionality(); 461 bool check_extensionality(expr* e1, enode* n1, enode* n2); 462 bool check_contains(); 463 bool check_lts(); 464 dependency* m_eq_deps { nullptr }; 465 bool solve_eqs(unsigned start); 466 bool solve_eq(unsigned idx); 467 bool simplify_eq(expr_ref_vector& l, expr_ref_vector& r, dependency* dep); 468 bool lift_ite(expr_ref_vector const& l, expr_ref_vector const& r, dependency* dep); 469 obj_pair_hashtable<expr, expr> m_nth_eq2_cache; 470 bool solve_nth_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* dep); 471 472 bool solve_binary_eq(expr_ref_vector const& l, expr_ref_vector const& r, dependency* dep); 473 bool propagate_max_length(expr* l, expr* r, dependency* dep); 474 475 bool get_length(expr* s, expr_ref& len, literal_vector& lits); 476 bool reduce_length(expr* l, expr* r, literal_vector& lits); 477 bool reduce_length_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* deps); 478 bool reduce_length(unsigned i, unsigned j, bool front, expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* deps); 479 mk_empty(sort * s)480 expr_ref mk_empty(sort* s) { return expr_ref(m_util.str.mk_empty(s), m); } mk_concat(unsigned n,expr * const * es)481 expr_ref mk_concat(unsigned n, expr*const* es) { return expr_ref(m_util.str.mk_concat(n, es, es[0]->get_sort()), m); } mk_concat(unsigned n,expr * const * es,sort * s)482 expr_ref mk_concat(unsigned n, expr*const* es, sort* s) { return expr_ref(m_util.str.mk_concat(n, es, s), m); } mk_concat(expr_ref_vector const & es,sort * s)483 expr_ref mk_concat(expr_ref_vector const& es, sort* s) { return mk_concat(es.size(), es.data(), s); } mk_concat(expr_ref_vector const & es)484 expr_ref mk_concat(expr_ref_vector const& es) { SASSERT(!es.empty()); return expr_ref(m_util.str.mk_concat(es.size(), es.data(), es[0]->get_sort()), m); } mk_concat(ptr_vector<expr> const & es)485 expr_ref mk_concat(ptr_vector<expr> const& es) { SASSERT(!es.empty()); return mk_concat(es.size(), es.data(), es[0]->get_sort()); } mk_concat(expr * e1,expr * e2)486 expr_ref mk_concat(expr* e1, expr* e2) { return expr_ref(m_util.str.mk_concat(e1, e2), m); } mk_concat(expr * e1,expr * e2,expr * e3)487 expr_ref mk_concat(expr* e1, expr* e2, expr* e3) { return expr_ref(m_util.str.mk_concat(e1, e2, e3), m); } 488 bool solve_nqs(unsigned i); 489 bool solve_ne(unsigned i); 490 bool solve_nc(unsigned i); 491 bool check_ne_literals(unsigned idx, unsigned& num_undef_lits); 492 bool propagate_ne2lit(unsigned idx); 493 bool propagate_ne2eq(unsigned idx); 494 bool propagate_ne2eq(unsigned idx, expr_ref_vector const& es); 495 bool reduce_ne(unsigned idx); 496 bool branch_nqs(); 497 lbool branch_nq(ne const& n); 498 499 struct cell { 500 cell* m_parent; 501 expr* m_expr; 502 dependency* m_dep; 503 unsigned m_last; cellcell504 cell(cell* p, expr* e, dependency* d): m_parent(p), m_expr(e), m_dep(d), m_last(0) {} 505 }; 506 scoped_ptr_vector<cell> m_all_cells; 507 cell* mk_cell(cell* p, expr* e, dependency* d); 508 void unfold(cell* c, ptr_vector<cell>& cons); 509 void display_explain(std::ostream& out, unsigned indent, expr* e); 510 bool explain_eq(expr* e1, expr* e2, dependency*& dep); 511 bool explain_empty(expr_ref_vector& es, dependency*& dep); 512 513 // asserting consequences 514 void linearize(dependency* dep, enode_pair_vector& eqs, literal_vector& lits) const; propagate_lit(dependency * dep,literal lit)515 bool propagate_lit(dependency* dep, literal lit) { return propagate_lit(dep, 0, nullptr, lit); } 516 bool propagate_lit(dependency* dep, unsigned n, literal const* lits, literal lit); 517 bool propagate_eq(dependency* dep, enode* n1, enode* n2); 518 bool propagate_eq(literal lit, expr* e1, expr* e2, bool add_to_eqs); 519 bool propagate_eq(dependency* dep, literal_vector const& lits, expr* e1, expr* e2, bool add_to_eqs = true); 520 bool propagate_eq(dependency* dep, expr* e1, expr* e2, bool add_to_eqs = true); 521 bool propagate_eq(dependency* dep, literal lit, expr* e1, expr* e2, bool add_to_eqs = true); 522 void set_conflict(dependency* dep, literal_vector const& lits = literal_vector()); 523 void set_conflict(enode_pair_vector const& eqs, literal_vector const& lits); 524 525 // self-validation 526 void validate_axiom(literal_vector const& lits); 527 void validate_conflict(enode_pair_vector const& eqs, literal_vector const& lits); 528 void validate_assign(literal lit, enode_pair_vector const& eqs, literal_vector const& lits); 529 void validate_assign_eq(enode* a, enode* b, enode_pair_vector const& eqs, literal_vector const& lits); 530 void validate_fmls(enode_pair_vector const& eqs, literal_vector const& lits, expr_ref_vector& fmls); 531 expr_ref elim_skolem(expr* e); 532 533 u_map<unsigned> m_branch_start; 534 void insert_branch_start(unsigned k, unsigned s); 535 unsigned find_branch_start(unsigned k); 536 bool find_branch_candidate(unsigned& start, dependency* dep, expr_ref_vector const& ls, expr_ref_vector const& rs); 537 expr_ref_vector expand_strings(expr_ref_vector const& es); 538 bool can_be_equal(unsigned szl, expr* const* ls, unsigned szr, expr* const* rs) const; 539 bool assume_equality(expr* l, expr* r); 540 541 // variable solving utilities 542 bool is_var(expr* b) const; 543 bool add_solution(expr* l, expr* r, dependency* dep); 544 bool is_unit_nth(expr* a) const; 545 expr_ref mk_nth(expr* s, expr* idx); 546 bool canonize(expr* e, dependency*& eqs, expr_ref& result); 547 bool canonize(expr* e, expr_ref_vector& es, dependency*& eqs, bool& change); 548 bool canonize(expr_ref_vector const& es, expr_ref_vector& result, dependency*& eqs, bool& change); 549 ptr_vector<expr> m_expand_todo; 550 bool expand(expr* e, dependency*& eqs, expr_ref& result); 551 bool expand1(expr* e, dependency*& eqs, expr_ref& result); 552 expr_ref try_expand(expr* e, dependency*& eqs); 553 void add_dependency(dependency*& dep, enode* a, enode* b); 554 555 // terms whose meaning are encoded using axioms. 556 void enque_axiom(expr* e); 557 void deque_axiom(expr* e); 558 void add_axiom(literal l1, literal l2 = null_literal, literal l3 = null_literal, literal l4 = null_literal, literal l5 = null_literal); 559 void add_axiom(literal_vector& lits); 560 has_length(expr * e)561 bool has_length(expr *e) const { return m_has_length.contains(e); } 562 void add_length(expr* l); 563 bool add_length_to_eqc(expr* n); 564 bool enforce_length(expr_ref_vector const& es, vector<rational>& len); 565 void enforce_length_coherence(enode* n1, enode* n2); 566 567 void add_length_limit(expr* s, unsigned k, bool is_searching); 568 569 // model-check the functions that convert integers to strings and the other way. 570 void add_int_string(expr* e); 571 bool check_int_string(); 572 bool check_int_string(expr* e); 573 bool branch_itos(); 574 bool branch_itos(expr* e); 575 576 // functions that convert ubv to string 577 void add_ubv_string(expr* e); 578 bool check_ubv_string(); 579 bool check_ubv_string(expr* e); 580 581 expr_ref add_elim_string_axiom(expr* n); 582 void add_in_re_axiom(expr* n); 583 literal mk_simplified_literal(expr* n); 584 literal mk_eq_empty(expr* n, bool phase = true); 585 literal mk_seq_eq(expr* a, expr* b); 586 void tightest_prefix(expr* s, expr* x); 587 expr_ref mk_sub(expr* a, expr* b); 588 expr_ref mk_add(expr* a, expr* b); 589 expr_ref mk_len(expr* s); 590 dependency* mk_join(dependency* deps, literal lit); 591 dependency* mk_join(dependency* deps, literal_vector const& lits); 592 593 594 // arithmetic integration 595 bool get_num_value(expr* s, rational& val) const; 596 bool lower_bound(expr* s, rational& lo) const; 597 bool lower_bound2(expr* s, rational& lo); 598 bool upper_bound(expr* s, rational& hi) const; 599 600 void mk_decompose(expr* e, expr_ref& head, expr_ref& tail); 601 602 // unfold definitions based on length limits 603 void propagate_length_limit(expr* n); 604 605 void set_incomplete(app* term); 606 607 void propagate_not_prefix(expr* e); 608 void propagate_not_suffix(expr* e); 609 void ensure_nth(literal lit, expr* s, expr* idx); 610 bool canonizes(bool sign, expr* e); 611 void propagate_non_empty(literal lit, expr* s); 612 bool propagate_is_conc(expr* e, expr* conc); 613 void propagate_step(literal lit, expr* n); 614 void propagate_accept(literal lit, expr* e); 615 void new_eq_eh(dependency* dep, enode* n1, enode* n2); 616 617 // diagnostics 618 std::ostream& display_equations(std::ostream& out) const; 619 std::ostream& display_equation(std::ostream& out, depeq const& e) const; 620 std::ostream& display_disequations(std::ostream& out) const; 621 std::ostream& display_disequation(std::ostream& out, ne const& e) const; 622 std::ostream& display_deps(std::ostream& out, dependency* deps) const; 623 std::ostream& display_deps(std::ostream& out, literal_vector const& lits, enode_pair_vector const& eqs) const; 624 std::ostream& display_deps_smt2(std::ostream& out, literal_vector const& lits, enode_pair_vector const& eqs) const; 625 std::ostream& display_nc(std::ostream& out, nc const& nc) const; 626 std::ostream& display_lit(std::ostream& out, literal l) const; 627 public: 628 theory_seq(context& ctx); 629 ~theory_seq() override; 630 631 void init() override; 632 // model building 633 app* mk_value(app* a); 634 get_trail_stack()635 trail_stack& get_trail_stack() { return m_trail_stack; } merge_eh(theory_var,theory_var,theory_var v1,theory_var v2)636 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)637 void after_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) { } unmerge_eh(theory_var v1,theory_var v2)638 void unmerge_eh(theory_var v1, theory_var v2) {} 639 640 // eq_solver callbacks 641 void add_consequence(bool uses_eq, expr_ref_vector const& clause) override; add_solution(expr * var,expr * term)642 void add_solution(expr* var, expr* term) override { SASSERT(var != term); add_solution(var, term, m_eq_deps); } 643 expr* expr2rep(expr* e) override; 644 bool get_length(expr* e, rational& r) override; 645 }; 646 }; 647 648 649