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... | |
The main interaction with Z3 happens via the Context.
Definition at line 31 of file Deprecated.cs.
Assert a constraint (or multiple) into the solver.
Definition at line 54 of file Deprecated.cs.
|
inlinestatic |
Checks whether the assertions in the context are consistent or not.
Definition at line 68 of file Deprecated.cs.
Retrieves an assignment to atomic propositions for a satisfiable context.
Definition at line 104 of file Deprecated.cs.
|
inlinestatic |
Backtracks n backtracking points.
Note that an exception is thrown if n is not smaller than NumScopes
Definition at line 47 of file Deprecated.cs.
|
inlinestatic |