add mutex preprocessing to maxsat, add parsing functions to C++ API

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

src/api/c++/z3++.h

@@ -63,7 +63,6 @@ namespace z3 {
     class func_entry;
     class statistics;
     class apply_result;
-    class fixedpoint;
     template<typename T> class ast_vector_tpl;
     typedef ast_vector_tpl<ast>       ast_vector;
     typedef ast_vector_tpl<expr>      expr_vector;
@@ -286,6 +285,15 @@ namespace z3 {
 
         expr num_val(int n, sort const & s);
 
+        /**
+           \brief parsing
+         */
+        expr parse_string(char const* s);
+        expr parse_file(char const* file);
+
+        expr parse_string(char const* s, sort_vector const& sorts, func_decl_vector const& decls);
+        expr parse_file(char const* s, sort_vector const& sorts, func_decl_vector const& decls);
+
         /**
            \brief Interpolation support
         */
@@ -442,7 +450,10 @@ namespace z3 {
            \brief Return the internal sort kind.
         */
         Z3_sort_kind sort_kind() const { return Z3_get_sort_kind(*m_ctx, *this); }
-
+        /**
+           \brief Return name of sort.
+        */
+        symbol name() const { Z3_symbol s = Z3_get_sort_name(ctx(), *this); check_error(); return symbol(ctx(), s); }
         /**
             \brief Return true if this sort is the Boolean sort.
         */
@@ -2454,6 +2465,37 @@ namespace z3 {
         return expr(a.ctx(), Z3_mk_interpolant(a.ctx(), a));
     }
 
+    inline expr context::parse_string(char const* s) {
+        Z3_ast r = Z3_parse_smtlib2_string(*this, s, 0, 0, 0, 0, 0, 0);
+        check_error();
+        return expr(*this, r);
+        
+    }
+    inline expr context::parse_file(char const* s) {
+        Z3_ast r = Z3_parse_smtlib2_file(*this, s, 0, 0, 0, 0, 0, 0);
+        check_error();
+        return expr(*this, r);
+    }
+
+    inline expr context::parse_string(char const* s, sort_vector const& sorts, func_decl_vector const& decls) {
+        array<Z3_symbol> sort_names(sorts.size());
+        array<Z3_symbol> decl_names(decls.size());
+        array<Z3_sort>   sorts1(sorts);
+        array<Z3_func_decl> decls1(decls);
+        for (unsigned i = 0; i < sorts.size(); ++i) {
+            sort_names[i] = sorts[i].name();
+        }
+        for (unsigned i = 0; i < decls.size(); ++i) {
+            decl_names[i] = decls[i].name();
+        }
+        Z3_ast r = Z3_parse_smtlib2_string(*this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr());
+        check_error();
+        return expr(*this, r);
+    }
+
+    // inline expr context::parse_file(char const* s, sort_vector const& sorts, func_decl_vector const& decls);
+
+
     inline check_result context::compute_interpolant(expr const& pat, params const& p, expr_vector& i, model& m) {
         Z3_ast_vector interp = 0;
         Z3_model mdl = 0;

src/opt/maxres.cpp

@@ -197,6 +197,7 @@ public:
         is_sat = process_mutex();
         if (is_sat != l_true) return is_sat;
         while (m_lower < m_upper) {
+            if (m_lower >= m_upper) break;
             TRACE("opt", 
                   display_vec(tout, m_asms);
                   s().display(tout);
@@ -235,8 +236,10 @@ public:
         init_local();
         trace();
         exprs cs;
+        lbool is_sat = process_mutex();
+        if (is_sat != l_true) return is_sat;
         while (m_lower < m_upper) {
-            lbool is_sat = check_sat_hill_climb(m_asms);
+            is_sat = check_sat_hill_climb(m_asms);
             if (m.canceled()) {
                 return l_undef;
             }
@@ -272,7 +275,6 @@ public:
     }
 
     lbool process_mutex() {
-#if 0
         vector<expr_ref_vector> mutexes;
         lbool is_sat = s().find_mutexes(m_asms, mutexes);
         if (is_sat != l_true) {
@@ -281,7 +283,9 @@ public:
         for (unsigned i = 0; i < mutexes.size(); ++i) {
             process_mutex(mutexes[i]);
         }
-#endif
+        if (!mutexes.empty()) {
+            trace();
+        }
         return l_true;
     }
 

src/sat/sat_solver.cpp

@@ -835,48 +835,66 @@ namespace sat {
     lbool solver::bounded_search() {
         while (true) {
             checkpoint();
-            while (true) {
+            bool done = false;
-                propagate(true);
+            while (!done) {
-                if (!inconsistent())
+                lbool is_sat = propagate_and_backjump_step(done);
-                    break;
+                if (is_sat != l_true) return is_sat;
-                if (!resolve_conflict())
-                    return l_false;
-                if (m_conflicts > m_config.m_max_conflicts)
-                    return l_undef;
-                if (m_conflicts_since_restart > m_restart_threshold)
-                    return l_undef;
-                if (scope_lvl() == 0) {
-                    cleanup(); // cleaner may propagate frozen clauses
-                    if (inconsistent()) {
-                        TRACE("sat", tout << "conflict at level 0\n";);
-                        return l_false;
-                    }
-                    gc();
-                }
             }
 
             gc();
 
             if (!decide()) {
-                if (m_ext) {
+                lbool is_sat = final_check();
-                    switch (m_ext->check()) {
+                if (is_sat != l_undef) {
-                    case CR_DONE:
+                    return is_sat;
-                        mk_model();
-                        return l_true;
-                    case CR_CONTINUE:
-                        break;
-                    case CR_GIVEUP:
-                        throw abort_solver();
-                    }
-                }
-                else {
-                    mk_model();
-                    return l_true;
                 }
             }
         }
     }
 
+    lbool solver::propagate_and_backjump_step(bool& done) {
+        done = true;
+        propagate(true);
+        if (!inconsistent())
+            return l_true;
+        if (!resolve_conflict())
+            return l_false;
+        if (m_conflicts > m_config.m_max_conflicts)
+            return l_undef;
+        if (m_conflicts_since_restart > m_restart_threshold)
+            return l_undef;
+        if (scope_lvl() == 0) {
+            cleanup(); // cleaner may propagate frozen clauses
+            if (inconsistent()) {
+                TRACE("sat", tout << "conflict at level 0\n";);
+                return l_false;
+            }
+            gc();
+        }
+        done = false;
+        return l_true;
+    }
+
+    lbool solver::final_check() {
+        if (m_ext) {
+            switch (m_ext->check()) {
+            case CR_DONE:
+                mk_model();
+                return l_true;
+            case CR_CONTINUE:
+                break;
+            case CR_GIVEUP:
+                throw abort_solver();
+            }
+            return l_undef;
+        }
+        else {
+            mk_model();
+            return l_true;
+        }        
+    }
+
+
     bool solver::check_inconsistent() {
         if (inconsistent()) {
             if (tracking_assumptions())
@@ -3035,6 +3053,220 @@ namespace sat {
         return r;
     }
 
+    lbool solver::find_mutexes(literal_vector const& lits, vector<literal_vector> & mutexes) {
+        literal_vector ps(lits);
+        m_user_bin_clauses.reset();
+        m_binary_clause_graph.reset();
+        collect_bin_clauses(m_user_bin_clauses, true);
+        collect_bin_clauses(m_user_bin_clauses, false);
+        for (unsigned i = 0; i < m_user_bin_clauses.size(); ++i) {
+            literal l1 = m_user_bin_clauses[i].first;
+            literal l2 = m_user_bin_clauses[i].second;
+            m_binary_clause_graph.reserve(l1.index() + 1);
+            m_binary_clause_graph.reserve(l2.index() + 1);
+            m_binary_clause_graph.reserve((~l1).index() + 1);
+            m_binary_clause_graph.reserve((~l2).index() + 1);
+            m_binary_clause_graph[l1.index()].push_back(l2);
+            m_binary_clause_graph[l2.index()].push_back(l1);
+        }
+        while (!ps.empty()) {            
+            literal_vector mutex;
+            literal_set other(ps);
+            while (!other.empty()) {
+                literal_set conseq;
+                literal p = other.pop();
+                mutex.push_back(p);
+                if (other.empty()) {
+                    break;
+                }
+                get_reachable(p, other, conseq);
+                other = conseq;
+            }
+            if (mutex.size() > 1) {
+                mutexes.push_back(mutex);            
+            }
+            for (unsigned i = 0; i < mutex.size(); ++i) {
+                ps.erase(mutex[i]);
+            }
+        }
+        return l_true;
+    }
+
+    void solver::get_reachable(literal p, literal_set const& goal, literal_set& reachable) {
+        literal_set seen;
+        literal_vector todo;
+        todo.push_back(p);
+        while (!todo.empty()) {
+            p = todo.back();
+            todo.pop_back();
+            if (seen.contains(p)) {
+                continue;
+            }
+            seen.insert(p);
+            literal np = ~p;
+            if (goal.contains(np)) {
+                reachable.insert(np);
+            }
+            todo.append(m_binary_clause_graph[np.index()]);
+        }
+    }
+
+    lbool solver::get_consequences(literal_vector const& asms, bool_var_vector const& vars, vector<literal_vector>& conseq) {
+        literal_vector lits;
+        lbool is_sat = check(asms.size(), asms.c_ptr());
+        if (is_sat != l_true) {
+            return is_sat;
+        }
+        for (unsigned i = 0; i < vars.size(); ++i) {
+            bool_var v = vars[i];
+            switch (get_model()[v]) {
+            case l_true: lits.push_back(literal(v, false)); break;
+            case l_false: lits.push_back(literal(v, true)); break;
+            default: break;                
+            }
+        }
+        return get_consequences(asms, lits, conseq);
+    }
+
+    lbool solver::get_consequences(literal_vector const& asms, literal_vector const& lits, vector<literal_vector>& conseq) {
+        m_antecedents.reset();
+        literal_set unfixed(lits), assumptions(asms);
+
+        pop_to_base_level();
+        if (inconsistent()) return l_false;
+        init_search();
+        propagate(false);
+        if (inconsistent()) return l_false;
+        init_assumptions(asms.size(), asms.c_ptr(), 0, 0);
+        propagate(false);
+        if (check_inconsistent()) return l_false;
+       
+        unsigned num_units = 0;
+        extract_fixed_consequences(num_units, assumptions, unfixed, conseq);
+        while (!unfixed.empty()) {
+            checkpoint();
+            literal_set::iterator it = unfixed.begin(), end = unfixed.end();
+            unsigned chunk_size = 100;
+            for (; it != end && chunk_size > 0; ++it) {
+                literal lit = *it;
+                if (value(lit) != l_undef) {
+                    continue;
+                }
+                --chunk_size;
+                push();
+                assign(~lit, justification());
+                propagate(false);
+                while (inconsistent()) {      
+                    if (!resolve_conflict()) {
+                        TRACE("sat", tout << "inconsistent\n";);
+                        return l_false;
+                    }
+                    propagate(false);
+                }
+            }
+            lbool is_sat;
+            while (true) {
+                is_sat = bounded_search();
+                if (is_sat == l_undef) {
+                    restart();                  
+                    continue;
+                }
+                break;
+            }
+            if (is_sat == l_false) {
+                TRACE("sat", tout << "unsat\n";);
+                m_inconsistent = false;
+            }
+            if (is_sat == l_true) {
+                delete_unfixed(unfixed);
+            }
+            extract_fixed_consequences(num_units, assumptions, unfixed, conseq);            
+        }
+        return l_true;
+    }
+
+    void solver::delete_unfixed(literal_set& unfixed) {
+        literal_set to_keep;
+        literal_set::iterator it = unfixed.begin(), end = unfixed.end();
+        for (; it != end; ++it) {
+            literal lit = *it;
+            if (value(lit) == l_true) {
+                to_keep.insert(lit);
+            }
+        }        
+        unfixed = to_keep;
+    }
+    
+    void solver::extract_fixed_consequences(unsigned& start, literal_set const& assumptions, literal_set& unfixed, vector<literal_vector>& conseq) {
+        if (scope_lvl() > 1) {
+            pop(scope_lvl() - 1);
+        }
+        SASSERT(!inconsistent());
+        unsigned sz = m_trail.size();
+        for (unsigned i = start; i < sz; ++i) {
+            extract_fixed_consequences(m_trail[i], assumptions, unfixed, conseq);
+        }
+        start = sz;
+    }
+
+    void solver::extract_assumptions(literal lit, index_set& s) {
+        justification js = m_justification[lit.var()];
+        switch (js.get_kind()) {
+        case justification::NONE:
+            break;
+        case justification::BINARY:
+            s |= m_antecedents.find(js.get_literal().var());
+            break;
+        case justification::TERNARY:
+            s |= m_antecedents.find(js.get_literal1().var());
+            s |= m_antecedents.find(js.get_literal2().var());
+            break;
+        case justification::CLAUSE: {
+            clause & c = *(m_cls_allocator.get_clause(js.get_clause_offset()));
+            for (unsigned i = 0; i < c.size(); ++i) {
+                if (c[i] != lit) {
+                    s |= m_antecedents.find(c[i].var());
+                }
+            }
+            break;
+        }
+        case justification::EXT_JUSTIFICATION: {
+            fill_ext_antecedents(lit, js);
+            literal_vector::iterator it  = m_ext_antecedents.begin();
+            literal_vector::iterator end = m_ext_antecedents.end();
+            for (; it != end; ++it) {
+                s |= m_antecedents.find(it->var());
+            }
+            break;
+        }
+        default:
+            UNREACHABLE();
+            break;
+        }
+    }
+
+    void solver::extract_fixed_consequences(literal lit, literal_set const& assumptions, literal_set& unfixed, vector<literal_vector>& conseq) {
+        index_set s;        
+        if (assumptions.contains(lit)) {
+            s.insert(lit.index());
+        }
+        else {
+            add_assumption(lit);
+            extract_assumptions(lit, s);
+        }
+        m_antecedents.insert(lit.var(), s);
+        if (unfixed.contains(lit)) {
+            literal_vector cons;
+            cons.push_back(lit);
+            index_set::iterator it = s.begin(), end = s.end();
+            for (; it != end; ++it) {
+                cons.push_back(to_literal(*it));
+            }
+            unfixed.remove(lit);
+            conseq.push_back(cons);
+        }
+    }
+
     void solver::asymmetric_branching() {
         if (scope_lvl() > 0 || inconsistent())
             return;

src/sat/sat_solver.h

@@ -300,6 +300,8 @@ namespace sat {
         bool decide();
         bool_var next_var();
         lbool bounded_search();
+        lbool final_check();
+        lbool propagate_and_backjump_step(bool& done);
         void init_search();
         
         literal_vector m_min_core;
@@ -409,6 +411,7 @@ namespace sat {
         void gc_lit(clause_vector& clauses, literal lit);
         void gc_bin(bool learned, literal nlit);
         void gc_var(bool_var v);
+
         bool_var max_var(clause_vector& clauses, bool_var v);
         bool_var max_var(bool learned, bool_var v);
 
@@ -428,6 +431,35 @@ namespace sat {
         void asymmetric_branching();
         unsigned scc_bin();
 
+        // -----------------------
+        //
+        // Auxiliary methods.
+        //
+        // -----------------------
+    public:
+        lbool find_mutexes(literal_vector const& lits, vector<literal_vector> & mutexes);
+
+        lbool get_consequences(literal_vector const& assms, bool_var_vector const& vars, vector<literal_vector>& conseq);
+
+    private:
+
+        typedef hashtable<unsigned, u_hash, u_eq> index_set;
+
+        u_map<index_set>       m_antecedents;
+        vector<literal_vector> m_binary_clause_graph;
+
+        void extract_assumptions(literal lit, index_set& s);
+
+        void get_reachable(literal p, literal_set const& goal, literal_set& reachable);
+
+        lbool get_consequences(literal_vector const& assms, literal_vector const& lits, vector<literal_vector>& conseq);
+
+        void delete_unfixed(literal_set& unfixed);
+
+        void extract_fixed_consequences(unsigned& start, literal_set const& assumptions, literal_set& unfixed, vector<literal_vector>& conseq);
+
+        void extract_fixed_consequences(literal lit, literal_set const& assumptions, literal_set& unfixed, vector<literal_vector>& conseq);
+
         // -----------------------
         //
         // Activity related stuff

src/sat/sat_solver/inc_sat_solver.cpp

@@ -107,6 +107,7 @@ public:
         return check_sat(num_assumptions, assumptions, 0, 0);
     }
 
+
     void display_weighted(std::ostream& out, unsigned sz, expr * const * assumptions, unsigned const* weights) {
         m_weights.reset();
         if (weights != 0) {
@@ -231,6 +232,33 @@ public:
         return 0;
     }
 
+    virtual lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) {
+        sat::literal_vector ls;
+        u_map<expr*> lit2var;
+        for (unsigned i = 0; i < vars.size(); ++i) {
+            expr* e = vars[i];
+            bool neg = m.is_not(e, e);
+            sat::bool_var v = m_map.to_bool_var(e);
+            if (v != sat::null_bool_var) {
+                sat::literal lit(v, neg);
+                ls.push_back(lit);
+                lit2var.insert(lit.index(), vars[i]);
+            }
+        }
+        vector<sat::literal_vector> ls_mutexes;
+        m_solver.find_mutexes(ls, ls_mutexes);
+        for (unsigned i = 0; i < ls_mutexes.size(); ++i) {
+            sat::literal_vector const ls_mutex = ls_mutexes[i];
+            expr_ref_vector mutex(m);
+            for (unsigned j = 0; j < ls_mutex.size(); ++j) {
+                mutex.push_back(lit2var.find(ls_mutex[j].index()));
+            }
+            mutexes.push_back(mutex);
+        }
+        return l_true;
+    }
+
+
     virtual std::string reason_unknown() const {
         return m_unknown;
     }

src/sat/sat_types.h

@@ -105,6 +105,7 @@ namespace sat {
     inline std::ostream & operator<<(std::ostream & out, literal l) { out << (l.sign() ? "-" : "") << l.var(); return out; }
 
     typedef svector<literal> literal_vector;
+    typedef std::pair<literal, literal> literal_pair;
 
     typedef unsigned clause_offset;
     typedef unsigned ext_constraint_idx;
@@ -161,6 +162,17 @@ namespace sat {
             m_set.push_back(v); 
         }
 
+        void remove(unsigned v) {
+            if (contains(v)) {
+                m_in_set[v] = false;
+                unsigned i = 0;
+                for (i = 0; i < m_set.size() && m_set[i] != v; ++i);
+                SASSERT(i < m_set.size());
+                m_set[i] = m_set.back();
+                m_set.pop_back();
+            }
+        }
+
         uint_set& operator=(uint_set const& other) {
             m_in_set = other.m_in_set;
             m_set = other.m_set;
@@ -228,6 +240,7 @@ namespace sat {
             return result;
         }
         void insert(literal l) { m_set.insert(l.index()); }
+        void remove(literal l) { m_set.remove(l.index()); }
         literal pop() { return to_literal(m_set.erase()); }
         bool contains(literal l) const { return m_set.contains(l.index()); }
         bool empty() const { return m_set.empty(); }

src/solver/solver.cpp

@@ -137,6 +137,11 @@ lbool solver::get_consequences_core(expr_ref_vector const& asms, expr_ref_vector
 }
 
 lbool solver::find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) {
+    return l_true;
+#if 0
+    // complete for literals, but inefficient.
+    // see more efficient (incomplete) version in sat_solver
+
     mutexes.reset();
     ast_manager& m = vars.get_manager();
 
@@ -187,19 +192,9 @@ lbool solver::find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>&
             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;
+#endif
+
 }
 
 bool solver::is_literal(ast_manager& m, expr* e) {