Package org.sosy_lab.java_smt.api
Enum SolverContext.ProverOptions
- java.lang.Object
-
- java.lang.Enum<SolverContext.ProverOptions>
-
- org.sosy_lab.java_smt.api.SolverContext.ProverOptions
-
- All Implemented Interfaces:
Serializable
,Comparable<SolverContext.ProverOptions>
- Enclosing interface:
- SolverContext
public static enum SolverContext.ProverOptions extends Enum<SolverContext.ProverOptions>
Options for the prover environment.
-
-
Enum Constant Summary
Enum Constants Enum Constant Description ENABLE_SEPARATION_LOGIC
Whether the solver should enable support for formulae build in SL theory.GENERATE_ALL_SAT
Whether the solver should allow to query all satisfying assignments for satisfiable formulas.GENERATE_MODELS
Whether the solver should generate models (i.e., satisfying assignments) for satisfiable formulas.GENERATE_UNSAT_CORE
Whether the solver should generate an unsat core for unsatisfiable formulas.GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS
Whether the solver should generate an unsat core for unsatisfiable formulas only over the assumptions explicitly passed to the solver.
-
Method Summary
All Methods Static Methods Concrete Methods Modifier and Type Method Description static SolverContext.ProverOptions
valueOf(String name)
Returns the enum constant of this type with the specified name.static SolverContext.ProverOptions[]
values()
Returns an array containing the constants of this enum type, in the order they are declared.
-
-
-
Enum Constant Detail
-
GENERATE_MODELS
public static final SolverContext.ProverOptions GENERATE_MODELS
Whether the solver should generate models (i.e., satisfying assignments) for satisfiable formulas.
-
GENERATE_ALL_SAT
public static final SolverContext.ProverOptions GENERATE_ALL_SAT
Whether the solver should allow to query all satisfying assignments for satisfiable formulas.
-
GENERATE_UNSAT_CORE
public static final SolverContext.ProverOptions GENERATE_UNSAT_CORE
Whether the solver should generate an unsat core for unsatisfiable formulas. Unsat core is generated over all formulas asserted withBasicProverEnvironment.addConstraint(BooleanFormula)
orBasicProverEnvironment.push(BooleanFormula)
.
-
GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS
public static final SolverContext.ProverOptions GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS
Whether the solver should generate an unsat core for unsatisfiable formulas only over the assumptions explicitly passed to the solver.
-
ENABLE_SEPARATION_LOGIC
public static final SolverContext.ProverOptions ENABLE_SEPARATION_LOGIC
Whether the solver should enable support for formulae build in SL theory.
-
-
Method Detail
-
values
public static SolverContext.ProverOptions[] values()
Returns an array containing the constants of this enum type, in the order they are declared. This method may be used to iterate over the constants as follows:for (SolverContext.ProverOptions c : SolverContext.ProverOptions.values()) System.out.println(c);
- Returns:
- an array containing the constants of this enum type, in the order they are declared
-
valueOf
public static SolverContext.ProverOptions valueOf(String name)
Returns the enum constant of this type with the specified name. The string must match exactly an identifier used to declare an enum constant in this type. (Extraneous whitespace characters are not permitted.)- Parameters:
name
- the name of the enum constant to be returned.- Returns:
- the enum constant with the specified name
- Throws:
IllegalArgumentException
- if this enum type has no constant with the specified nameNullPointerException
- if the argument is null
-
-