Inheritance diagram for Solver:

Data Structures
class	DecRefQueue

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

Public Member Functions inherited from Z3Object
void	Dispose ()
	Disposes of the underlying native Z3 object. More...

Properties
string	Help `[get]`
	A string that describes all available solver parameters. More...

Params	Parameters `[set]`
	Sets the solver parameters. More...

ParamDescrs	ParameterDescriptions `[get]`
	Retrieves parameter descriptions for solver. More...

uint	NumScopes `[get]`
	The current number of backtracking points (scopes). More...

uint	NumAssertions `[get]`
	The number of assertions in the solver. More...

BoolExpr[]	Assertions `[get]`
	The set of asserted formulas. More...

BoolExpr[]	Units `[get]`
	Currently inferred units. More...

Model	Model `[get]`
	The model of the last `Check(params Expr[] assumptions)`. More...

Expr	Proof `[get]`
	The proof of the last `Check(params Expr[] assumptions)`. More...

BoolExpr[]	UnsatCore `[get]`
	The unsat core of the last `Check`. More...

string	ReasonUnknown `[get]`
	A brief justification of why the last call to `Check` returned `UNKNOWN`. More...

uint	BacktrackLevel `[get, set]`
	Backtrack level that can be adjusted by conquer process More...

BoolExpr[]	CubeVariables `[get, set]`
	Variables available and returned by the cuber. More...

Statistics	Statistics `[get]`
	Solver statistics. More...

Detailed Description

Solvers.

Definition at line 30 of file Solver.cs.

Member Function Documentation

◆ Add() [1/2]

void Add ( IEnumerable< BoolExpr > constraints )

inline

Alias for Assert.

Definition at line 174 of file Solver.cs.

         {
             Assert(constraints.ToArray());
         }

◆ Add() [2/2]

void Add ( params BoolExpr[] constraints )

inline

Alias for Assert.

Definition at line 166 of file Solver.cs.

         {
             Assert(constraints);
         }

◆ Assert()

void Assert ( params BoolExpr[] constraints )

inline

Assert a constraint (or multiple) into the solver.

Definition at line 151 of file Solver.cs.

         {
             Debug.Assert(constraints != null);
             Debug.Assert(constraints.All(c => c != null));
  
             Context.CheckContextMatch<BoolExpr>(constraints);
             foreach (BoolExpr a in constraints)
             {
                 Native.Z3_solver_assert(Context.nCtx, NativeObject, a.NativeObject);
             }
         }

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

◆ AssertAndTrack() [1/2]

void AssertAndTrack	(	BoolExpr	constraint,
		BoolExpr	p
	)

inline

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 215 of file Solver.cs.

         {
             Debug.Assert(constraint != null);
             Debug.Assert(p != null);
             Context.CheckContextMatch(constraint);
             Context.CheckContextMatch(p);
                         
             Native.Z3_solver_assert_and_track(Context.nCtx, NativeObject, constraint.NativeObject, p.NativeObject);
         }

◆ AssertAndTrack() [2/2]

void AssertAndTrack	(	BoolExpr[]	constraints,
		BoolExpr[]	ps
	)

inline

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 190 of file Solver.cs.

         {
             Debug.Assert(constraints != null);
             Debug.Assert(constraints.All(c => c != null));
             Debug.Assert(ps.All(c => c != null));
             Context.CheckContextMatch<BoolExpr>(constraints);
             Context.CheckContextMatch<BoolExpr>(ps);
             if (constraints.Length != ps.Length)
                 throw new Z3Exception("Argument size mismatch");
             
             for (int i = 0 ; i < constraints.Length; i++)
                 Native.Z3_solver_assert_and_track(Context.nCtx, NativeObject, constraints[i].NativeObject, ps[i].NativeObject);
         }

◆ Check() [1/2]

Status Check ( IEnumerable< BoolExpr > assumptions )

inline

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

See also: Model, UnsatCore, Proof

