Merge branch 'opt' of https://git01.codeplex.com/z3 into opt

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

@@ -652,6 +652,8 @@ namespace z3 {
             return expr(c.ctx(), r);
         }
 
+        friend expr distinct(expr_vector const& args);
+
         friend expr operator==(expr const & a, expr const & b) {
             check_context(a, b);
             Z3_ast r = Z3_mk_eq(a.ctx(), a, b);
@@ -1065,6 +1067,16 @@ namespace z3 {
         array<Z3_app> vars(xs);  
         Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, vars.size(), vars.ptr(), 0, 0, b); b.check_error(); return expr(b.ctx(), r);
     }
+
+
+    inline expr distinct(expr_vector const& args) {
+        assert(args.size() > 0);
+        context& ctx = args[0].ctx();
+        array<Z3_ast> _args(args);
+        Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr());
+        ctx.check_error();
+        return expr(ctx, r);
+    }
     
     class func_entry : public object {
         Z3_func_entry m_entry;
@@ -1467,6 +1479,56 @@ namespace z3 {
         }
     };
 
+    class optimize : public object {
+        Z3_optimize m_opt;
+    public:
+        class handle {
+            unsigned m_h;
+        public:
+            handle(unsigned h): m_h(h) {}
+            unsigned h() const { return m_h; }
+        };
+        optimize(context& c):object(c) { m_opt = Z3_mk_optimize(c); Z3_optimize_inc_ref(c, m_opt); }
+        ~optimize() { Z3_optimize_dec_ref(ctx(), m_opt); }
+        operator Z3_optimize() const { return m_opt; }
+        void add(expr const& e) {
+            assert(e.is_bool());
+            Z3_optimize_assert(ctx(), m_opt, e);
+        }
+        handle add(expr const& e, unsigned weight) {
+            assert(e.is_bool());
+            std::stringstream strm;
+            strm << weight; 
+            return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, strm.str().c_str(), 0)); 
+        }
+        handle add(expr const& e, char const* weight) {
+            assert(e.is_bool());
+            return handle(Z3_optimize_assert_soft(ctx(), m_opt, e, weight, 0)); 
+        }
+        handle maximzie(expr const& e) {
+            return handle(Z3_optimize_maximize(ctx(), m_opt, e));
+        }
+        handle minimize(expr const& e) {
+            return handle(Z3_optimize_minimize(ctx(), m_opt, e));
+        }
+        check_result check() { Z3_lbool r = Z3_optimize_check(ctx(), m_opt); check_error(); return to_check_result(r); }
+        model get_model() const { Z3_model m = Z3_optimize_get_model(ctx(), m_opt); check_error(); return model(ctx(), m); }
+        void set(params const & p) { Z3_optimize_set_params(ctx(), m_opt, p); check_error(); }
+        expr lower(handle const& h) {
+            Z3_ast r = Z3_optimize_get_lower(ctx(), m_opt, h.h());
+            check_error();
+            return expr(ctx(), r);
+        }
+        expr upper(handle const& h) {
+            Z3_ast r = Z3_optimize_get_upper(ctx(), m_opt, h.h());
+            check_error();
+            return expr(ctx(), r);
+        }
+        stats statistics() const { Z3_stats r = Z3_optimize_get_statistics(ctx(), m_opt); check_error(); return stats(ctx(), r); }        
+        friend std::ostream & operator<<(std::ostream & out, optimize const & s) { out << Z3_optimize_to_string(s.ctx(), s.m_opt); return out; }
+        std::string help() const { char const * r = Z3_optimize_get_help(ctx(), m_opt); check_error();  return r; }        
+    };
+
     inline tactic fail_if(probe const & p) {
         Z3_tactic r = Z3_tactic_fail_if(p.ctx(), p);
         p.check_error();

src/api/dotnet/Context.cs

@@ -916,6 +916,8 @@ namespace Microsoft.Z3
             CheckContextMatch(t);
             return new BoolExpr(this, Native.Z3_mk_or(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
         }
+
+
         #endregion
 
         #region Arithmetic

src/api/dotnet/Expr.cs

@@ -320,6 +320,7 @@ namespace Microsoft.Z3
         /// Indicates whether the term is an implication
         /// </summary>
         public bool IsImplies { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IMPLIES; } }
+
         #endregion
 
         #region Arithmetic Terms

src/duality/duality.h

@@ -29,7 +29,7 @@ using namespace stl_ext;
 
 namespace Duality {
 
-  class implicant_solver;
+  struct implicant_solver;
 
   /* Generic operations on Z3 formulas */
 

src/duality/duality_solver.cpp

@@ -2201,7 +2201,7 @@ namespace Duality {
 #endif
 	    int expand_max = 1;
 	    if(0&&duality->BatchExpand){
-	      int thing = stack.size() * 0.1;
+                int thing = stack.size() /10; 
 	      expand_max = std::max(1,thing);
 	      if(expand_max > 1)
 		std::cout << "foo!\n";

src/interp/iz3hash.h

@@ -52,7 +52,7 @@ namespace hash_space {
     class hash<std::string> {
   public:
     size_t operator()(const std::string &s) const {
-      return string_hash(s.c_str(), s.size(), 0);
+        return string_hash(s.c_str(), static_cast<unsigned>(s.size()), 0);
     }
   };
 
@@ -107,7 +107,7 @@ namespace hash_space {
       4294967291ul
     };
 
-  inline unsigned long next_prime(unsigned long n) {
+  inline size_t next_prime(size_t n) {
     const unsigned long* to = primes + (int)num_primes;
     for(const unsigned long* p = primes; p < to; p++)
       if(*p >= n) return *p;
@@ -374,7 +374,7 @@ namespace hash_space {
     void resize(size_t new_size) {
       const size_t old_n = buckets.size();
       if (new_size <= old_n) return;
-      const size_t n = next_prime(new_size);
+      const size_t n = next_prime(static_cast<unsigned>(new_size));
       if (n <= old_n) return;
       Table tmp(n, (Entry*)(0));
       for (size_t i = 0; i < old_n; ++i) {

src/opt/weighted_maxsat.cpp

@@ -59,6 +59,7 @@ namespace smt {
         rational                 m_rmin_cost;   // current maximal cost assignment.
         scoped_mpz               m_zcost;       // current sum of asserted costs
         scoped_mpz               m_zmin_cost;   // current maximal cost assignment.
+        bool                     m_found_optimal; 
         u_map<theory_var>        m_bool2var;    // bool_var -> theory_var
         svector<bool_var>        m_var2bool;    // theory_var -> bool_var
         bool                     m_propagate;  
@@ -79,6 +80,7 @@ namespace smt {
             m_old_values(m_mpz),
             m_zcost(m_mpz),
             m_zmin_cost(m_mpz),
+            m_found_optimal(false),
             m_propagate(false),
             m_normalize(false)
         {}
@@ -93,14 +95,21 @@ namespace smt {
         void get_assignment(svector<bool>& result) {
             result.reset();
 
-            std::sort(m_cost_save.begin(), m_cost_save.end());
+            if (!m_found_optimal) {
-            for (unsigned i = 0, j = 0; i < m_vars.size(); ++i) {
+                for (unsigned i = 0; i < m_vars.size(); ++i) {
-                if (j < m_cost_save.size() && m_cost_save[j] == i) {
                     result.push_back(false);
-                    ++j;
                 }
-                else {
+            }
-                    result.push_back(true);
+            else {
+                std::sort(m_cost_save.begin(), m_cost_save.end());
+                for (unsigned i = 0, j = 0; i < m_vars.size(); ++i) {
+                    if (j < m_cost_save.size() && m_cost_save[j] == i) {
+                        result.push_back(false);
+                        ++j;
+                    }
+                    else {
+                        result.push_back(true);
+                    }
                 }
             }
             TRACE("opt",
@@ -189,10 +198,6 @@ namespace smt {
             return m_min_cost_atom;
         }
 
-        bool found_solution() const {
-            return !m_cost_save.empty();
-        }
-
         // scoped_mpz leaks.
 
         class numeral_trail : public trail<context> {
@@ -273,6 +278,7 @@ namespace smt {
             m_min_cost_atom = 0;
             m_min_cost_atoms.reset();
             m_propagate = false;
+            m_found_optimal = false;
             m_assigned.reset();
         }
 
@@ -303,7 +309,7 @@ namespace smt {
         }       
 
         bool is_optimal() const {
-            return m_mpz.lt(m_zcost, m_zmin_cost);
+            return !m_found_optimal || m_zcost < m_zmin_cost;
         }
 
         expr_ref mk_block() {
@@ -329,22 +335,22 @@ namespace smt {
                 rational rw = rational(q);
                 IF_VERBOSE(1, verbose_stream() << "(wmaxsat with upper bound: " << rw << ")\n";);
                 m_zmin_cost = weight;
+                m_found_optimal = true;
                 m_cost_save.reset();
                 m_cost_save.append(m_costs);
-            }
+                TRACE("opt",
-
-            expr_ref result(m.mk_or(disj.size(), disj.c_ptr()), m);
-
-            TRACE("opt",
-                  tout << result << "\n";
-                  if (is_optimal()) {
                       tout << "costs: ";
                       for (unsigned i = 0; i < m_costs.size(); ++i) {
                           tout << mk_pp(get_enode(m_costs[i])->get_owner(), get_manager()) << " ";
                       }
                       tout << "\n";
                       get_context().display(tout);                      
-                  });
+                      );
+            }
+            expr_ref result(m.mk_or(disj.size(), disj.c_ptr()), m);
+            TRACE("opt",
+                  tout << result << " weight: " << weight << "\n";
+                  tout << "cost: " << m_zcost << " min-cost: " << m_zmin_cost << "\n";);
             return result;
         }