Packages

object Param

Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. Param
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. Protected

Type Members

  1. abstract class LOG_FLAG extends AnyRef

Value Members

  1. case object ABBREV_LABELS extends Param with Product with Serializable
  2. case object ADT_MEASURE extends Param with Product with Serializable
  3. 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)

  4. case object ASSERTIONS extends Param with Product with Serializable
  5. case object BOOLEAN_FUNCTIONS_AS_PREDICATES extends Param with Product with Serializable
  6. case object CLAUSIFIER extends Param with Product with Serializable
  7. case object COMPUTE_MODEL extends Param with Product with Serializable
  8. case object COMPUTE_UNSAT_CORE extends Param with Product with Serializable
  9. case object CONSTRAINT_SIMPLIFIER extends Param with Product with Serializable
  10. case object COUNTER_TIMEOUT extends Param with Product with Serializable
  11. object ClausifierOptions extends Enumeration
  12. object ConstraintSimplifierOptions extends Enumeration
  13. case object DNF_CONSTRAINTS extends Param with Product with Serializable

    Turn ground constraints into disjunctive normal form

  14. case object ELIMINATE_INTERPOLANT_QUANTIFIERS extends Param with Product with Serializable
  15. 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.

  16. case object FULL_HELP extends Param with Product with Serializable
  17. case object FULL_SPLITTING extends Param with Product with Serializable

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

  18. case object FUNCTIONAL_PREDICATES extends Param with Product with Serializable
  19. case object FUNCTION_GC extends Param with Product with Serializable
  20. object FunctionGCOptions extends Enumeration
  21. case object GARBAGE_COLLECTED_FUNCTIONS extends Param with Product with Serializable
  22. case object GENERATE_TOTALITY_AXIOMS extends Param with Product with Serializable
  23. 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.

  24. case object INCREMENTAL extends Param with Product with Serializable
  25. case object INLINE_SIZE_LIMIT extends Param with Product with Serializable

    Maximum size of function bodies to inline.

  26. case object INPUT_FORMAT extends Param with Product with Serializable
  27. object InputFormat extends Enumeration
  28. case object LOGO extends Param with Product with Serializable
  29. case object LOG_BACKTRACKING extends LOG_FLAG with Product with Serializable
  30. case object LOG_COUNTERS extends LOG_FLAG with Product with Serializable
  31. case object LOG_COUNTERS_CONT extends LOG_FLAG with Product with Serializable
  32. case object LOG_LEMMAS extends LOG_FLAG with Product with Serializable
  33. case object LOG_LEVEL extends Param with Product with Serializable

    Enable logging to stderr for specific aspects of the system.

  34. case object LOG_SPLITS extends LOG_FLAG with Product with Serializable
  35. case object LOG_STATS extends LOG_FLAG with Product with Serializable
  36. case object LOG_TASKS extends LOG_FLAG with Product with Serializable
  37. 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

  38. case object MATCHING_BASE_PRIORITY extends Param with Product with Serializable
  39. object MGCFormatOptions extends Enumeration
  40. case object MGC_FORMAT extends Param with Product with Serializable
  41. case object MODEL_GENERATION extends Param with Product with Serializable
  42. case object MOST_GENERAL_CONSTRAINT extends Param with Product with Serializable
  43. case object MUL_PROCEDURE extends Param with Product with Serializable
  44. object MulProcedure extends Enumeration
  45. case object NEG_SOLVING extends Param with Product with Serializable

    Options for solving problems in positive or negated version

  46. case object NONLINEAR_SPLITTING extends Param with Product with Serializable
  47. object NegSolvingOptions extends Enumeration
  48. object NonLinearSplitting extends Enumeration
  49. case object PORTFOLIO extends Param with Product with Serializable

    Portfolios optimised for particular domains

  50. case object PORTFOLIO_THREAD_NUM extends Param with Product with Serializable
  51. case object POS_UNIT_RESOLUTION extends Param with Product with Serializable

    Resolve negative predicate literals in clauses with positive facts

  52. case object PREDICATE_MATCH_CONFIG extends Param with Product with Serializable
  53. case object PRINT_CERTIFICATE extends Param with Product with Serializable
  54. case object PRINT_DOT_CERTIFICATE_FILE extends Param with Product with Serializable
  55. case object PRINT_RUNTIME extends Param with Product with Serializable
  56. case object PRINT_SMT_FILE extends Param with Product with Serializable
  57. case object PRINT_TPTP_FILE extends Param with Product with Serializable
  58. case object PRINT_TREE extends Param with Product with Serializable
  59. case object PROOF_CONSTRUCTION extends Param with Product with Serializable
  60. case object PROOF_CONSTRUCTION_GLOBAL extends Param with Product with Serializable
  61. case object PROOF_SIMPLIFICATION extends Param with Product with Serializable
  62. object ProofConstructionOptions extends Enumeration

    Globally, we can also choose to construct proofs depending on whether interpolation specs were given (the default)

  63. case object QUIET extends Param with Product with Serializable
  64. case object RANDOM_DATA_SOURCE extends Param with Product with Serializable
  65. case object RANDOM_SEED extends Param with Product with Serializable
  66. case object REAL_RAT_SATURATION_ROUNDS extends Param with Product with Serializable
  67. case object REDUCER_PLUGIN extends Param with Product with Serializable
  68. case object REDUCER_SETTINGS extends Param with Product with Serializable
  69. case object REVERSE_FUNCTIONALITY_PROPAGATION extends Param with Product with Serializable
  70. case object SEQ_THEORY_DESC extends Param with Product with Serializable
  71. case object SIMPLIFY_CONSTRAINTS extends Param with Product with Serializable
  72. case object SINGLE_INSTANTIATION_PREDICATES extends Param with Product with Serializable
  73. case object SMTParserExtraTheories extends Param with Product with Serializable
  74. case object STDIN extends Param with Product with Serializable
  75. 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

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

  77. case object STRING_THEORY_DESC extends Param with Product with Serializable
  78. case object SYMBOL_WEIGHTS extends Param with Product with Serializable
  79. case object THEORY_PLUGIN extends Param with Product with Serializable
  80. case object TIGHT_FUNCTION_SCOPES extends Param with Product with Serializable
  81. case object TIMEOUT extends Param with Product with Serializable
  82. case object TIMEOUT_PER extends Param with Product with Serializable
  83. case object TRACE_CONSTRAINT_SIMPLIFIER extends Param with Product with Serializable
  84. case object TRIGGERS_IN_CONJECTURE extends Param with Product with Serializable
  85. case object TRIGGER_GENERATION extends Param with Product with Serializable
  86. case object TRIGGER_STRATEGY extends Param with Product with Serializable
  87. object TriggerGenerationOptions extends Enumeration
  88. object TriggerStrategyOptions extends Enumeration
  89. case object USE_FUNCTIONAL_CONSISTENCY_THEORY extends Param with Product with Serializable

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

  90. case object VERSION extends Param with Product with Serializable
  91. 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.