21 using System.Collections.Generic;
22 using System.Runtime.InteropServices;
23 using System.Diagnostics.Contracts;
30 [ContractVerification(
true)]
56 Contract.Requires(constraints != null);
57 Contract.Requires(Contract.ForAll(constraints, c => c != null));
59 ctx.CheckContextMatch(constraints);
73 if (assumptions == null || assumptions.Length == 0)
76 IntPtr mdl = IntPtr.Zero, prf = IntPtr.Zero;
78 IntPtr[] native_core =
new IntPtr[assumptions.Length];
80 (uint)assumptions.Length,
AST.ArrayToNative(assumptions),
81 ref mdl, ref prf, ref core_size, native_core);
83 for (uint i = 0; i < core_size; i++)
85 if (mdl != IntPtr.Zero) {
86 model =
new Model(ctx, mdl);
88 if (prf != IntPtr.Zero) {
89 proof =
Expr.Create(ctx, prf);
97 default:
return Status.UNKNOWN;
static BoolExpr GetAssignment(Context ctx)
Retrieves an assignment to atomic propositions for a satisfiable context.
The main interaction with Z3 happens via the Context.
static int Z3_check_assumptions(Z3_context a0, uint a1, [In] Z3_ast[] a2, [In, Out] ref Z3_model a3, [In, Out] ref Z3_ast a4, [In, Out] ref uint a5, [Out] Z3_ast[] a6)
static void Push(Context ctx)
Creates a backtracking point.
static void Assert(Context ctx, params BoolExpr[] constraints)
Assert a constraint (or multiple) into the solver.
Z3_lbool
Lifted Boolean type: false, undefined, true.
static void Pop(Context ctx, uint n=1)
Backtracks n backtracking points.
static void Z3_pop(Z3_context a0, uint a1)
static void Z3_push(Z3_context a0)
static int Z3_check(Z3_context a0)
static void Z3_assert_cnstr(Z3_context a0, Z3_ast a1)
A Model contains interpretations (assignments) of constants and functions.
The main interaction with Z3 happens via the Context.
static Status Check(Context ctx, List< BoolExpr > core, ref Model model, ref Expr proof, params Expr[] assumptions)
Checks whether the assertions in the context are consistent or not.
The abstract syntax tree (AST) class.
static Z3_ast Z3_get_context_assignment(Z3_context a0)