Param

Value Members

1. final def !=(arg0: Any): Boolean

   

   Definition Classes

   AnyRef → Any

2. final def ##(): Int

   

   Definition Classes

   AnyRef → Any

3. final def ==(arg0: Any): Boolean

   

   Definition Classes

   AnyRef → Any

4. object ABBREV_LABELS extends Param with Product with Serializable

   

5. object ADT_MEASURE extends Param with Product with Serializable

   

6. 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)

7. object ASSERTIONS extends Param with Product with Serializable

   

8. object BOOLEAN_FUNCTIONS_AS_PREDICATES extends Param with Product with Serializable

   

9. object CLAUSIFIER extends Param with Product with Serializable

   

10. object COMPUTE_MODEL extends Param with Product with Serializable

    

11. object COMPUTE_UNSAT_CORE extends Param with Product with Serializable

    

12. object CONSTRAINT_SIMPLIFIER extends Param with Product with Serializable

    

13. object ClausifierOptions extends Enumeration

    

14. object ConstraintSimplifierOptions extends Enumeration

    

15. object DNF_CONSTRAINTS extends Param with Product with Serializable

    

    Turn ground constraints into disjunctive normal form

16. object ELIMINATE_INTERPOLANT_QUANTIFIERS extends Param with Product with Serializable

    

17. object FULL_HELP extends Param with Product with Serializable

    

18. object FULL_SPLITTING extends Param with Product with Serializable

    

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

19. object FUNCTIONAL_PREDICATES extends Param with Product with Serializable

    

20. object FUNCTION_GC extends Param with Product with Serializable

    

21. object FunctionGCOptions extends Enumeration

    

22. object GARBAGE_COLLECTED_FUNCTIONS extends Param with Product with Serializable

    

23. object GENERATE_TOTALITY_AXIOMS extends Param with Product with Serializable

    

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

25. object INCREMENTAL extends Param with Product with Serializable

    

26. object INPUT_FORMAT extends Param with Product with Serializable

    

27. object InputFormat extends Enumeration

    

28. object LOGO extends Param with Product with Serializable

    

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

30. object MATCHING_BASE_PRIORITY extends Param with Product with Serializable

    

31. object MODEL_GENERATION extends Param with Product with Serializable

    

32. object MOST_GENERAL_CONSTRAINT extends Param with Product with Serializable

    

33. object MUL_PROCEDURE extends Param with Product with Serializable

    

34. object MulProcedure extends Enumeration

    

35. object NEG_SOLVING extends Param with Product with Serializable

    

    Options for solving problems in positive or negated version

36. object NONLINEAR_SPLITTING extends Param with Product with Serializable

    

37. object NegSolvingOptions extends Enumeration

    

38. object NonLinearSplitting extends Enumeration

    

39. object PORTFOLIO extends Param with Product with Serializable

    

40. object POS_UNIT_RESOLUTION extends Param with Product with Serializable

    

    Resolve negative predicate literals in clauses with positive facts

41. object PREDICATE_MATCH_CONFIG extends Param with Product with Serializable

    

42. object PRINT_CERTIFICATE extends Param with Product with Serializable

    

43. object PRINT_DOT_CERTIFICATE_FILE extends Param with Product with Serializable

    

44. object PRINT_SMT_FILE extends Param with Product with Serializable

    

45. object PRINT_TPTP_FILE extends Param with Product with Serializable

    

46. object PRINT_TREE extends Param with Product with Serializable

    

47. object PROOF_CONSTRUCTION extends Param with Product with Serializable

    

48. object PROOF_CONSTRUCTION_GLOBAL extends Param with Product with Serializable

    

49. object PROOF_SIMPLIFICATION extends Param with Product with Serializable

    

50. object PortfolioOptions extends Enumeration

    

    Portfolios optimised for particular domains

51. object ProofConstructionOptions extends Enumeration

    

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

52. object QUIET extends Param with Product with Serializable

    

53. object RANDOM_DATA_SOURCE extends Param with Product with Serializable

    

54. object RANDOM_SEED extends Param with Product with Serializable

    

55. object REAL_RAT_SATURATION_ROUNDS extends Param with Product with Serializable

    

56. object REDUCER_PLUGIN extends Param with Product with Serializable

    

57. object REDUCER_SETTINGS extends Param with Product with Serializable

    

58. object REVERSE_FUNCTIONALITY_PROPAGATION extends Param with Product with Serializable

    

59. object SIMPLIFY_CONSTRAINTS extends Param with Product with Serializable

    

60. object SINGLE_INSTANTIATION_PREDICATES extends Param with Product with Serializable

    

61. object STDIN extends Param with Product with Serializable

    

62. object STRENGTHEN_TREE_FOR_SIDE_CONDITIONS extends Param with Product with Serializable

    

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

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

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

64. object STRING_THEORY_DESC extends Param with Product with Serializable

    

65. object SYMBOL_WEIGHTS extends Param with Product with Serializable

    

66. object THEORY_PLUGIN extends Param with Product with Serializable

    

67. object TIGHT_FUNCTION_SCOPES extends Param with Product with Serializable

    

68. object TIMEOUT extends Param with Product with Serializable

    

69. object TIMEOUT_PER extends Param with Product with Serializable

    

70. object TRACE_CONSTRAINT_SIMPLIFIER extends Param with Product with Serializable

    

71. object TRIGGERS_IN_CONJECTURE extends Param with Product with Serializable

    

72. object TRIGGER_GENERATION extends Param with Product with Serializable

    

73. object TRIGGER_STRATEGY extends Param with Product with Serializable

    

74. object TriggerGenerationOptions extends Enumeration

    

75. object TriggerStrategyOptions extends Enumeration

    

76. object USE_FUNCTIONAL_CONSISTENCY_THEORY extends Param with Product with Serializable

    

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

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

77. object VERSION extends Param with Product with Serializable

    

78. final def asInstanceOf[T0]: T0

    

    Definition Classes

    Any

79. def clone(): AnyRef

    

    Attributes

    protected[java.lang]

    Definition Classes

    AnyRef

    Annotations

    @throws( ... )

80. final def eq(arg0: AnyRef): Boolean

    

    Definition Classes

    AnyRef

81. def equals(arg0: Any): Boolean

    

    Definition Classes

    AnyRef → Any

82. def finalize(): Unit

    

    Attributes

    protected[java.lang]

    Definition Classes

    AnyRef

    Annotations

    @throws( classOf[java.lang.Throwable] )

83. final def getClass(): Class[_]

    

    Definition Classes

    AnyRef → Any

84. def hashCode(): Int

    

    Definition Classes

    AnyRef → Any

85. final def isInstanceOf[T0]: Boolean

    

    Definition Classes

    Any

86. final def ne(arg0: AnyRef): Boolean

    

    Definition Classes

    AnyRef

87. final def notify(): Unit

    

    Definition Classes

    AnyRef

88. final def notifyAll(): Unit

    

    Definition Classes

    AnyRef

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

    

    Definition Classes

    AnyRef

90. def toString(): String

    

    Definition Classes

    AnyRef → Any

91. final def wait(): Unit

    

    Definition Classes

    AnyRef

    Annotations

    @throws( ... )

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

    

    Definition Classes

    AnyRef

    Annotations

    @throws( ... )

93. final def wait(arg0: Long): Unit

    

    Definition Classes

    AnyRef

    Annotations

    @throws( ... )