add mutex pass

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/opt/maxres.cpp

@@ -194,6 +194,8 @@ public:
         if (!init()) return l_undef;
         init_local();
         trace();
+        is_sat = process_mutex();
+        if (is_sat != l_true) return is_sat;
         while (m_lower < m_upper) {
             TRACE("opt", 
                   display_vec(tout, m_asms);
@@ -269,6 +271,42 @@ public:
         return l_true;
     }
 
+    lbool process_mutex() {
+#if 0
+        vector<expr_ref_vector> mutexes;
+        lbool is_sat = s().find_mutexes(m_asms, mutexes);
+        if (is_sat != l_true) {
+            return is_sat;
+        }
+        for (unsigned i = 0; i < mutexes.size(); ++i) {
+            process_mutex(mutexes[i]);
+        }
+#endif
+        return l_true;
+    }
+
+    void process_mutex(expr_ref_vector& mutex) {
+        TRACE("opt", tout << mutex << "\n";);
+        if (mutex.size() <= 1) {
+            return;
+        }
+        sort_assumptions(mutex);
+        ptr_vector<expr> core(mutex.size(), mutex.c_ptr());
+        remove_soft(core, m_asms);
+        rational weight(0);
+        while (!mutex.empty()) {
+            expr_ref soft = mk_or(mutex);
+            rational w = get_weight(mutex.back());
+            weight = w - weight;
+            m_lower += weight*rational(mutex.size()-1);
+            add_soft(soft, weight);
+            mutex.pop_back();
+            while (!mutex.empty() && get_weight(mutex.back()) == w) {
+                mutex.pop_back();
+            }
+            weight = w;
+        }        
+    }
 
     lbool check_sat_hill_climb(expr_ref_vector& asms1) {
         expr_ref_vector asms(asms1);

src/solver/solver.cpp

@@ -136,4 +136,73 @@ lbool solver::get_consequences_core(expr_ref_vector const& asms, expr_ref_vector
     return l_true;
 }
 
+lbool solver::find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) {
+    mutexes.reset();
+    ast_manager& m = vars.get_manager();
+
+    typedef obj_hashtable<expr> expr_set;
+    
+    expr_set A, P;
+
+    for (unsigned i = 0; i < vars.size(); ++i) {
+        A.insert(vars[i]);
+    }
+
+    while (!A.empty()) {
+        P = A;
+        expr_ref_vector mutex(m);
+        while (!P.empty()) {
+            expr_ref_vector asms(m);
+            expr* p = *P.begin();
+            P.remove(p);
+            if (!is_literal(m, p)) {
+                break;
+            }
+            mutex.push_back(p);
+            asms.push_back(p);
+            expr_set Q;
+            expr_set::iterator it = P.begin(), end = P.end();
+            for (; it != end; ++it) {
+                expr* q = *it;
+                scoped_assumption_push _scoped_push(asms, q);
+                if (is_literal(m, q)) {
+                    lbool is_sat = check_sat(asms);
+                    switch (is_sat) {
+                    case l_false: 
+                        Q.insert(q);
+                        break;
+                    case l_true:
+                        break;
+                    case l_undef:
+                        return l_undef;
+                    }
+                }
+            }
+            P = Q;
+        }
+        if (mutex.size() > 1) {
+            mutexes.push_back(mutex);            
+        }
+        for (unsigned i = 0; i < mutex.size(); ++i) {
+            A.remove(mutex[i].get());
+        }
+    }
+
+    // While A != {}:
+    // R = {} 
+    // P = ~A
+    //    While P != {}:
+    //       Pick p in ~P, 
+    //       R = R u { p }
+    //       Let Q be consequences over P of p modulo F. 
+    //       Let P &= Q
+    //    If |R| > 1: Yield R
+    //   A \= R               
+
+    return l_true;
+}
+
+bool solver::is_literal(ast_manager& m, expr* e) {
+    return is_uninterp_const(e) || (m.is_not(e, e) && is_uninterp_const(e));
+}
 

src/solver/solver.h

@@ -158,6 +158,14 @@ public:
     
     virtual lbool get_consequences(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences);
 
+
+    /**
+       \brief Find maximal subsets A' of A such that |A'| <= 1. These subsets look somewhat similar to cores: cores have the property 
+       that |~A'| >= 1, where ~A' is the set of negated formulas from A'
+     */
+
+    virtual lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes);
+
     /**
        \brief Display the content of this solver.
     */
@@ -176,6 +184,8 @@ protected:
 
     virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences);
 
+    bool is_literal(ast_manager& m, expr* e);
+
 };
 
 #endif