Inheritance diagram for Solver:

Public Member Functions
String	getHelp ()

void	setParameters (Params value)

ParamDescrs	getParameterDescriptions ()

int	getNumScopes ()

void	push ()

void	pop ()

void	pop (int n)

void	reset ()

void	interrupt ()

void	add (Expr< BoolSort >... constraints)

void	assertAndTrack (Expr< BoolSort >[] constraints, Expr< BoolSort >[] ps)

void	assertAndTrack (Expr< BoolSort > constraint, Expr< BoolSort > p)

void	fromFile (String file)
	Load solver assertions from a file.

void	fromString (String str)
	Load solver assertions from a string.

int	getNumAssertions ()

BoolExpr[]	getAssertions ()

final Status	check (Expr< BoolSort >... assumptions)

Status	check ()

Status	getConsequences (Expr< BoolSort >[] assumptions, Expr<?>[] variables, List< Expr< BoolSort > > consequences)

Model	getModel ()

Expr<?>	getProof ()

BoolExpr[]	getUnsatCore ()

BoolExpr[]	getUnits ()

BoolExpr[]	getNonUnits ()

BoolExpr[]	getTrail ()

String	getReasonUnknown ()

int[]	getTrailLevels ()

java.util.Iterator< BoolExpr[]>	cube (Expr<?>[] vars, int cutoff)

Expr<?>	congruenceRoot (Expr<?> t)

Expr<?>	congruenceNext (Expr<?> t)

Expr<?>	congruenceExplain (Expr<?> a, Expr<?> b)

void	solveFor (Expr<?>[] variables, Expr<?>[] terms, BoolExpr[] guards)

void	setInitialValue (Expr<?> var, Expr<?> value)

void	importModelConverter (Solver src)

Solver	translate (Context ctx)

Solver	addSimplifier (Simplifier simplifier)

String	toDimacs (boolean includeNames)

Statistics	getStatistics ()

String	toString ()

Additional Inherited Members
Static Public Member Functions inherited from Z3Object
static long[]	arrayToNative (Z3Object[] a)

static int	arrayLength (Z3Object[] a)

Detailed Description

Solvers.

Definition at line 30 of file Solver.java.

Member Function Documentation

◆ add()

void add ( Expr< BoolSort >... constraints )

inline

Assert a multiple constraints into the solver.

Exceptions

Z3Exception

Definition at line 128 of file Solver.java.

    {
        getContext().checkContextMatch(constraints);
        for (Expr<BoolSort> a : constraints)
        {
            Native.solverAssert(getContext().nCtx(), getNativeObject(),
                    a.getNativeObject());
        }
    }

Referenced by Solver.__iadd__().

◆ addSimplifier()

Solver addSimplifier ( Simplifier simplifier )

inline

Create a new solver with pre-processing simplification attached.

Parameters

simplifier The simplifier to attach for pre-processing

Returns: A new solver with the simplifier applied

Definition at line 578 of file Solver.java.

    {
        return new Solver(getContext(), Native.solverAddSimplifier(
                getContext().nCtx(), getNativeObject(), simplifier.getNativeObject()));
    }

◆ assertAndTrack() [1/2]

void assertAndTrack	(	Expr< BoolSort >	constraint,
		Expr< BoolSort >	p
	)

inline

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

Remarks: This API is an alternative to check 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 and the Boolean literals provided using check with assumptions.

See also: Solver::check; Solver::assertAndTrack

Definition at line 184 of file Solver.java.

    {
        getContext().checkContextMatch(constraint);
        getContext().checkContextMatch(p);
 
        Native.solverAssertAndTrack(getContext().nCtx(), getNativeObject(),
                constraint.getNativeObject(), p.getNativeObject());
    }

◆ assertAndTrack() [2/2]

void assertAndTrack	(	Expr< BoolSort >[]	constraints,
		Expr< BoolSort >[]	ps
	)

inline

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

Remarks: This API is an alternative to check 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 and the Boolean literals provided using check with assumptions.

See also: Solver::check; Solver::assertAndTrack

Definition at line 155 of file Solver.java.

    {
        getContext().checkContextMatch(constraints);
        getContext().checkContextMatch(ps);
        if (constraints.length != ps.length) {
            throw new Z3Exception("Argument size mismatch");
        }
 
        for (int i = 0; i < constraints.length; i++) {
            Native.solverAssertAndTrack(getContext().nCtx(), getNativeObject(),
                constraints[i].getNativeObject(), ps[i].getNativeObject());
        }
    }

