List of all items
Structs
- max_align_t
- vampire_clause_t
- vampire_formula_t
- vampire_literal_t
- vampire_problem_t
- vampire_proof_step_t
- vampire_term_t
- vampire_unit_t
Functions
- vampire_add_function
- vampire_add_predicate
- vampire_and
- vampire_atom
- vampire_axiom_clause
- vampire_axiom_formula
- vampire_clause
- vampire_clause_is_empty
- vampire_clause_to_string
- vampire_conjecture_clause
- vampire_conjecture_formula
- vampire_constant
- vampire_eq
- vampire_exists
- vampire_extract_proof
- vampire_false
- vampire_forall
- vampire_formula_equal
- vampire_formula_hash
- vampire_formula_to_string
- vampire_free_literals
- vampire_free_proof_steps
- vampire_free_string
- vampire_get_literals
- vampire_get_refutation
- vampire_iff
- vampire_imp
- vampire_input_type_name
- vampire_lit
- vampire_literal_to_string
- vampire_neg
- vampire_not
- vampire_or
- vampire_prepare_for_next_proof
- vampire_print_proof
- vampire_print_proof_to_file
- vampire_problem_from_clauses
- vampire_problem_from_units
- vampire_prove
- vampire_reset
- vampire_rule_name
- vampire_set_saturation_algorithm
- vampire_set_show_proof
- vampire_set_time_limit
- vampire_set_time_limit_deciseconds
- vampire_set_time_limit_milliseconds
- vampire_term
- vampire_term_equal
- vampire_term_hash
- vampire_term_to_string
- vampire_true
- vampire_unit_as_clause
- vampire_unit_as_formula
- vampire_var
Type Aliases
Constants
- __bool_true_false_are_defined
- false_
- true_
- vampire_inference_rule_t_ADD_SORT_FUNCTIONS
- vampire_inference_rule_t_ADD_SORT_PREDICATES
- vampire_inference_rule_t_ALASCA_ABSTRACTION
- vampire_inference_rule_t_ALASCA_BWD_DEMODULATION
- vampire_inference_rule_t_ALASCA_COHERENCE
- vampire_inference_rule_t_ALASCA_COHERENCE_NORMALIZATION
- vampire_inference_rule_t_ALASCA_EQ_FACTORING
- vampire_inference_rule_t_ALASCA_FLOOR_BOUNDS
- vampire_inference_rule_t_ALASCA_FLOOR_ELIMINATION
- vampire_inference_rule_t_ALASCA_FOURIER_MOTZKIN
- vampire_inference_rule_t_ALASCA_FWD_DEMODULATION
- vampire_inference_rule_t_ALASCA_INTEGER_FOURIER_MOTZKIN
- vampire_inference_rule_t_ALASCA_INTEGER_TRANSFORMATION
- vampire_inference_rule_t_ALASCA_LITERAL_FACTORING
- vampire_inference_rule_t_ALASCA_NORMALIZATION
- vampire_inference_rule_t_ALASCA_SUPERPOSITION
- vampire_inference_rule_t_ALASCA_TERM_FACTORING
- vampire_inference_rule_t_ALASCA_VARIABLE_ELIMINATION
- vampire_inference_rule_t_ALASCA_VIRAS_QE
- vampire_inference_rule_t_ANSWER_LITERAL_INJECTION
- vampire_inference_rule_t_ANSWER_LITERAL_INPUT_SKOLEMISATION
- vampire_inference_rule_t_ANSWER_LITERAL_JOIN_AS_ITE
- vampire_inference_rule_t_ANSWER_LITERAL_JOIN_WITH_CONSTRAINTS
- vampire_inference_rule_t_ANSWER_LITERAL_REMOVAL
- vampire_inference_rule_t_ANSWER_LITERAL_RESOLVER
- vampire_inference_rule_t_ARG_CONG
- vampire_inference_rule_t_ARITHMETIC_SUBTERM_GENERALIZATION
- vampire_inference_rule_t_AVATAR_ASSERTION_REINTRODUCTION
- vampire_inference_rule_t_AVATAR_COMPONENT
- vampire_inference_rule_t_AVATAR_CONTRADICTION_CLAUSE
- vampire_inference_rule_t_AVATAR_DEFINITION
- vampire_inference_rule_t_AVATAR_REFUTATION
- vampire_inference_rule_t_AVATAR_REFUTATION_SMT
- vampire_inference_rule_t_AVATAR_SPLIT_CLAUSE
- vampire_inference_rule_t_BACKWARD_DEMODULATION
- vampire_inference_rule_t_BACKWARD_SUBSUMPTION_DEMODULATION
- vampire_inference_rule_t_BACKWARD_SUBSUMPTION_RESOLUTION
- vampire_inference_rule_t_BINARY_CONN_ELIMINATION
- vampire_inference_rule_t_BOOLEAN_TERM_ENCODING
- vampire_inference_rule_t_BOOL_SIMP
- vampire_inference_rule_t_CANCELLATION
- vampire_inference_rule_t_CASES_SIMP
- vampire_inference_rule_t_CLAIM_DEFINITION
- vampire_inference_rule_t_CLAUSIFY
- vampire_inference_rule_t_CLOSURE
- vampire_inference_rule_t_COLOR_UNBLOCKING
- vampire_inference_rule_t_CONDENSATION
- vampire_inference_rule_t_CONSTRAINED_FACTORING
- vampire_inference_rule_t_CONSTRAINED_RESOLUTION
- vampire_inference_rule_t_CONSTRAINED_SUPERPOSITION
- vampire_inference_rule_t_DEFINITION_FOLDING
- vampire_inference_rule_t_DEFINITION_UNFOLDING
- vampire_inference_rule_t_DISTINCTNESS_AXIOM
- vampire_inference_rule_t_DISTINCT_EQUALITY_REMOVAL
- vampire_inference_rule_t_ENNF
- vampire_inference_rule_t_EQUALITY_FACTORING
- vampire_inference_rule_t_EQUALITY_PROXY_AXIOM1
- vampire_inference_rule_t_EQUALITY_PROXY_AXIOM2
- vampire_inference_rule_t_EQUALITY_PROXY_REPLACEMENT
- vampire_inference_rule_t_EQUALITY_RESOLUTION
- vampire_inference_rule_t_EQUALITY_RESOLUTION_WITH_DELETION
- vampire_inference_rule_t_EQ_TO_DISEQ
- vampire_inference_rule_t_EVALUATION
- vampire_inference_rule_t_EXTENSIONALITY_RESOLUTION
- vampire_inference_rule_t_FACTORING
- vampire_inference_rule_t_FLATTEN
- vampire_inference_rule_t_FMB_DEF_INTRO
- vampire_inference_rule_t_FMB_FLATTENING
- vampire_inference_rule_t_FMB_FUNC_DEF
- vampire_inference_rule_t_FOOL_AXIOM_ALL_IS_TRUE_OR_FALSE
- vampire_inference_rule_t_FOOL_AXIOM_TRUE_NEQ_FALSE
- vampire_inference_rule_t_FOOL_ELIMINATION
- vampire_inference_rule_t_FOOL_FORMULA_DEFINITION
- vampire_inference_rule_t_FOOL_ITE_DEFINITION
- vampire_inference_rule_t_FOOL_LET_DEFINITION
- vampire_inference_rule_t_FOOL_MATCH_DEFINITION
- vampire_inference_rule_t_FOOL_PARAMODULATION
- vampire_inference_rule_t_FORMULIFY
- vampire_inference_rule_t_FORWARD_DEMODULATION
- vampire_inference_rule_t_FORWARD_LITERAL_REWRITING
- vampire_inference_rule_t_FORWARD_SUBSUMPTION_DEMODULATION
- vampire_inference_rule_t_FORWARD_SUBSUMPTION_RESOLUTION
- vampire_inference_rule_t_FUNCTION_DEFINITION
- vampire_inference_rule_t_FUNCTION_DEFINITION_DEMODULATION
- vampire_inference_rule_t_FUNCTION_DEFINITION_REWRITING
- vampire_inference_rule_t_GAUSSIAN_VARIABLE_ELIMINIATION
- vampire_inference_rule_t_GENERAL_SPLITTING
- vampire_inference_rule_t_GENERAL_SPLITTING_COMPONENT
- vampire_inference_rule_t_GENERIC_AVATAR_INFERENCE
- vampire_inference_rule_t_GENERIC_AVATAR_INFERENCE_LAST
- vampire_inference_rule_t_GENERIC_FORMULA_CLAUSE_TRANSFORMATION
- vampire_inference_rule_t_GENERIC_FORMULA_CLAUSE_TRANSFORMATION_LAST
- vampire_inference_rule_t_GENERIC_GENERATING_INFERENCE
- vampire_inference_rule_t_GENERIC_GENERATING_INFERENCE_LAST
- vampire_inference_rule_t_GENERIC_SIMPLIFYING_INFERENCE
- vampire_inference_rule_t_GENERIC_SIMPLIFYING_INFERENCE_LAST
- vampire_inference_rule_t_GENERIC_THEORY_AXIOM
- vampire_inference_rule_t_GLOBAL_SUBSUMPTION
- vampire_inference_rule_t_HILBERTS_CHOICE_INSTANCE
- vampire_inference_rule_t_HOL_EQUALITY_ELIMINATION
- vampire_inference_rule_t_HOL_NOT_ELIMINATION
- vampire_inference_rule_t_INDUCTION_HYPERRESOLUTION
- vampire_inference_rule_t_INEQUALITY_SPLITTING
- vampire_inference_rule_t_INEQUALITY_SPLITTING_NAME_INTRODUCTION
- vampire_inference_rule_t_INJECTIVITY
- vampire_inference_rule_t_INNER_REWRITING
- vampire_inference_rule_t_INPUT
- vampire_inference_rule_t_INSTANTIATION
- vampire_inference_rule_t_INTERPRETED_SIMPLIFICATION
- vampire_inference_rule_t_INT_DB_DOWN_INDUCTION_AXIOM
- vampire_inference_rule_t_INT_DB_UP_INDUCTION_AXIOM
- vampire_inference_rule_t_INT_FIN_DOWN_INDUCTION_AXIOM
- vampire_inference_rule_t_INT_FIN_UP_INDUCTION_AXIOM
- vampire_inference_rule_t_INT_INF_DOWN_INDUCTION_AXIOM
- vampire_inference_rule_t_INT_INF_UP_INDUCTION_AXIOM
- vampire_inference_rule_t_LEIBNIZ_ELIMINATION
- vampire_inference_rule_t_MODEL_NOT_FOUND
- vampire_inference_rule_t_NEGATED_CONJECTURE
- vampire_inference_rule_t_NEGATIVE_EXT
- vampire_inference_rule_t_NNF
- vampire_inference_rule_t_POLARITY_FLIPPING
- vampire_inference_rule_t_PREDICATE_DEFINITION
- vampire_inference_rule_t_PREDICATE_DEFINITION_MERGING
- vampire_inference_rule_t_PREDICATE_DEFINITION_UNFOLDING
- vampire_inference_rule_t_PRIMITIVE_INSTANTIATION
- vampire_inference_rule_t_PURE_PREDICATE_REMOVAL
- vampire_inference_rule_t_RECTIFY
- vampire_inference_rule_t_REDUCE_FALSE_TRUE
- vampire_inference_rule_t_REMOVE_DUPLICATE_LITERALS
- vampire_inference_rule_t_REORDER_LITERALS
- vampire_inference_rule_t_REORIENT_EQUATIONS
- vampire_inference_rule_t_RESOLUTION
- vampire_inference_rule_t_SAT_COLOR_ELIMINATION
- vampire_inference_rule_t_SKOLEMIZE
- vampire_inference_rule_t_SKOLEM_SYMBOL_INTRODUCTION
- vampire_inference_rule_t_STRUCT_INDUCTION_AXIOM_ONE
- vampire_inference_rule_t_STRUCT_INDUCTION_AXIOM_RECURSION
- vampire_inference_rule_t_STRUCT_INDUCTION_AXIOM_THREE
- vampire_inference_rule_t_STRUCT_INDUCTION_AXIOM_TWO
- vampire_inference_rule_t_SUPERPOSITION
- vampire_inference_rule_t_TERM_ALGEBRA_ACYCLICITY
- vampire_inference_rule_t_TERM_ALGEBRA_ACYCLICITY_AXIOM
- vampire_inference_rule_t_TERM_ALGEBRA_DIRECT_SUBTERMS_AXIOM
- vampire_inference_rule_t_TERM_ALGEBRA_DISCRIMINATION_AXIOM
- vampire_inference_rule_t_TERM_ALGEBRA_DISTINCTNESS
- vampire_inference_rule_t_TERM_ALGEBRA_DISTINCTNESS_AXIOM
- vampire_inference_rule_t_TERM_ALGEBRA_EXHAUSTIVENESS_AXIOM
- vampire_inference_rule_t_TERM_ALGEBRA_INJECTIVITY_AXIOM
- vampire_inference_rule_t_TERM_ALGEBRA_INJECTIVITY_GENERATING
- vampire_inference_rule_t_TERM_ALGEBRA_NEGATIVE_INJECTIVITY_SIMPLIFYING
- vampire_inference_rule_t_TERM_ALGEBRA_POSITIVE_INJECTIVITY_SIMPLIFYING
- vampire_inference_rule_t_TERM_ALGEBRA_SUBTERMS_TRANSITIVE_AXIOM
- vampire_inference_rule_t_THA_ABS_EQUALS
- vampire_inference_rule_t_THA_ABS_MINUS_EQUALS
- vampire_inference_rule_t_THA_ALASCA
- vampire_inference_rule_t_THA_ARRAY_EXTENSIONALITY
- vampire_inference_rule_t_THA_ARRAY_WRITE1
- vampire_inference_rule_t_THA_ARRAY_WRITE2
- vampire_inference_rule_t_THA_ASSOCIATIVITY
- vampire_inference_rule_t_THA_BOOLEAN_ARRAY_EXTENSIONALITY
- vampire_inference_rule_t_THA_BOOLEAN_ARRAY_WRITE1
- vampire_inference_rule_t_THA_BOOLEAN_ARRAY_WRITE2
- vampire_inference_rule_t_THA_CEILING_BIG
- vampire_inference_rule_t_THA_CEILING_SMALL
- vampire_inference_rule_t_THA_COMMUTATIVITY
- vampire_inference_rule_t_THA_DISTRIBUTIVITY
- vampire_inference_rule_t_THA_DIVIDES_MULTIPLY
- vampire_inference_rule_t_THA_DIVISIBILITY
- vampire_inference_rule_t_THA_EXTRA_INTEGER_ORDERING
- vampire_inference_rule_t_THA_FLOOR_BIG
- vampire_inference_rule_t_THA_FLOOR_SMALL
- vampire_inference_rule_t_THA_INVERSE_ASSOC
- vampire_inference_rule_t_THA_INVERSE_OP_OP_INVERSES
- vampire_inference_rule_t_THA_INVERSE_OP_UNIT
- vampire_inference_rule_t_THA_LEFT_IDENTITY
- vampire_inference_rule_t_THA_MINUS_MINUS_X
- vampire_inference_rule_t_THA_MODULO_MULTIPLY
- vampire_inference_rule_t_THA_MODULO_POSITIVE
- vampire_inference_rule_t_THA_MODULO_SMALL
- vampire_inference_rule_t_THA_NONDIVIDES_SKOLEM
- vampire_inference_rule_t_THA_NONREFLEX
- vampire_inference_rule_t_THA_ORDER_MONOTONICITY
- vampire_inference_rule_t_THA_ORDER_PLUS_ONE_DICHOTOMY
- vampire_inference_rule_t_THA_ORDER_TOTALITY
- vampire_inference_rule_t_THA_PLUS_ONE_GREATER
- vampire_inference_rule_t_THA_QUOTIENT_MULTIPLY
- vampire_inference_rule_t_THA_QUOTIENT_NON_ZERO
- vampire_inference_rule_t_THA_RIGHT_IDENTITY
- vampire_inference_rule_t_THA_TIMES_ZERO
- vampire_inference_rule_t_THA_TRANSITIVITY
- vampire_inference_rule_t_THA_TRUNC1
- vampire_inference_rule_t_THA_TRUNC2
- vampire_inference_rule_t_THA_TRUNC3
- vampire_inference_rule_t_THA_TRUNC4
- vampire_inference_rule_t_THEORY_FLATTENING
- vampire_inference_rule_t_THEORY_NORMALIZATION
- vampire_inference_rule_t_THEORY_TAUTOLOGY_SAT_CONFLICT
- vampire_inference_rule_t_TRIVIAL_INEQUALITY_REMOVAL
- vampire_inference_rule_t_UNIT_RESULTING_RESOLUTION
- vampire_inference_rule_t_UNUSED_PREDICATE_DEFINITION_REMOVAL
- vampire_inference_rule_t_VPI_ELIMINATION
- vampire_inference_rule_t_VSIGMA_ELIMINATION
- vampire_input_type_t_VAMPIRE_AXIOM
- vampire_input_type_t_VAMPIRE_CONJECTURE
- vampire_input_type_t_VAMPIRE_NEGATED_CONJECTURE
- vampire_proof_result_t_VAMPIRE_INCOMPLETE
- vampire_proof_result_t_VAMPIRE_MEMORY_LIMIT
- vampire_proof_result_t_VAMPIRE_PROOF
- vampire_proof_result_t_VAMPIRE_SATISFIABLE
- vampire_proof_result_t_VAMPIRE_TIMEOUT
- vampire_proof_result_t_VAMPIRE_UNKNOWN