add clausification features

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

src/api/python/z3/z3.py

@@ -1407,6 +1407,17 @@ def is_or(a):
     """
     return is_app_of(a, Z3_OP_OR)
 
+def is_implies(a):
+    """Return `True` if `a` is a Z3 implication expression.
+
+    >>> p, q = Bools('p q')
+    >>> is_implies(Implies(p, q))
+    True
+    >>> is_implies(And(p, q))
+    False
+    """
+    return is_app_of(a, Z3_OP_IMPLIES)
+
 def is_not(a):
     """Return `True` if `a` is a Z3 not expression.
 

src/opt/maxres.cpp

@@ -285,13 +285,13 @@ public:
             m_last_index = 0;
             bool first = index > 0;
             SASSERT(index < asms.size() || asms.empty());
-			IF_VERBOSE(1, verbose_stream() << "start hill climb " << index << " asms: " << asms.size() << "\n";);
+            IF_VERBOSE(10, verbose_stream() << "start hill climb " << index << " asms: " << asms.size() << "\n";);
             while (index < asms.size() && is_sat == l_true) {
                 while (!first && asms.size() > 20*(index - m_last_index) && index < asms.size()) {
                     index = next_index(asms, index);
                 }
-				IF_VERBOSE(1, verbose_stream() << "hill climb " << index << "\n";);
                 first = false;
+                IF_VERBOSE(3, verbose_stream() << "hill climb " << index << "\n";);
                 // IF_VERBOSE(3, verbose_stream() << "weight: " << get_weight(asms[0].get()) << " " << get_weight(asms[index-1].get()) << " num soft: " << index << "\n";);
                 m_last_index = index;
                 is_sat = check_sat(index, asms.c_ptr());

src/opt/maxsmt.cpp

@@ -353,12 +353,26 @@ namespace opt {
         m_upper += w;
     }
 
+    struct cmp_first {
+        bool operator()(std::pair<unsigned, rational> const& x, std::pair<unsigned, rational> const& y) const {
+            return x.first < y.first;
+        }
+    };
+
     void maxsmt::display_answer(std::ostream& out) const {
-        for (unsigned i = 0; i < m_soft_constraints.size(); ++i) {
-            expr* e = m_soft_constraints[i];
+        vector<std::pair<unsigned, rational>> sorted_weights;
+        unsigned n = m_weights.size();
+        for (unsigned i = 0; i < n; ++i) {
+            sorted_weights.push_back(std::make_pair(i, m_weights[i]));
+        }
+        std::sort(sorted_weights.begin(), sorted_weights.end(), cmp_first());
+        sorted_weights.reverse();
+        for (unsigned i = 0; i < n; ++i) {
+            unsigned idx = sorted_weights[i].first;
+            expr* e = m_soft_constraints[idx];
             bool is_not = m.is_not(e, e);
-            out << m_weights[i] << ": " << mk_pp(e, m)
-                << ((is_not != get_assignment(i))?" |-> true ":" |-> false ")
+            out << m_weights[idx] << ": " << mk_pp(e, m)
+                << ((is_not != get_assignment(idx))?" |-> true ":" |-> false ")
                 << "\n";
             
         }

src/opt/opt_cmds.cpp

@@ -166,7 +166,9 @@ public:
     }
 
     virtual void execute(cmd_context & ctx) {
-        get_opt(ctx, m_opt).display_assignment(ctx.regular_stream());        
+        if (!ctx.ignore_check()) {
+            get_opt(ctx, m_opt).display_assignment(ctx.regular_stream());        
+        }
     }
 };
 

src/sat/ba_solver.cpp

@@ -446,7 +446,7 @@ namespace sat {
     }
 
     /*
-      \brief slit PB constraint into two because root is reused in arguments.
+      \brief split PB constraint into two because root is reused in arguments.
     
       x <=> a*x + B*y >= k
      
@@ -825,6 +825,9 @@ namespace sat {
             p.set_k(k);
             SASSERT(p.well_formed());
             
+            if (clausify(p)) {
+                return;
+            }
             if (p.lit() == null_literal || value(p.lit()) == l_true) {
                 init_watch(p);
             }
@@ -1543,6 +1546,9 @@ namespace sat {
             s().mk_clause(_lits.size(), _lits.c_ptr(), learned);
             return 0;
         }
+        if (!learned && clausify(lit, lits.size(), lits.c_ptr(), k)) {
+            return 0;
+        }
         void * mem = m_allocator.allocate(card::get_obj_size(lits.size()));
         card* c = new (mem) card(next_id(), lit, lits, k);
         c->set_learned(learned);
@@ -2370,13 +2376,16 @@ namespace sat {
         SASSERT(s().at_base_lvl());
         switch (c.tag()) {
         case card_t:
-            simplify(c.to_card());
+            if (!clausify(c.to_card())) 
+                simplify(c.to_card());
             break;
         case pb_t:
-            simplify(c.to_pb());
+            if (!clausify(c.to_pb()))
+                simplify(c.to_pb());
             break;
         case xor_t:
-            simplify(c.to_xor());
+            if (!clausify(c.to_xor()))
+                simplify(c.to_xor());
             break;
         default:
             UNREACHABLE();
@@ -2480,8 +2489,9 @@ namespace sat {
     }
 
     void ba_solver::ba_sort::mk_clause(unsigned n, literal const* lits) {
-        literal_vector _lits(n, lits);
-        s.s().mk_clause(n, _lits.c_ptr());
+        m_lits.reset();
+        m_lits.append(n, lits);
+        s.s().mk_clause(n, m_lits.c_ptr());
     }
     
     // -------------------------------
@@ -2623,8 +2633,25 @@ namespace sat {
         }        
     }
 
+    bool ba_solver::clausify(literal lit, unsigned n, literal const* lits, unsigned k) {
+        bool is_def = lit != null_literal;
+        if ((!is_def || !s().was_eliminated(lit)) && 
+            !std::any_of(lits, lits + n, [&](literal l) { return s().was_eliminated(l); })) {
+            literal def_lit = m_sort.ge(is_def, k, n, lits);
+            if (is_def) {
+                s().mk_clause(~lit,  def_lit);
+                s().mk_clause( lit, ~def_lit);
+            }
+            return true;
+        }
+        return false;
+    }
+
+    bool ba_solver::clausify(xor& x) {
+        return false;
+    }
+
     bool ba_solver::clausify(card& c) {
-#if 0
         if (get_config().m_card_solver)
             return false;
 
@@ -2632,18 +2659,54 @@ namespace sat {
         // TBD: conditions for when to clausify are TBD and
         // handling of conditional cardinality as well.
         // 
-        if (c.lit() == null_literal) {
-            if (!c.learned() && !std::any_of(c.begin(), c.end(), [&](literal l) { return s().was_eliminated(l.var()); })) {
-                IF_VERBOSE(0, verbose_stream() << "clausify " << c << "\n";
-                m_sort.ge(false, c.k(), c.size(), c.begin());
-            }
-            remove_constraint(c, "recompiled to clauses");
+        if (!c.learned() && clausify(c.lit(), c.size(), c.begin(), c.k())) {
+            IF_VERBOSE(0, verbose_stream() << "clausify " << c << "\n";);                       
+            // compiled
+        }        
+        remove_constraint(c, "recompiled to clauses");
+        return true;        
+    }
+
+    bool ba_solver::clausify(pb& p) {
+        if (get_config().m_card_solver) 
+            return false;
+
+        bool ok = !p.learned();
+        bool is_def = p.lit() != null_literal;
+        for (wliteral wl : p) {
+            ok &= !s().was_eliminated(wl.second);
+        }
+        ok &= !is_def || !s().was_eliminated(p.lit());
+        if (!ok) {
+            remove_constraint(p, "recompiled to clauses");
+            return true;
+        }
+
+        if (is_cardinality(p, m_lemma)) {
+            literal lit = m_sort.ge(is_def, p.k(), m_lemma.size(), m_lemma.c_ptr());
+            if (is_def) {
+                s().mk_clause(p.lit(), ~lit);
+                s().mk_clause(~p.lit(), lit);
+            }
+            remove_constraint(p, "recompiled to clauses");
             return true;
         }
-#endif
         return false;
     }
 
+    bool ba_solver::is_cardinality(pb const& p, literal_vector& lits) {
+        lits.reset();
+        p.size();
+        for (wliteral wl : p) {
+            if (lits.size() > 2*p.size() + wl.first) {
+                return false;
+            }
+            for (unsigned i = 0; i < wl.first; ++i) {
+                lits.push_back(wl.second);
+            }
+        }
+        return true;
+    }
 
     void ba_solver::split_root(constraint& c) {
         switch (c.tag()) {

src/sat/ba_solver.h

@@ -234,6 +234,7 @@ namespace sat {
         struct ba_sort {
             ba_solver& s;
             literal m_true;
+            literal_vector m_lits;
 
             typedef sat::literal literal;
             typedef sat::literal_vector literal_vector;
@@ -343,6 +344,7 @@ namespace sat {
         void flush_roots(card& c);
         void recompile(card& c);
         bool clausify(card& c);
+        bool clausify(literal lit, unsigned n, literal const* lits, unsigned k);
         lbool eval(card const& c) const;
         double get_reward(card const& c, literal_occs_fun& occs) const;
 
@@ -355,6 +357,7 @@ namespace sat {
         void get_xor_antecedents(literal l, unsigned index, justification js, literal_vector& r);
         void get_antecedents(literal l, xor const& x, literal_vector & r);
         void simplify(xor& x);
+        bool clausify(xor& x);
         void flush_roots(xor& x);
         lbool eval(xor const& x) const;
         
@@ -371,6 +374,8 @@ namespace sat {
         bool is_cardinality(pb const& p);
         void flush_roots(pb& p);
         void recompile(pb& p);
+        bool clausify(pb& p);
+        bool is_cardinality(pb const& p, literal_vector& lits);
         lbool eval(pb const& p) const;
         double get_reward(pb const& p, literal_occs_fun& occs) const;
 

src/sat/sat_solver.h

@@ -270,6 +270,7 @@ namespace sat {
         void set_non_external(bool_var v);
         bool was_eliminated(bool_var v) const { return m_eliminated[v] != 0; }
         void set_eliminated(bool_var v, bool f) { m_eliminated[v] = f; }
+        bool was_eliminated(literal l) const { return was_eliminated(l.var()); }
         unsigned scope_lvl() const { return m_scope_lvl; }
         unsigned search_lvl() const { return m_search_lvl; }
         bool  at_search_lvl() const { return m_scope_lvl == m_search_lvl; }