mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
add 'distinct' to C++ API
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
d1376343c7
commit
4c95bb4dd9
|
@ -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;
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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
|
||||
|
|
Loading…
Reference in a new issue