object Param
- Alphabetic
- By Inheritance
- Param
- AnyRef
- Any
- Hide All
- Show All
- Public
- Protected
Value Members
- final def !=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- final def ##: Int
- Definition Classes
- AnyRef → Any
- final def ==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- final def asInstanceOf[T0]: T0
- Definition Classes
- Any
- def clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.CloneNotSupportedException]) @HotSpotIntrinsicCandidate() @native()
- final def eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- def equals(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef → Any
- final def getClass(): Class[_ <: AnyRef]
- Definition Classes
- AnyRef → Any
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- def hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- final def isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- final def ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- final def notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- final def notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- final def synchronized[T0](arg0: => T0): T0
- Definition Classes
- AnyRef
- def toString(): String
- Definition Classes
- AnyRef → Any
- final def wait(arg0: Long, arg1: Int): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException])
- final def wait(arg0: Long): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException]) @native()
- final def wait(): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException])
- case object ABBREV_LABELS extends Param with Product with Serializable
- case object ADT_MEASURE extends Param with Product with Serializable
- case object APPLY_BLOCKED_TASKS extends Param with Product with Serializable
Even apply formulas that have been blocked, as last steps in a proof.
Even apply formulas that have been blocked, as last steps in a proof. this can be necessary in order to generate genuine models (
ModelSearchProver
) - case object ASSERTIONS extends Param with Product with Serializable
- case object BOOLEAN_FUNCTIONS_AS_PREDICATES extends Param with Product with Serializable
- case object CLAUSIFIER extends Param with Product with Serializable
- case object COMPUTE_MODEL extends Param with Product with Serializable
- case object COMPUTE_UNSAT_CORE extends Param with Product with Serializable
- case object CONSTRAINT_SIMPLIFIER extends Param with Product with Serializable
- case object COUNTER_TIMEOUT extends Param with Product with Serializable
- object ClausifierOptions extends Enumeration
- object ConstraintSimplifierOptions extends Enumeration
- case object DNF_CONSTRAINTS extends Param with Product with Serializable
Turn ground constraints into disjunctive normal form
- case object ELIMINATE_INTERPOLANT_QUANTIFIERS extends Param with Product with Serializable
- case object EQUIV_INLINING extends Param with Product with Serializable
During pre-processing, inline equivalences of the form
p <-> f
, for some Boolean variable p. - case object FULL_HELP extends Param with Product with Serializable
- case object FULL_SPLITTING extends Param with Product with Serializable
Even split propositional formulae that do not contain quantifiers or eliminated constants
- case object FUNCTIONAL_PREDICATES extends Param with Product with Serializable
- case object FUNCTION_GC extends Param with Product with Serializable
- object FunctionGCOptions extends Enumeration
- case object GARBAGE_COLLECTED_FUNCTIONS extends Param with Product with Serializable
- case object GENERATE_TOTALITY_AXIOMS extends Param with Product with Serializable
- case object IGNORE_QUANTIFIERS extends Param with Product with Serializable
Ignore universal quantifiers in a problem that would require free variables, by converting the quantifiers to existential ones.
- case object INCREMENTAL extends Param with Product with Serializable
- case object INLINE_SIZE_LIMIT extends Param with Product with Serializable
Maximum size of function bodies to inline.
- case object INPUT_FORMAT extends Param with Product with Serializable
- object InputFormat extends Enumeration
- case object LOGO extends Param with Product with Serializable
- case object LOG_BACKTRACKING extends LOG_FLAG with Product with Serializable
- case object LOG_COUNTERS extends LOG_FLAG with Product with Serializable
- case object LOG_COUNTERS_CONT extends LOG_FLAG with Product with Serializable
- case object LOG_LEMMAS extends LOG_FLAG with Product with Serializable
- case object LOG_LEVEL extends Param with Product with Serializable
Enable logging to stderr for specific aspects of the system.
- case object LOG_SPLITS extends LOG_FLAG with Product with Serializable
- case object LOG_STATS extends LOG_FLAG with Product with Serializable
- case object LOG_TASKS extends LOG_FLAG with Product with Serializable
- case object MAKE_QUERIES_PARTIAL extends Param with Product with Serializable
Use heuristics to distinguish between constructor and query function symbols, and make the latter ones partial
- case object MATCHING_BASE_PRIORITY extends Param with Product with Serializable
- object MGCFormatOptions extends Enumeration
- case object MGC_FORMAT extends Param with Product with Serializable
- case object MODEL_GENERATION extends Param with Product with Serializable
- case object MOST_GENERAL_CONSTRAINT extends Param with Product with Serializable
- case object MUL_PROCEDURE extends Param with Product with Serializable
- object MulProcedure extends Enumeration
- case object NEG_SOLVING extends Param with Product with Serializable
Options for solving problems in positive or negated version
- case object NONLINEAR_SPLITTING extends Param with Product with Serializable
- object NegSolvingOptions extends Enumeration
- object NonLinearSplitting extends Enumeration
- case object PORTFOLIO extends Param with Product with Serializable
Portfolios optimised for particular domains
- case object PORTFOLIO_THREAD_NUM extends Param with Product with Serializable
- case object POS_UNIT_RESOLUTION extends Param with Product with Serializable
Resolve negative predicate literals in clauses with positive facts
- case object PREDICATE_MATCH_CONFIG extends Param with Product with Serializable
- case object PRINT_CERTIFICATE extends Param with Product with Serializable
- case object PRINT_DOT_CERTIFICATE_FILE extends Param with Product with Serializable
- case object PRINT_RUNTIME extends Param with Product with Serializable
- case object PRINT_SMT_FILE extends Param with Product with Serializable
- case object PRINT_TPTP_FILE extends Param with Product with Serializable
- case object PRINT_TREE extends Param with Product with Serializable
- case object PROOF_CONSTRUCTION extends Param with Product with Serializable
- case object PROOF_CONSTRUCTION_GLOBAL extends Param with Product with Serializable
- case object PROOF_SIMPLIFICATION extends Param with Product with Serializable
- object ProofConstructionOptions extends Enumeration
Globally, we can also choose to construct proofs depending on whether interpolation specs were given (the default)
- case object QUIET extends Param with Product with Serializable
- case object RANDOM_DATA_SOURCE extends Param with Product with Serializable
- case object RANDOM_SEED extends Param with Product with Serializable
- case object REAL_RAT_SATURATION_ROUNDS extends Param with Product with Serializable
- case object REDUCER_PLUGIN extends Param with Product with Serializable
- case object REDUCER_SETTINGS extends Param with Product with Serializable
- case object REVERSE_FUNCTIONALITY_PROPAGATION extends Param with Product with Serializable
- case object SEQ_THEORY_DESC extends Param with Product with Serializable
- case object SIMPLIFY_CONSTRAINTS extends Param with Product with Serializable
- case object SINGLE_INSTANTIATION_PREDICATES extends Param with Product with Serializable
- case object SMTParserExtraTheories extends Param with Product with Serializable
- case object STDIN extends Param with Product with Serializable
- case object STRENGTHEN_TREE_FOR_SIDE_CONDITIONS extends Param with Product with Serializable
Represent numeric side conditions (inequalities) in quantified formulas using the
StrengthenTree
constructor - case object STRING_ESCAPES extends Param with Product with Serializable
Accept an extended set of escape sequences in strings: \\, \x, \a, \b, \f, \n, \r, \t, \v.
Accept an extended set of escape sequences in strings: \\, \x, \a, \b, \f, \n, \r, \t, \v. Without this option, only the official SMT-LIB escapes are accepted.
- case object STRING_THEORY_DESC extends Param with Product with Serializable
- case object SYMBOL_WEIGHTS extends Param with Product with Serializable
- case object THEORY_PLUGIN extends Param with Product with Serializable
- case object TIGHT_FUNCTION_SCOPES extends Param with Product with Serializable
- case object TIMEOUT extends Param with Product with Serializable
- case object TIMEOUT_PER extends Param with Product with Serializable
- case object TRACE_CONSTRAINT_SIMPLIFIER extends Param with Product with Serializable
- case object TRIGGERS_IN_CONJECTURE extends Param with Product with Serializable
- case object TRIGGER_GENERATION extends Param with Product with Serializable
- case object TRIGGER_STRATEGY extends Param with Product with Serializable
- object TriggerGenerationOptions extends Enumeration
- object TriggerStrategyOptions extends Enumeration
- case object USE_FUNCTIONAL_CONSISTENCY_THEORY extends Param with Product with Serializable
Use the
FunctionalConsistency
dummy theory to represent applications of functionality in proofs. - case object VERSION extends Param with Product with Serializable
- case object WARM_UP extends Param with Product with Serializable
Before solving any actual tasks, run some other problems for warmup purposes.
Before solving any actual tasks, run some other problems for warmup purposes. This will reduce the effect of a JVM cold-start.
Deprecated Value Members
- def finalize(): Unit
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.Throwable]) @Deprecated
- Deprecated
(Since version 9)