Add C++ functions for set operations per stackoverflow post, set relevancy = 2 for quantified maxsmt per example from Aaron Gember, fix conversion of default weights based on bug report from Patrick Trentin on maxsat. Annotating soft constraints with weight=0 caused the weight to be adjusted to 1 and therefore produce wrong results

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

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

@@ -2331,11 +2331,68 @@ namespace z3 {
     inline expr store(expr const & a, int i, int v) {
         return store(a, a.ctx().num_val(i, a.get_sort().array_domain()), a.ctx().num_val(v, a.get_sort().array_range()));
     }
+
+#define MK_EXPR1(_fn, _arg)                     \
+    Z3_ast r = _fn(_arg.ctx(), _arg);           \
+    _arg.check_error();                         \
+    return expr(_arg.ctx(), r);
+
+#define MK_EXPR2(_fn, _arg1, _arg2)             \
+    check_context(_arg1, _arg2);                \
+    Z3_ast r = _fn(_arg1.ctx(), _arg1, _arg2);  \
+    _arg1.check_error();                        \
+    return expr(_arg1.ctx(), r);
+
     inline expr const_array(sort const & d, expr const & v) {
-        check_context(d, v);
-        Z3_ast r = Z3_mk_const_array(d.ctx(), d, v);
-        d.check_error();
-        return expr(d.ctx(), r);
+        MK_EXPR2(Z3_mk_const_array, d, v);
+    }
+
+    inline expr empty_set(sort const& s) {
+        MK_EXPR1(Z3_mk_empty_set, s);
+    }
+
+    inline expr full_set(sort const& s) {
+        MK_EXPR1(Z3_mk_full_set, s);
+    }
+
+    inline expr set_add(expr const& s, expr const& e) {
+        MK_EXPR2(Z3_mk_set_add, s, e);
+    }
+
+    inline expr set_del(expr const& s, expr const& e) {
+        MK_EXPR2(Z3_mk_set_del, s, e);
+    }    
+
+    inline expr set_union(expr const& a, expr const& b) {
+        check_context(a, b); 
+        Z3_ast es[2] = { a, b };
+        Z3_ast r = Z3_mk_set_union(a.ctx(), 2, es);
+        a.check_error();                    
+        return expr(a.ctx(), r);
+    }
+
+    inline expr set_intersect(expr const& a, expr const& b) {
+        check_context(a, b); 
+        Z3_ast es[2] = { a, b };
+        Z3_ast r = Z3_mk_set_intersect(a.ctx(), 2, es);
+        a.check_error();                    
+        return expr(a.ctx(), r);
+    }
+
+    inline expr set_difference(expr const& a, expr const& b) {
+        MK_EXPR2(Z3_mk_set_difference, a, b);
+    }
+
+    inline expr set_complement(expr const& a) {
+        MK_EXPR1(Z3_mk_set_complement, a);
+    }
+
+    inline expr set_member(expr const& s, expr const& e) {
+        MK_EXPR2(Z3_mk_set_member, s, e);
+    }
+
+    inline expr set_subset(expr const& a, expr const& b) {
+        MK_EXPR2(Z3_mk_set_subset, a, b);
     }
 
     // sequence and regular expression operations.

src/opt/opt_cmds.cpp

@@ -97,10 +97,7 @@ public:
 
     virtual void execute(cmd_context & ctx) {
         symbol w("weight");
-        rational weight = ps().get_rat(symbol("weight"), rational(0));
-        if (weight.is_zero()) {
-            weight = rational::one();
-        }
+        rational weight = ps().get_rat(symbol("weight"), rational::one());
         symbol id = ps().get_sym(symbol("id"), symbol::null);        
         get_opt(ctx, m_opt).add_soft_constraint(m_formula, weight, id);
         reset(ctx);

src/opt/opt_context.cpp

@@ -91,10 +91,7 @@ namespace opt {
 
     unsigned context::scoped_state::add(expr* f, rational const& w, symbol const& id) {
         if (w.is_neg()) {
-            throw default_exception("Negative weight supplied. Weight should be positive");
-        }
-        if (w.is_zero()) {
-            throw default_exception("Zero weight supplied. Weight should be positive");
+            throw default_exception("Negative weight supplied. Weight should be non-negative");
         }
         if (!m.is_bool(f)) {
             throw default_exception("Soft constraint should be Boolean");
@@ -105,9 +102,11 @@ namespace opt {
         }
         SASSERT(m_indices.contains(id));        
         unsigned idx = m_indices[id];
-        m_objectives[idx].m_terms.push_back(f);
-        m_objectives[idx].m_weights.push_back(w);
-        m_objectives_term_trail.push_back(idx);
+        if (w.is_pos()) {
+            m_objectives[idx].m_terms.push_back(f);
+            m_objectives[idx].m_weights.push_back(w);
+            m_objectives_term_trail.push_back(idx);
+        }
         return idx;
     }
 
@@ -852,9 +851,7 @@ namespace opt {
         func_decl* f = m.mk_fresh_func_decl(name,"", domain.size(), domain.c_ptr(), m.mk_bool_sort());
         m_objective_fns.insert(f, index);
         m_objective_refs.push_back(f);
-        if (sz > 0) {
-            m_objective_orig.insert(f, args[0]);
-        }
+        m_objective_orig.insert(f, sz > 0 ? args[0] : 0);        
         return m.mk_app(f, sz, args);
     }
 
@@ -873,10 +870,7 @@ namespace opt {
     }
 
     void context::from_fmls(expr_ref_vector const& fmls) {
-        TRACE("opt",
-              for (unsigned i = 0; i < fmls.size(); ++i) {
-                  tout << mk_pp(fmls[i], m) << "\n";
-              });
+        TRACE("opt", tout << fmls << "\n";);
         m_hard_constraints.reset();
         expr_ref orig_term(m);
         for (unsigned i = 0; i < fmls.size(); ++i) {
@@ -1054,10 +1048,7 @@ namespace opt {
                 break;
             }
         }
-        TRACE("opt",
-              for (unsigned i = 0; i < fmls.size(); ++i) {
-                  tout << mk_pp(fmls[i].get(), m) << "\n";
-              });
+        TRACE("opt", tout << fmls << "\n";);
     }
 
     void context::internalize() {

src/opt/opt_solver.cpp

@@ -78,6 +78,9 @@ namespace opt {
     }
     
     void opt_solver::assert_expr(expr * t) {
+        if (has_quantifiers(t)) {
+            m_params.m_relevancy_lvl = 2;
+        }
         m_context.assert_expr(t);
     }