◆ check() [1/2]

Status check ( )

inline

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

See also: Solver::getModel; Solver::getUnsatCore; Solver::getProof

Definition at line 262 of file Solver.java.

    {
        return check((Expr[]) null);
    }

◆ check() [2/2]

final Status check ( Expr< BoolSort >... assumptions )

inline

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

See also: Solver::getModel; Solver::getUnsatCore; Solver::getProof

Definition at line 240 of file Solver.java.

    {
        Z3_lbool r;
        if (assumptions == null) {
            r = Z3_lbool.fromInt(Native.solverCheck(getContext().nCtx(),
                getNativeObject()));
        } else {
            r = Z3_lbool.fromInt(Native.solverCheckAssumptions(getContext()
                .nCtx(), getNativeObject(), assumptions.length, AST
                .arrayToNative(assumptions)));
        }
        return lboolToStatus(r);
    }

◆ congruenceExplain()

Expr<?> congruenceExplain	(	Expr<?>	a,
		Expr<?>	b
	)

inline

Return an explanation for why two expressions are congruent.

Parameters

a	First expression
b	Second expression

Returns: An expression explaining the congruence between a and b

Exceptions

Z3Exception

Definition at line 508 of file Solver.java.

    {
        getContext().checkContextMatch(a);
        getContext().checkContextMatch(b);
        return Expr.create(getContext(),
            Native.solverCongruenceExplain(getContext().nCtx(), getNativeObject(),
                a.getNativeObject(), b.getNativeObject()));
    }

◆ congruenceNext()

Expr<?> congruenceNext ( Expr<?> t )

inline

Return the next element in the congruence class of the given expression. The congruence class forms a circular linked list.

Parameters

t	The expression to find the next congruent expression for

Returns: The next expression in the congruence class

Exceptions

Z3Exception

Definition at line 493 of file Solver.java.

    {
        getContext().checkContextMatch(t);
        return Expr.create(getContext(),
            Native.solverCongruenceNext(getContext().nCtx(), getNativeObject(), t.getNativeObject()));
    }

◆ congruenceRoot()

Expr<?> congruenceRoot ( Expr<?> t )

inline

Return the congruence class representative of the given expression. This is useful for querying the equality reasoning performed by the solver.

Parameters

t	The expression to find the congruence root for

Returns: The root expression of the congruence class

Exceptions

Z3Exception

Definition at line 478 of file Solver.java.

    {
        getContext().checkContextMatch(t);
        return Expr.create(getContext(),
            Native.solverCongruenceRoot(getContext().nCtx(), getNativeObject(), t.getNativeObject()));
    }

◆ cube()

java.util.Iterator< BoolExpr[]> cube	(	Expr<?>[]	vars,
		int	cutoff
	)

inline

Return a sequence of cubes (conjunctions of literals) for partitioning the search space. Each cube represents a partial assignment that can be used as a starting point for parallel solving. This is primarily useful for cube-and-conquer parallel SAT solving strategies, where different cubes can be solved independently by different workers. The iterator yields cubes until the search space is exhausted.

Parameters

vars	Optional array of variables to use as initial cube variables. If null, solver decides.
cutoff	Backtrack level cutoff for cube generation

Returns: Iterator over arrays of Boolean expressions representing cubes

Exceptions

Z3Exception

Definition at line 425 of file Solver.java.

    {
        ASTVector cubeVars = new ASTVector(getContext());
        if (vars != null) {
            for (Expr<?> v : vars) {
                cubeVars.push(v);
            }
        }
        
        return new java.util.Iterator<BoolExpr[]>() {
            private BoolExpr[] nextCube = computeNext();
            
            private BoolExpr[] computeNext() {
                ASTVector result = new ASTVector(getContext(), 
                    Native.solverCube(getContext().nCtx(), getNativeObject(), 
                                     cubeVars.getNativeObject(), cutoff));
                BoolExpr[] cube = result.ToBoolExprArray();
                
                // Check for termination conditions
                if (cube.length == 1 && cube[0].isFalse()) {
                    return null; // No more cubes
                }
                if (cube.length == 0) {
                    return null; // Search space exhausted
                }
                return cube;
            }
            
            @Override
            public boolean hasNext() {
                return nextCube != null;
            }
            
            @Override
            public BoolExpr[] next() {
                if (nextCube == null) {
                    throw new java.util.NoSuchElementException();
                }
                BoolExpr[] current = nextCube;
                nextCube = computeNext();
                return current;
            }
        };
    }

