Z3
Static Public Member Functions
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.

55  {
56  Contract.Requires(constraints != null);
57  Contract.Requires(Contract.ForAll(constraints, c => c != null));
58 
59  ctx.CheckContextMatch(constraints);
60  foreach (BoolExpr a in constraints)
61  {
62  Native.Z3_assert_cnstr(ctx.nCtx, a.NativeObject);
63  }
64  }
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.

69  {
70  Z3_lbool r;
71  model = null;
72  proof = null;
73  if (assumptions == null || assumptions.Length == 0)
74  r = (Z3_lbool)Native.Z3_check(ctx.nCtx);
75  else {
76  IntPtr mdl = IntPtr.Zero, prf = IntPtr.Zero;
77  uint core_size = 0;
78  IntPtr[] native_core = new IntPtr[assumptions.Length];
79  r = (Z3_lbool)Native.Z3_check_assumptions(ctx.nCtx,
80  (uint)assumptions.Length, AST.ArrayToNative(assumptions),
81  ref mdl, ref prf, ref core_size, native_core);
82 
83  for (uint i = 0; i < core_size; i++)
84  core.Add((BoolExpr)Expr.Create(ctx, native_core[i]));
85  if (mdl != IntPtr.Zero) {
86  model = new Model(ctx, mdl);
87  }
88  if (prf != IntPtr.Zero) {
89  proof = Expr.Create(ctx, prf);
90  }
91 
92  }
93  switch (r)
94  {
95  case Z3_lbool.Z3_L_TRUE: return Status.SATISFIABLE;
96  case Z3_lbool.Z3_L_FALSE: return Status.UNSATISFIABLE;
97  default: return Status.UNKNOWN;
98  }
99  }
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:143
Status
Status values.
Definition: Status.cs:27
Z3_lbool
Z3_lbool
Definition: Enumerations.cs:10
static BoolExpr GetAssignment ( Context  ctx)
inlinestatic

Retrieves an assignment to atomic propositions for a satisfiable context.

Definition at line 104 of file Deprecated.cs.

105  {
106  IntPtr x = Native.Z3_get_context_assignment(ctx.nCtx);
107  return (BoolExpr)Expr.Create(ctx, x);
108  }
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.

47  {
48  Native.Z3_pop(ctx.nCtx, n);
49  }
static void Push ( Context  ctx)
inlinestatic

Creates a backtracking point.

See also
Pop

Definition at line 38 of file Deprecated.cs.

38  {
39  Native.Z3_push(ctx.nCtx);
40  }