diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 08a931fdc..fd2776079 100644 --- a/src/api/api_ast.cpp +++ b/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; } } diff --git a/src/api/api_pb.cpp b/src/api/api_pb.cpp index b7c28c34f..ee504146f 100644 --- a/src/api/api_pb.cpp +++ b/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 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) { diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index f12ad58ea..f5c4dc99d 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -2692,6 +2692,18 @@ namespace Microsoft.Z3 AST.ArrayToNative(args), k)); } + /// + /// Create an at-least-k constraint. + /// + public BoolExpr MkAtLeast(BoolExpr[] args, uint k) + { + Contract.Requires(args != null); + Contract.Requires(Contract.Result() != null); + CheckContextMatch(args); + return new BoolExpr(this, Native.Z3_mk_atleast(nCtx, (uint) args.Length, + AST.ArrayToNative(args), k)); + } + /// /// Create a pseudo-Boolean less-or-equal constraint. /// @@ -2707,6 +2719,20 @@ namespace Microsoft.Z3 coeffs, k)); } + /// + /// Create a pseudo-Boolean greater-or-equal constraint. + /// + 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() != null); + CheckContextMatch(args); + return new BoolExpr(this, Native.Z3_mk_pbge(nCtx, (uint) args.Length, + AST.ArrayToNative(args), + coeffs, k)); + } /// /// Create a pseudo-Boolean equal constraint. /// diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 22b2f60e6..01dacace7 100644 --- a/src/api/python/z3/z3.py +++ b/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 = len(args1) - args[-1] + k = 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) - 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] + ctx, sz, _args, _coeffs = _pb_args_coeffs(args) 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) - 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] + ctx, sz, _args, _coeffs = _pb_args_coeffs(args) return BoolRef(Z3_mk_pbeq(ctx.ref(), sz, _args, _coeffs, k), ctx) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index b80ce3177..fcf22961c 100644 --- a/src/api/z3_api.h +++ b/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. diff --git a/src/smt/smt_bool_var_data.h b/src/smt/smt_bool_var_data.h index e65036d9c..af0b7f9d2 100644 --- a/src/smt/smt_bool_var_data.h +++ b/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; } diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp index 4568abb55..7dd9144fe 100644 --- a/src/smt/smt_conflict_resolution.cpp +++ b/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; - if (not_l != null_literal) - consequent = ~not_l; - visit_b_justification(consequent, conflict); - if (not_l != null_literal) + literal consequent; + if (not_l == null_literal) { + consequent = false_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; diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index e6d4d0c07..476a419eb 100644 --- a/src/smt/smt_context.cpp +++ b/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); diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index c63d0614d..0d758196e 100644 --- a/src/smt/smt_context.h +++ b/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& cores, unsigned& min_core_size); diff --git a/src/smt/smt_context_inv.cpp b/src/smt/smt_context_inv.cpp index 5e3b091bc..7d009a037 100644 --- a/src/smt/smt_context_inv.cpp +++ b/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; diff --git a/src/smt/smt_literal.cpp b/src/smt/smt_literal.cpp index d510027f0..e6e795ed4 100644 --- a/src/smt/smt_literal.cpp +++ b/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