experimental new unsat core based overlap detection

src/smt/smt_context.cpp

@@ -37,7 +37,7 @@ Revision History:
 #include"model_pp.h"
 #include"ast_smt2_pp.h"
 #include"ast_translation.h"
-#include"theory_str.h"
+#include"theory_seq.h"
 
 namespace smt {
 
@@ -76,6 +76,8 @@ namespace smt {
         m_unsat_proof(m),
         m_unknown("unknown"),
         m_unsat_core(m),
+        m_use_theory_str_overlap_assumption(false),
+        m_theoryStrOverlapAssumption_term(m_manager),
 #ifdef Z3DEBUG
         m_trail_enabled(true),
 #endif
@@ -3269,21 +3271,38 @@ namespace smt {
 
         // PATCH for theory_str:
         // UNSAT + overlapping variables => UNKNOWN
-        if (r == l_false) {
-            ptr_vector<theory>::iterator it  = m_theory_set.begin();
-            ptr_vector<theory>::iterator end = m_theory_set.end();
-            for (; it != end; ++it) {
-                theory * th = *it;
-                if (strcmp(th->get_name(), "strings") == 0) {
-                    theory_str * str = (theory_str*)th;
-                    if (str->overlapping_variables_detected()) {
-                        TRACE("t_str", tout << "WARNING: overlapping variables detected, UNSAT changed to UNKNOWN!" << std::endl;);
-                        TRACE("context", tout << "WARNING: overlapping variables detected in theory_str. UNSAT changed to UNKNOWN!" << std::endl;);
-                        r = l_undef;
-                    }
+        if (r == l_false && use_theory_str_overlap_assumption()) {
+            // check the unsat core for an assumption from theory_str relating to overlaps.
+            // if we find this assumption, we have to answer UNKNOWN
+            // otherwise, we can pass through UNSAT
+            TRACE("t_str", tout << "unsat core:\n";
+            unsigned sz = m_unsat_core.size();
+            for (unsigned i = 0; i < sz; i++) {
+                tout << mk_pp(m_unsat_core.get(i), m_manager) << "\n";
+            });
+
+            bool assumptionFound = false;
+            unsigned sz = m_unsat_core.size();
+            app * target_term = to_app(m_manager.mk_not(m_theoryStrOverlapAssumption_term));
+            internalize_term(target_term);
+            for (unsigned i = 0; i < sz; ++i) {
+                app * core_term = to_app(m_unsat_core.get(i));
+                // not sure if this is the correct way to compare exprs in this context
+                enode * e1;
+                enode * e2;
+                e1 = get_enode(target_term);
+                e2 = get_enode(core_term);
+                if (e1 == e2) {
+                    // found match
+                    TRACE("t_str", tout << "overlap detected in unsat core; changing UNSAT to UNKNOWN" << std::endl;);
+                    assumptionFound = true;
+                    r = l_undef;
                     break;
                 }
             }
+            if (!assumptionFound) {
+                TRACE("t_str", tout << "no overlaps detected in unsat core, answering UNSAT" << std::endl;);
+            }
         }
 
         return r;
@@ -3302,6 +3321,22 @@ namespace smt {
         SASSERT(m_scope_lvl == 0);
         SASSERT(!m_setup.already_configured());
         setup_context(m_fparams.m_auto_config);
+
+        // theory_str requires the context to be set up with a special assumption.
+        // we need to wait until after setup_context() to know whether this is the case
+        if (m_use_theory_str_overlap_assumption) {
+            TRACE("t_str", tout << "enabling theory_str overlap assumption" << std::endl;);
+            // TODO maybe refactor this a bit
+            symbol strOverlap("!!TheoryStrOverlapAssumption!!");
+            expr_ref_vector assumption(get_manager());
+            seq_util m_sequtil(m_manager);
+            sort * s = m_manager.mk_bool_sort();
+            m_theoryStrOverlapAssumption_term = expr_ref(m_manager.mk_const(strOverlap, s), m_manager);
+            assumption.push_back(m_manager.mk_not(m_theoryStrOverlapAssumption_term));
+            // this might work, even though we already did a bit of setup
+            return check(assumption.size(), assumption.c_ptr(), reset_cancel);
+        }
+
         internalize_assertions();
         lbool r = l_undef;
         if (m_asserted_formulas.inconsistent()) {

src/smt/smt_context.h

@@ -226,6 +226,9 @@ namespace smt {
         literal2assumption         m_literal2assumption; // maps an expression associated with a literal to the original assumption
         expr_ref_vector            m_unsat_core;
 
+        // Unsat core assumption hint for theory_str
+        bool                       m_use_theory_str_overlap_assumption;
+
         // -----------------------------------
         //
         // Theory case split
@@ -846,6 +849,23 @@ namespace smt {
          */
         void add_theory_aware_branching_info(bool_var v, double priority, lbool phase);
 
+        // unsat core assumption hint for theory_str
+        void set_use_theory_str_overlap_assumption(bool f) {
+            m_use_theory_str_overlap_assumption = f;
+        }
+
+        bool use_theory_str_overlap_assumption() const {
+            return m_use_theory_str_overlap_assumption;
+        }
+
+        expr_ref get_theory_str_overlap_assumption_term() {
+            return m_theoryStrOverlapAssumption_term;
+        }
+
+    protected:
+        expr_ref m_theoryStrOverlapAssumption_term;
+    public:
+
         // helper function for trail
         void undo_th_case_split(literal l);
 

src/smt/smt_setup.cpp

@@ -706,6 +706,7 @@ namespace smt {
     }
 
     void setup::setup_QF_S() {
+        m_context.set_use_theory_str_overlap_assumption(true);
         m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
         m_context.register_plugin(alloc(smt::theory_str, m_manager, m_params));
     }
@@ -841,6 +842,7 @@ namespace smt {
 
     void setup::setup_str() {
         setup_arith();
+        m_context.set_use_theory_str_overlap_assumption(true);
         m_context.register_plugin(alloc(theory_str, m_manager, m_params));
     }
 

src/smt/theory_str.cpp

@@ -4304,6 +4304,8 @@ void theory_str::process_concat_eq_type6(expr * concatAst1, expr * concatAst2) {
         add_nonempty_constraint(commonVar);
     }
 
+    bool overlapAssumptionUsed = false;
+
     expr_ref_vector arrangement_disjunction(mgr);
     int pos = 1;
 
@@ -4339,6 +4341,12 @@ void theory_str::process_concat_eq_type6(expr * concatAst1, expr * concatAst2) {
         } else {
             TRACE("t_str", tout << "AVOID LOOP: SKIPPED." << std::endl;);
             TRACE("t_str", print_cut_var(m, tout); print_cut_var(y, tout););
+
+            // only add the overlap assumption one time
+            if (!overlapAssumptionUsed) {
+                arrangement_disjunction.push_back(ctx.get_theory_str_overlap_assumption_term());
+                overlapAssumptionUsed = true;
+            }
         }
     }
 
@@ -7239,6 +7247,9 @@ void theory_str::init_search_eh() {
     ast_manager & m = get_manager();
     context & ctx = get_context();
 
+    // safety
+    SASSERT(ctx.use_theory_str_overlap_assumption());
+
     TRACE("t_str_detail",
         tout << "dumping all asserted formulas:" << std::endl;
         unsigned nFormulas = ctx.get_num_asserted_formulas();
@@ -7301,6 +7312,7 @@ void theory_str::new_eq_eh(theory_var x, theory_var y) {
     //TRACE("t_str_detail", tout << "new eq: v#" << x << " = v#" << y << std::endl;);
     TRACE("t_str", tout << "new eq: " << mk_ismt2_pp(get_enode(x)->get_owner(), get_manager()) << " = " <<
                                   mk_ismt2_pp(get_enode(y)->get_owner(), get_manager()) << std::endl;);
+
     /*
     if (m_find.find(x) == m_find.find(y)) {
         return;

src/smt/theory_str.h

@@ -389,7 +389,6 @@ namespace smt {
         // finite model finding data
         // maps a finite model tester var to a list of variables that will be tested
         obj_map<expr, ptr_vector<expr> > finite_model_test_varlists;
-
     protected:
         void assert_axiom(expr * e);
         void assert_implication(expr * premise, expr * conclusion);