Definition at line 305 of file Solver.cs.

         {
             Z3_lbool r;
             BoolExpr[] asms = assumptions.ToArray();
             if (asms.Length == 0)
                 r = (Z3_lbool)Native.Z3_solver_check(Context.nCtx, NativeObject);
             else
                 r = (Z3_lbool)Native.Z3_solver_check_assumptions(Context.nCtx, NativeObject, (uint)asms.Length, AST.ArrayToNative(asms));
             return lboolToStatus(r);
         }

◆ Check() [2/2]

Status Check ( params Expr[] assumptions )

inline

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

See also: Model, UnsatCore, Proof

Definition at line 287 of file Solver.cs.

         {
             Z3_lbool r;
             if (assumptions == null || assumptions.Length == 0)
                 r = (Z3_lbool)Native.Z3_solver_check(Context.nCtx, NativeObject);
             else
                 r = (Z3_lbool)Native.Z3_solver_check_assumptions(Context.nCtx, NativeObject, (uint)assumptions.Length, AST.ArrayToNative(assumptions));
             return lboolToStatus(r);
         }

◆ Consequences()

Status Consequences	(	IEnumerable< BoolExpr >	assumptions,
		IEnumerable< Expr >	variables,
		out BoolExpr[]	consequences
	)

inline

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 331 of file Solver.cs.

         {
             ASTVector result = new ASTVector(Context);
             ASTVector asms = new ASTVector(Context);
             ASTVector vars = new ASTVector(Context);
             foreach (var asm in assumptions) asms.Push(asm);
             foreach (var v in variables) vars.Push(v);
             Z3_lbool r = (Z3_lbool)Native.Z3_solver_get_consequences(Context.nCtx, NativeObject, asms.NativeObject, vars.NativeObject, result.NativeObject);
             consequences = result.ToBoolExprArray();
             return lboolToStatus(r);
         }

◆ Cube()

IEnumerable<BoolExpr[]> Cube ( )

inline

Return a set of cubes.

Definition at line 425 of file Solver.cs.

         {
              ASTVector cv = new ASTVector(Context);
              if (CubeVariables != null) 
                 foreach (var b in CubeVariables) cv.Push(b);
  
              while (true) {
                 var lvl = BacktrackLevel;
                 BacktrackLevel = uint.MaxValue;
                 ASTVector r = new ASTVector(Context, Native.Z3_solver_cube(Context.nCtx, NativeObject, cv.NativeObject, lvl));
                 var v = r.ToBoolExprArray();
                 CubeVariables = cv.ToBoolExprArray();
                 if (v.Length == 1 && v[0].IsFalse) {
                    break;
                 }
                 yield return v; 
                 if (v.Length == 0) {
                    break;
                 }
              }
         }

◆ FromFile()

void FromFile ( string file )

inline

Load solver assertions from a file.

Definition at line 228 of file Solver.cs.

         {
              Native.Z3_solver_from_file(Context.nCtx, NativeObject, file);      
         }

◆ FromString()

void FromString ( string str )

inline

Load solver assertions from a string.

Definition at line 236 of file Solver.cs.

         {
              Native.Z3_solver_from_string(Context.nCtx, NativeObject, str);     
         }

◆ ImportModelConverter()

void ImportModelConverter ( Solver src )

inline

Import model converter from other solver.

Definition at line 459 of file Solver.cs.

         {
              Native.Z3_solver_import_model_converter(Context.nCtx, src.NativeObject, NativeObject);
         }

◆ Pop()

void Pop ( uint n = 1 )

inline

Backtracks n backtracking points.

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

See also: Push

Definition at line 134 of file Solver.cs.

         {
             Native.Z3_solver_pop(Context.nCtx, NativeObject, n);
         }

◆ Push()

void Push ( )

inline

Creates a backtracking point.

See also: Pop

Definition at line 124 of file Solver.cs.

         {
             Native.Z3_solver_push(Context.nCtx, NativeObject);
         }

◆ Reset()

void Reset ( )

inline

Resets the Solver.

This removes all assertions from the solver.

