A RetroSearch Logo

Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Search Query:

Showing content from https://z3prover.github.io/api/html/class_microsoft_1_1_z3_1_1_solver.html below:

Z3: Solver Class Reference

Solvers. More...

void  Set (string name, bool value)   Sets parameter on the solver More...
  void  Set (string name, uint value)   Sets parameter on the solver More...
  void  Set (string name, double value)   Sets parameter on the solver More...
  void  Set (string name, string value)   Sets parameter on the solver More...
  void  Set (string name, Symbol value)   Sets parameter on the solver More...
  void  Set (Symbol name, bool value)   Sets parameter on the solver More...
  void  Set (Symbol name, uint value)   Sets parameter on the solver More...
  void  Set (Symbol name, double value)   Sets parameter on the solver More...
  void  Set (Symbol name, string value)   Sets parameter on the solver More...
  void  Set (Symbol name, Symbol value)   Sets parameter on the solver More...
  void  Push ()   Creates a backtracking point. More...
  void  Pop (uint n=1)   Backtracks n backtracking points. More...
  void  Reset ()   Resets the Solver. More...
  void  Assert (params BoolExpr[] constraints)   Assert a constraint (or multiple) into the solver. More...
  void  Add (params BoolExpr[] constraints)   Alias for Assert. More...
  void  Add (IEnumerable< BoolExpr > constraints)   Alias for Assert. More...
  void  AssertAndTrack (BoolExpr[] constraints, BoolExpr[] ps)   Assert multiple constraints into the solver, and track them (in the unsat) core using the Boolean constants in ps. More...
  void  AssertAndTrack (BoolExpr constraint, BoolExpr p)   Assert a constraint into the solver, and track it (in the unsat) core using the Boolean constant p. More...
  void  FromFile (string file)   Load solver assertions from a file. More...
  void  FromString (string str)   Load solver assertions from a string. More...
  Status  Check (params Expr[] assumptions)   Checks whether the assertions in the solver are consistent or not. More...
  Status  Check (IEnumerable< BoolExpr > assumptions)   Checks whether the assertions in the solver are consistent or not. More...
  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 an implication of the form More...
  IEnumerable< BoolExpr[]>  Cube ()   Return a set of cubes. More...
  Solver  Translate (Context ctx)   Create a clone of the current solver with respect to ctx. More...
  void  ImportModelConverter (Solver src)   Import model converter from other solver. More...
  override string  ToString ()   A string representation of the solver. More...
  void  Dispose ()   Disposes of the underlying native Z3 object. More...
 

Solvers.

Definition at line 30 of file Solver.cs.

◆ Add() [1/2] void Add ( IEnumerable< BoolExpr >  constraints ) inline

Alias for Assert.

Definition at line 223 of file Solver.cs.

225  Assert

(constraints.ToArray());

void Assert(params BoolExpr[] constraints)

Assert a constraint (or multiple) into the solver.

◆ Add() [2/2] void Add ( params BoolExpr[]  constraints ) inline ◆ Assert() void Assert ( params BoolExpr[]  constraints ) inline

Assert a constraint (or multiple) into the solver.

Definition at line 200 of file Solver.cs.

202

Debug.Assert(constraints !=

null

);

203

Debug.Assert(constraints.All(c => c !=

null

));

205  Context

.CheckContextMatch<BoolExpr>(constraints);

206  foreach

(BoolExpr a

in

constraints)

208

Native.Z3_solver_assert(

Context

.nCtx, NativeObject, a.NativeObject);

Context Context

Access Context object

Referenced by Solver.Add(), Context.MkSolver(), and Solver.Translate().

◆ AssertAndTrack() [1/2]

Assert a constraint into the solver, and track it (in the unsat) core using the Boolean constant p.

This API is an alternative to Check(Expr[]) with assumptions for extracting unsat cores. Both APIs can be used in the same solver. The unsat core will contain a combination of the Boolean variables provided using AssertAndTrack(BoolExpr[],BoolExpr[]) and the Boolean literals provided using Check(Expr[]) with assumptions.

Definition at line 264 of file Solver.cs.

266

Debug.Assert(constraint !=

null

);

267

Debug.Assert(p !=

null

);

268  Context

.CheckContextMatch(constraint);

271

Native.Z3_solver_assert_and_track(

Context

.nCtx, NativeObject, constraint.NativeObject, p.NativeObject);

◆ AssertAndTrack() [2/2]

Assert multiple constraints into the solver, and track them (in the unsat) core using the Boolean constants in ps.

This API is an alternative to Check(Expr[]) with assumptions for extracting unsat cores. Both APIs can be used in the same solver. The unsat core will contain a combination of the Boolean variables provided using AssertAndTrack(BoolExpr[],BoolExpr[]) and the Boolean literals provided using Check(Expr[]) with assumptions.

Definition at line 239 of file Solver.cs.

241

Debug.Assert(constraints !=

null

);

242

