Param

final def !=(arg0: Any): Boolean

final def ##(): Int

final def ==(arg0: Any): Boolean

object ABBREV_LABELS extends Param with Product with Serializable

object ADT_MEASURE extends Param with Product with Serializable

object APPLY_BLOCKED_TASKS extends Param with Product with Serializable

Even apply formulas that have been blocked, as last steps in a proof.

object ASSERTIONS extends Param with Product with Serializable

object BOOLEAN_FUNCTIONS_AS_PREDICATES extends Param with Product with Serializable

object CLAUSIFIER extends Param with Product with Serializable

object COMPUTE_MODEL extends Param with Product with Serializable

object COMPUTE_UNSAT_CORE extends Param with Product with Serializable

object CONSTRAINT_SIMPLIFIER extends Param with Product with Serializable

object COUNTER_TIMEOUT extends Param with Product with Serializable

object ClausifierOptions extends Enumeration

object ConstraintSimplifierOptions extends Enumeration

object DNF_CONSTRAINTS extends Param with Product with Serializable

Turn ground constraints into disjunctive normal form

object ELIMINATE_INTERPOLANT_QUANTIFIERS extends Param with Product with Serializable

object EQUIV_INLINING extends Param with Product with Serializable

During pre-processing, inline equivalences of the form p <-> f, for some Boolean variable p.

object FULL_HELP extends Param with Product with Serializable

object FULL_SPLITTING extends Param with Product with Serializable

Even split propositional formulae that do not contain quantifiers or eliminated constants

object FUNCTIONAL_PREDICATES extends Param with Product with Serializable

object FUNCTION_GC extends Param with Product with Serializable

object FunctionGCOptions extends Enumeration

object GARBAGE_COLLECTED_FUNCTIONS extends Param with Product with Serializable

object GENERATE_TOTALITY_AXIOMS extends Param with Product with Serializable

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.

object INCREMENTAL extends Param with Product with Serializable

object INLINE_SIZE_LIMIT extends Param with Product with Serializable

Maximum size of function bodies to inline.

object INPUT_FORMAT extends Param with Product with Serializable

object InputFormat extends Enumeration

object LOGO extends Param with Product with Serializable

object LOG_BACKTRACKING extends LOG_FLAG with Product with Serializable

object LOG_COUNTERS extends LOG_FLAG with Product with Serializable

object LOG_COUNTERS_CONT extends LOG_FLAG with Product with Serializable

object LOG_LEMMAS extends LOG_FLAG with Product with Serializable

object LOG_LEVEL extends Param with Product with Serializable

Enable logging to stderr for specific aspects of the system.

object LOG_SPLITS extends LOG_FLAG with Product with Serializable

object LOG_STATS extends LOG_FLAG with Product with Serializable

object LOG_TASKS extends LOG_FLAG with Product with Serializable

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

object MATCHING_BASE_PRIORITY extends Param with Product with Serializable

object MGCFormatOptions extends Enumeration

object MGC_FORMAT extends Param with Product with Serializable

object MODEL_GENERATION extends Param with Product with Serializable

object MOST_GENERAL_CONSTRAINT extends Param with Product with Serializable

object MUL_PROCEDURE extends Param with Product with Serializable

object MulProcedure extends Enumeration

object NEG_SOLVING extends Param with Product with Serializable

Options for solving problems in positive or negated version

object NONLINEAR_SPLITTING extends Param with Product with Serializable

object NegSolvingOptions extends Enumeration

object NonLinearSplitting extends Enumeration

object PORTFOLIO extends Param with Product with Serializable

Portfolios optimised for particular domains

object PORTFOLIO_THREAD_NUM extends Param with Product with Serializable

object POS_UNIT_RESOLUTION extends Param with Product with Serializable

Resolve negative predicate literals in clauses with positive facts

object PREDICATE_MATCH_CONFIG extends Param with Product with Serializable

object PRINT_CERTIFICATE extends Param with Product with Serializable

object PRINT_DOT_CERTIFICATE_FILE extends Param with Product with Serializable

object PRINT_RUNTIME extends Param with Product with Serializable

object PRINT_SMT_FILE extends Param with Product with Serializable

object PRINT_TPTP_FILE extends Param with Product with Serializable

object PRINT_TREE extends Param with Product with Serializable

object PROOF_CONSTRUCTION extends Param with Product with Serializable

object PROOF_CONSTRUCTION_GLOBAL extends Param with Product with Serializable

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)

object QUIET extends Param with Product with Serializable

object RANDOM_DATA_SOURCE extends Param with Product with Serializable

object RANDOM_SEED extends Param with Product with Serializable

object REAL_RAT_SATURATION_ROUNDS extends Param with Product with Serializable

object REDUCER_PLUGIN extends Param with Product with Serializable

object REDUCER_SETTINGS extends Param with Product with Serializable

object REVERSE_FUNCTIONALITY_PROPAGATION extends Param with Product with Serializable

object SEQ_THEORY_DESC extends Param with Product with Serializable

object SIMPLIFY_CONSTRAINTS extends Param with Product with Serializable

object SINGLE_INSTANTIATION_PREDICATES extends Param with Product with Serializable

object SMTParserExtraTheories extends Param with Product with Serializable

object STDIN extends Param with Product with Serializable

object STRENGTHEN_TREE_FOR_SIDE_CONDITIONS extends Param with Product with Serializable

Represent numeric side conditions (inequalities) in quantified formulas using the StrengthenTree constructor

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.

object STRING_THEORY_DESC extends Param with Product with Serializable

object SYMBOL_WEIGHTS extends Param with Product with Serializable

object THEORY_PLUGIN extends Param with Product with Serializable

object TIGHT_FUNCTION_SCOPES extends Param with Product with Serializable

object TIMEOUT extends Param with Product with Serializable

object TIMEOUT_PER extends Param with Product with Serializable

object TRACE_CONSTRAINT_SIMPLIFIER extends Param with Product with Serializable

object TRIGGERS_IN_CONJECTURE extends Param with Product with Serializable

object TRIGGER_GENERATION extends Param with Product with Serializable

object TRIGGER_STRATEGY extends Param with Product with Serializable

object TriggerGenerationOptions extends Enumeration

object TriggerStrategyOptions extends Enumeration

object USE_FUNCTIONAL_CONSISTENCY_THEORY extends Param with Product with Serializable

Use the FunctionalConsistency dummy theory to represent applications of functionality in proofs.

object VERSION extends Param with Product with Serializable

object WARM_UP extends Param with Product with Serializable

Before solving any actual tasks, run some other problems for warmup purposes.

final def asInstanceOf[T0]: T0

def clone(): AnyRef

final def eq(arg0: AnyRef): Boolean

def equals(arg0: Any): Boolean

final def getClass(): Class[_]

def hashCode(): Int

final def isInstanceOf[T0]: Boolean

final def ne(arg0: AnyRef): Boolean

final def notify(): Unit

final def notifyAll(): Unit

final def synchronized[T0](arg0: ⇒ T0): T0

def toString(): String

final def wait(arg0: Long, arg1: Int): Unit

final def wait(arg0: Long): Unit

final def wait(): Unit

def finalize(): Unit