Deprecated Class Reference

The main interaction with Z3 happens via the Context. More...

Static Public Member Functions
static void	Push (Context ctx)
	Creates a backtracking point. More...
static void	Pop (Context ctx, uint n=1)
	Backtracks n backtracking points. More...
static void	Assert (Context ctx, params BoolExpr[] constraints)
	Assert a constraint (or multiple) into the solver. More...
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. More...
static BoolExpr	GetAssignment (Context ctx)
	Retrieves an assignment to atomic propositions for a satisfiable context. More...

Detailed Description

The main interaction with Z3 happens via the Context.

Definition at line 31 of file Deprecated.cs.

Member Function Documentation

static void Assert ( Context  ctx, params BoolExpr[]  constraints  )

inlinestatic

Assert a constraint (or multiple) into the solver.

Definition at line 54 of file Deprecated.cs.

         {
            Contract.Requires(constraints != null);
            Contract.Requires(Contract.ForAll(constraints, c => c != null));

            ctx.CheckContextMatch(constraints);
            foreach (BoolExpr a in constraints)
            {
                Native.Z3_assert_cnstr(ctx.nCtx, a.NativeObject);
            }
         }

static Status Check ( Context  ctx, List< BoolExpr >  core, ref Model  model, ref Expr  proof, params Expr[]  assumptions  )

inlinestatic

Checks whether the assertions in the context are consistent or not.

Definition at line 68 of file Deprecated.cs.

        {
            Z3_lbool r;
            model = null;
            proof = null;
            if (assumptions == null || assumptions.Length == 0)
                r = (Z3_lbool)Native.Z3_check(ctx.nCtx);
            else {
                IntPtr mdl = IntPtr.Zero, prf = IntPtr.Zero;
                uint core_size = 0;
                IntPtr[] native_core = new IntPtr[assumptions.Length];
                r = (Z3_lbool)Native.Z3_check_assumptions(ctx.nCtx, 
                                   (uint)assumptions.Length, AST.ArrayToNative(assumptions),
                                   ref mdl, ref prf, ref core_size, native_core);

                for (uint i = 0; i < core_size; i++)
                    core.Add((BoolExpr)Expr.Create(ctx, native_core[i]));
                if (mdl != IntPtr.Zero) {
                    model = new Model(ctx, mdl);
                }
                if (prf != IntPtr.Zero) {
                    proof = Expr.Create(ctx, prf);
                }

            }
            switch (r)
            {
                case Z3_lbool.Z3_L_TRUE: return Status.SATISFIABLE;
                case Z3_lbool.Z3_L_FALSE: return Status.UNSATISFIABLE;
                default: return Status.UNKNOWN;
            }
        }

static BoolExpr GetAssignment ( Context  ctx )

inlinestatic

Retrieves an assignment to atomic propositions for a satisfiable context.

Definition at line 104 of file Deprecated.cs.

         {
             IntPtr x = Native.Z3_get_context_assignment(ctx.nCtx);
             return (BoolExpr)Expr.Create(ctx, x);
         }

static void Pop ( Context  ctx, uint  n = 1  )

inlinestatic

Backtracks n backtracking points.

Note that an exception is thrown if n is not smaller than NumScopes

See Also

Push

Definition at line 47 of file Deprecated.cs.

                                                         {
             Native.Z3_pop(ctx.nCtx, n);
         }

static void Push ( Context  ctx )

inlinestatic

Creates a backtracking point.

See Also

Pop

Definition at line 38 of file Deprecated.cs.

                                              {
             Native.Z3_push(ctx.nCtx);
         }