◆ fromFile()

void fromFile ( String file )

inline

Load solver assertions from a file.

Definition at line 196 of file Solver.java.

    {
        Native.solverFromFile(getContext().nCtx(), getNativeObject(), file);    
    }

◆ fromString()

void fromString ( String str )

inline

Load solver assertions from a string.

Definition at line 204 of file Solver.java.

    {
        Native.solverFromString(getContext().nCtx(), getNativeObject(), str);   
    }

◆ getAssertions()

BoolExpr[] getAssertions ( )

inline

The set of asserted formulas.

Exceptions

Z3Exception

Definition at line 226 of file Solver.java.

    {
        ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(getContext().nCtx(), getNativeObject()));
        return assrts.ToBoolExprArray();
    }

◆ getConsequences()

Status getConsequences	(	Expr< BoolSort >[]	assumptions,
		Expr<?>[]	variables,
		List< Expr< BoolSort > >	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.

Definition at line 278 of file Solver.java.

    {
        ASTVector result = new ASTVector(getContext());
        ASTVector asms = new ASTVector(getContext());
        ASTVector vars = new ASTVector(getContext());
        for (Expr<BoolSort> asm : assumptions) asms.push(asm);
        for (Expr<?> v : variables) vars.push(v);
        int r = Native.solverGetConsequences(getContext().nCtx(), getNativeObject(), asms.getNativeObject(), vars.getNativeObject(), result.getNativeObject());
        for (int i = 0; i < result.size(); ++i) consequences.add((BoolExpr) Expr.create(getContext(), result.get(i).getNativeObject()));
        return lboolToStatus(Z3_lbool.fromInt(r));
    }

◆ getHelp()

String getHelp ( )

inline

A string that describes all available solver parameters.

Definition at line 34 of file Solver.java.

    {
        return Native.solverGetHelp(getContext().nCtx(), getNativeObject());
    }

◆ getModel()

Model getModel ( )

inline

The model of the last Check. Remarks: The result is null if Check was not invoked before, if its results was not SATISFIABLE, or if model production is not enabled.

Exceptions

Z3Exception

Definition at line 300 of file Solver.java.

    {
        long x = Native.solverGetModel(getContext().nCtx(), getNativeObject());
        if (x == 0) {
            return null;
        } else {
            return new Model(getContext(), x);
        }
    }

◆ getNonUnits()

BoolExpr[] getNonUnits ( )

inline

Retrieve non-unit atomic formulas in the solver state. Remarks: This retrieves atomic formulas that are not units after a check call.

Returns: An array of Boolean expressions representing the non-unit formulas

Exceptions

Z3Exception

Definition at line 366 of file Solver.java.

    {
        ASTVector nonUnits = new ASTVector(getContext(), Native.solverGetNonUnits(getContext().nCtx(), getNativeObject()));
        return nonUnits.ToBoolExprArray();
    }

◆ getNumAssertions()

int getNumAssertions ( )

inline

The number of assertions in the solver.

Exceptions

Z3Exception

Definition at line 215 of file Solver.java.

    {
        ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(getContext().nCtx(), getNativeObject()));
        return assrts.size();
    }

◆ getNumScopes()

int getNumScopes ( )

inline

The current number of backtracking points (scopes).

See also: Solver::pop; Solver::push

Definition at line 67 of file Solver.java.

    {
        return Native
                .solverGetNumScopes(getContext().nCtx(), getNativeObject());
    }

◆ getParameterDescriptions()

ParamDescrs getParameterDescriptions ( )

inline

Retrieves parameter descriptions for solver.

Exceptions

Z3Exception

Definition at line 56 of file Solver.java.

    {
        return new ParamDescrs(getContext(), Native.solverGetParamDescrs(
                getContext().nCtx(), getNativeObject()));
    }

◆ getProof()

Expr<?> getProof ( )

inline

The proof of the last Check. Remarks: The result is null if Check was not invoked before, if its results was not UNSATISFIABLE, or if proof production is disabled.

Exceptions

Z3Exception

