add at-least and pbge to API, fix for issue #864

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

src/api/api_ast.cpp

@@ -1211,7 +1211,9 @@ extern "C" {
             switch(_d->get_decl_kind()) {
             case OP_PB_LE: return Z3_OP_PB_LE;
             case OP_PB_GE: return Z3_OP_PB_GE;
+            case OP_PB_EQ: return Z3_OP_PB_EQ;
             case OP_AT_MOST_K: return Z3_OP_PB_AT_MOST;
+            case OP_AT_LEAST_K: return Z3_OP_PB_AT_LEAST;
             default: return Z3_OP_INTERNAL;
             }
         }

src/api/api_pb.cpp

@@ -39,6 +39,20 @@ extern "C" {
     }
 
 
+    Z3_ast Z3_API Z3_mk_atleast(Z3_context c, unsigned num_args, 
+                               Z3_ast const args[], unsigned k) {
+        Z3_TRY;
+        LOG_Z3_mk_atmost(c, num_args, args, k);
+        RESET_ERROR_CODE();
+        parameter param(k);
+        pb_util util(mk_c(c)->m());
+        ast* a = util.mk_at_least_k(num_args, to_exprs(args), k);
+        mk_c(c)->save_ast_trail(a);
+        check_sorts(c, a);
+        RETURN_Z3(of_ast(a));
+        Z3_CATCH_RETURN(0);
+    }
+
     Z3_ast Z3_API Z3_mk_pble(Z3_context c, unsigned num_args, 
                              Z3_ast const args[], int _coeffs[],
                              int k) {
@@ -57,6 +71,24 @@ extern "C" {
         Z3_CATCH_RETURN(0);
     }
 
+    Z3_ast Z3_API Z3_mk_pbge(Z3_context c, unsigned num_args, 
+                             Z3_ast const args[], int _coeffs[],
+                             int k) {
+        Z3_TRY;
+        LOG_Z3_mk_pble(c, num_args, args, _coeffs, k);
+        RESET_ERROR_CODE();
+        pb_util util(mk_c(c)->m());
+        vector<rational> coeffs;
+        for (unsigned i = 0; i < num_args; ++i) {
+            coeffs.push_back(rational(_coeffs[i]));
+        }
+        ast* a = util.mk_ge(num_args, coeffs.c_ptr(), to_exprs(args), rational(k));
+        mk_c(c)->save_ast_trail(a);
+        check_sorts(c, a);
+        RETURN_Z3(of_ast(a));
+        Z3_CATCH_RETURN(0);
+    }
+
     Z3_ast Z3_API Z3_mk_pbeq(Z3_context c, unsigned num_args, 
                              Z3_ast const args[], int _coeffs[],
                              int k) {

src/api/dotnet/Context.cs

@@ -2692,6 +2692,18 @@ namespace Microsoft.Z3
                                                           AST.ArrayToNative(args), k));
         }
 
+        /// <summary>
+        /// Create an at-least-k constraint.
+        /// </summary>
+        public BoolExpr MkAtLeast(BoolExpr[] args, uint k)
+        {
+           Contract.Requires(args != null);
+           Contract.Requires(Contract.Result<BoolExpr[]>() != null);
+           CheckContextMatch<BoolExpr>(args);
+           return new BoolExpr(this, Native.Z3_mk_atleast(nCtx, (uint) args.Length,
+                                                          AST.ArrayToNative(args), k));
+        }
+
         /// <summary>
         /// Create a pseudo-Boolean less-or-equal constraint.
         /// </summary>
@@ -2707,6 +2719,20 @@ namespace Microsoft.Z3
                                                           coeffs, k));
         }
 
