improve pre-processing

src/api/api_solver.cpp

@@ -564,7 +564,7 @@ extern "C" {
         init_solver(c, s);
         Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
         mk_c(c)->save_object(v);
-        expr_ref_vector trail = to_solver_ref(s)->get_trail();
+        expr_ref_vector trail = to_solver_ref(s)->get_trail(UINT_MAX);
         for (expr* f : trail) {
             v->m_ast_vector.push_back(f);
         }

src/muz/spacer/spacer_iuc_solver.h

@@ -126,7 +126,7 @@ public:
     void move_to_front(expr* e) override { m_solver.move_to_front(e); }
     expr_ref_vector cube(expr_ref_vector&, unsigned) override { return expr_ref_vector(m); }
     void get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) override { m_solver.get_levels(vars, depth); }
-    expr_ref_vector get_trail() override { return m_solver.get_trail(); }
+    expr_ref_vector get_trail(unsigned max_level) override { return m_solver.get_trail(max_level); }
 
     void push() override;
     void pop(unsigned n) override;

src/opt/opt_preprocess.cpp

@@ -23,10 +23,9 @@ Author:
 
 namespace opt {
 
-    bool preprocess::find_mutexes(vector<soft>& softs, rational& lower) {
+    obj_map<expr, rational> preprocess::soft2map(vector<soft> const& softs, expr_ref_vector& fmls) {
-        expr_ref_vector fmls(m);
         obj_map<expr, rational> new_soft;
-        for (soft& sf : softs) {
+        for (soft const& sf : softs) {
             m_trail.push_back(sf.s);
             if (new_soft.contains(sf.s))
                 new_soft[sf.s] += sf.weight;
@@ -34,6 +33,12 @@ namespace opt {
                 new_soft.insert(sf.s, sf.weight);
             fmls.push_back(sf.s);
         }
+        return new_soft;
+    }
+
+    bool preprocess::find_mutexes(vector<soft>& softs, rational& lower) {
+        expr_ref_vector fmls(m);
+        obj_map<expr, rational> new_soft = soft2map(softs, fmls);
         vector<expr_ref_vector> mutexes;
         lbool is_sat = s.find_mutexes(fmls, mutexes);
         if (is_sat == l_false)
@@ -97,6 +102,8 @@ namespace opt {
     preprocess::preprocess(solver& s):  m(s.get_manager()), s(s), m_trail(m) {}
     
     bool preprocess::operator()(vector<soft>& soft, rational& lower) {
-        return find_mutexes(soft, lower);
+        if (!find_mutexes(soft, lower))
+            return false;
+        return true;
     }
 };

src/opt/opt_preprocess.h

@@ -28,6 +28,7 @@ namespace opt {
         solver&          s;
         expr_ref_vector  m_trail;
 
+        obj_map<expr, rational> soft2map(vector<soft> const& softs, expr_ref_vector& fmls);
         bool find_mutexes(vector<soft>& softs, rational& lower);
         void process_mutex(expr_ref_vector& mutex, obj_map<expr, rational>& new_soft, rational& lower);
 

src/opt/opt_solver.h

@@ -108,7 +108,7 @@ namespace opt {
         lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) override;
         lbool preferred_sat(expr_ref_vector const& asms, vector<expr_ref_vector>& cores) override;
         void get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) override; 
-        expr_ref_vector get_trail() override { return m_context.get_trail(); }
+        expr_ref_vector get_trail(unsigned max_level) override { return m_context.get_trail(max_level); }
         expr_ref_vector cube(expr_ref_vector&, unsigned) override { return expr_ref_vector(m); }
         void set_phase(expr* e) override { m_context.set_phase(e); }
         phase* get_phase() override { return m_context.get_phase(); }

src/sat/sat_solver.cpp

@@ -4194,7 +4194,7 @@ namespace sat {
         unsigned_vector ps;
         for (literal lit : _lits) 
             ps.push_back(lit.index());
-        mc.cliques(ps, _mutexes);
+        mc.cliques2(ps, _mutexes);
         vector<vector<literal_vector>> sorted;
         for (auto const& mux : _mutexes) {
             literal_vector clique;

src/sat/sat_solver/inc_sat_solver.cpp

@@ -390,7 +390,7 @@ public:
         }
     }
 
-    expr_ref_vector get_trail() override {
+    expr_ref_vector get_trail(unsigned max_level) override {
         expr_ref_vector result(m);
         unsigned sz = m_solver.trail_size();
         expr_ref_vector lit2expr(m);
@@ -398,7 +398,11 @@ public:
         m_map.mk_inv(lit2expr);
         for (unsigned i = 0; i < sz; ++i) {
             sat::literal lit = m_solver.trail_literal(i);
-            result.push_back(lit2expr[lit.index()].get());
+            if (m_solver.lvl(lit) > max_level)
+                continue;
+            expr_ref e(lit2expr.get(lit.index()), m);
+            if (e)
+                result.push_back(e);
         }
         return result;
     }

src/sat/smt/atom2bool_var.cpp

@@ -41,12 +41,12 @@ void atom2bool_var::mk_var_inv(expr_ref_vector & var2expr) const {
 
 sat::bool_var atom2bool_var::to_bool_var(expr * n) const {
     unsigned idx = m_id2map.get(n->get_id(), UINT_MAX);
-    if (idx == UINT_MAX) {
+    if (idx == UINT_MAX) 
         return sat::null_bool_var;
-    }
+    else if (idx >= m_mapping.size())
-    else {
+        return sat::null_bool_var;
+    else 
         return m_mapping[idx].m_value;
-    }
 }
 
 struct collect_boolean_interface_proc {

src/smt/smt_context.cpp

@@ -4612,9 +4612,15 @@ namespace smt {
         }
     }
 
-    expr_ref_vector context::get_trail() {        
+    expr_ref_vector context::get_trail(unsigned max_level) {        
         expr_ref_vector result(get_manager());
-        get_assignments(result);
+        for (literal lit : m_assigned_literals) {
+            if (get_assign_level(lit) > max_level + m_base_lvl)
+                continue;
+            expr_ref e(m);
+            literal2expr(lit, e);
+            result.push_back(std::move(e));
+        }
         return result;
     }
 
@@ -4622,15 +4628,10 @@ namespace smt {
         expr_mark visited;
         for (expr* fml : result)
             visited.mark(fml);
-        for (literal lit : m_assigned_literals) {
+        expr_ref_vector trail = get_trail(0);
-            if (get_assign_level(lit) > m_base_lvl)
+        for (expr* t : trail) 
-                break;
+            if (!visited.is_marked(t))
-            expr_ref e(m);
+                result.push_back(t);
-            literal2expr(lit, e);
-            if (visited.is_marked(e))
-                continue;
-            result.push_back(std::move(e));
-        }
     }
 
 

src/smt/smt_context.h

@@ -1667,7 +1667,7 @@ namespace smt {
 
         void get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth);
 
-        expr_ref_vector get_trail();
+        expr_ref_vector get_trail(unsigned max_level);
 
         void get_model(model_ref & m);
 

src/smt/smt_kernel.cpp

@@ -248,8 +248,8 @@ namespace smt {
         m_imp->m_kernel.get_levels(vars, depth);
     }
 
-    expr_ref_vector kernel::get_trail() {
+    expr_ref_vector kernel::get_trail(unsigned max_level) {
-        return m_imp->m_kernel.get_trail();
+        return m_imp->m_kernel.get_trail(max_level);
     }
 
     void kernel::user_propagate_init(

src/smt/smt_kernel.h

@@ -248,7 +248,7 @@ namespace smt {
         /**
            \brief retrieve trail of assignment stack.
         */
-        expr_ref_vector get_trail();
+        expr_ref_vector get_trail(unsigned max_level);
 
         /**
            \brief (For debubbing purposes) Prints the state of the kernel

src/smt/smt_solver.cpp

@@ -208,8 +208,8 @@ namespace {
             m_context.get_levels(vars, depth);
         }
 
-        expr_ref_vector get_trail() override {
+        expr_ref_vector get_trail(unsigned max_level) override {
-            return m_context.get_trail();
+            return m_context.get_trail(max_level);
         }
 
         void user_propagate_init(

src/solver/combined_solver.cpp

@@ -311,11 +311,11 @@ public:
             m_solver2->get_levels(vars, depth);
     }
 
-    expr_ref_vector get_trail() override {
+    expr_ref_vector get_trail(unsigned max_level) override {
         if (m_use_solver1_results)
-            return m_solver1->get_trail();
+            return m_solver1->get_trail(max_level);
         else
-            return m_solver2->get_trail();
+            return m_solver2->get_trail(max_level);
     }
 
     proof * get_proof() override {

src/solver/solver.h

@@ -265,7 +265,7 @@ public:
 
     expr_ref_vector get_non_units();
 
-    virtual expr_ref_vector get_trail() = 0; // { return expr_ref_vector(get_manager()); }
+    virtual expr_ref_vector get_trail(unsigned max_level) = 0; // { return expr_ref_vector(get_manager()); }
     
     virtual void get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) = 0;
 

src/solver/solver_pool.cpp

@@ -127,8 +127,8 @@ public:
         m_base->get_levels(vars, depth);
     }
 
-    expr_ref_vector get_trail() override {
+    expr_ref_vector get_trail(unsigned max_level) override {
-        return m_base->get_trail();
+        return m_base->get_trail(max_level);
     }
 
     lbool check_sat_core2(unsigned num_assumptions, expr * const * assumptions) override {

src/solver/tactic2solver.cpp

@@ -134,7 +134,7 @@ public:
         throw default_exception("cannot retrieve depth from solvers created using tactics");
     }
 
-    expr_ref_vector get_trail() override {
+    expr_ref_vector get_trail(unsigned max_level) override {
         throw default_exception("cannot retrieve trail from solvers created using tactics");
     }
 };

src/tactic/fd_solver/bounded_int2bv_solver.cpp

@@ -165,8 +165,8 @@ public:
     void get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) override {
         m_solver->get_levels(vars, depth);
     }
-    expr_ref_vector get_trail() override {
+    expr_ref_vector get_trail(unsigned max_level) override {
-        return m_solver->get_trail();
+        return m_solver->get_trail(max_level);
     }
 
     model_converter* external_model_converter() const {

src/tactic/fd_solver/enum2bv_solver.cpp

@@ -189,8 +189,8 @@ public:
         m_solver->get_levels(vars, depth);
     }
 
-    expr_ref_vector get_trail() override {
+    expr_ref_vector get_trail(unsigned max_level) override {
-        return m_solver->get_trail();
+        return m_solver->get_trail(max_level);
     }
 
     unsigned get_num_assertions() const override {

src/tactic/fd_solver/pb2bv_solver.cpp

@@ -105,8 +105,8 @@ public:
         m_solver->get_levels(vars, depth);
     }
 
-    expr_ref_vector get_trail() override {
+    expr_ref_vector get_trail(unsigned max_level) override {
-        return m_solver->get_trail();
+        return m_solver->get_trail(max_level);
     }
 
     model_converter* external_model_converter() const{

src/tactic/fd_solver/smtfd_solver.cpp

@@ -2098,9 +2098,9 @@ namespace smtfd {
             m_fd_sat_solver->get_levels(vars, depth);
         }
         
-        expr_ref_vector get_trail() override {
+        expr_ref_vector get_trail(unsigned max_level) override {
             init();
-            return m_fd_sat_solver->get_trail();
+            return m_fd_sat_solver->get_trail(max_level);
         }
         
         unsigned get_num_assertions() const override {

src/util/max_cliques.h

@@ -20,6 +20,7 @@ Notes:
 
 #include "util/vector.h"
 #include "util/uint_set.h"
+#include "util/heap.h"
 
 
 template<class T>
@@ -43,12 +44,9 @@ class max_cliques : public T {
             m_seen1.insert(p);
             if (m_seen2.contains(p)) {
                 unsigned_vector const& tc = m_tc[p];
-                for (unsigned j = 0; j < tc.size(); ++j) {
+                for (unsigned np : tc) 
-                    unsigned np = tc[j];
+                    if (goal.contains(np)) 
-                    if (goal.contains(np)) {
                         reachable.insert(np);
-                    }
-                }
             }
             else {
                 unsigned np = negate(p);
@@ -61,30 +59,31 @@ class max_cliques : public T {
         for (unsigned i = m_todo.size(); i > 0; ) {
             --i;
             p = m_todo[i];
-            if (m_seen2.contains(p)) {
+            if (m_seen2.contains(p)) 
                 continue;
-            }
             m_seen2.insert(p);
             unsigned np = negate(p);
             unsigned_vector& tc = m_tc[p];
-            if (goal.contains(np)) {
+            if (goal.contains(np)) 
                 tc.push_back(np);
-            }
+            else 
-            else {
+                for (unsigned s : next(np))
-                unsigned_vector const& succ = next(np);
+                    tc.append(m_tc[s]);
-                for (unsigned j = 0; j < succ.size(); ++j) {
-                    tc.append(m_tc[succ[j]]);
-                }
-            }
         }
     }
 
-    
-
-
-
     unsigned_vector const& next(unsigned vertex) const { return m_next[vertex]; }
 
+    void init(unsigned_vector const& ps) {
+        unsigned max = 0;
+        for (unsigned p : ps) {
+            unsigned np = negate(p);
+            max = std::max(max, std::max(np, p) + 1);
+        }
+        m_next.reserve(max);
+        m_tc.reserve(m_next.size());
+    }
+    
 public:
     void add_edge(unsigned src, unsigned dst) {
         m_next.reserve(std::max(src, dst) + 1);
@@ -94,20 +93,11 @@ public:
     }
 
     void cliques(unsigned_vector const& ps, vector<unsigned_vector>& cliques) {     
-        unsigned max = 0;
+        init(ps);
-        unsigned num_ps = ps.size();
-        for (unsigned i = 0; i < num_ps; ++i) {
-            unsigned  p = ps[i];
-            unsigned np = negate(p);
-            max = std::max(max, std::max(np, p) + 1);
-        }
-        m_next.reserve(max);
-        m_tc.reserve(m_next.size());
         unsigned_vector clique;
         uint_set vars;
-        for (unsigned i = 0; i < num_ps; ++i) {
+        for (unsigned v : ps)
-            vars.insert(ps[i]);
+            vars.insert(v);
-        }
 
         while (!vars.empty()) {
             clique.reset();
@@ -118,9 +108,8 @@ public:
                 m_reachable[turn].remove(p);
                 vars.remove(p);
                 clique.push_back(p);
-                if (m_reachable[turn].empty()) {
+                if (m_reachable[turn].empty()) 
                     break;
-                }
                 m_reachable[!turn].reset();
                 get_reachable(p, m_reachable[turn], m_reachable[!turn]);
                 turn = !turn;
@@ -129,10 +118,75 @@ public:
                 if (clique.size() == 2 && clique[0] == negate(clique[1])) {
                     // no op
                 }
-                else {
+                else 
                     cliques.push_back(clique);
+            }
+        }        
+    }
+
+
+    // better quality cliques
+    void cliques2(unsigned_vector const& ps, vector<unsigned_vector>& cliques) {     
+
+        uint_set all_vars, todo;
+        u_map<uint_set> conns;
+
+        init(ps);
+
+        struct compare_degree {
+            u_map<uint_set>& conns;
+            compare_degree(u_map<uint_set>& conns): conns(conns) {}
+            bool operator()(unsigned x, unsigned y) const {
+                return conns[x].num_elems() < conns[y].num_elems();
+            }
+        };
+        compare_degree lt(conns);
+        heap<compare_degree> heap(m_next.size(), lt);
+
+        for (unsigned p : ps) {
+            all_vars.insert(p);
+            todo.insert(p);
+        }
+
+        for (unsigned v : ps) {
+            uint_set reach;
+            get_reachable(v, all_vars, reach);
+            conns.insert(v, reach);
+            heap.insert(v);
+        }
+
+        while (!todo.empty()) {
+            unsigned v = heap.min_value();                        
+            uint_set am1;
+            unsigned_vector next;
+            for (unsigned n : conns[v])
+                if (todo.contains(n))
+                    next.push_back(n);
+            std::sort(next.begin(), next.end(), [&](unsigned a, unsigned b) { return conns[a].num_elems() < conns[b].num_elems(); });
+            for (unsigned x : next) {
+                if (std::all_of(am1.begin(), am1.end(), [&](unsigned y) { return conns[x].contains(y); }))
+                    am1.insert(x);
+            }
+            am1.insert(v);
+            for (unsigned x : am1) {
+                todo.remove(x);
+                for (unsigned y : conns[x]) {
+                    conns[y].remove(x);
+                    heap.decreased(y);
                 }
             }
+            for (unsigned x : am1) 
+                heap.erase(x);
+                
+            if (am1.num_elems() > 1) {
+                unsigned_vector mux;
+                for (unsigned x : am1)
+                    mux.push_back(x);
+                if (mux.size() == 2 && mux[0] == negate(mux[1])) {
+                    continue;
+                }
+                cliques.push_back(mux);
+            }
         }
     }