only handle equalities in assignments during init_search_eh

src/smt/theory_str.cpp

@@ -266,6 +266,10 @@ void theory_str::reset_eh() {
     pop_scope_eh(0);
 }
 
+void theory_str::handle_equality(expr * lhs, expr * rhs) {
+
+}
+
 void theory_str::set_up_axioms(expr * ex) {
     // TODO check to make sure we don't set up axioms on the same term twice
     TRACE("t_str_detail", tout << "setting up axioms for " << mk_ismt2_pp(ex, get_manager()) << std::endl;);
@@ -308,13 +312,40 @@ void theory_str::init_search_eh() {
             tout << mk_ismt2_pp(ex, m) << std::endl;
         }
     );
-    // recursive descent through all asserted formulas to set up axioms
+    /*
+     * Recursive descent through all asserted formulas to set up axioms.
+     * Note that this is just the input structure and not necessarily things
+     * that we know to be true or false. We're just doing this to see
+     * which terms are explicitly mentioned.
+     */
     unsigned nFormulas = ctx.get_num_asserted_formulas();
     for (unsigned i = 0; i < nFormulas; ++i) {
         expr * ex = ctx.get_asserted_formula(i);
         set_up_axioms(ex);
     }
 
+    /*
+     * Similar recursive descent, except over all initially assigned terms.
+     * This is done to find equalities between terms, etc. that we otherwise
+     * wouldn't get a chance to see.
+     */
+    expr_ref_vector assignments(m);
+    ctx.get_assignments(assignments);
+    for (expr_ref_vector::iterator i = assignments.begin(); i != assignments.end(); ++i) {
+        expr * ex = *i;
+        TRACE("t_str_detail", tout << "processing assignment " << mk_ismt2_pp(ex, m) << std::endl;);
+        if (m.is_eq(ex)) {
+            TRACE("t_str_detail", tout << "expr is equality" << std::endl;);
+            app * eq = (app*)ex;
+            SASSERT(eq->get_num_args() == 2);
+            expr * lhs = eq->get_arg(0);
+            expr * rhs = eq->get_arg(1);
+            handle_equality(lhs, rhs);
+        } else {
+            TRACE("t_str_detail", tout << "expr ignored" << std::endl;);
+        }
+    }
+
     search_started = true;
 }
 
@@ -323,6 +354,7 @@ void theory_str::new_eq_eh(theory_var x, theory_var y) {
     TRACE("t_str", tout << "new eq: v#" << x << " = v#" << y << std::endl;);
     TRACE("t_str_detail", tout << mk_ismt2_pp(get_enode(x)->get_owner(), get_manager()) << " = " <<
                                   mk_ismt2_pp(get_enode(y)->get_owner(), get_manager()) << std::endl;);
+    handle_equality(get_enode(x)->get_owner(), get_enode(y)->get_owner());
 }
 
 void theory_str::new_diseq_eh(theory_var x, theory_var y) {

src/smt/theory_str.h

@@ -49,6 +49,7 @@ namespace smt {
         void instantiate_basic_string_axioms(enode * str);
 
         void set_up_axioms(expr * ex);
+        void handle_equality(expr * lhs, expr * rhs);
     public:
         theory_str(ast_manager & m);
         virtual ~theory_str();
@@ -58,14 +59,12 @@ namespace smt {
 
         virtual void new_eq_eh(theory_var, theory_var);
         virtual void new_diseq_eh(theory_var, theory_var);
+
         virtual theory* mk_fresh(context*) { return alloc(theory_str, get_manager()); }
-
         virtual void init_search_eh();
-
         virtual void relevant_eh(app * n);
         virtual void assign_eh(bool_var v, bool is_true);
         virtual void push_scope_eh();
-
         virtual void reset_eh();
 
         virtual bool can_propagate();