+        /// <summary>
+        /// Create a pseudo-Boolean greater-or-equal constraint.
+        /// </summary>
+        public BoolExpr MkPBGe(int[] coeffs, BoolExpr[] args, int k)
+        {
+           Contract.Requires(args != null);
+           Contract.Requires(coeffs != null);
+           Contract.Requires(args.Length == coeffs.Length);
+           Contract.Requires(Contract.Result<BoolExpr[]>() != null);
+           CheckContextMatch<BoolExpr>(args);
+           return new BoolExpr(this, Native.Z3_mk_pbge(nCtx, (uint) args.Length,
+                                                          AST.ArrayToNative(args),
+                                                          coeffs, k));
+        }
         /// <summary>
         /// Create a pseudo-Boolean equal constraint.
         /// </summary>

src/api/python/z3/z3.py

@@ -7617,11 +7617,6 @@ def AtLeast(*args):
     >>> a, b, c = Bools('a b c')
     >>> f = AtLeast(a, b, c, 2)
     """
-    def mk_not(a):
-        if is_not(a):
-            return a.arg(0)
-        else:
-            return Not(a)
     args  = _get_args(args)
     if __debug__:
         _z3_assert(len(args) > 1, "Non empty list of arguments expected")
@@ -7629,10 +7624,25 @@ def AtLeast(*args):
     if __debug__:
         _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression")
     args1 = _coerce_expr_list(args[:-1], ctx)
-    args1 = [ mk_not(a) for a in args1 ]
+    k = args[-1]
-    k = len(args1) - args[-1] 
     _args, sz = _to_ast_array(args1)
-    return BoolRef(Z3_mk_atmost(ctx.ref(), sz, _args, k), ctx)
+    return BoolRef(Z3_mk_atleast(ctx.ref(), sz, _args, k), ctx)
+
+
+def _pb_args_coeffs(args):
+    args  = _get_args(args)
+    args, coeffs = zip(*args)
+    if __debug__:
+        _z3_assert(len(args) > 0, "Non empty list of arguments expected")
+    ctx   = _ctx_from_ast_arg_list(args)
+    if __debug__:
+        _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression")
+    args = _coerce_expr_list(args, ctx)
+    _args, sz = _to_ast_array(args)
+    _coeffs = (ctypes.c_int * len(coeffs))()
+    for i in range(len(coeffs)):
+        _coeffs[i] = coeffs[i]
+    return ctx, sz, _args, _coeffs
 
 def PbLe(args, k):
     """Create a Pseudo-Boolean inequality k constraint.