Debug.Assert(constraints.All(c => c !=

null

));

243

Debug.Assert(ps.All(c => c !=

null

));

244  Context

.CheckContextMatch<BoolExpr>(constraints);

245  Context

.CheckContextMatch<BoolExpr>(ps);

246  if

(constraints.Length != ps.Length)

247  throw new

Z3Exception(

"Argument size mismatch"

);

249  for

(

int

i = 0 ; i < constraints.Length; i++)

250

Native.Z3_solver_assert_and_track(

Context

.nCtx, NativeObject, constraints[i].NativeObject, ps[i].NativeObject);

◆ Check() [1/2]

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

See also
Model, UnsatCore, Proof

Definition at line 354 of file Solver.cs.

357

BoolExpr[] asms = assumptions.ToArray();

358  if

(asms.Length == 0)

361

r = (

Z3_lbool

)Native.Z3_solver_check_assumptions(

Context

.nCtx, NativeObject, (uint)asms.Length, AST.ArrayToNative(asms));

362  return

lboolToStatus(r);

Z3_lbool

Lifted Boolean type: false, undefined, true.

◆ Check() [2/2]

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

See also
Model, UnsatCore, Proof

Definition at line 336 of file Solver.cs.

339  if

(assumptions ==

null

|| assumptions.Length == 0)

342

r = (

Z3_lbool

)Native.Z3_solver_check_assumptions(

Context

.nCtx, NativeObject, (uint)assumptions.Length, AST.ArrayToNative(assumptions));

343  return

lboolToStatus(r);

◆ Consequences()

Retrieve fixed assignments to the set of variables in the form of consequences. Each consequence is an implication of the form

  relevant-assumptions Implies variable = value

where the relevant assumptions is a subset of the assumptions that are passed in and the equality on the right side of the implication indicates how a variable is fixed.

See also
Model, UnsatCore, Proof

Definition at line 380 of file Solver.cs.

382  using

ASTVector result =

new

ASTVector(

Context

);

383  using

ASTVector asms =

new

ASTVector(

Context

);

384  using

ASTVector vars =

new

ASTVector(

Context

);

385  foreach

(var

asm in

assumptions) asms.Push(

asm

);

386  foreach

(var v

in

variables) vars.Push(v);

387  Z3_lbool

r = (

Z3_lbool

)Native.Z3_solver_get_consequences(

Context

.nCtx, NativeObject, asms.NativeObject, vars.NativeObject, result.NativeObject);

388

consequences = result.ToBoolExprArray();

389  return

lboolToStatus(r);

◆ Cube()

Return a set of cubes.

Definition at line 474 of file Solver.cs.

476  using

ASTVector cv =

new

ASTVector(

Context

);

483  using

ASTVector r =

new

ASTVector(

Context

, Native.Z3_solver_cube(

Context

.nCtx, NativeObject, cv.NativeObject, lvl));

484

var v = r.ToBoolExprArray();

486  if

