21 using System.Diagnostics.Contracts;
28 [ContractVerification(
true)]
38 Contract.Ensures(Contract.Result<
Expr>() != null);
53 Contract.Ensures(Contract.Result<
FuncDecl>() != null);
82 Contract.Ensures(Contract.Result<
Expr[]>() != null);
86 for (uint i = 0; i < n; i++)
98 Contract.Requires(args != null);
99 Contract.Requires(Contract.ForAll(args, a => a != null));
101 Context.CheckContextMatch(args);
102 if (IsApp && args.Length != NumArgs)
103 throw new Z3Exception(
"Number of arguments does not match");
117 Contract.Requires(from != null);
118 Contract.Requires(to != null);
119 Contract.Requires(Contract.ForAll(from, f => f != null));
120 Contract.Requires(Contract.ForAll(to, t => t != null));
121 Contract.Ensures(Contract.Result<
Expr>() != null);
123 Context.CheckContextMatch(from);
125 if (from.Length != to.Length)
126 throw new Z3Exception(
"Argument sizes do not match");
136 Contract.Requires(from != null);
137 Contract.Requires(to != null);
138 Contract.Ensures(Contract.Result<
Expr>() != null);
140 return Substitute(
new Expr[] { from },
new Expr[] { to });
151 Contract.Requires(to != null);
152 Contract.Requires(Contract.ForAll(to, t => t != null));
153 Contract.Ensures(Contract.Result<
Expr>() != null);
166 Contract.Requires(ctx != null);
167 Contract.Ensures(Contract.Result<
Expr>() != null);
169 if (ReferenceEquals(
Context, ctx))
180 return base.ToString();
186 public bool IsNumeral
195 public bool IsWellSorted
207 Contract.Ensures(Contract.Result<
Sort>() != null);
222 #region Integer Numerals
228 get {
return IsNumeral &&
IsInt; }
232 #region Real Numerals
238 get {
return IsNumeral && IsReal; }
242 #region Algebraic Numbers
243 public bool IsAlgebraicNumber
252 #region Term Kind Tests
254 #region Boolean Terms
326 #region Interpolation
334 #region Arithmetic Terms
515 #region Bit-vector terms
592 internal bool IsBVUDiv0 {
get {
return IsApp && FuncDecl.DeclKind ==
Z3_decl_kind.Z3_OP_BUDIV0; } }
597 internal bool IsBVSRem0 {
get {
return IsApp && FuncDecl.DeclKind ==
Z3_decl_kind.Z3_OP_BSREM0; } }
602 internal bool IsBVURem0 {
get {
return IsApp && FuncDecl.DeclKind ==
Z3_decl_kind.Z3_OP_BUREM0; } }
607 internal bool IsBVSMod0 {
get {
return IsApp && FuncDecl.DeclKind ==
Z3_decl_kind.Z3_OP_BSMOD0; } }
1312 #region Relational Terms
1313 public bool IsRelation
1434 #region Finite domain terms
1435 public bool IsFiniteDomain
1454 #region Bound Variables
1479 throw new Z3Exception(
"Term is not a bound variable.");
1481 Contract.EndContractBlock();
1489 internal protected Expr(
Context ctx) : base(ctx) { Contract.Requires(ctx != null); }
1496 internal protected Expr(
Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
1500 internal override void CheckNativeObject(IntPtr obj)
1505 throw new Z3Exception(
"Underlying object is not a term");
1506 base.CheckNativeObject(obj);
1511 internal static Expr Create(Context ctx, FuncDecl f, params Expr[] arguments)
1513 Contract.Requires(ctx != null);
1514 Contract.Requires(f != null);
1515 Contract.Ensures(Contract.Result<Expr>() != null);
1517 IntPtr obj = Native.Z3_mk_app(ctx.nCtx, f.NativeObject,
1518 AST.ArrayLength(arguments),
1519 AST.ArrayToNative(arguments));
1520 return Create(ctx, obj);
1524 new internal static Expr Create(Context ctx, IntPtr obj)
1526 Contract.Requires(ctx != null);
1527 Contract.Ensures(Contract.Result<Expr>() != null);
1531 return new Quantifier(ctx, obj);
1532 IntPtr s = Native.Z3_get_sort(ctx.nCtx, obj);
1535 if (Native.Z3_is_algebraic_number(ctx.nCtx, obj) != 0)
1536 return new AlgebraicNum(ctx, obj);
1538 if (Native.Z3_is_numeral_ast(ctx.nCtx, obj) != 0)
1542 case Z3_sort_kind.Z3_INT_SORT:
return new IntNum(ctx, obj);
1543 case Z3_sort_kind.Z3_REAL_SORT:
return new RatNum(ctx, obj);
1544 case Z3_sort_kind.Z3_BV_SORT:
return new BitVecNum(ctx, obj);
1551 case Z3_sort_kind.Z3_INT_SORT:
return new IntExpr(ctx, obj);
1552 case Z3_sort_kind.Z3_REAL_SORT:
return new RealExpr(ctx, obj);
1553 case Z3_sort_kind.Z3_BV_SORT:
return new BitVecExpr(ctx, obj);
1554 case Z3_sort_kind.Z3_ARRAY_SORT:
return new ArrayExpr(ctx, obj);
1555 case Z3_sort_kind.Z3_DATATYPE_SORT:
return new DatatypeExpr(ctx, obj);
1558 return new Expr(ctx, obj);
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
static Z3_ast Z3_update_term(Z3_context a0, Z3_ast a1, uint a2, [In] Z3_ast[] a3)
Expr Simplify(Params p=null)
Returns a simplified version of the expression.
static uint Z3_get_app_num_args(Z3_context a0, Z3_app a1)
uint DomainSize
The size of the domain of the function declaration Arity
static uint Z3_get_sort_kind(Z3_context a0, Z3_sort a1)
static uint Z3_get_bool_value(Z3_context a0, Z3_ast a1)
static Z3_ast Z3_substitute(Z3_context a0, Z3_ast a1, uint a2, [In] Z3_ast[] a3, [In] Z3_ast[] a4)
static Z3_ast Z3_substitute_vars(Z3_context a0, Z3_ast a1, uint a2, [In] Z3_ast[] a3)
static Z3_ast Z3_translate(Z3_context a0, Z3_ast a1, Z3_context a2)
Expr SubstituteVars(Expr[] to)
Substitute the free variables in the expression with the expressions in to
Expr Substitute(Expr[] from, Expr[] to)
Substitute every occurrence of from[i] in the expression with to[i], for i smaller than num_exprs...
Z3_decl_kind DeclKind
The kind of the function declaration.
static int Z3_is_well_sorted(Z3_context a0, Z3_ast a1)
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types...
static uint Z3_get_index_value(Z3_context a0, Z3_ast a1)
static Z3_sort Z3_get_sort(Z3_context a0, Z3_ast a1)
new Expr Translate(Context ctx)
Translates (copies) the term to the Context ctx .
override string ToString()
Returns a string representation of the expression.
static Z3_ast Z3_get_app_arg(Z3_context a0, Z3_app a1, uint a2)
static int Z3_is_eq_sort(Z3_context a0, Z3_sort a1, Z3_sort a2)
static Z3_ast Z3_simplify_ex(Z3_context a0, Z3_ast a1, Z3_params a2)
A ParameterSet represents a configuration in the form of Symbol/value pairs.
static int Z3_is_algebraic_number(Z3_context a0, Z3_ast a1)
static uint Z3_get_ast_kind(Z3_context a0, Z3_ast a1)
void Update(Expr[] args)
Update the arguments of the expression using the arguments args The number of new arguments should c...
The main interaction with Z3 happens via the Context.
The Sort class implements type information for ASTs.
The exception base class for error reporting from Z3
static Z3_ast Z3_simplify(Z3_context a0, Z3_ast a1)
The abstract syntax tree (AST) class.
Expr(Context ctx, IntPtr obj)
Constructor for Expr
static int Z3_is_app(Z3_context a0, Z3_ast a1)
Expr Substitute(Expr from, Expr to)
Substitute every occurrence of from in the expression with to.
static Z3_func_decl Z3_get_app_decl(Z3_context a0, Z3_app a1)
Z3_decl_kind
The different kinds of interpreted function kinds.
static Z3_sort Z3_mk_bool_sort(Z3_context a0)
static int Z3_is_numeral_ast(Z3_context a0, Z3_ast a1)