@@ -7640,38 +7650,25 @@ def PbLe(args, k):
     >>> a, b, c = Bools('a b c')
     >>> f = PbLe(((a,1),(b,3),(c,2)), 3)
     """
-    args  = _get_args(args)
+    ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
-    args, coeffs = zip(*args)
-    if __debug__:
-        _z3_assert(len(args) > 0, "Non empty list of arguments expected")
-    ctx   = _ctx_from_ast_arg_list(args)
-    if __debug__:
-        _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression")
-    args = _coerce_expr_list(args, ctx)
-    _args, sz = _to_ast_array(args)
-    _coeffs = (ctypes.c_int * len(coeffs))()
-    for i in range(len(coeffs)):
-        _coeffs[i] = coeffs[i]
     return BoolRef(Z3_mk_pble(ctx.ref(), sz, _args, _coeffs, k), ctx)
 
+def PbGe(args, k):
+    """Create a Pseudo-Boolean inequality k constraint.
+
+    >>> a, b, c = Bools('a b c')
+    >>> f = PbGe(((a,1),(b,3),(c,2)), 3)
+    """
+    ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
+    return BoolRef(Z3_mk_pbge(ctx.ref(), sz, _args, _coeffs, k), ctx)
+
 def PbEq(args, k):
     """Create a Pseudo-Boolean inequality k constraint.
 
     >>> a, b, c = Bools('a b c')
     >>> f = PbEq(((a,1),(b,3),(c,2)), 3)
     """
-    args  = _get_args(args)
+    ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
-    args, coeffs = zip(*args)
-    if __debug__:
-        _z3_assert(len(args) > 0, "Non empty list of arguments expected")
-    ctx   = _ctx_from_ast_arg_list(args)
-    if __debug__:
-        _z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression")
-    args = _coerce_expr_list(args, ctx)
-    _args, sz = _to_ast_array(args)
-    _coeffs = (ctypes.c_int * len(coeffs))()
-    for i in range(len(coeffs)):
-        _coeffs[i] = coeffs[i]
     return BoolRef(Z3_mk_pbeq(ctx.ref(), sz, _args, _coeffs, k), ctx)
 
 

src/api/z3_api.h

@@ -855,6 +855,9 @@ typedef enum
       - Z3_OP_PB_AT_MOST: Cardinality constraint.
               E.g., x + y + z <= 2
 
+      - Z3_OP_PB_AT_LEAST: Cardinality constraint.
+              E.g., x + y + z >= 2
+
       - Z3_OP_PB_LE: Generalized Pseudo-Boolean cardinality constraint.
               Example  2*x + 3*y <= 4
 
@@ -1174,6 +1177,7 @@ typedef enum {
 
     // Pseudo Booleans
     Z3_OP_PB_AT_MOST=0x900,
+    Z3_OP_PB_AT_LEAST,
     Z3_OP_PB_LE,
     Z3_OP_PB_GE,
     Z3_OP_PB_EQ,
@@ -3966,6 +3970,17 @@ extern "C" {
     Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args,
                                Z3_ast const args[], unsigned k);
 
+
+    /**
+       \brief Pseudo-Boolean relations.
+
+       Encode p1 + p2 + ... + pn >= k
+
+       def_API('Z3_mk_atleast', AST, (_in(CONTEXT), _in(UINT), _in_array(1,AST), _in(UINT)))
+    */
+
+    Z3_ast Z3_mk_atleast(Z3_context c, unsigned num_args,
+                                Z3_ast const args[], unsigned k);
     /**
        \brief Pseudo-Boolean relations.
 
@@ -3978,6 +3993,19 @@ extern "C" {
                              Z3_ast const args[], int coeffs[],
                              int k);
 
+
+    /**
+       \brief Pseudo-Boolean relations.
+
+       Encode k1*p1 + k2*p2 + ... + kn*pn >= k
+
+       def_API('Z3_mk_pbge', AST, (_in(CONTEXT), _in(UINT), _in_array(1,AST), _in_array(1,INT), _in(INT)))
+    */
+
+    Z3_ast Z3_mk_pbge(Z3_context c, unsigned num_args,
+                             Z3_ast const args[], int coeffs[],
+                             int k);
+
     /**
        \brief Pseudo-Boolean relations.
 

src/smt/smt_bool_var_data.h

@@ -24,7 +24,9 @@ Revision History:
 namespace smt {
 
     struct bool_var_data {
+    private:
         b_justification         m_justification;
+    public:
         unsigned                m_scope_lvl:24;    //!< scope level of when the variable was assigned.
         unsigned                m_mark:1;
         unsigned                m_assumption:1;
@@ -45,6 +47,14 @@ namespace smt {
     public:
         
         unsigned get_intern_level() const { return m_iscope_lvl; }
+
+        b_justification justification() const { return m_justification; }
+
+        void set_axiom() { m_justification = b_justification::mk_axiom(); }
+
+        void set_null_justification() { m_justification = null_b_justification; }
+
+        void set_justification(b_justification const& j) { m_justification = j; }
         
         bool is_atom() const { return m_atom; }
 

src/smt/smt_conflict_resolution.cpp

@@ -496,13 +496,15 @@ namespace smt {
 
         unsigned idx = skip_literals_above_conflict_level();
 
+        TRACE("conflict", m_ctx.display_literal_verbose(tout, not_l); m_ctx.display(tout << " ", conflict););
+
         // save space for first uip
         m_lemma.push_back(null_literal);
         m_lemma_atoms.push_back(0);
 
         unsigned num_marks = 0;
         if (not_l != null_literal) {
-            TRACE("conflict", tout << "not_l: "; m_ctx.display_literal(tout, not_l); tout << "\n";);
+            TRACE("conflict", tout << "not_l: "; m_ctx.display_literal_verbose(tout, not_l); tout << "\n";);
             process_antecedent(not_l, num_marks);
         }
 
@@ -514,7 +516,7 @@ namespace smt {
                 get_manager().trace_stream() << "\n";
             }
 
-            TRACE("conflict", tout << "processing consequent: "; m_ctx.display_literal(tout, consequent); tout << "\n";
+            TRACE("conflict", tout << "processing consequent: "; m_ctx.display_literal_verbose(tout, consequent); tout << "\n";
                   tout << "num_marks: " << num_marks << ", js kind: " << js.get_kind() << "\n";);
             SASSERT(js != null_b_justification);
             switch (js.get_kind()) {
@@ -1076,6 +1078,7 @@ namespace smt {
             return true;
         SASSERT(js.get_kind() != b_justification::BIN_CLAUSE);
         CTRACE("visit_b_justification_bug", js.get_kind() == b_justification::AXIOM, tout << "l: " << l << "\n"; m_ctx.display(tout););
+
         if (js.get_kind() == b_justification::AXIOM) 
             return true;
         SASSERT(js.get_kind() != b_justification::AXIOM);
@@ -1089,14 +1092,17 @@ namespace smt {
                     i = 1;
                 }
                 else {
+                    SASSERT(cls->get_literal(1) == l);
                     if (get_proof(~cls->get_literal(0)) == 0)
                         visited = false;
                     i = 2;
                 }
             }
-            for (; i < num_lits; i++)
+            for (; i < num_lits; i++) {
+                SASSERT(cls->get_literal(i) != l);
                 if (get_proof(~cls->get_literal(i)) == 0)
                     visited = false;
+            }
             return visited;
         }
         else
@@ -1251,14 +1257,19 @@ namespace smt {
               }
               tout << "\n";);
         init_mk_proof();
-        literal consequent  = false_literal;
+        literal consequent;
-        if (not_l != null_literal)
+        if (not_l == null_literal) {
-            consequent      = ~not_l;
+            consequent = false_literal;
-        visit_b_justification(consequent, conflict);
+        }
-        if (not_l != null_literal)
+        else {
+            consequent = ~not_l;
             m_todo_pr.push_back(tp_elem(not_l));
+        }
+        visit_b_justification(consequent, conflict);
+        
         while (!m_todo_pr.empty()) {
             tp_elem & elem = m_todo_pr.back();
+
             switch (elem.m_kind) {
             case tp_elem::EQUALITY: {
                 enode * lhs        = elem.m_lhs;

src/smt/smt_context.cpp

@@ -261,10 +261,11 @@ namespace smt {
         m_assignment[false_literal.index()]    = l_false;
         if (m_manager.proofs_enabled()) {
             proof * pr = m_manager.mk_true_proof();
-            m_bdata[true_bool_var].m_justification = b_justification(mk_justification(justification_proof_wrapper(*this, pr)));
+
+            set_justification(true_bool_var, m_bdata[true_bool_var], b_justification(mk_justification(justification_proof_wrapper(*this, pr))));
         }
         else {
-            m_bdata[true_bool_var].m_justification = b_justification::mk_axiom();
+            m_bdata[true_bool_var].set_axiom();
         }
         m_true_enode  = mk_enode(t, true, true, false);
         // internalizer is marking enodes as interpreted whenever the associated ast is a value and a constant.
@@ -292,6 +293,12 @@ namespace smt {
             std::swap(lhs, rhs);
         return m_manager.mk_eq(lhs, rhs);
     }
+
+    void context::set_justification(bool_var v, bool_var_data& d, b_justification const& j) {
+        SASSERT(validate_justification(v, d, j));
+        d.set_justification(j);
+    }
+
     
     void context::assign_core(literal l, b_justification j, bool decision) {
         TRACE("assign_core", tout << (decision?"decision: ":"propagating: ") << l << " ";              
@@ -302,7 +309,7 @@ namespace smt {
         m_assignment[l.index()]    = l_true;
         m_assignment[(~l).index()] = l_false;
         bool_var_data & d          = get_bdata(l.var());
-        d.m_justification          = j;
+        set_justification(l.var(), d, j);
         d.m_scope_lvl              = m_scope_lvl;
         if (m_fparams.m_restart_adaptive && d.m_phase_available) {
             m_agility             *= m_fparams.m_agility_factor;
@@ -1406,7 +1413,8 @@ namespace smt {
                 else {
                     TRACE("add_diseq", display_eq_detail(tout, bool_var2enode(v)););
                     if (!add_diseq(get_enode(lhs), get_enode(rhs)) && !inconsistent()) {
-                        set_conflict(b_justification(mk_justification(eq_propagation_justification(get_enode(lhs), get_enode(rhs)))), ~l);                        
+                        literal not_eq = literal(l.var(), true);
+                        set_conflict(b_justification(mk_justification(eq_propagation_justification(get_enode(lhs), get_enode(rhs)))), not_eq);                        
                     }
                 }
             }
@@ -2042,7 +2050,7 @@ namespace smt {
             m_assignment[(~l).index()] = l_undef;
             bool_var v                 = l.var();
             bool_var_data & d          = get_bdata(v);
-            d.m_justification          = null_b_justification;
+            d.set_null_justification();
             m_case_split_queue->unassign_var_eh(v);
         }
         
@@ -2593,10 +2601,10 @@ namespace smt {
                                 cls->set_justification(0);
                                 m_justifications.push_back(js);
                             }
-                            m_bdata[v0].m_justification = b_justification(js);
+                            set_justification(v0, m_bdata[v0], b_justification(js));
                         }
                         else
-                            m_bdata[v0].m_justification = b_justification::mk_axiom();
+                            m_bdata[v0].set_axiom();
                     }
                 }
                 del_clause(cls);

src/smt/smt_context.h

@@ -363,9 +363,11 @@ namespace smt {
         void get_assignments(expr_ref_vector& assignments);
 
         b_justification get_justification(bool_var v) const {
-            return get_bdata(v).m_justification;
+            return get_bdata(v).justification();
         }
 
+        void set_justification(bool_var v, bool_var_data& d, b_justification const& j);
+
         bool has_th_justification(bool_var v, theory_id th_id) const {
             b_justification js = get_justification(v);
             return js.get_kind() == b_justification::JUSTIFICATION && js.get_justification()->get_from_theory() == th_id;
@@ -1381,6 +1383,8 @@ namespace smt {
         void validate_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, 
                                    expr_ref_vector const& conseq, expr_ref_vector const& unfixed);
 
+        bool validate_justification(bool_var v, bool_var_data const& d, b_justification const& j);
+
         void justify(literal lit, index_set& s);
 
         void extract_cores(expr_ref_vector const& asms, vector<expr_ref_vector>& cores, unsigned& min_core_size);

src/smt/smt_context_inv.cpp

@@ -402,6 +402,20 @@ namespace smt {
 
 #endif
 
+    bool context::validate_justification(bool_var v, bool_var_data const& d, b_justification const& j) {
+        if (j.get_kind() == b_justification::CLAUSE && v != true_bool_var) {
+            clause* cls = j.get_clause();
+            unsigned num_lits = cls->get_num_literals();
+            literal l = cls->get_literal(0);
+            if (l.var() != v) {
+                l = cls->get_literal(1);
+            }
+            SASSERT(l.var() == v);
+            SASSERT(m_assignment[l.index()] == l_true);
+        }
+        return true;
+    }
+
     bool context::validate_model() {
         if (!m_proto_model) {
             return true;

src/smt/smt_literal.cpp

@@ -27,6 +27,8 @@ namespace smt {
             out << "true";
         else if (*this == false_literal)
             out << "false";
+        else if (*this == null_literal)
+            out << "null";
         else if (sign())
             out << "(not " << mk_pp(bool_var2expr_map[var()], m) << ")";
         else