21using System.Diagnostics;
23using System.Collections.Generic;
40 return Native.Z3_solver_get_help(
Context.nCtx, NativeObject);
51 Debug.Assert(value !=
null);
53 Context.CheckContextMatch(value);
54 Native.Z3_solver_set_params(
Context.nCtx, NativeObject, value.NativeObject);
117 get {
return Native.Z3_solver_get_num_scopes(
Context.nCtx, NativeObject); }
126 Native.Z3_solver_push(
Context.nCtx, NativeObject);
134 public void Pop(uint n = 1)
136 Native.Z3_solver_pop(
Context.nCtx, NativeObject, n);
145 Native.Z3_solver_reset(
Context.nCtx, NativeObject);
153 Debug.Assert(constraints !=
null);
154 Debug.Assert(constraints.All(c => c !=
null));
159 Native.Z3_solver_assert(
Context.nCtx, NativeObject, a.NativeObject);
174 public void Add(IEnumerable<BoolExpr> constraints)
176 Assert(constraints.ToArray());
192 Debug.Assert(constraints !=
null);
193 Debug.Assert(constraints.All(c => c !=
null));
194 Debug.Assert(ps.All(c => c !=
null));
197 if (constraints.Length != ps.Length)
200 for (
int i = 0 ; i < constraints.Length; i++)
201 Native.Z3_solver_assert_and_track(
Context.nCtx, NativeObject, constraints[i].NativeObject, ps[i].NativeObject);
217 Debug.Assert(constraint !=
null);
218 Debug.Assert(p !=
null);
219 Context.CheckContextMatch(constraint);
222 Native.Z3_solver_assert_and_track(
Context.nCtx, NativeObject, constraint.NativeObject, p.NativeObject);
230 Native.Z3_solver_from_file(
Context.nCtx, NativeObject, file);
238 Native.Z3_solver_from_string(
Context.nCtx, NativeObject, str);
249 return assertions.
Size;
290 if (assumptions ==
null || assumptions.Length == 0)
293 r = (
Z3_lbool)Native.Z3_solver_check_assumptions(
Context.nCtx, NativeObject, (uint)assumptions.Length,
AST.ArrayToNative(assumptions));
294 return lboolToStatus(r);
308 BoolExpr[] asms = assumptions.ToArray();
309 if (asms.Length == 0)
312 r = (
Z3_lbool)Native.Z3_solver_check_assumptions(
Context.nCtx, NativeObject, (uint)asms.Length,
AST.ArrayToNative(asms));
313 return lboolToStatus(r);
336 foreach (var
asm in assumptions) asms.Push(
asm);
337 foreach (var v
in variables) vars.Push(v);
338 Z3_lbool r = (
Z3_lbool)Native.Z3_solver_get_consequences(
Context.nCtx, NativeObject, asms.NativeObject, vars.NativeObject, result.NativeObject);
339 consequences = result.ToBoolExprArray();
340 return lboolToStatus(r);
354 IntPtr x = Native.Z3_solver_get_model(
Context.nCtx, NativeObject);
355 if (x == IntPtr.Zero)
373 IntPtr x = Native.Z3_solver_get_proof(
Context.nCtx, NativeObject);
374 if (x == IntPtr.Zero)
407 return Native.Z3_solver_get_reason_unknown(
Context.nCtx, NativeObject);
425 public IEnumerable<BoolExpr[]>
Cube()
437 if (v.Length == 1 && v[0].IsFalse) {
452 Debug.
Assert(ctx !=
null);
453 return new Solver(ctx, Native.Z3_solver_translate(
Context.nCtx, NativeObject, ctx.nCtx));
461 Native.Z3_solver_import_model_converter(
Context.nCtx, src.NativeObject, NativeObject);
481 return Native.Z3_solver_to_string(
Context.nCtx, NativeObject);
488 Debug.Assert(ctx !=
null);
492 internal class DecRefQueue : IDecRefQueue
494 public DecRefQueue() : base() { }
495 public DecRefQueue(uint move_limit) : base(move_limit) { }
496 internal override void IncRef(Context ctx, IntPtr obj)
498 Native.Z3_solver_inc_ref(ctx.nCtx, obj);
501 internal override void DecRef(Context ctx, IntPtr obj)
503 Native.Z3_solver_dec_ref(ctx.nCtx, obj);
507 internal override void IncRef(IntPtr o)
513 internal override void DecRef(IntPtr o)
525 default:
return Status.UNKNOWN;
The abstract syntax tree (AST) class.
BoolExpr[] ToBoolExprArray()
Translates an ASTVector into a BoolExpr[]
uint Size
The size of the vector
The main interaction with Z3 happens via the Context.
Params MkParams()
Creates a new ParameterSet.
IDecRefQueue Solver_DRQ
Solver DRQ
A Model contains interpretations (assignments) of constants and functions.
A ParamDescrs describes a set of parameters.
A Params objects represents a configuration in the form of Symbol/value pairs.
Params Add(Symbol name, bool value)
Adds a parameter setting.
void Set(string name, uint value)
Sets parameter on the solver
BoolExpr[] Assertions
The set of asserted formulas.
void Set(string name, double value)
Sets parameter on the solver
Model Model
The model of the last Check(params Expr[] assumptions).
string Help
A string that describes all available solver parameters.
void Set(string name, string value)
Sets parameter on the solver
void Pop(uint n=1)
Backtracks n backtracking points.
Solver Translate(Context ctx)
Create a clone of the current solver with respect to ctx.
void Add(IEnumerable< BoolExpr > constraints)
Alias for Assert.
void Reset()
Resets the Solver.
void AssertAndTrack(BoolExpr constraint, BoolExpr p)
Assert a constraint into the solver, and track it (in the unsat) core using the Boolean constant p.
void Set(Symbol name, Symbol value)
Sets parameter on the solver
void Push()
Creates a backtracking point.
void Assert(params BoolExpr[] constraints)
Assert a constraint (or multiple) into the solver.
IEnumerable< BoolExpr[]> Cube()
Return a set of cubes.
void FromString(string str)
Load solver assertions from a string.
uint NumAssertions
The number of assertions in the solver.
Params Parameters
Sets the solver parameters.
Statistics Statistics
Solver statistics.
uint NumScopes
The current number of backtracking points (scopes).
Status Check(IEnumerable< BoolExpr > assumptions)
Checks whether the assertions in the solver are consistent or not.
void Set(Symbol name, string value)
Sets parameter on the solver
void ImportModelConverter(Solver src)
Import model converter from other solver.
ParamDescrs ParameterDescriptions
Retrieves parameter descriptions for solver.
Expr Proof
The proof of the last Check(params Expr[] assumptions).
Status Check(params Expr[] assumptions)
Checks whether the assertions in the solver are consistent or not.
BoolExpr[] UnsatCore
The unsat core of the last Check.
BoolExpr[] Units
Currently inferred units.
uint BacktrackLevel
Backtrack level that can be adjusted by conquer process
override string ToString()
A string representation of the solver.
void FromFile(string file)
Load solver assertions from a file.
void Set(string name, bool value)
Sets parameter on the solver
string ReasonUnknown
A brief justification of why the last call to Check returned UNKNOWN.
void Set(Symbol name, double value)
Sets parameter on the solver
void Set(Symbol name, bool value)
Sets parameter on the solver
void Add(params BoolExpr[] constraints)
Alias for Assert.
BoolExpr[] CubeVariables
Variables available and returned by the cuber.
void AssertAndTrack(BoolExpr[] constraints, BoolExpr[] ps)
Assert multiple constraints into the solver, and track them (in the unsat) core using the Boolean con...
Status Consequences(IEnumerable< BoolExpr > assumptions, IEnumerable< Expr > variables, out BoolExpr[] consequences)
Retrieve fixed assignments to the set of variables in the form of consequences. Each consequence is a...
void Set(string name, Symbol value)
Sets parameter on the solver
void Set(Symbol name, uint value)
Sets parameter on the solver
Objects of this class track statistical information about solvers.
Symbols are used to name several term and type constructors.
The exception base class for error reporting from Z3
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Z3_lbool
Lifted Boolean type: false, undefined, true.