Definition at line 319 of file Solver.java.

    {
        long x = Native.solverGetProof(getContext().nCtx(), getNativeObject());
        if (x == 0) {
            return null;
        } else {
            return Expr.create(getContext(), x);
        }
    }

◆ getReasonUnknown()

String getReasonUnknown ( )

inline

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

Definition at line 391 of file Solver.java.

    {
        return Native.solverGetReasonUnknown(getContext().nCtx(),
                getNativeObject());
    }

◆ getStatistics()

Statistics getStatistics ( )

inline

Solver statistics.

Exceptions

Z3Exception

Definition at line 600 of file Solver.java.

    {
        return new Statistics(getContext(), Native.solverGetStatistics(
                getContext().nCtx(), getNativeObject()));
    }

◆ getTrail()

BoolExpr[] getTrail ( )

inline

Retrieve the solver decision trail. Remarks: This retrieves the trail of decisions made by the solver after a check call. The trail represents the sequence of Boolean literals (decisions and propagations) in the order they were assigned.

Returns: An array of Boolean expressions representing the decision trail

Exceptions

Z3Exception

Definition at line 381 of file Solver.java.

    {
        ASTVector trail = new ASTVector(getContext(), Native.solverGetTrail(getContext().nCtx(), getNativeObject()));
        return trail.ToBoolExprArray();
    }

◆ getTrailLevels()

int[] getTrailLevels ( )

inline

Retrieve the decision levels for each literal in the solver's trail after a check call. The trail contains Boolean literals (decisions and propagations) in the order they were assigned. The returned array has one entry per trail literal, indicating at which decision level it was assigned.

Returns: An array where element i contains the decision level for the i-th trail literal

Exceptions

Z3Exception

Definition at line 405 of file Solver.java.

    {
        ASTVector trailVector = new ASTVector(getContext(), Native.solverGetTrail(getContext().nCtx(), getNativeObject()));
        int[] levels = new int[trailVector.size()];
        Native.solverGetLevels(getContext().nCtx(), getNativeObject(), trailVector.getNativeObject(), trailVector.size(), levels);
        return levels;
    }

◆ getUnits()

BoolExpr[] getUnits ( )

inline

Retrieve currently inferred units. Remarks: This retrieves the set of literals that the solver has inferred at the current decision level after a check call.

Returns: An array of Boolean expressions representing the inferred units

Exceptions

Z3Exception

Definition at line 353 of file Solver.java.

    {
        ASTVector units = new ASTVector(getContext(), Native.solverGetUnits(getContext().nCtx(), getNativeObject()));
        return units.ToBoolExprArray();
    }

◆ getUnsatCore()

BoolExpr[] getUnsatCore ( )

inline

The unsat core of the last Check. Remarks: 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.

Exceptions

Z3Exception

Definition at line 338 of file Solver.java.

    {
 
        ASTVector core = new ASTVector(getContext(), Native.solverGetUnsatCore(getContext().nCtx(), getNativeObject()));        
        return core.ToBoolExprArray();
    }

◆ importModelConverter()

void importModelConverter ( Solver src )

inline

Import model converter from other solver.

Parameters

src	The solver to import the model converter from

Definition at line 559 of file Solver.java.

    {
        Native.solverImportModelConverter(getContext().nCtx(), src.getNativeObject(), getNativeObject());
    }

◆ interrupt()

void interrupt ( )

inline

Interrupt the execution of the solver object. Remarks: This ensures that the interrupt applies only to the given solver object and it applies only if it is running.

Definition at line 118 of file Solver.java.

    {
        Native.solverInterrupt(getContext().nCtx(), getNativeObject());
    }

◆ pop() [1/2]

void pop ( )

inline

Backtracks one backtracking point. Remarks: .

Definition at line 86 of file Solver.java.

    {
        pop(1);
    }

Referenced by Solver.__exit__().

◆ pop() [2/2]

void pop ( int n )

inline

Backtracks n backtracking points. Remarks: Note that an exception is thrown if n is not smaller than NumScopes

See also: Solver::push

Definition at line 98 of file Solver.java.

    {
        Native.solverPop(getContext().nCtx(), getNativeObject(), n);
    }

Referenced by Solver.__exit__().

◆ push()

void push ( )

inline

Creates a backtracking point.

See also: Solver::pop

Definition at line 77 of file Solver.java.

    {
        Native.solverPush(getContext().nCtx(), getNativeObject());
    }

Referenced by Solver.__enter__().

◆ reset()