Definition at line 143 of file Solver.cs.

         {
             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.

61 { Parameters = Context.MkParams().Add(name, value); }

◆ Set() [2/10]

void Set	(	string	name,
		double	value
	)

inline

Sets parameter on the solver

Definition at line 69 of file Solver.cs.

69 { Parameters = Context.MkParams().Add(name, value); }

◆ Set() [3/10]

void Set	(	string	name,
		string	value
	)

inline

Sets parameter on the solver

Definition at line 73 of file Solver.cs.

73 { Parameters = Context.MkParams().Add(name, value); }

◆ Set() [4/10]

void Set	(	string	name,
		Symbol	value
	)

inline

Sets parameter on the solver

Definition at line 77 of file Solver.cs.

77 { Parameters = Context.MkParams().Add(name, value); }

◆ Set() [5/10]

void Set	(	string	name,
		uint	value
	)

inline

Sets parameter on the solver

Definition at line 65 of file Solver.cs.

65 { Parameters = Context.MkParams().Add(name, value); }

◆ Set() [6/10]

void Set	(	Symbol	name,
		bool	value
	)

inline

Sets parameter on the solver

Definition at line 81 of file Solver.cs.

81 { Parameters = Context.MkParams().Add(name, value); }

◆ Set() [7/10]

void Set	(	Symbol	name,
		double	value
	)

inline

Sets parameter on the solver

Definition at line 89 of file Solver.cs.

89 { Parameters = Context.MkParams().Add(name, value); }

◆ Set() [8/10]

void Set	(	Symbol	name,
		string	value
	)

inline

Sets parameter on the solver

Definition at line 93 of file Solver.cs.

93 { Parameters = Context.MkParams().Add(name, value); }

◆ Set() [9/10]

void Set	(	Symbol	name,
		Symbol	value
	)

inline

Sets parameter on the solver

Definition at line 97 of file Solver.cs.

97 { Parameters = Context.MkParams().Add(name, value); }

◆ Set() [10/10]

void Set	(	Symbol	name,
		uint	value
	)

inline

Sets parameter on the solver

Definition at line 85 of file Solver.cs.

85 { Parameters = Context.MkParams().Add(name, value); }

◆ ToString()

override string ToString ( )

inline

A string representation of the solver.

Definition at line 479 of file Solver.cs.

         {
             return Native.Z3_solver_to_string(Context.nCtx, NativeObject);
         }

◆ Translate()

Solver Translate ( Context ctx )

inline

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

Definition at line 450 of file Solver.cs.

         {
              Debug.Assert(ctx != null);
              return new Solver(ctx, Native.Z3_solver_translate(Context.nCtx, NativeObject, ctx.nCtx));
         }

Property Documentation

◆ Assertions

BoolExpr [] Assertions

get

The set of asserted formulas.

Definition at line 257 of file Solver.cs.

         {
             get
             {
  
                 ASTVector assertions = new ASTVector(Context, Native.Z3_solver_get_assertions(Context.nCtx, NativeObject));
                 return assertions.ToBoolExprArray();
             }
         }

◆ BacktrackLevel

uint BacktrackLevel

getset

Backtrack level that can be adjusted by conquer process

Definition at line 414 of file Solver.cs.

414 { get; set; }

Referenced by Solver.Cube().

◆ CubeVariables

BoolExpr [] CubeVariables

getset

Variables available and returned by the cuber.

Definition at line 419 of file Solver.cs.

419 { get; set; }

Referenced by Solver.Cube().

◆ Help

string Help

get

A string that describes all available solver parameters.

Definition at line 36 of file Solver.cs.

         {
             get
             {
  
                 return Native.Z3_solver_get_help(Context.nCtx, NativeObject);
             }
         }

◆ Model

Model Model

get

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 351 of file Solver.cs.

         {
             get
             {
                 IntPtr x = Native.Z3_solver_get_model(Context.nCtx, NativeObject);
                 if (x == IntPtr.Zero)
                     return null;
                 else
                     return new Model(Context, x);
             }
         }

◆ NumAssertions

uint NumAssertions

get

The number of assertions in the solver.

Definition at line 245 of file Solver.cs.

         {
             get
             {
                 ASTVector assertions = new ASTVector(Context, Native.Z3_solver_get_assertions(Context.nCtx, NativeObject));
                 return assertions.Size;
             }
         }

◆ NumScopes

uint NumScopes

get

The current number of backtracking points (scopes).

See also: Pop, Push

Definition at line 116 of file Solver.cs.

         {
             get { return Native.Z3_solver_get_num_scopes(Context.nCtx, NativeObject); }
         }

◆ ParameterDescriptions

ParamDescrs ParameterDescriptions

get

Retrieves parameter descriptions for solver.

Definition at line 105 of file Solver.cs.

         {
             get { return new ParamDescrs(Context, Native.Z3_solver_get_param_descrs(Context.nCtx, NativeObject)); }
         }

◆ Parameters

Params Parameters

set

Sets the solver parameters.

Definition at line 48 of file Solver.cs.

         {
             set
             {
                 Debug.Assert(value != null);
  
                 Context.CheckContextMatch(value);
                 Native.Z3_solver_set_params(Context.nCtx, NativeObject, value.NativeObject);
             }
         }

Referenced by Solver.Set().

◆ Proof

Expr Proof

get

The proof 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 UNSATISFIABLE, or if proof production is disabled.

Definition at line 370 of file Solver.cs.

         {
             get
             {
                 IntPtr x = Native.Z3_solver_get_proof(Context.nCtx, NativeObject);
                 if (x == IntPtr.Zero)
                     return null;
                 else
                     return Expr.Create(Context, x);
             }
         }

◆ ReasonUnknown

string ReasonUnknown

get

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

Definition at line 403 of file Solver.cs.

         {
             get
             {
  
                 return Native.Z3_solver_get_reason_unknown(Context.nCtx, NativeObject);
             }
         }

◆ Statistics

Statistics Statistics

get

Solver statistics.

Definition at line 468 of file Solver.cs.

         {
             get
             {
  
                 return new Statistics(Context, Native.Z3_solver_get_statistics(Context.nCtx, NativeObject));
             }
         }

◆ Units

BoolExpr [] Units

get

Currently inferred units.

Definition at line 270 of file Solver.cs.

         {
             get
             {
  
                 ASTVector assertions = new ASTVector(Context, Native.Z3_solver_get_units(Context.nCtx, NativeObject));
                 return assertions.ToBoolExprArray();
             }
         }

◆ UnsatCore

BoolExpr [] UnsatCore

get

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 390 of file Solver.cs.

         {
             get
             {
  
                 ASTVector core = new ASTVector(Context, Native.Z3_solver_get_unsat_core(Context.nCtx, NativeObject));                
                 return core.ToBoolExprArray();
             }
         }

Data Structures

Public Member Functions

Properties

Detailed Description

Member Function Documentation

◆ Add() [1/2]

◆ Add() [2/2]

◆ Assert()

◆ AssertAndTrack() [1/2]

◆ AssertAndTrack() [2/2]

◆ Check() [1/2]

◆ Check() [2/2]

◆ Consequences()

◆ Cube()

◆ FromFile()

◆ FromString()

◆ ImportModelConverter()

◆ Pop()

◆ Push()

◆ Reset()

◆ Set() [1/10]

◆ Set() [2/10]

◆ Set() [3/10]

◆ Set() [4/10]

◆ Set() [5/10]

◆ Set() [6/10]

◆ Set() [7/10]

◆ Set() [8/10]

◆ Set() [9/10]

◆ Set() [10/10]

◆ ToString()

◆ Translate()

Property Documentation

◆ Assertions

◆ BacktrackLevel

◆ CubeVariables

◆ Help

◆ Model

◆ NumAssertions

◆ NumScopes

◆ ParameterDescriptions

◆ Parameters

◆ Proof

◆ ReasonUnknown

◆ Statistics

◆ Units

◆ UnsatCore