(v.Length == 1 && v[0].IsFalse) {

uint BacktrackLevel

Backtrack level that can be adjusted by conquer process

BoolExpr[] CubeVariables

Variables available and returned by the cuber.

◆ FromFile() void FromFile ( string  file ) inline

Load solver assertions from a file.

Definition at line 277 of file Solver.cs.

279

Native.Z3_solver_from_file(

Context

.nCtx, NativeObject, file);

◆ FromString() void FromString ( string  str ) inline

Load solver assertions from a string.

Definition at line 285 of file Solver.cs.

287

Native.Z3_solver_from_string(

Context

.nCtx, NativeObject, str);

◆ ImportModelConverter() void ImportModelConverter ( Solver  src ) inline

Import model converter from other solver.

Definition at line 508 of file Solver.cs.

510

Native.Z3_solver_import_model_converter(

Context

.nCtx, src.NativeObject, NativeObject);

◆ Pop()

Backtracks n backtracking points.

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

See also
Push

Definition at line 183 of file Solver.cs.

185

Native.Z3_solver_pop(

Context

.nCtx, NativeObject, n);

◆ Push()

Creates a backtracking point.

See also
Pop

Definition at line 173 of file Solver.cs.

175

Native.Z3_solver_push(

Context

.nCtx, NativeObject);

◆ Reset()

Resets the Solver.

This removes all assertions from the solver.

Definition at line 192 of file Solver.cs.

194

Native.Z3_solver_reset(

Context

.nCtx, NativeObject);

◆ Set() [1/10] void Set ( string  name, bool  value  ) inline

Sets parameter on the solver

Definition at line 61 of file Solver.cs.

Params MkParams()

Creates a new ParameterSet.

Params Add(Symbol name, bool value)

Adds a parameter setting.

Params Parameters

Sets the solver parameters.

◆ Set() [2/10] void Set ( string  name, double  value  ) inline

Sets parameter on the solver

Definition at line 79 of file Solver.cs.

◆ Set() [3/10] void Set ( string  name, string  value  ) inline

Sets parameter on the solver

Definition at line 88 of file Solver.cs.

◆ Set() [4/10] void Set ( string  name, Symbol  value  ) inline

Sets parameter on the solver

Definition at line 97 of file Solver.cs.

◆ Set() [5/10] void Set ( string  name, uint  value  ) inline

Sets parameter on the solver

Definition at line 70 of file Solver.cs.

◆ Set() [6/10] void Set ( Symbol  name, bool  value  ) inline

Sets parameter on the solver

Definition at line 106 of file Solver.cs.

◆ Set() [7/10] void Set ( Symbol  name, double  value  ) inline

Sets parameter on the solver

Definition at line 124 of file Solver.cs.

◆ Set() [8/10] void Set ( Symbol  name, string  value  ) inline

Sets parameter on the solver

Definition at line 133 of file Solver.cs.

◆ Set() [9/10]

Sets parameter on the solver

Definition at line 142 of file Solver.cs.

◆ Set() [10/10] void Set ( Symbol  name, uint  value  ) inline

Sets parameter on the solver

Definition at line 115 of file Solver.cs.

◆ ToString() override string ToString ( ) inline

A string representation of the solver.

Definition at line 528 of file Solver.cs.

530  return

Native.Z3_solver_to_string(

Context

.nCtx, NativeObject);

◆ Translate()

Create a clone of the current solver with respect to ctx.

Definition at line 499 of file Solver.cs.

501

Debug.Assert(ctx !=

null

);

502  return new

Solver(ctx, Native.Z3_solver_translate(

Context

.nCtx, NativeObject, ctx.nCtx));

◆ Assertions

The set of asserted formulas.

Definition at line 305 of file Solver.cs.

310  using

ASTVector assertions =

new

ASTVector(

Context

, Native.Z3_solver_get_assertions(

Context

.nCtx, NativeObject));

311  return

assertions.ToBoolExprArray();

◆ BacktrackLevel

Backtrack level that can be adjusted by conquer process

Definition at line 463 of file Solver.cs.

Referenced by Solver.Cube().

◆ CubeVariables ◆ Help

A string that describes all available solver parameters.

Definition at line 35 of file Solver.cs.

40  return

Native.Z3_solver_get_help(

Context

.nCtx, NativeObject);

◆ Model

The model of the last Check(params Expr[] assumptions).

The result is null if Check(params Expr[] assumptions) was not invoked before, if its results was not SATISFIABLE, or if model production is not enabled.

Definition at line 399 of file Solver.cs.

403

IntPtr x = Native.Z3_solver_get_model(

Context

.nCtx, NativeObject);

404  if

(x == IntPtr.Zero)

Model Model

The model of the last Check(params Expr[] assumptions).

◆ NumAssertions

The number of assertions in the solver.

Definition at line 293 of file Solver.cs.

297  using

ASTVector assertions =

new

ASTVector(

Context

, Native.Z3_solver_get_assertions(

Context

.nCtx, NativeObject));

298  return

assertions.Size;

◆ NumScopes

The current number of backtracking points (scopes).

See also
Pop, Push

Definition at line 164 of file Solver.cs.

166  get

{

return

Native.Z3_solver_get_num_scopes(

Context

.nCtx, NativeObject); }

◆ ParameterDescriptions

Retrieves parameter descriptions for solver.

Definition at line 153 of file Solver.cs.

155  get

{

return new

ParamDescrs(

Context

, Native.Z3_solver_get_param_descrs(

Context

.nCtx, NativeObject)); }

◆ Parameters

Sets the solver parameters.

Definition at line 47 of file Solver.cs.

51

Debug.Assert(value !=

null

);

53  Context

.CheckContextMatch(value);

54

Native.Z3_solver_set_params(

Context

.nCtx, NativeObject, value.NativeObject);

Referenced by Solver.Set().

◆ Proof ◆ ReasonUnknown

A brief justification of why the last call to Check returned UNKNOWN.

Definition at line 451 of file Solver.cs.

456  return

Native.Z3_solver_get_reason_unknown(

Context

.nCtx, NativeObject);

◆ Statistics

Solver statistics.

Definition at line 516 of file Solver.cs.

Statistics Statistics

Solver statistics.

◆ Units

Currently inferred units.

Definition at line 318 of file Solver.cs.

323  using

ASTVector assertions =

new

ASTVector(

Context

, Native.Z3_solver_get_units(

Context

.nCtx, NativeObject));

324  return

assertions.ToBoolExprArray();

◆ UnsatCore

The unsat core of the last Check.

The unsat core is a subset of Assertions The result is empty if Check was not invoked before, if its results was not UNSATISFIABLE, or if core production is disabled.

Definition at line 438 of file Solver.cs.

443  using

ASTVector core =

new

ASTVector(

Context

, Native.Z3_solver_get_unsat_core(

Context

.nCtx, NativeObject));

444  return

core.ToBoolExprArray();

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4