void reset ( )

inline

Resets the Solver. Remarks: This removes all assertions from the solver.

Definition at line 108 of file Solver.java.

    {
        Native.solverReset(getContext().nCtx(), getNativeObject());
    }

◆ setInitialValue()

void setInitialValue	(	Expr<?>	var,
		Expr<?>	value
	)

inline

Set an initial value for a variable to guide the solver's search heuristics. This can improve performance when good initial values are known for the problem domain.

Parameters

var	The variable to set an initial value for
value	The initial value for the variable

Exceptions

Z3Exception

Definition at line 546 of file Solver.java.

    {
        getContext().checkContextMatch(var);
        getContext().checkContextMatch(value);
        Native.solverSetInitialValue(getContext().nCtx(), getNativeObject(), 
                                     var.getNativeObject(), value.getNativeObject());
    }

◆ setParameters()

void setParameters ( Params value )

inline

Sets the solver parameters.

Exceptions

Z3Exception

Definition at line 44 of file Solver.java.

    {
        getContext().checkContextMatch(value);
        Native.solverSetParams(getContext().nCtx(), getNativeObject(),
                value.getNativeObject());
    }

◆ solveFor()

void solveFor	(	Expr<?>[]	variables,
		Expr<?>[]	terms,
		BoolExpr[]	guards
	)

inline

Solve constraints for given variables, replacing their occurrences by terms. Guards are used to guard substitutions.

Parameters

variables	Array of variables to solve for
terms	Array of terms to substitute for the variables
guards	Array of Boolean guards for the substitutions

Exceptions

Z3Exception

Definition at line 526 of file Solver.java.

    {
        ASTVector vars = new ASTVector(getContext());
        ASTVector termVec = new ASTVector(getContext());
        ASTVector guardVec = new ASTVector(getContext());
        for (Expr<?> v : variables) vars.push(v);
        for (Expr<?> t : terms) termVec.push(t);
        for (BoolExpr g : guards) guardVec.push(g);
        Native.solverSolveFor(getContext().nCtx(), getNativeObject(),
            vars.getNativeObject(), termVec.getNativeObject(), guardVec.getNativeObject());
    }

◆ toDimacs()

String toDimacs ( boolean includeNames )

inline

Convert the solver's Boolean formula to DIMACS CNF format.

Parameters

includeNames If true, include variable names in the DIMACS output

Returns: A string containing the DIMACS CNF representation

Definition at line 590 of file Solver.java.

    {
        return Native.solverToDimacsString(getContext().nCtx(), getNativeObject(), includeNames);
    }

◆ toString()

String toString ( )

inline

A string representation of the solver.

Definition at line 610 of file Solver.java.

    {
        return Native
                .solverToString(getContext().nCtx(), getNativeObject());
    }

◆ translate()

Solver translate ( Context ctx )

inline

Create a clone of the current solver with respect toctx.

Definition at line 567 of file Solver.java.

    {
        return new Solver(ctx, Native.solverTranslate(getContext().nCtx(), getNativeObject(), ctx.nCtx()));
    }

Referenced by AstRef.__copy__(), Goal.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), ModelRef.__copy__(), Goal.__deepcopy__(), AstVector.__deepcopy__(), FuncInterp.__deepcopy__(), and ModelRef.__deepcopy__().

Public Member Functions

Additional Inherited Members

Detailed Description

Member Function Documentation

◆ add()

◆ addSimplifier()

◆ assertAndTrack() [1/2]

◆ assertAndTrack() [2/2]

◆ check() [1/2]

◆ check() [2/2]

◆ congruenceExplain()

◆ congruenceNext()

◆ congruenceRoot()

◆ cube()

◆ fromFile()

◆ fromString()

◆ getAssertions()

◆ getConsequences()

◆ getHelp()

◆ getModel()

◆ getNonUnits()

◆ getNumAssertions()

◆ getNumScopes()

◆ getParameterDescriptions()

◆ getProof()

◆ getReasonUnknown()

◆ getStatistics()

◆ getTrail()

◆ getTrailLevels()

◆ getUnits()

◆ getUnsatCore()

◆ importModelConverter()

◆ interrupt()

◆ pop() [1/2]

◆ pop() [2/2]

◆ push()

◆ reset()

◆ setInitialValue()

◆ setParameters()

◆ solveFor()

◆ toDimacs()

◆ toString()

◆ translate()