Merge pull request #1855 from mtrberzi/refactoring-arith

Z3str3: refactoring, arith_value

src/smt/smt_arith_value.cpp

@@ -94,4 +94,10 @@ namespace smt {
         while (next != n);
         return false;
     }
+
+    final_check_status arith_value::final_check() {
+        family_id afid = a.get_family_id();
+        theory * th = m_ctx.get_theory(afid);
+        return th->final_check_eh();
+    }
 };

src/smt/smt_arith_value.h

@@ -33,5 +33,6 @@ namespace smt {
         bool get_lo(expr* e, rational& lo, bool& strict);
         bool get_up(expr* e, rational& up, bool& strict);
         bool get_value(expr* e, rational& value);
+        final_check_status final_check();
     };
 };

src/smt/smt_theory.h

@@ -36,6 +36,7 @@ namespace smt {
         unsigned_vector m_var2enode_lim;
 
         friend class context;
+        friend class arith_value;
     protected:
         virtual void init(context * ctx);
 

src/smt/theory_str.cpp

@@ -4835,25 +4835,13 @@ namespace smt {
         return n;
     }
 
-    // from Z3: theory_seq.cpp
-
-    static theory_mi_arith* get_th_arith(context& ctx, theory_id afid, expr* e) {
-        theory* th = ctx.get_theory(afid);
-        if (th && ctx.e_internalized(e)) {
-            return dynamic_cast<theory_mi_arith*>(th);
-        }
-        else {
-            return nullptr;
-        }
-    }
-
     bool theory_str::get_arith_value(expr* e, rational& val) const {
          context& ctx = get_context();
          ast_manager & m = get_manager();
-        // safety
          if (!ctx.e_internalized(e)) {
              return false;
          }
+         // check root of the eqc for an integer constant
          // if an integer constant exists in the eqc, it should be the root
          enode * en_e = ctx.get_enode(e);
          enode * root_e = en_e->get_root();
@@ -4863,12 +4851,8 @@ namespace smt {
          } else {
              TRACE("str", tout << "root of eqc of " << mk_pp(e, m) << " is not a numeral" << std::endl;);
              return false;
-            theory_mi_arith* tha = get_th_arith(ctx, m_autil.get_family_id(), e);
-            if (!tha) return false;
-            expr_ref val_e(m);
-            if (tha->get_value(root_e, val_e) && m_autil.is_numeral(val_e, val) && val.is_int()) return true;
-            return false;
          }
+
      }
 
     bool theory_str::lower_bound(expr* _e, rational& lo) {
@@ -4877,12 +4861,9 @@ namespace smt {
             return false;
         }
 
-        context& ctx = get_context();
+        arith_value v(get_context());
-        ast_manager & m = get_manager();
+        bool strict;
-        theory_mi_arith* tha = get_th_arith(ctx, m_autil.get_family_id(), _e);
+        return v.get_lo(_e, lo, strict);
-        expr_ref _lo(m);
-        if (!tha || !tha->get_lower(ctx.get_enode(_e), _lo)) return false;
-        return m_autil.is_numeral(_lo, lo) && lo.is_int();
     }
 
     bool theory_str::upper_bound(expr* _e, rational& hi) {
@@ -4891,12 +4872,9 @@ namespace smt {
             return false;
         }
 
-        context& ctx = get_context();
+        arith_value v(get_context());
-        ast_manager & m = get_manager();
+        bool strict;
-        theory_mi_arith* tha = get_th_arith(ctx, m_autil.get_family_id(), _e);
+        return v.get_up(_e, hi, strict);
-        expr_ref _hi(m);
-        if (!tha || !tha->get_upper(ctx.get_enode(_e), _hi)) return false;
-        return m_autil.is_numeral(_hi, hi) && hi.is_int();
     }
 
     bool theory_str::get_len_value(expr* e, rational& val) {
@@ -4908,17 +4886,6 @@ namespace smt {
         context& ctx = get_context();
         ast_manager & m = get_manager();
 
-        theory* th = ctx.get_theory(m_autil.get_family_id());
-        if (!th) {
-            TRACE("str", tout << "oops, can't get m_autil's theory" << std::endl;);
-            return false;
-        }
-        theory_mi_arith* tha = dynamic_cast<theory_mi_arith*>(th);
-        if (!tha) {
-            TRACE("str", tout << "oops, can't cast to theory_mi_arith" << std::endl;);
-            return false;
-        }
-
         TRACE("str", tout << "checking len value of " << mk_ismt2_pp(e, m) << std::endl;);
 
         rational val1;
@@ -8145,31 +8112,7 @@ namespace smt {
 
         // BEGIN new_eq_handler() in strTheory
 
-        {
+        check_eqc_empty_string(lhs, rhs);
-            rational nn1Len, nn2Len;
-            bool nn1Len_exists = get_len_value(lhs, nn1Len);
-            bool nn2Len_exists = get_len_value(rhs, nn2Len);
-            expr_ref emptyStr(mk_string(""), m);
-
-            if (nn1Len_exists && nn1Len.is_zero()) {
-                if (!in_same_eqc(lhs, emptyStr) && rhs != emptyStr) {
-                    expr_ref eql(ctx.mk_eq_atom(mk_strlen(lhs), mk_int(0)), m);
-                    expr_ref eqr(ctx.mk_eq_atom(lhs, emptyStr), m);
-                    expr_ref toAssert(ctx.mk_eq_atom(eql, eqr), m);
-                    assert_axiom(toAssert);
-                }
-            }
-
-            if (nn2Len_exists && nn2Len.is_zero()) {
-                if (!in_same_eqc(rhs, emptyStr) && lhs != emptyStr) {
-                    expr_ref eql(ctx.mk_eq_atom(mk_strlen(rhs), mk_int(0)), m);
-                    expr_ref eqr(ctx.mk_eq_atom(rhs, emptyStr), m);
-                    expr_ref toAssert(ctx.mk_eq_atom(eql, eqr), m);
-                    assert_axiom(toAssert);
-                }
-            }
-        }
-
         instantiate_str_eq_length_axiom(ctx.get_enode(lhs), ctx.get_enode(rhs));
 
         // group terms by equivalence class (groupNodeInEqc())
@@ -8221,52 +8164,7 @@ namespace smt {
               );
 
         // step 1: Concat == Concat
-        int hasCommon = 0;
+        check_eqc_concat_concat(eqc_concat_lhs, eqc_concat_rhs);
-        if (eqc_concat_lhs.size() != 0 && eqc_concat_rhs.size() != 0) {
-            std::set<expr*>::iterator itor1 = eqc_concat_lhs.begin();
-            std::set<expr*>::iterator itor2 = eqc_concat_rhs.begin();
-            for (; itor1 != eqc_concat_lhs.end(); itor1++) {
-                if (eqc_concat_rhs.find(*itor1) != eqc_concat_rhs.end()) {
-                    hasCommon = 1;
-                    break;
-                }
-            }
-            for (; itor2 != eqc_concat_rhs.end(); itor2++) {
-                if (eqc_concat_lhs.find(*itor2) != eqc_concat_lhs.end()) {
-                    hasCommon = 1;
-                    break;
-                }
-            }
-            if (hasCommon == 0) {
-                if (opt_ConcatOverlapAvoid) {
-                    bool found = false;
-                    // check each pair and take the first ones that won't immediately overlap
-                    for (itor1 = eqc_concat_lhs.begin(); itor1 != eqc_concat_lhs.end() && !found; ++itor1) {
-                        expr * concat_lhs = *itor1;
-                        for (itor2 = eqc_concat_rhs.begin(); itor2 != eqc_concat_rhs.end() && !found; ++itor2) {
-                            expr * concat_rhs = *itor2;
-                            if (will_result_in_overlap(concat_lhs, concat_rhs)) {
-                                TRACE("str", tout << "Concats " << mk_pp(concat_lhs, m) << " and "
-                                      << mk_pp(concat_rhs, m) << " will result in overlap; skipping." << std::endl;);
-                            } else {
-                                TRACE("str", tout << "Concats " << mk_pp(concat_lhs, m) << " and "
-                                      << mk_pp(concat_rhs, m) << " won't overlap. Simplifying here." << std::endl;);
-                                simplify_concat_equality(concat_lhs, concat_rhs);
-                                found = true;
-                                break;
-                            }
-                        }
-                    }
-                    if (!found) {
-                        TRACE("str", tout << "All pairs of concats expected to overlap, falling back." << std::endl;);
-                        simplify_concat_equality(*(eqc_concat_lhs.begin()), *(eqc_concat_rhs.begin()));
-                    }
-                } else {
-                    // default behaviour
-                    simplify_concat_equality(*(eqc_concat_lhs.begin()), *(eqc_concat_rhs.begin()));
-                }
-            }
-        }
 
         // step 2: Concat == Constant
 
@@ -8319,6 +8217,86 @@ namespace smt {
 
     }
 
+    // Check that a string's length can be 0 iff it is the empty string.
+    void theory_str::check_eqc_empty_string(expr * lhs, expr * rhs) {
+        context & ctx = get_context();
+        ast_manager & m = get_manager();
+
+        rational nn1Len, nn2Len;
+        bool nn1Len_exists = get_len_value(lhs, nn1Len);
+        bool nn2Len_exists = get_len_value(rhs, nn2Len);
+        expr_ref emptyStr(mk_string(""), m);
+
+        if (nn1Len_exists && nn1Len.is_zero()) {
+            if (!in_same_eqc(lhs, emptyStr) && rhs != emptyStr) {
+                expr_ref eql(ctx.mk_eq_atom(mk_strlen(lhs), mk_int(0)), m);
+                expr_ref eqr(ctx.mk_eq_atom(lhs, emptyStr), m);
+                expr_ref toAssert(ctx.mk_eq_atom(eql, eqr), m);
+                assert_axiom(toAssert);
+            }
+        }
+
+        if (nn2Len_exists && nn2Len.is_zero()) {
+            if (!in_same_eqc(rhs, emptyStr) && lhs != emptyStr) {
+                expr_ref eql(ctx.mk_eq_atom(mk_strlen(rhs), mk_int(0)), m);
+                expr_ref eqr(ctx.mk_eq_atom(rhs, emptyStr), m);
+                expr_ref toAssert(ctx.mk_eq_atom(eql, eqr), m);
+                assert_axiom(toAssert);
+            }
+        }
+    }
+
+    void theory_str::check_eqc_concat_concat(std::set<expr*> & eqc_concat_lhs, std::set<expr*> & eqc_concat_rhs) {
+        ast_manager & m = get_manager();
+
+        int hasCommon = 0;
+        if (eqc_concat_lhs.size() != 0 && eqc_concat_rhs.size() != 0) {
+            std::set<expr*>::iterator itor1 = eqc_concat_lhs.begin();
+            std::set<expr*>::iterator itor2 = eqc_concat_rhs.begin();
+            for (; itor1 != eqc_concat_lhs.end(); itor1++) {
+                if (eqc_concat_rhs.find(*itor1) != eqc_concat_rhs.end()) {
+                    hasCommon = 1;
+                    break;
+                }
+            }
+            for (; itor2 != eqc_concat_rhs.end(); itor2++) {
+                if (eqc_concat_lhs.find(*itor2) != eqc_concat_lhs.end()) {
+                    hasCommon = 1;
+                    break;
+                }
+            }
+            if (hasCommon == 0) {
+                if (opt_ConcatOverlapAvoid) {
+                    bool found = false;
+                    // check each pair and take the first ones that won't immediately overlap
+                    for (itor1 = eqc_concat_lhs.begin(); itor1 != eqc_concat_lhs.end() && !found; ++itor1) {
+                        expr * concat_lhs = *itor1;
+                        for (itor2 = eqc_concat_rhs.begin(); itor2 != eqc_concat_rhs.end() && !found; ++itor2) {
+                            expr * concat_rhs = *itor2;
+                            if (will_result_in_overlap(concat_lhs, concat_rhs)) {
+                                TRACE("str", tout << "Concats " << mk_pp(concat_lhs, m) << " and "
+                                        << mk_pp(concat_rhs, m) << " will result in overlap; skipping." << std::endl;);
+                            } else {
+                                TRACE("str", tout << "Concats " << mk_pp(concat_lhs, m) << " and "
+                                        << mk_pp(concat_rhs, m) << " won't overlap. Simplifying here." << std::endl;);
+                                simplify_concat_equality(concat_lhs, concat_rhs);
+                                found = true;
+                                break;
+                            }
+                        }
+                    }
+                    if (!found) {
+                        TRACE("str", tout << "All pairs of concats expected to overlap, falling back." << std::endl;);
+                        simplify_concat_equality(*(eqc_concat_lhs.begin()), *(eqc_concat_rhs.begin()));
+                    }
+                } else {
+                    // default behaviour
+                    simplify_concat_equality(*(eqc_concat_lhs.begin()), *(eqc_concat_rhs.begin()));
+                }
+            }
+        }
+    }
+
     void theory_str::set_up_axioms(expr * ex) {
         ast_manager & m = get_manager();
         context & ctx = get_context();
@@ -9830,153 +9808,10 @@ namespace smt {
         }
     }
 
-    final_check_status theory_str::final_check_eh() {
+    void theory_str::solve_regex_automata() {
         context & ctx = get_context();
         ast_manager & m = get_manager();
 
-        //expr_ref_vector assignments(m);
-        //ctx.get_assignments(assignments);
-
-        if (opt_VerifyFinalCheckProgress) {
-            finalCheckProgressIndicator = false;
-        }
-
-        TRACE("str", tout << "final check" << std::endl;);
-        TRACE_CODE(if (is_trace_enabled("t_str_dump_assign")) { dump_assignments(); });
-        check_variable_scope();
-
-        if (opt_DeferEQCConsistencyCheck) {
-            TRACE("str", tout << "performing deferred EQC consistency check" << std::endl;);
-            std::set<enode*> eqc_roots;
-            for (ptr_vector<enode>::const_iterator it = ctx.begin_enodes(); it != ctx.end_enodes(); ++it) {
-                enode * e = *it;
-                enode * root = e->get_root();
-                eqc_roots.insert(root);
-            }
-
-            bool found_inconsistency = false;
-
-            for (std::set<enode*>::iterator it = eqc_roots.begin(); it != eqc_roots.end(); ++it) {
-                enode * e = *it;
-                app * a = e->get_owner();
-                if (!(m.get_sort(a) == u.str.mk_string_sort())) {
-                    TRACE("str", tout << "EQC root " << mk_pp(a, m) << " not a string term; skipping" << std::endl;);
-                } else {
-                    TRACE("str", tout << "EQC root " << mk_pp(a, m) << " is a string term. Checking this EQC" << std::endl;);
-                    // first call check_concat_len_in_eqc() on each member of the eqc
-                    enode * e_it = e;
-                    enode * e_root = e_it;
-                    do {
-                        bool status = check_concat_len_in_eqc(e_it->get_owner());
-                        if (!status) {
-                            TRACE("str", tout << "concat-len check asserted an axiom on " << mk_pp(e_it->get_owner(), m) << std::endl;);
-                            found_inconsistency = true;
-                        }
-                        e_it = e_it->get_next();
-                    } while (e_it != e_root);
-
-                    // now grab any two distinct elements from the EQC and call new_eq_check() on them
-                    enode * e1 = e;
-                    enode * e2 = e1->get_next();
-                    if (e1 != e2) {
-                        TRACE("str", tout << "deferred new_eq_check() over EQC of " << mk_pp(e1->get_owner(), m) << " and " << mk_pp(e2->get_owner(), m) << std::endl;);
-                        bool result = new_eq_check(e1->get_owner(), e2->get_owner());
-                        if (!result) {
-                            TRACE("str", tout << "new_eq_check found inconsistencies" << std::endl;);
-                            found_inconsistency = true;
-                        }
-                    }
-                }
-            }
-
-            if (found_inconsistency) {
-                TRACE("str", tout << "Found inconsistency in final check! Returning to search." << std::endl;);
-                return FC_CONTINUE;
-            } else {
-                TRACE("str", tout << "Deferred consistency check passed. Continuing in final check." << std::endl;);
-            }
-        }
-
-        // run dependence analysis to find free string variables
-        std::map<expr*, int> varAppearInAssign;
-        std::map<expr*, int> freeVar_map;
-        std::map<expr*, std::set<expr*> > unrollGroup_map;
-        std::map<expr*, std::map<expr*, int> > var_eq_concat_map;
-        int conflictInDep = ctx_dep_analysis(varAppearInAssign, freeVar_map, unrollGroup_map, var_eq_concat_map);
-        if (conflictInDep == -1) {
-            // return Z3_TRUE;
-            return FC_DONE;
-        }
-
-        // enhancement: improved backpropagation of string constants into var=concat terms
-        bool backpropagation_occurred = false;
-        for (std::map<expr*, std::map<expr*, int> >::iterator veqc_map_it = var_eq_concat_map.begin();
-             veqc_map_it != var_eq_concat_map.end(); ++veqc_map_it) {
-            expr * var = veqc_map_it->first;
-            for (std::map<expr*, int>::iterator concat_map_it = veqc_map_it->second.begin();
-                 concat_map_it != veqc_map_it->second.end(); ++concat_map_it) {
-                app * concat = to_app(concat_map_it->first);
-                expr * concat_lhs = concat->get_arg(0);
-                expr * concat_rhs = concat->get_arg(1);
-                // If the concat LHS and RHS both have a string constant in their EQC,
-                // but the var does not, then we assert an axiom of the form
-                // (lhs = "lhs" AND rhs = "rhs") --> (Concat lhs rhs) = "lhsrhs"
-                bool concat_lhs_haseqc, concat_rhs_haseqc, var_haseqc;
-                expr * concat_lhs_str = get_eqc_value(concat_lhs, concat_lhs_haseqc);
-                expr * concat_rhs_str = get_eqc_value(concat_rhs, concat_rhs_haseqc);
-                get_eqc_value(var, var_haseqc);
-                if (concat_lhs_haseqc && concat_rhs_haseqc && !var_haseqc) {
-                    TRACE("str", tout << "backpropagate into " << mk_pp(var, m) << " = " << mk_pp(concat, m) << std::endl
-                          << "LHS ~= " << mk_pp(concat_lhs_str, m) << " RHS ~= " << mk_pp(concat_rhs_str, m) << std::endl;);
-
-                    zstring lhsString, rhsString;
-                    u.str.is_string(concat_lhs_str, lhsString);
-                    u.str.is_string(concat_rhs_str, rhsString);
-                    zstring concatString = lhsString + rhsString;
-
-                    // special handling: don't assert that string constants are equal to themselves
-                    expr_ref_vector lhs_terms(m);
-                    if (!u.str.is_string(concat_lhs)) {
-                        lhs_terms.push_back(ctx.mk_eq_atom(concat_lhs, concat_lhs_str));
-                    }
-                    if (!u.str.is_string(concat_rhs)) {
-                        lhs_terms.push_back(ctx.mk_eq_atom(concat_rhs, concat_rhs_str));
-                    }
-
-                    if (lhs_terms.empty()) {
-                        // no assumptions on LHS
-                        expr_ref rhs(ctx.mk_eq_atom(concat, mk_string(concatString)), m);
-                        assert_axiom(rhs);
-                    } else {
-                        expr_ref lhs(mk_and(lhs_terms), m);
-                        expr_ref rhs(ctx.mk_eq_atom(concat, mk_string(concatString)), m);
-                        assert_implication(lhs, rhs);
-                    }
-                    backpropagation_occurred = true;
-                }
-            }
-        }
-
-        if (backpropagation_occurred) {
-            TRACE("str", tout << "Resuming search due to axioms added by backpropagation." << std::endl;);
-            return FC_CONTINUE;
-        }
-
-        // enhancement: improved backpropagation of length information
-        {
-            std::set<expr*> varSet;
-            std::set<expr*> concatSet;
-            std::map<expr*, int> exprLenMap;
-
-            bool length_propagation_occurred = propagate_length(varSet, concatSet, exprLenMap);
-            if (length_propagation_occurred) {
-                TRACE("str", tout << "Resuming search due to axioms added by length propagation." << std::endl;);
-                return FC_CONTINUE;
-            }
-        }
-
-        // regex automata
-        if (m_params.m_RegexAutomata) {
         // TODO since heuristics might fail, the "no progress" flag might need to be handled specially here
         bool regex_axiom_add = false;
         for (obj_hashtable<expr>::iterator it = regex_terms.begin(); it != regex_terms.end(); ++it) {
@@ -10582,12 +10417,12 @@ namespace smt {
                 }
             } // foreach(term in str_in_re_terms)
 
-                eautomaton * aut_inter = nullptr;
+            eautomaton * aut_inter = NULL;
             CTRACE("str", !intersect_constraints.empty(), tout << "check intersection of automata constraints for " << mk_pp(str, m) << std::endl;);
             for (svector<regex_automaton_under_assumptions>::iterator aut_it = intersect_constraints.begin();
                     aut_it != intersect_constraints.end(); ++aut_it) {
                 regex_automaton_under_assumptions aut = *aut_it;
-                    if (aut_inter == nullptr) {
+                if (aut_inter == NULL) {
                     // start somewhere
                     aut_inter = aut.get_automaton();
                     used_intersect_constraints.push_back(aut);
@@ -10637,7 +10472,7 @@ namespace smt {
                     }
                 }
             } // foreach(entry in intersect_constraints)
-                if (aut_inter != nullptr) {
+            if (aut_inter != NULL) {
                 aut_inter->compress();
             }
             TRACE("str", tout << "intersected " << used_intersect_constraints.size() << " constraints" << std::endl;);
@@ -10668,7 +10503,7 @@ namespace smt {
             }
             conflict_lhs = mk_and(conflict_terms);
 
-                if (used_intersect_constraints.size() > 1 && aut_inter != nullptr) {
+            if (used_intersect_constraints.size() > 1 && aut_inter != NULL) {
                 // check whether the intersection is only the empty string
                 unsigned initial_state = aut_inter->init();
                 if (aut_inter->final_states().size() == 1 && aut_inter->is_final_state(initial_state)) {
@@ -10686,7 +10521,7 @@ namespace smt {
                 }
             }
 
-                if (aut_inter != nullptr && aut_inter->is_empty()) {
+            if (aut_inter != NULL && aut_inter->is_empty()) {
                 TRACE("str", tout << "product automaton is empty; asserting conflict clause" << std::endl;);
                 expr_ref conflict_clause(m.mk_not(mk_and(conflict_terms)), m);
                 assert_axiom(conflict_clause);
@@ -10697,6 +10532,158 @@ namespace smt {
         if (regex_axiom_add) {
             //return FC_CONTINUE;
         }
+    }
+
+    final_check_status theory_str::final_check_eh() {
+        context & ctx = get_context();
+        ast_manager & m = get_manager();
+
+        //expr_ref_vector assignments(m);
+        //ctx.get_assignments(assignments);
+
+        if (opt_VerifyFinalCheckProgress) {
+            finalCheckProgressIndicator = false;
+        }
+
+        TRACE("str", tout << "final check" << std::endl;);
+        TRACE_CODE(if (is_trace_enabled("t_str_dump_assign")) { dump_assignments(); });
+        check_variable_scope();
+
+        if (opt_DeferEQCConsistencyCheck) {
+            TRACE("str", tout << "performing deferred EQC consistency check" << std::endl;);
+            std::set<enode*> eqc_roots;
+            for (ptr_vector<enode>::const_iterator it = ctx.begin_enodes(); it != ctx.end_enodes(); ++it) {
+                enode * e = *it;
+                enode * root = e->get_root();
+                eqc_roots.insert(root);
+            }
+
+            bool found_inconsistency = false;
+
+            for (std::set<enode*>::iterator it = eqc_roots.begin(); it != eqc_roots.end(); ++it) {
+                enode * e = *it;
+                app * a = e->get_owner();
+                if (!(m.get_sort(a) == u.str.mk_string_sort())) {
+                    TRACE("str", tout << "EQC root " << mk_pp(a, m) << " not a string term; skipping" << std::endl;);
+                } else {
+                    TRACE("str", tout << "EQC root " << mk_pp(a, m) << " is a string term. Checking this EQC" << std::endl;);
+                    // first call check_concat_len_in_eqc() on each member of the eqc
+                    enode * e_it = e;
+                    enode * e_root = e_it;
+                    do {
+                        bool status = check_concat_len_in_eqc(e_it->get_owner());
+                        if (!status) {
+                            TRACE("str", tout << "concat-len check asserted an axiom on " << mk_pp(e_it->get_owner(), m) << std::endl;);
+                            found_inconsistency = true;
+                        }
+                        e_it = e_it->get_next();
+                    } while (e_it != e_root);
+
+                    // now grab any two distinct elements from the EQC and call new_eq_check() on them
+                    enode * e1 = e;
+                    enode * e2 = e1->get_next();
+                    if (e1 != e2) {
+                        TRACE("str", tout << "deferred new_eq_check() over EQC of " << mk_pp(e1->get_owner(), m) << " and " << mk_pp(e2->get_owner(), m) << std::endl;);
+                        bool result = new_eq_check(e1->get_owner(), e2->get_owner());
+                        if (!result) {
+                            TRACE("str", tout << "new_eq_check found inconsistencies" << std::endl;);
+                            found_inconsistency = true;
+                        }
+                    }
+                }
+            }
+
+            if (found_inconsistency) {
+                TRACE("str", tout << "Found inconsistency in final check! Returning to search." << std::endl;);
+                return FC_CONTINUE;
+            } else {
+                TRACE("str", tout << "Deferred consistency check passed. Continuing in final check." << std::endl;);
+            }
+        }
+
+        // run dependence analysis to find free string variables
+        std::map<expr*, int> varAppearInAssign;
+        std::map<expr*, int> freeVar_map;
+        std::map<expr*, std::set<expr*> > unrollGroup_map;
+        std::map<expr*, std::map<expr*, int> > var_eq_concat_map;
+        int conflictInDep = ctx_dep_analysis(varAppearInAssign, freeVar_map, unrollGroup_map, var_eq_concat_map);
+        if (conflictInDep == -1) {
+            // return Z3_TRUE;
+            return FC_DONE;
+        }
+
+        // enhancement: improved backpropagation of string constants into var=concat terms
+        bool backpropagation_occurred = false;
+        for (std::map<expr*, std::map<expr*, int> >::iterator veqc_map_it = var_eq_concat_map.begin();
+             veqc_map_it != var_eq_concat_map.end(); ++veqc_map_it) {
+            expr * var = veqc_map_it->first;
+            for (std::map<expr*, int>::iterator concat_map_it = veqc_map_it->second.begin();
+                 concat_map_it != veqc_map_it->second.end(); ++concat_map_it) {
+                app * concat = to_app(concat_map_it->first);
+                expr * concat_lhs = concat->get_arg(0);
+                expr * concat_rhs = concat->get_arg(1);
+                // If the concat LHS and RHS both have a string constant in their EQC,
+                // but the var does not, then we assert an axiom of the form
+                // (lhs = "lhs" AND rhs = "rhs") --> (Concat lhs rhs) = "lhsrhs"
+                bool concat_lhs_haseqc, concat_rhs_haseqc, var_haseqc;
+                expr * concat_lhs_str = get_eqc_value(concat_lhs, concat_lhs_haseqc);
+                expr * concat_rhs_str = get_eqc_value(concat_rhs, concat_rhs_haseqc);
+                get_eqc_value(var, var_haseqc);
+                if (concat_lhs_haseqc && concat_rhs_haseqc && !var_haseqc) {
+                    TRACE("str", tout << "backpropagate into " << mk_pp(var, m) << " = " << mk_pp(concat, m) << std::endl
+                          << "LHS ~= " << mk_pp(concat_lhs_str, m) << " RHS ~= " << mk_pp(concat_rhs_str, m) << std::endl;);
+
+                    zstring lhsString, rhsString;
+                    u.str.is_string(concat_lhs_str, lhsString);
+                    u.str.is_string(concat_rhs_str, rhsString);
+                    zstring concatString = lhsString + rhsString;
+
+                    // special handling: don't assert that string constants are equal to themselves
+                    expr_ref_vector lhs_terms(m);
+                    if (!u.str.is_string(concat_lhs)) {
+                        lhs_terms.push_back(ctx.mk_eq_atom(concat_lhs, concat_lhs_str));
+                    }
+
+                    if (!u.str.is_string(concat_rhs)) {
+                        lhs_terms.push_back(ctx.mk_eq_atom(concat_rhs, concat_rhs_str));
+
+                    }
+
+                    if (lhs_terms.empty()) {
+                        // no assumptions on LHS
+                        expr_ref rhs(ctx.mk_eq_atom(concat, mk_string(concatString)), m);
+                        assert_axiom(rhs);
+                    } else {
+                        expr_ref lhs(mk_and(lhs_terms), m);
+                        expr_ref rhs(ctx.mk_eq_atom(concat, mk_string(concatString)), m);
+                        assert_implication(lhs, rhs);
+                    }
+                    backpropagation_occurred = true;
+                }
+            }
+        }
+
+        if (backpropagation_occurred) {
+            TRACE("str", tout << "Resuming search due to axioms added by backpropagation." << std::endl;);
+            return FC_CONTINUE;
+        }
+
+        // enhancement: improved backpropagation of length information
+        {
+            std::set<expr*> varSet;
+            std::set<expr*> concatSet;
+            std::map<expr*, int> exprLenMap;
+
+            bool length_propagation_occurred = propagate_length(varSet, concatSet, exprLenMap);
+            if (length_propagation_occurred) {
+                TRACE("str", tout << "Resuming search due to axioms added by length propagation." << std::endl;);
+                return FC_CONTINUE;
+            }
+        }
+
+        // regex automata
+        if (m_params.m_RegexAutomata) {
+            solve_regex_automata();
         } // RegexAutomata
 
         bool needToAssignFreeVars = false;

src/smt/theory_str.h

@@ -30,6 +30,7 @@
 #include "smt/params/theory_str_params.h"
 #include "smt/proto_model/value_factory.h"
 #include "smt/smt_model_generator.h"
+#include "smt/smt_arith_value.h"
 #include<set>
 #include<stack>
 #include<vector>
@@ -546,6 +547,7 @@ protected:
     void process_concat_eq_unroll(expr * concat, expr * unroll);
 
     // regex automata and length-aware regex
+    void solve_regex_automata();
     unsigned estimate_regex_complexity(expr * re);
     unsigned estimate_regex_complexity_under_complement(expr * re);
     unsigned estimate_automata_intersection_difficulty(eautomaton * aut1, eautomaton * aut2);
@@ -580,6 +582,8 @@ protected:
     bool can_concat_eq_str(expr * concat, zstring& str);
     bool can_concat_eq_concat(expr * concat1, expr * concat2);
     bool check_concat_len_in_eqc(expr * concat);
+    void check_eqc_empty_string(expr * lhs, expr * rhs);
+    void check_eqc_concat_concat(std::set<expr*> & eqc_concat_lhs, std::set<expr*> & eqc_concat_rhs);
     bool check_length_consistency(expr * n1, expr * n2);
     bool check_length_const_string(expr * n1, expr * constStr);
     bool check_length_eq_var_concat(expr * n1, expr * n2);