Crate cvc5_sys

Expand description

§cvc5-sys

Low-level FFI bindings for the cvc5 SMT solver.

This crate provides raw C API bindings generated by bindgen from the cvc5 C header (cvc5/c/cvc5.h). For a safe, idiomatic Rust API, see the higher-level cvc5 crate.

§Build

cvc5 must be built from source first. Point CVC5_DIR to the cvc5 source root (containing include/ and build/), or place a built cvc5 checkout as a sibling cvc5/ directory.

CVC5_DIR=/path/to/cvc5 cargo build

§Example

use cvc5_sys::*;

unsafe {
    let tm = cvc5_term_manager_new();
    let slv = cvc5_new(tm);

    cvc5_set_logic(slv, c"QF_LIA".as_ptr());
    cvc5_set_option(slv, c"produce-models".as_ptr(), c"true".as_ptr());

    let int_sort = cvc5_get_integer_sort(tm);
    let x = cvc5_mk_const(tm, int_sort, c"x".as_ptr());
    let zero = cvc5_mk_integer_int64(tm, 0);

    let gt = cvc5_mk_term(tm, Cvc5Kind::CVC5_KIND_GT, 2, [x, zero].as_ptr());
    cvc5_assert_formula(slv, gt);

    let result = cvc5_check_sat(slv);
    assert!(cvc5_result_is_sat(result));

    cvc5_delete(slv);
    cvc5_term_manager_delete(tm);
}

Modules§

parser

Structs§

Cvc5
Cvc5OptionInfo: \verbatim embed:rst:leading-asterisk Holds information about a specific option, including its name, its aliases, whether the option was explicitly set by the user, and information concerning its value. It can be obtained via :cpp:func:cvc5_get_option_info() and allows for a more detailed inspection of options than :cpp:func:cvc5_get_option(). Union member info holds any of the following alternatives:
Cvc5OptionInfo_BoolInfo: Information for boolean option values.
Cvc5OptionInfo_DoubleInfo: Information for double values.
Cvc5OptionInfo_IntInfo: Information for int64 values.
Cvc5OptionInfo_ModeInfo: Information for mode option values.
Cvc5OptionInfo_StringInfo: Information for string option values.
Cvc5OptionInfo_UIntInfo: Information for uint64 values.
Cvc5Plugin: A cvc5 plugin.
Cvc5TermManager
cvc5_dt_cons_decl_t
cvc5_dt_cons_t
cvc5_dt_decl_t
cvc5_dt_sel_t
cvc5_dt_t
cvc5_grammar_t
cvc5_op_t
cvc5_proof_t
cvc5_result_t
cvc5_sort_t
cvc5_stat_t
cvc5_stats_t
cvc5_synth_result_t
cvc5_term_t

Enums§

Cvc5BlockModelsMode
Cvc5FindSynthTarget
Cvc5InputLanguage
Cvc5Kind
Cvc5LearnedLitType
Cvc5ProofComponent
Cvc5ProofFormat
Cvc5ProofRule
Cvc5RoundingMode
Cvc5SkolemId
Cvc5SortKind
Cvc5UnknownExplanation

Constants§

Cvc5OptionCategory_CVC5_OPTION_CATEGORY_COMMON
Cvc5OptionCategory_CVC5_OPTION_CATEGORY_EXPERT
Cvc5OptionCategory_CVC5_OPTION_CATEGORY_LAST
Cvc5OptionCategory_CVC5_OPTION_CATEGORY_REGULAR
Cvc5OptionCategory_CVC5_OPTION_CATEGORY_UNDOCUMENTED
Cvc5OptionInfoKind_CVC5_OPTION_INFO_BOOL: Information for option with boolean option value.
Cvc5OptionInfoKind_CVC5_OPTION_INFO_DOUBLE: Information for option with double value.
Cvc5OptionInfoKind_CVC5_OPTION_INFO_INT64: Information for option with int64 option value.
Cvc5OptionInfoKind_CVC5_OPTION_INFO_MODES: Information for option with option modes.
Cvc5OptionInfoKind_CVC5_OPTION_INFO_STR: Information for option with string option value.
Cvc5OptionInfoKind_CVC5_OPTION_INFO_UINT64: Information for option with uint64 option value.
Cvc5OptionInfoKind_CVC5_OPTION_INFO_VOID: The empty option info, does not hold value information.
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARITH_ABS_EQ
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARITH_ABS_INT_GT
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARITH_ABS_REAL_GT
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARITH_COSECENT_ELIM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARITH_COSINE_ELIM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARITH_COTANGENT_ELIM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARITH_DIVISIBLE_ELIM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARITH_DIV_ELIM_TO_REAL1
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARITH_DIV_ELIM_TO_REAL2
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARITH_DIV_TOTAL_ZERO_INT
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARITH_DIV_TOTAL_ZERO_REAL
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARITH_ELIM_GT
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARITH_ELIM_INT_GT
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARITH_ELIM_INT_LT
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARITH_ELIM_LEQ
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARITH_ELIM_LT
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARITH_EQ_ELIM_INT
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARITH_EQ_ELIM_REAL
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARITH_GEQ_ITE_LIFT
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARITH_GEQ_NORM1_INT
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARITH_GEQ_NORM1_REAL
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARITH_GEQ_TIGHTEN
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARITH_INT_DIV_TOTAL
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARITH_INT_DIV_TOTAL_NEG
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARITH_INT_DIV_TOTAL_ONE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARITH_INT_DIV_TOTAL_ZERO
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARITH_INT_EQ_CONFLICT
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARITH_INT_GEQ_TIGHTEN
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARITH_INT_MOD_TOTAL
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARITH_INT_MOD_TOTAL_NEG
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARITH_INT_MOD_TOTAL_ONE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARITH_INT_MOD_TOTAL_ZERO
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARITH_LEQ_ITE_LIFT
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARITH_LEQ_NORM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARITH_MAX_GEQ1
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARITH_MAX_GEQ2
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARITH_MIN_LT1
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARITH_MIN_LT2
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARITH_MOD_OVER_MOD
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARITH_PI_NOT_INT
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARITH_POW_ELIM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARITH_SECENT_ELIM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARITH_SINE_PI2
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARITH_SINE_ZERO
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARITH_STRING_PRED_ENTAIL
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARITH_STRING_PRED_SAFE_APPROX
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARITH_TANGENT_ELIM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARITH_TO_INT_ELIM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARITH_TO_INT_ELIM_TO_REAL
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARRAYS_EQ_RANGE_EXPAND
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARRAYS_SELECT_CONST
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARRAY_READ_OVER_WRITE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARRAY_READ_OVER_WRITE2
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARRAY_READ_OVER_WRITE_SPLIT
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARRAY_STORE_OVERWRITE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARRAY_STORE_SELF
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ARRAY_STORE_SWAP
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BETA_REDUCE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BOOL_AND_CONF
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BOOL_AND_CONF2
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BOOL_AND_DE_MORGAN
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BOOL_DOUBLE_NOT_ELIM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BOOL_DUAL_IMPL_EQ
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BOOL_EQ_FALSE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BOOL_EQ_NREFL
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BOOL_EQ_TRUE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BOOL_IMPLIES_DE_MORGAN
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BOOL_IMPLIES_OR_DISTRIB
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BOOL_IMPL_ELIM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BOOL_IMPL_FALSE1
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BOOL_IMPL_FALSE2
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BOOL_IMPL_TRUE1
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BOOL_IMPL_TRUE2
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BOOL_NOT_EQ_ELIM1
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BOOL_NOT_EQ_ELIM2
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BOOL_NOT_FALSE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BOOL_NOT_ITE_ELIM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BOOL_NOT_TRUE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BOOL_NOT_XOR_ELIM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BOOL_OR_AND_DISTRIB
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BOOL_OR_DE_MORGAN
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BOOL_OR_TAUT
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BOOL_OR_TAUT2
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BOOL_XOR_COMM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BOOL_XOR_ELIM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BOOL_XOR_FALSE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BOOL_XOR_NREFL
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BOOL_XOR_REFL
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BOOL_XOR_TRUE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_AND_CONCAT_PULLUP
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_AND_CONCAT_PULLUP2
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_AND_CONCAT_PULLUP3
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_AND_SIMPLIFY_1
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_AND_SIMPLIFY_2
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_ASHR_BY_CONST_0
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_ASHR_BY_CONST_1
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_ASHR_BY_CONST_2
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_ASHR_ZERO
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_BITWISE_SLICING
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_COMMUTATIVE_ADD
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_COMMUTATIVE_COMP
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_COMMUTATIVE_XOR
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_COMP_ELIMINATE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_CONCAT_EXTRACT_MERGE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_CONCAT_MERGE_CONST
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_EQ_EXTRACT_ELIM1
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_EQ_EXTRACT_ELIM2
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_EQ_EXTRACT_ELIM3
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_EQ_NOT_SOLVE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_EQ_XOR_SOLVE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_EXTRACT_CONCAT_1
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_EXTRACT_CONCAT_2
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_EXTRACT_CONCAT_3
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_EXTRACT_CONCAT_4
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_EXTRACT_EXTRACT
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_EXTRACT_MULT_LEADING_BIT
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_EXTRACT_NOT
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_EXTRACT_SIGN_EXTEND_1
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_EXTRACT_SIGN_EXTEND_2
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_EXTRACT_SIGN_EXTEND_3
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_EXTRACT_WHOLE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_ITE_CONST_CHILDREN_1
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_ITE_CONST_CHILDREN_2
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_ITE_EQUAL_CHILDREN
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_ITE_EQUAL_COND_1
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_ITE_EQUAL_COND_2
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_ITE_EQUAL_COND_3
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_ITE_MERGE_ELSE_ELSE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_ITE_MERGE_ELSE_IF
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_ITE_MERGE_THEN_ELSE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_ITE_MERGE_THEN_IF
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_ITE_WIDTH_ONE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_ITE_WIDTH_ONE_NOT
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_LSHR_BY_CONST_0
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_LSHR_BY_CONST_1
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_LSHR_BY_CONST_2
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_LSHR_ZERO
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_LT_SELF
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_MERGE_SIGN_EXTEND_1
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_MERGE_SIGN_EXTEND_2
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_MULT_POW2_1
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_MULT_POW2_2
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_MULT_POW2_2B
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_MULT_SLT_MULT_1
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_MULT_SLT_MULT_2
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_NAND_ELIMINATE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_NEGO_ELIMINATE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_NOR_ELIMINATE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_NOT_IDEMP
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_NOT_NEQ
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_NOT_ULT
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_NOT_XOR
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_OR_CONCAT_PULLUP
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_OR_CONCAT_PULLUP2
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_OR_CONCAT_PULLUP3
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_OR_SIMPLIFY_1
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_OR_SIMPLIFY_2
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_REDAND_ELIMINATE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_REDOR_ELIMINATE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_REPEAT_ELIM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_ROTATE_LEFT_ELIMINATE_1
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_ROTATE_LEFT_ELIMINATE_2
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_ROTATE_RIGHT_ELIMINATE_1
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_ROTATE_RIGHT_ELIMINATE_2
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_SADDO_ELIMINATE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_SDIVO_ELIMINATE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_SDIV_ELIMINATE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_SGE_ELIMINATE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_SGT_ELIMINATE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_SHL_BY_CONST_0
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_SHL_BY_CONST_1
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_SHL_BY_CONST_2
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_SHL_ZERO
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_SIGN_EXTEND_ELIMINATE_0
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_SIGN_EXTEND_EQ_CONST_1
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_SIGN_EXTEND_EQ_CONST_2
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_SIGN_EXTEND_ULT_CONST_1
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_SIGN_EXTEND_ULT_CONST_2
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_SIGN_EXTEND_ULT_CONST_3
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_SIGN_EXTEND_ULT_CONST_4
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_SLE_ELIMINATE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_SLE_SELF
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_SMOD_ELIMINATE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_SMULO_ELIM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_SREM_ELIMINATE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_SSUBO_ELIMINATE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_SUB_ELIMINATE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_UADDO_ELIMINATE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_UDIV_ONE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_UDIV_POW2_NOT_ONE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_UDIV_ZERO
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_UGE_ELIMINATE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_UGT_ELIMINATE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_UGT_UREM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_ULE_ELIMINATE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_ULE_MAX
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_ULE_SELF
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_ULE_ZERO
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_ULT_ADD_ONE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_ULT_ONE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_ULT_ONES
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_ULT_SELF
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_ULT_ZERO_1
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_ULT_ZERO_2
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_UMULO_ELIM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_UREM_ONE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_UREM_POW2_NOT_ONE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_UREM_SELF
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_USUBO_ELIMINATE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_XNOR_ELIMINATE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_XOR_CONCAT_PULLUP
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_XOR_CONCAT_PULLUP2
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_XOR_CONCAT_PULLUP3
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_XOR_DUPLICATE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_XOR_NOT
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_XOR_ONES
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_XOR_SIMPLIFY_1
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_XOR_SIMPLIFY_2
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_XOR_SIMPLIFY_3
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_ZERO_EXTEND_ELIMINATE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_ZERO_EXTEND_ELIMINATE_0
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_ZERO_EXTEND_EQ_CONST_1
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_ZERO_EXTEND_EQ_CONST_2
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_ZERO_EXTEND_ULT_CONST_1
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_ZERO_EXTEND_ULT_CONST_2
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_BV_ZERO_ULE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_DISTINCT_BINARY_ELIM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_DISTINCT_CARD_CONFLICT
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_DISTINCT_ELIM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_DT_COLLAPSE_SELECTOR
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_DT_COLLAPSE_TESTER
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_DT_COLLAPSE_TESTER_SINGLETON
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_DT_COLLAPSE_UPDATER
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_DT_CONS_EQ
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_DT_CONS_EQ_CLASH
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_DT_CYCLE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_DT_INST
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_DT_MATCH_ELIM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_DT_UPDATER_ELIM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_EQ_COND_DEQ
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_EQ_ITE_LIFT
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_EQ_REFL
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_EQ_SYMM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_EXISTS_ELIM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_INT_TO_BV_ELIM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ITE_ELSE_FALSE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ITE_ELSE_LOOKAHEAD
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ITE_ELSE_LOOKAHEAD_NOT_SELF
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ITE_ELSE_LOOKAHEAD_SELF
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ITE_ELSE_NEG_LOOKAHEAD
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ITE_ELSE_TRUE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ITE_EQ_BRANCH
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ITE_EXPAND
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ITE_FALSE_COND
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ITE_NEG_BRANCH
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ITE_NOT_COND
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ITE_THEN_FALSE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ITE_THEN_LOOKAHEAD
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ITE_THEN_LOOKAHEAD_NOT_SELF
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ITE_THEN_LOOKAHEAD_SELF
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ITE_THEN_NEG_LOOKAHEAD
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ITE_THEN_TRUE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_ITE_TRUE_COND
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_LAMBDA_ELIM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_LAST
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_MACRO_ARITH_INT_EQ_CONFLICT
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_MACRO_ARITH_INT_GEQ_TIGHTEN
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_MACRO_ARITH_STRING_PRED_ENTAIL
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_MACRO_ARRAYS_NORMALIZE_CONSTANT
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_MACRO_ARRAYS_NORMALIZE_OP
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_MACRO_BOOL_BV_INVERT_SOLVE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_MACRO_BOOL_NNF_NORM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_MACRO_BV_AND_OR_XOR_CONCAT_PULLUP
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_MACRO_BV_AND_SIMPLIFY
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_MACRO_BV_CONCAT_CONSTANT_MERGE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_MACRO_BV_CONCAT_EXTRACT_MERGE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_MACRO_BV_EQ_SOLVE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_MACRO_BV_EXTRACT_CONCAT
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_MACRO_BV_MULT_SLT_MULT
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_MACRO_BV_OR_SIMPLIFY
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_MACRO_BV_XOR_SIMPLIFY
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_MACRO_DT_CONS_EQ
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_MACRO_LAMBDA_CAPTURE_AVOID
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_MACRO_QUANT_DT_VAR_EXPAND
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_MACRO_QUANT_MERGE_PRENEX
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_MACRO_QUANT_MINISCOPE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_MACRO_QUANT_PARTITION_CONNECTED_FV
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_MACRO_QUANT_PRENEX
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_MACRO_QUANT_REWRITE_BODY
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_MACRO_QUANT_VAR_ELIM_EQ
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_MACRO_QUANT_VAR_ELIM_INEQ
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_MACRO_RE_INTER_UNION_CONST_ELIM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_MACRO_RE_INTER_UNION_INCLUSION
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_MACRO_STR_COMPONENT_CTN
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_MACRO_STR_CONST_NCTN_CONCAT
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_MACRO_STR_EQ_LEN_UNIFY
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_MACRO_STR_EQ_LEN_UNIFY_PREFIX
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_MACRO_STR_IN_RE_INCLUSION
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_MACRO_STR_SPLIT_CTN
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_MACRO_STR_STRIP_ENDPOINTS
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_MACRO_SUBSTR_STRIP_SYM_LENGTH
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_NONE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_QUANT_DT_SPLIT
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_QUANT_MERGE_PRENEX
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_QUANT_MINISCOPE_AND
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_QUANT_MINISCOPE_ITE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_QUANT_MINISCOPE_OR
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_QUANT_UNUSED_VARS
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_QUANT_VAR_ELIM_EQ
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_RE_ALL_ELIM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_RE_CONCAT_MERGE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_RE_CONCAT_STAR_REPEAT
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_RE_CONCAT_STAR_SUBSUME1
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_RE_CONCAT_STAR_SUBSUME2
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_RE_CONCAT_STAR_SWAP
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_RE_DIFF_ELIM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_RE_EQ_ELIM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_RE_INTER_ALL
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_RE_INTER_CSTRING
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_RE_INTER_CSTRING_NEG
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_RE_INTER_INCLUSION
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_RE_IN_COMP
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_RE_IN_CSTRING
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_RE_IN_EMPTY
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_RE_IN_SIGMA
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_RE_IN_SIGMA_STAR
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_RE_LOOP_ELIM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_RE_LOOP_NEG
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_RE_OPT_ELIM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_RE_PLUS_ELIM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_RE_REPEAT_ELIM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_RE_STAR_EMP
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_RE_STAR_NONE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_RE_STAR_STAR
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_RE_STAR_UNION_DROP_EMP
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_RE_UNION_ALL
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_RE_UNION_CONST_ELIM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_RE_UNION_INCLUSION
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_SEQ_EVAL_OP
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_SEQ_LEN_EMPTY
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_SEQ_LEN_REV
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_SEQ_LEN_UNIT
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_SEQ_NTH_UNIT
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_SEQ_REV_CONCAT
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_SEQ_REV_REV
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_SEQ_REV_UNIT
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_SETS_CARD_EMP
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_SETS_CARD_MINUS
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_SETS_CARD_SINGLETON
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_SETS_CARD_UNION
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_SETS_CHOOSE_SINGLETON
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_SETS_EQ_SINGLETON_EMP
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_SETS_EVAL_OP
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_SETS_INSERT_ELIM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_SETS_INTER_COMM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_SETS_INTER_EMP1
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_SETS_INTER_EMP2
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_SETS_INTER_MEMBER
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_SETS_IS_EMPTY_ELIM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_SETS_IS_SINGLETON_ELIM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_SETS_MEMBER_EMP
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_SETS_MEMBER_SINGLETON
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_SETS_MINUS_EMP1
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_SETS_MINUS_EMP2
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_SETS_MINUS_MEMBER
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_SETS_MINUS_SELF
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_SETS_SUBSET_ELIM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_SETS_UNION_COMM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_SETS_UNION_EMP1
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_SETS_UNION_EMP2
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_SETS_UNION_MEMBER
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_AT_ELIM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_CONCAT_CLASH
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_CONCAT_CLASH2
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_CONCAT_CLASH2_REV
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_CONCAT_CLASH_REV
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_CONCAT_UNIFY
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_CONCAT_UNIFY_BASE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_CONCAT_UNIFY_BASE_REV
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_CONCAT_UNIFY_REV
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_CONTAINS_CHAR
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_CONTAINS_CONCAT_FIND
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_CONTAINS_CONCAT_FIND_CONTRA
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_CONTAINS_EMP
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_CONTAINS_LEQ_LEN_EQ
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_CONTAINS_REFL
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_CONTAINS_REPL_CHAR
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_CONTAINS_REPL_SELF
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_CONTAINS_REPL_SELF_TGT_CHAR
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_CONTAINS_REPL_TGT
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_CONTAINS_SPLIT_CHAR
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_CTN_MULTISET_SUBSET
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_EQ_CTN_FALSE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_EQ_CTN_FULL_FALSE1
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_EQ_CTN_FULL_FALSE2
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_EQ_LEN_FALSE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_EQ_REPL_EMP_TGT_NEMP
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_EQ_REPL_LEN_ONE_EMP_PREFIX
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_EQ_REPL_NEMP_SRC_EMP
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_EQ_REPL_NO_CHANGE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_EQ_REPL_SELF_EMP
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_EQ_REPL_SELF_SRC
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_EQ_REPL_TGT_EQ_LEN
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_FROM_INT_NO_CTN_NONDIGIT
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_INDEXOF_CONTAINS_PRE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_INDEXOF_EQ_IRR
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_INDEXOF_FIND_EMP
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_INDEXOF_NO_CONTAINS
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_INDEXOF_OOB
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_INDEXOF_OOB2
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_INDEXOF_RE_EMP_RE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_INDEXOF_RE_EVAL
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_INDEXOF_RE_NONE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_INDEXOF_SELF
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_IN_RE_CONCAT_STAR_CHAR
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_IN_RE_CONSUME
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_IN_RE_CONTAINS
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_IN_RE_EVAL
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_IN_RE_FROM_INT_DIG_RANGE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_IN_RE_FROM_INT_NEMP_DIG_RANGE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_IN_RE_INTER_ELIM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_IN_RE_RANGE_ELIM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_IN_RE_SIGMA
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_IN_RE_SIGMA_STAR
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_IN_RE_UNION_ELIM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_LEN_CONCAT_REC
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_LEN_EQ_ZERO_BASE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_LEN_EQ_ZERO_CONCAT_REC
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_LEN_REPLACE_ALL_INV
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_LEN_REPLACE_INV
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_LEN_SUBSTR_IN_RANGE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_LEN_UPDATE_INV
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_LEQ_CONCAT_BASE_1
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_LEQ_CONCAT_BASE_2
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_LEQ_CONCAT_FALSE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_LEQ_CONCAT_TRUE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_LEQ_EMPTY
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_LEQ_EMPTY_EQ
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_LT_ELIM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_OVERLAP_ENDPOINTS_CTN
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_OVERLAP_ENDPOINTS_INDEXOF
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_OVERLAP_ENDPOINTS_REPLACE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_OVERLAP_SPLIT_CTN
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_PREFIXOF_ELIM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_PREFIXOF_EQ
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_PREFIXOF_ONE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_REPLACE_ALL_NO_CONTAINS
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_REPLACE_DUAL_CTN
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_REPLACE_DUAL_CTN_FALSE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_REPLACE_EMPTY
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_REPLACE_EMP_CTN_SRC
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_REPLACE_FIND_BASE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_REPLACE_FIND_FIRST_CONCAT
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_REPLACE_FIND_PRE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_REPLACE_ID
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_REPLACE_NO_CONTAINS
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_REPLACE_ONE_PRE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_REPLACE_PREFIX
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_REPLACE_RE_ALL_EVAL
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_REPLACE_RE_ALL_NONE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_REPLACE_RE_EVAL
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_REPLACE_RE_NONE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_REPLACE_SELF
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_REPLACE_SELF_CTN_SIMP
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_REPL_REPL_DUAL_ITE1
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_REPL_REPL_DUAL_ITE2
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_REPL_REPL_DUAL_SELF
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_REPL_REPL_LEN_ID
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_REPL_REPL_LOOKAHEAD_ID_SIMP
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_REPL_REPL_SRC_INV_NO_CTN1
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_REPL_REPL_SRC_INV_NO_CTN2
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_REPL_REPL_SRC_INV_NO_CTN3
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_REPL_REPL_SRC_SELF
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_REPL_REPL_SRC_TGT_NO_CTN
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_REPL_REPL_TGT_NO_CTN
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_REPL_REPL_TGT_SELF
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_SUBSTR_CHAR_START_EQ_LEN
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_SUBSTR_COMBINE1
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_SUBSTR_COMBINE2
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_SUBSTR_COMBINE3
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_SUBSTR_COMBINE4
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_SUBSTR_CONCAT1
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_SUBSTR_CONCAT2
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_SUBSTR_CTN
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_SUBSTR_CTN_CONTRA
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_SUBSTR_EMPTY_RANGE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_SUBSTR_EMPTY_START
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_SUBSTR_EMPTY_START_NEG
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_SUBSTR_EMPTY_STR
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_SUBSTR_EQ_EMPTY
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_SUBSTR_EQ_EMPTY_LEQ_LEN
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_SUBSTR_FULL
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_SUBSTR_FULL_EQ
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_SUBSTR_LEN_INCLUDE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_SUBSTR_LEN_INCLUDE_PRE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_SUBSTR_LEN_NORM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_SUBSTR_REPLACE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_SUBSTR_SUBSTR_START_GEQ_LEN
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_SUBSTR_Z_EQ_EMPTY_LEQ
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_SUFFIXOF_ELIM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_SUFFIXOF_EQ
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_SUFFIXOF_ONE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_TO_INT_CONCAT_NEG_ONE
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_TO_LOWER_CONCAT
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_TO_LOWER_FROM_INT
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_TO_LOWER_LEN
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_TO_LOWER_UPPER
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_TO_UPPER_CONCAT
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_TO_UPPER_FROM_INT
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_TO_UPPER_LEN
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_TO_UPPER_LOWER
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_STR_UPDATE_IN_FIRST_CONCAT
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_UBV_TO_INT_ELIM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_UF_BV2NAT_GEQ_ELIM
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_UF_BV2NAT_INT2BV
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_UF_BV2NAT_INT2BV_EXTEND
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_UF_BV2NAT_INT2BV_EXTRACT
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_UF_INT2BV_BV2NAT
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_UF_INT2BV_BVULE_EQUIV
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_UF_INT2BV_BVULT_EQUIV
Cvc5ProofRewriteRule_CVC5_PROOF_REWRITE_RULE_UF_SBV_TO_INT_ELIM

Functions§

cvc5_add_plugin^⚠: Add plugin to this solver. Its callbacks will be called throughout the lifetime of this solver. @warning This function is experimental and may change in future versions. @param cvc5 The solver instance. @param plugin The plugin to add to this solver.
cvc5_add_sygus_assume^⚠: Add a forumla to the set of Sygus assumptions.
cvc5_add_sygus_constraint^⚠: Add a forumla to the set of Sygus constraints.
cvc5_add_sygus_inv_constraint^⚠: Add a set of Sygus constraints to the current state that correspond to an invariant synthesis problem.
cvc5_assert_formula^⚠: Assert a formula.
cvc5_block_model^⚠: Block the current model. Can be called only if immediately preceded by a SAT or INVALID query.
cvc5_block_model_values^⚠: Block the current model values of (at least) the values in terms. Can be called only if immediately preceded by a SAT query.
cvc5_check_sat^⚠: Check satisfiability.
cvc5_check_sat_assuming^⚠: Check satisfiability assuming the given formulas.
cvc5_check_synth^⚠: Try to find a solution for the synthesis conjecture corresponding to the current list of functions-to-synthesize, universal variables and constraints.
cvc5_check_synth_next^⚠: Try to find a next solution for the synthesis conjecture corresponding to the current list of functions-to-synthesize, universal variables and constraints. Must be called immediately after a successful call to check-synth or check-synth-next.
cvc5_close_output^⚠: Close output file configured for an output tag via cvc5_get_output().
cvc5_declare_dt^⚠: Create datatype sort.
cvc5_declare_fun^⚠: Declare n-ary function symbol.
cvc5_declare_oracle_fun^⚠: Declare an oracle function with reference to an implementation.
cvc5_declare_pool^⚠: Declare a symbolic pool of terms with the given initial value.
cvc5_declare_sep_heap^⚠: When using separation logic, this sets the location sort and the datatype sort to the given ones. This function should be invoked exactly once, before any separation logic constraints are provided.
cvc5_declare_sort^⚠: Declare uninterpreted sort.
cvc5_declare_sygus_var^⚠: Append \p symbol to the current list of universal variables.
cvc5_define_fun^⚠: Define n-ary function.
cvc5_define_fun_rec^⚠: Define recursive function.
cvc5_define_fun_rec_from_const^⚠: Define recursive function.
cvc5_define_funs_rec^⚠: Define recursive functions.
cvc5_delete^⚠: Delete a cvc5 solver instance. @param cvc5 The solver instance.
cvc5_dt_cons_copy^⚠: Make copy of datatype constructor, increases reference counter of cons.
cvc5_dt_cons_decl_add_selector^⚠: Add datatype selector declaration to a given constructor declaration. @param decl The datatype constructor declaration. @param name The name of the datatype selector declaration to add. @param sort The codomain sort of the datatype selector declaration to add.
cvc5_dt_cons_decl_add_selector_self^⚠: Add datatype selector declaration whose codomain type is the datatype itself to a given constructor declaration. @param decl The datatype constructor declaration. @param name The name of the datatype selector declaration to add.
cvc5_dt_cons_decl_add_selector_unresolved^⚠: Add datatype selector declaration whose codomain sort is an unresolved datatype with the given name to a given constructor declaration. @param decl The datatype constructor declaration. @param name The name of the datatype selector declaration to add. @param unres_name The name of the unresolved datatype. The codomain of the selector will be the resolved datatype with the given name.
cvc5_dt_cons_decl_copy^⚠: Make copy of datatype constructor declaration, increases reference counter of decl.
cvc5_dt_cons_decl_hash^⚠: Compute the hash value of a datatype constructor declaration. @param decl The datatype constructor declaration. @return The hash value of the datatype constructor declaration.
cvc5_dt_cons_decl_is_equal^⚠: Compare two datatype constructor declarations for structural equality. @param a The first datatype constructor declaration. @param b The second datatype constructor declaration. @return True if the datatype constructor declarations are equal.
cvc5_dt_cons_decl_release^⚠: Release copy of datatype constructor declaration, decrements reference counter of decl.
cvc5_dt_cons_decl_to_string^⚠: Get a string representation of a given constructor declaration. @param decl The datatype constructor declaration. @return The string representation. @note The returned char* pointer is only valid until the next call to this function.
cvc5_dt_cons_get_instantiated_term^⚠: Get the constructor term of this datatype constructor whose return type is sort.
cvc5_dt_cons_get_name^⚠: Get the name of a given datatype constructor. @param cons The datatype constructor. @return The name. @note The returned char* pointer is only valid until the next call to this function.
cvc5_dt_cons_get_num_selectors^⚠: Get the number of selectors of a given datatype constructor. @param cons The datatype constructor. @return The number of selectors.
cvc5_dt_cons_get_selector^⚠: Get the selector at index i of a given datatype constructor. @param cons The datatype constructor. @param index The index of the selector. @return The i^th DatatypeSelector.
cvc5_dt_cons_get_selector_by_name^⚠: Get the datatype selector with the given name. @note This is a linear search through the selectors, so in case of multiple, similarly-named selectors, the first is returned. @param cons The datatype constructor. @param name The name of the datatype selector. @return The first datatype selector with the given name.
cvc5_dt_cons_get_term^⚠: Get the constructor term of a given datatype constructor.
cvc5_dt_cons_get_tester_term^⚠: Get the tester term of a given datatype constructor.
cvc5_dt_cons_hash^⚠: Compute the hash value of a datatype constructor. @param cons The datatype constructor. @return The hash value of the datatype constructor.
cvc5_dt_cons_is_equal^⚠: Compare two datatype constructors for structural equality. @param a The first datatype constructor. @param b The second datatype constructor. @return True if the datatype constructors are equal.
cvc5_dt_cons_release^⚠: Release copy of datatype constructor, decrements reference counter of cons.
cvc5_dt_cons_to_string^⚠: Get a string representation of a given datatype constructor. @param cons The datatype constructor. @return The string representation. @note The returned char* pointer is only valid until the next call to this function.
cvc5_dt_copy^⚠: Make copy of datatype, increases reference counter of dt.
cvc5_dt_decl_add_constructor^⚠: Add datatype constructor declaration. @param decl The datatype declaration. @param ctor The datatype constructor declaration to add.
cvc5_dt_decl_copy^⚠: Make copy of datatype declaration, increases reference counter of decl.
cvc5_dt_decl_get_name^⚠: Get the name of a given datatype declaration. @param decl The datatype declaration. @return The name of the datatype declaration. @note The returned char* pointer is only valid until the next call to this function.
cvc5_dt_decl_get_num_constructors^⚠: Get the number of constructors for a given Datatype declaration. @param decl The datatype declaration. @return The number of constructors.
cvc5_dt_decl_hash^⚠: Compute the hash value of a datatype declaration. @param decl The datatype declaration. @return The hash value of the datatype declaration.
cvc5_dt_decl_is_equal^⚠: Compare two datatype declarations for structural equality. @param a The first datatype declaration. @param b The second datatype declaration. @return True if the datatype declarations are equal.
cvc5_dt_decl_is_parametric^⚠: Determine if a given Datatype declaration is parametric. @warning This function is experimental and may change in future versions. @param decl The datatype declaration. @return True if the datatype declaration is parametric.
cvc5_dt_decl_is_resolved^⚠: Determine if a given datatype declaration is resolved (has already been used to declare a datatype). @param decl The datatype declaration. @return True if the datatype declaration is resolved.
cvc5_dt_decl_release^⚠: Release copy of datatype declaration, decrements reference counter of decl.
cvc5_dt_decl_to_string^⚠: Get a string representation of a given datatype declaration. @param decl The datatype declaration. @return A string representation of the datatype declaration. @note The returned char* pointer is only valid until the next call to this function.
cvc5_dt_get_constructor^⚠: Get the datatype constructor of a given datatype at a given index. @param dt The datatype. @param idx The index of the datatype constructor to return. @return The datatype constructor with the given index.
cvc5_dt_get_constructor_by_name^⚠: Get the datatype constructor of a given datatype with the given name. @note This is a linear search through the constructors, so in case of multiple, similarly-named constructors, the first is returned. @param dt The datatype. @param name The name of the datatype constructor. @return The datatype constructor with the given name.
cvc5_dt_get_name^⚠: Get the name of a given datatype. @param dt The datatype. @return The name. @note The returned char* pointer is only valid until the next call to this function.
cvc5_dt_get_num_constructors^⚠: Get the number of constructors of a given datatype. @param dt The datatype. @return The number of constructors.
cvc5_dt_get_parameters^⚠: Get the parameters of a given datatype, if it is parametric. @note Asserts that this datatype is parametric. @warning This function is experimental and may change in future versions. @param dt The datatype. @param size The size of the resulting array. @return The parameters of this datatype.
cvc5_dt_get_selector^⚠: Get the datatype selector of a given datatype with the given name. @note This is a linear search through the constructors and their selectors, so in case of multiple, similarly-named selectors, the first is returned. @param dt The datatype. @param name The name of the datatype selector. @return The datatype selector with the given name.
cvc5_dt_hash^⚠: Compute the hash value of a datatype. @param dt The datatype. @return The hash value of the datatype.
cvc5_dt_is_codatatype^⚠: Determine if a given datatype corresponds to a co-datatype. @param dt The datatype. @return True if the datatype corresponds to a co-datatype.
cvc5_dt_is_equal^⚠: Compare two datatypes for structural equality. @param a The first datatype. @param b The second datatype. @return True if the datatypes are equal.
cvc5_dt_is_finite^⚠: Determine if a given datatype is finite. @param dt The datatype. @return True if the datatype is finite.
cvc5_dt_is_parametric^⚠: Determine if a given datatype is parametric. @warning This function is experimental and may change in future versions. @param dt The datatype. @return True if the datatype is parametric.
cvc5_dt_is_record^⚠: Determine if a given datatype corresponds to a record. @warning This function is experimental and may change in future versions. @param dt The datatype. @return True if the datatype corresponds to a record.
cvc5_dt_is_tuple^⚠: Determine if a given datatype corresponds to a tuple. @param dt The datatype. @return True if this datatype corresponds to a tuple.
cvc5_dt_is_well_founded^⚠: Determine if a given datatype is well-founded.
cvc5_dt_release^⚠: Release copy of datatype, decrements reference counter of dt.
cvc5_dt_sel_copy^⚠: Make copy of datatype selector, increases reference counter of sel.
cvc5_dt_sel_get_codomain_sort^⚠: Get the codomain sort of a given datatype selector. @param sel The datatype selector. @return The codomain sort of the selector.
cvc5_dt_sel_get_name^⚠: Get the name of a given datatype selector. @param sel The datatype selector. @return The name of the Datatype selector. @note The returned char* pointer is only valid until the next call to this function.
cvc5_dt_sel_get_term^⚠: Get the selector term of a given datatype selector.
cvc5_dt_sel_get_updater_term^⚠: Get the updater term of a given datatype selector.
cvc5_dt_sel_hash^⚠: Compute the hash value of a datatype selector. @param sel The datatype selector. @return The hash value of the datatype selector.
cvc5_dt_sel_is_equal^⚠: Compare two datatype selectors for structural equality. @param a The first datatype selector. @param b The second datatype selector. @return True if the datatype selectors are equal.
cvc5_dt_sel_release^⚠: Release copy of datatype selector, decrements reference counter of sel.
cvc5_dt_sel_to_string^⚠: Get the string representation of a given datatype selector. @param sel The datatype selector. @return The string representation. @note The returned char* pointer is only valid until the next call to this function.
cvc5_dt_to_string^⚠: Get a string representation of a given datatype. @return The string representation. @note The returned char* pointer is only valid until the next call to this function.
cvc5_find_synth^⚠: Find a target term of interest using sygus enumeration, with no provided grammar.
cvc5_find_synth_next^⚠: Try to find a next target term of interest using sygus enumeration. Must be called immediately after a successful call to find-synth or find-synth-next.
cvc5_find_synth_with_grammar^⚠: Find a target term of interest using sygus enumeration with a provided grammar.
cvc5_get_abduct^⚠: Get an abduct.
cvc5_get_abduct_next^⚠: Get the next abduct. Can only be called immediately after a successful call to get-abduct or get-abduct-next. Is guaranteed to produce a syntactically different abduct wrt the last returned abduct if successful.
cvc5_get_abduct_with_grammar^⚠: Get an abduct.
cvc5_get_assertions^⚠: Get the list of asserted formulas.
cvc5_get_boolean_sort^⚠: Get the Boolean sort. @param tm The term manager instance. @return Sort Boolean.
cvc5_get_difficulty^⚠: Get a difficulty estimate for an asserted formula. This function is intended to be called immediately after any response to a checkSat.
cvc5_get_info^⚠: Get info from the solver.
cvc5_get_instantiations^⚠: @warning This function is experimental and may change in future versions.
cvc5_get_integer_sort^⚠: Get the Integer sort. @param tm The term manager instance. @return Sort Integer.
cvc5_get_interpolant^⚠: Get an interpolant.
cvc5_get_interpolant_next^⚠: Get the next interpolant. Can only be called immediately after a successful call to get-interpolant or get-interpolant-next. Is guaranteed to produce a syntactically different interpolant wrt the last returned interpolant if successful.
cvc5_get_interpolant_with_grammar^⚠: Get an interpolant
cvc5_get_learned_literals^⚠: Get a list of learned literals that are entailed by the current set of assertions.
cvc5_get_logic^⚠: Get the logic set the solver. @note Asserts `cvc5_is_logic_set()1. @return The logic used by the solver. @note The returned char* pointer is only valid until the next call to this function.
cvc5_get_model^⚠: Get the model
cvc5_get_model_domain_elements^⚠: Get the domain elements of uninterpreted sort s in the current model. The current model interprets s as the finite sort whose domain elements are given in the return value of this function.
cvc5_get_num_idxs_for_skolem_id^⚠: Get the number of indices for a skolem id. @param tm The term manager instance. @param id The skolem id. @return The number of indices for the skolem id.
cvc5_get_option^⚠: Get the value of a given option.
cvc5_get_option_info^⚠: Get some information about a given option. See struct Cvc5OptionInfo for more details on which information is available. @param cvc5 The solver instance. @param option The option for which the info is queried. @param info The output parameter for the queried info. @note The returned Cvc5OptionInfo data is only valid until the next call to this function.
cvc5_get_option_names^⚠: Get all option names that can be used with cvc5_set_option(), cvc5_get_option() and cvc5_get_option_info(). @param cvc5 The solver instance. @param size The size of the resulting option names array. @return All option names. @note The returned char* pointer is only valid until the next call to this function.
cvc5_get_output^⚠: Configure a file to write the output for a given tag.
cvc5_get_proof^⚠: Get a proof associated with the most recent call to checkSat.
cvc5_get_quantifier_elimination^⚠: Do quantifier elimination.
cvc5_get_quantifier_elimination_disjunct^⚠: Do partial quantifier elimination, which can be used for incrementally computing the result of a quantifier elimination.
cvc5_get_real_sort^⚠: Get the Real sort. @param tm The term manager instance. @return Sort Real.
cvc5_get_regexp_sort^⚠: Get the regular expression sort. @param tm The term manager instance. @return Sort RegExp.
cvc5_get_rm_sort^⚠: Get the rounding mode sort. @param tm The term manager instance. @return The rounding mode sort.
cvc5_get_statistics^⚠: Get a snapshot of the current state of the statistic values of this solver. The returned object is completely decoupled from the solver and will not change when the solver is used again. @param cvc5 The solver instance. @return A snapshot of the current state of the statistic values.
cvc5_get_string_sort^⚠: Get the string sort. @param tm The term manager instance. @return Sort String.
cvc5_get_sygus_assumptions^⚠: Get the list of sygus assumptions.
cvc5_get_sygus_constraints^⚠: Get the list of sygus constraints.
cvc5_get_synth_solution^⚠: Get the synthesis solution of the given term. This function should be called immediately after the solver answers unsat for sygus input. @param cvc5 The solver instance. @param term The term for which the synthesis solution is queried. @return The synthesis solution of the given term.
cvc5_get_synth_solutions^⚠: Get the synthesis solutions of the given terms. This function should be called immediately after the solver answers unsat for sygus input. @param cvc5 The solver instance. @param size The size of the terms array. @param terms The terms for which the synthesis solutions is queried. @return The synthesis solutions of the given terms.
cvc5_get_timeout_core^⚠: Get a timeout core.
cvc5_get_timeout_core_assuming^⚠: Get a timeout core of the given assumptions.
cvc5_get_tm^⚠: Get the associated term manager of a cvc5 solver instance. @param cvc5 The solver instance. @return The term manager.
cvc5_get_unsat_assumptions^⚠: Get the set of unsat (“failed”) assumptions.
cvc5_get_unsat_core^⚠: Get the unsatisfiable core.
cvc5_get_unsat_core_lemmas^⚠: Get the lemmas used to derive unsatisfiability.
cvc5_get_value^⚠: Get the value of the given term in the current model.
cvc5_get_value_sep_heap^⚠: When using separation logic, obtain the term for the heap.
cvc5_get_value_sep_nil^⚠: When using separation logic, obtain the term for nil.
cvc5_get_values^⚠: Get the values of the given terms in the current model.
cvc5_get_version^⚠: Get a string representation of the version of this solver. @param cvc5 The solver instance. @return The version string. @note The returned char* pointer is only valid until the next call to this function.
cvc5_grammar_add_any_constant^⚠: Allow symbol to be an arbitrary constant of a given grammar. @param grammar The grammar. @param symbol The non-terminal allowed to be any constant.
cvc5_grammar_add_any_variable^⚠: Allow symbol to be any input variable of a given grammar to corresponding synth-fun/synth-inv with the same sort as symbol. @param grammar The grammar. @param symbol The non-terminal allowed to be any input variable.
cvc5_grammar_add_rule^⚠: Add rule to the set of rules corresponding to symbol of a given grammar. @param grammar The grammar. @param symbol The non-terminal to which the rule is added. @param rule The rule to add.
cvc5_grammar_add_rules^⚠: Add rules to the set of rules corresponding to symbol of a given grammar. @param grammar The grammar. @param symbol The non-terminal to which the rules are added. @param size The number of rules to add. @param rules The rules to add.
cvc5_grammar_copy^⚠: Make copy of grammar, increases reference counter of grammar.
cvc5_grammar_hash^⚠: Compute the hash value of a grammar. @param grammar The grammar. @return The hash value of the grammar.
cvc5_grammar_is_disequal^⚠: Compare two grammars for referential disequality. @param a The first grammar. @param b The second grammar. @return True if both grammar pointers point to different internal grammar objects.
cvc5_grammar_is_equal^⚠: Compare two grammars for referential equality. @param a The first grammar. @param b The second grammar. @return True if both grammar pointers point to the same internal grammar object.
cvc5_grammar_release^⚠: Release copy of grammar, decrements reference counter of grammar.
cvc5_grammar_to_string^⚠: Get a string representation of a given grammar. @param grammar The grammar. @return A string representation of the grammar. @note The returned char* pointer is only valid until the next call to this function.
cvc5_is_logic_set^⚠: Determine if cvc5_set_logic() has been called.
cvc5_is_model_core_symbol^⚠: Determine if the model value of the given free constant was essential for showing satisfiability of the last cvc5_check_sat() query based on the current model.
cvc5_is_output_on^⚠: Determines if the output stream for the given tag is enabled. Tags can be enabled with the output option (and -o <tag> on the command line).
cvc5_kind_hash^⚠: Hash function for Cvc5Kinds. @param kind The kind. @return The hash value.
cvc5_kind_to_string^⚠: Get a string representation of a Cvc5Kind. @param kind The kind. @return The string representation.
cvc5_mk_abstract_sort^⚠: Create an abstract sort. An abstract sort represents a sort for a given kind whose parameters and arguments are unspecified.
cvc5_mk_array_sort^⚠: Create an array sort. @param tm The term manager instance. @param index The array index sort. @param elem The array element sort. @return The array sort.
cvc5_mk_bag_sort^⚠: Create a bag sort. @param tm The term manager instance. @param sort The sort of the bag elements. @return The bag sort.
cvc5_mk_boolean^⚠: Create a Boolean constant. @param tm The term manager instance. @return The Boolean constant. @param val The value of the constant.
cvc5_mk_bv^⚠: Create a bit-vector constant of a given bit-width from a given string of base 2, 10 or 16.
cvc5_mk_bv_sort^⚠: Create a bit-vector sort. @param tm The term manager instance. @param size The bit-width of the bit-vector sort. @return The bit-vector sort.
cvc5_mk_bv_uint64^⚠: Create a bit-vector constant of given size and value.
cvc5_mk_cardinality_constraint^⚠: Create a cardinality constraint for an uninterpreted sort.
cvc5_mk_const^⚠: Create a free constant.
cvc5_mk_const_array^⚠: Create a constant array with the provided constant value stored at every index. @param tm The term manager instance. @param sort The sort of the constant array (must be an array sort). @param val The constant value to store (must match the sort’s element sort). @return The constant array term.
cvc5_mk_dt_cons_decl^⚠: Create a datatype constructor declaration. @param tm The term manager instance. @param name The name of the datatype constructor. @return The DatatypeConstructorDecl.
cvc5_mk_dt_decl^⚠: Create a datatype declaration. @param tm The term manager instance. @param name The name of the datatype. @param is_codt True if a codatatype is to be constructed. @return The Cvc5DatatypeDecl.
cvc5_mk_dt_decl_with_params^⚠: Create a datatype declaration. Create sorts parameter with cvc5_mk_param_sort().
cvc5_mk_dt_sort^⚠: Create a datatype sort. @param tm The term manager instance. @param decl The datatype declaration from which the sort is created. @return The datatype sort.
cvc5_mk_dt_sorts^⚠: Create a vector of datatype sorts. @note The names of the datatype declarations must be distinct. @param tm The term manager instance. @param size The number of datatype declarations. @param decls The datatype declarations from which the sort is created. @return The datatype sorts.
cvc5_mk_empty_bag^⚠: Create a constant representing an empty bag of the given sort. @param tm The term manager instance. @param sort The sort of the bag elements. @return The empty bag constant.
cvc5_mk_empty_sequence^⚠: Create an empty sequence of the given element sort. @param tm The term manager instance. @param sort The element sort of the sequence. @return The empty sequence with given element sort.
cvc5_mk_empty_set^⚠: Create a constant representing an empty set of the given sort. @param tm The term manager instance. @param sort The sort of the set elements. @return The empty set constant.
cvc5_mk_false^⚠: Create a Boolean false constant. @param tm The term manager instance. @return The false constant.
cvc5_mk_ff_elem^⚠: Create a finite field constant in a given field from a given string of base n.
cvc5_mk_ff_sort^⚠: Create a finite-field sort from a given string of base n.
cvc5_mk_fp^⚠: Create a floating-point value from a bit-vector given in IEEE-754 format. @param tm The term manager instance. @param exp Size of the exponent. @param sig Size of the significand. @param val Value of the floating-point constant as a bit-vector term. @return The floating-point value.
cvc5_mk_fp_from_ieee^⚠: Create a floating-point value from its three IEEE-754 bit-vector value components (sign bit, exponent, significand). @param tm The term manager instance. @param sign The sign bit. @param exp The bit-vector representing the exponent. @param sig The bit-vector representing the significand. @return The floating-point value.
cvc5_mk_fp_nan^⚠: Create a not-a-number floating-point constant (Cvc5TermManager* tm, SMT-LIB: NaN). @param tm The term manager instance. @param exp Number of bits in the exponent. @param sig Number of bits in the significand. @return The floating-point constant.
cvc5_mk_fp_neg_inf^⚠: Create a negative infinity floating-point constant (SMT-LIB: -oo). @param tm The term manager instance. @param exp Number of bits in the exponent. @param sig Number of bits in the significand. @return The floating-point constant.
cvc5_mk_fp_neg_zero^⚠: Create a negative zero floating-point constant (Cvc5TermManager* tm, SMT-LIB: -zero). @param tm The term manager instance. @param exp Number of bits in the exponent. @param sig Number of bits in the significand. @return The floating-point constant.
cvc5_mk_fp_pos_inf^⚠: Create a positive infinity floating-point constant (SMT-LIB: +oo). @param tm The term manager instance. @param exp Number of bits in the exponent. @param sig Number of bits in the significand. @return The floating-point constant.
cvc5_mk_fp_pos_zero^⚠: Create a positive zero floating-point constant (Cvc5TermManager* tm, SMT-LIB: +zero). @param tm The term manager instance. @param exp Number of bits in the exponent. @param sig Number of bits in the significand. @return The floating-point constant.
cvc5_mk_fp_sort^⚠: Create a floating-point sort. @param tm The term manager instance. @param exp The bit-width of the exponent of the floating-point sort. @param sig The bit-width of the significand of the floating-point sort.
cvc5_mk_fun_sort^⚠: Create function sort. @param tm The term manager instance. @param size The number of domain sorts. @param sorts The sort of the function arguments (the domain sorts). @param codomain The sort of the function return value. @return The function sort.
cvc5_mk_grammar^⚠: Create a Sygus grammar. The first non-terminal is treated as the starting non-terminal, so the order of non-terminals matters.
cvc5_mk_integer^⚠: Create an integer constant from a string. @param tm The term manager instance. @param s The string representation of the constant, may represent an integer (e.g., “123”). @return A constant of sort Integer assuming s represents an integer)
cvc5_mk_integer_int64^⚠: Create an integer constant from a c++ int. @param tm The term manager instance. @param val The value of the constant. @return A constant of sort Integer.
cvc5_mk_nullable_is_null^⚠: Create a null tester for a nullable term. @param tm The term manager instance. @param term A nullable term. @return A tester whether term is null.
cvc5_mk_nullable_is_some^⚠: Create a some tester for a nullable term. @param tm The term manager instance. @param term A nullable term. @return A tester whether term is some.
cvc5_mk_nullable_lift^⚠: Create a term that lifts kind to nullable terms.
cvc5_mk_nullable_null^⚠: Create a constant representing an null of the given sort. @param tm The term manager instance. @param sort The sort of the Nullable element. @return The null constant.
cvc5_mk_nullable_some^⚠: Create a nullable some term. @param tm The term manager instance. @param term The element value. @return the Element value wrapped in some constructor.
cvc5_mk_nullable_sort^⚠: Create a nullable sort. @param tm The term manager instance. @param sort The sort of the element of the nullable. @return The nullable sort.
cvc5_mk_nullable_val^⚠: Create a selector for nullable term. @param tm The term manager instance. @param term A nullable term. @return The element value of the nullable term.
cvc5_mk_op^⚠: Create operator of Kind:
cvc5_mk_op_from_str^⚠: Create operator of kind:
cvc5_mk_param_sort^⚠: Create a sort parameter. @warning This function is experimental and may change in future versions. @param tm The term manager instance. @param symbol The name of the sort, may be NULL. @return The sort parameter.
cvc5_mk_pi^⚠: Create a constant representing the number Pi. @param tm The term manager instance. @return A constant representing Pi.
cvc5_mk_predicate_sort^⚠: Create a predicate sort. @note This is equivalent to calling mkFunctionSort() with the Boolean sort as the codomain. @param tm The term manager instance. @param size The number of sorts. @param sorts The list of sorts of the predicate. @return The predicate sort.
cvc5_mk_real^⚠: Create a real constant from a string. @param tm The term manager instance. @param s The string representation of the constant, may represent an integer (e.g., “123”) or real constant (e.g., “12.34” or “12/34”). @return A constant of sort Real.
cvc5_mk_real_int64^⚠: Create a real constant from an integer. @param tm The term manager instance. @param val The value of the constant. @return A constant of sort Integer.
cvc5_mk_real_num_den^⚠: Create a real constant from a rational. @param tm The term manager instance. @param num The value of the numerator. @param den The value of the denominator. @return A constant of sort Real.
cvc5_mk_record_sort^⚠: Create a record sort @warning This function is experimental and may change in future versions. @param tm The term manager instance. @param size The number of fields of the record. @param names The names of the fields of the record. @param sorts The sorts of the fields of the record. @return The record sort.
cvc5_mk_regexp_all^⚠: Create a regular expression all (re.all) term. @param tm The term manager instance. @return The all term.
cvc5_mk_regexp_allchar^⚠: Create a regular expression allchar (re.allchar) term. @param tm The term manager instance. @return The allchar term.
cvc5_mk_regexp_none^⚠: Create a regular expression none (re.none) term. @param tm The term manager instance. @return The none term.
cvc5_mk_rm^⚠: Create a rounding mode value. @param tm The term manager instance. @param rm The floating point rounding mode this constant represents. @return The rounding mode value.
cvc5_mk_sep_emp^⚠: Create a separation logic empty term.
cvc5_mk_sep_nil^⚠: Create a separation logic nil term.
cvc5_mk_sequence_sort^⚠: Create a sequence sort. @param tm The term manager instance. @param sort The sort of the sequence elements. @return The sequence sort.
cvc5_mk_set_sort^⚠: Create a set sort. @param tm The term manager instance. @param sort The sort of the set elements. @return The set sort.
cvc5_mk_skolem^⚠: Create a skolem. @param tm The term manager instance. @param id The skolem identifier. @param size The number of arguments of the lifted operator. @param indices The indices of the skolem. @return The skolem.
cvc5_mk_string^⚠: Create a String constant from a regular character string which may contain SMT-LIB compatible escape sequences like \u1234 to encode unicode characters. @param tm The term manager instance. @param s The string this constant represents. @param use_esc_seq Determines whether escape sequences in s should. be converted to the corresponding unicode character @return The String constant.
cvc5_mk_string_from_char32^⚠: Create a String constant from a UTF-32 string. This function does not support escape sequences as wide character already supports unicode characters. @param tm The term manager instance. @param s The UTF-32 string this constant represents. @return The String constant.
cvc5_mk_string_from_wchar^⚠: Create a String constant from a wide character string. This function does not support escape sequences as wide character already supports unicode characters. @param tm The term manager instance. @param s The string this constant represents. @return The String constant.
cvc5_mk_term^⚠: Create n-ary term of given kind. @param tm The term manager instance. @param kind The kind of the term. @param size The number of childrens. @param children The children of the term. @return The Term
cvc5_mk_term_from_op^⚠: Create n-ary term of given kind from a given operator. Create operators with cvc5_mk_op() and cvc5_mk_op_from_str(). @param tm The term manager instance. @param op The operator. @param size The number of children. @param children The children of the term. @return The Term.
cvc5_mk_true^⚠: Create a Boolean true constant. @param tm The term manager instance. @return The true constant.
cvc5_mk_tuple^⚠: Create a tuple term. @param tm The term manager instance. @param size The number of elements in the tuple. @param terms The elements. @return The tuple Term.
cvc5_mk_tuple_sort^⚠: Create a tuple sort. @param tm The term manager instance. @param size The number of sorts. @param sorts The sorts of f the elements of the tuple. @return The tuple sort.
cvc5_mk_uninterpreted_sort^⚠: Create an uninterpreted sort. @param tm The term manager instance. @param symbol The name of the sort, may be NULL. @return The uninterpreted sort.
cvc5_mk_uninterpreted_sort_constructor_sort^⚠: Create an uninterpreted sort constructor sort.
cvc5_mk_universe_set^⚠: Create a universe set of the given sort. @param tm The term manager instance. @param sort The sort of the set elements. @return The universe set constant.
cvc5_mk_unresolved_dt_sort^⚠: Create an unresolved datatype sort.
cvc5_mk_var^⚠: Create a bound variable to be used in a binder (i.e., a quantifier, a lambda, or a witness binder). @param tm The term manager instance. @param sort The sort of the variable. @param symbol The name of the variable, may be NULL. @return The variable.
cvc5_modes_block_models_mode_to_string^⚠: Get a string representation of a Cvc5BlockModelsMode. @param mode The mode. @return The string representation.
cvc5_modes_find_synth_target_to_string^⚠: Get a string representation of a Cvc5FindSynthTarget. @param target The synthesis find target. @return The string representation.
cvc5_modes_input_language_to_string^⚠: Get a string representation of a Cvc5InputLanguage. @param lang The input language. @return The string representation.
cvc5_modes_learned_lit_type_to_string^⚠: Get a string representation of a Cvc5LearnedLitType. @param type The learned literal type. @return The string representation.
cvc5_modes_option_category_to_string^⚠: Get a string representation of a Cvc5OptionCategory. @param cat The option category. @return The string representation.
cvc5_modes_proof_component_to_string^⚠: Get a string representation of a Cvc5ProofComponent. @param pc The proof component. @return The string representation.
cvc5_modes_proof_format_to_string^⚠: Get a string representation of a Cvc5ProofFormat. @param format The proof format. @return The string representation.
cvc5_new^⚠: Construct a new instance of a cvc5 solver. @param tm The associated term manager instance. @return The cvc5 solver instance.
cvc5_op_copy^⚠: Make copy of operator, increases reference counter of op.
cvc5_op_get_index^⚠: Get the index at position i of an indexed operator. @param op The operator. @param i The position of the index to return. @return The index at position i.
cvc5_op_get_kind^⚠: Get the kind of a given operator. @param op The operator. @return The kind of the operator.
cvc5_op_get_num_indices^⚠: Get the number of indices of a given operator. @param op The operator. @return The number of indices of the operator.
cvc5_op_hash^⚠: Compute the hash value of an operator. @param op The operator. @return The hash value of the operator.
cvc5_op_is_disequal^⚠: Compare two operators for syntactic disequality.
cvc5_op_is_equal^⚠: Compare two operators for syntactic equality.
cvc5_op_is_indexed^⚠: Determine if a given operator is indexed. @param op The operator. @return True iff the operator is indexed.
cvc5_op_release^⚠: Release copy of operator, decrements reference counter of op.
cvc5_op_to_string^⚠: Get a string representation of a given operator. @param op The operator. @return A string representation of the operator. @note The returned char* pointer is only valid until the next call to this function.
cvc5_option_info_to_string^⚠: Get a string representation of a given option info. @param info The option info. @return The string representation. @note The returned char* pointer is only valid until the next call to this function.
cvc5_pop^⚠: Pop (a) level(s) from the assertion stack.
cvc5_print_stats_safe^⚠: Print the statistics to the given file descriptor, suitable for usage in signal handlers. @param cvc5 The solver instance. @param fd The file descriptor.
cvc5_proof_copy^⚠: Make copy of proof, increases reference counter of proof.
cvc5_proof_get_arguments^⚠: Get the arguments of the root step of a given proof. @param proof The proof. @param size Output parameter to store the number of resulting argument terms. @return The argument terms.
cvc5_proof_get_children^⚠: Get the premises of the root step of a given proof. @param proof The proof. @param size Output parameter to store the number of resulting premise proofs. @return The premise proofs. @note The returned Cvc5Proof array pointer is only valid until the next call to this function.
cvc5_proof_get_result^⚠: Get the conclusion of the root step of a given proof. @param proof The proof. @return The conclusion term.
cvc5_proof_get_rewrite_rule^⚠: Get the proof rewrite rule used by the root step of the proof.
cvc5_proof_get_rule^⚠: Get the proof rule used by the root step of a given proof. @return The proof rule.
cvc5_proof_hash^⚠: Compute the hash value of a proof. @param proof The proof. @return The hash value of the proof.
cvc5_proof_is_disequal^⚠: Compare two proofs for referential disequality. @param a The first proof. @param b The second proof. @return True if both proof pointers point to different internal proof objects.
cvc5_proof_is_equal^⚠: Compare two proofs for referential equality. @param a The first proof. @param b The second proof. @return True if both proof pointers point to the same internal proof object.
cvc5_proof_release^⚠: Release copy of proof, decrements reference counter of proof.
cvc5_proof_rewrite_rule_hash^⚠: Hash function for Cvc5ProofRewriteRule. @param rule The proof rewrite rule. @return The hash value.
cvc5_proof_rewrite_rule_to_string^⚠: Get a string representation of a Cvc5ProofRewriteRule. @param rule The proof rewrite rule. @return The string representation.
cvc5_proof_rule_hash^⚠: Hash function for Cvc5ProofRule. @param rule The proof rule. @return The hash value.
cvc5_proof_rule_to_string^⚠: Get a string representation of a Cvc5ProofRule. @param rule The proof rule. @return The string representation.
cvc5_proof_to_string^⚠: Prints a proof as a string in a selected proof format mode. Other aspects of printing are taken from the solver options.
cvc5_push^⚠: Push (a) level(s) to the assertion stack.
cvc5_reset_assertions^⚠: Remove all assertions.
cvc5_result_copy^⚠: Make copy of result, increases reference counter of result.
cvc5_result_get_unknown_explanation^⚠: Get the explanation for an unknown result. @param result The result. @return An explanation for an unknown query result.
cvc5_result_hash^⚠: Compute the hash value of a result. @param result The result. @return The hash value of the result.
cvc5_result_is_disequal^⚠: Operator overloading for disequality of two results. @param a The first result to compare to for disequality. @param b The second result to compare to for disequality. @return True if the results are disequal.
cvc5_result_is_equal^⚠: Determine equality of two results. @param a The first result to compare to for equality. @param b The second result to compare to for equality. @return True if the results are equal.
cvc5_result_is_null^⚠: Determine if a given result is empty (a nullary result) and not an actual result returned from a cvc5_check_sat() (and friends) query. @param result The result. @return True if the given result is a nullary result.
cvc5_result_is_sat^⚠: Determine if given result is from a satisfiable cvc5_check_sat() or cvc5_check_sat_ssuming() query. @param result The result. @return True if result is from a satisfiable query.
cvc5_result_is_unknown^⚠: Determine if given result is from a cvc5_check_sat() or cvc5_check_sat_assuming() query and cvc5 was not able to determine (un)satisfiability. @param result The result. @return True if result is from a query where cvc5 was not able to determine (un)satisfiability.
cvc5_result_is_unsat^⚠: Determine if given result is from an unsatisfiable cvc5_check_sat() or cvc5_check_sat_assuming() query. @param result The result. @return True if result is from an unsatisfiable query.
cvc5_result_release^⚠: Release copy of result, decrements reference counter of result.
cvc5_result_to_string^⚠: Get the string representation of a given result. @param result The result. @return The string representation. @note The returned char* pointer is only valid until the next call to this function.
cvc5_rm_to_string^⚠: Get a string representation of a Cvc5RoundingMode. @param rm The rounding mode. @return The string representation.
cvc5_set_info^⚠: Set info.
cvc5_set_logic^⚠: Set logic.
cvc5_set_option^⚠: Set option.
cvc5_simplify^⚠: Simplify a formula without doing “much” work.
cvc5_skolem_id_hash^⚠: Hash function for Cvc5SkolemId. @param id The skolem id. @return The hash value.
cvc5_skolem_id_to_string^⚠: Get a string representation of a Cvc5SkolemId. @param id The skolem id. @return The string representation.
cvc5_sort_abstract_get_kind^⚠: Get the kind of an abstract sort, which denotes the sort kinds that the abstract sort denotes.
cvc5_sort_array_get_element_sort^⚠: Get the element sort of a given array sort. @param sort The sort. @return The array element sort of an array sort.
cvc5_sort_array_get_index_sort^⚠: Get the index sort of a given array sort. @param sort The sort. @return The array index sort of an array sort.
cvc5_sort_bag_get_element_sort^⚠: Get the element sort of a given bag sort. @param sort The sort. @return The element sort of a bag sort.
cvc5_sort_bv_get_size^⚠: Get the size of a bit-vector sort. @param sort The sort. @return The bit-width of the bit-vector sort.
cvc5_sort_compare^⚠: Compare two sorts for ordering. @param a The first sort. @param b The second sort. @return An integer value indicating the ordering: 0 if both sorts are equal, -1 if a < b, and 1 if b > a.
cvc5_sort_copy^⚠: Make copy of sort, increases reference counter of sort.
cvc5_sort_dt_constructor_get_arity^⚠: Get the arity of a datatype constructor sort. @param sort The sort. @return The arity of a datatype constructor sort.
cvc5_sort_dt_constructor_get_codomain^⚠: Get the codomain sort of a datatype constructor sort. @param sort The sort. @return The codomain sort of a constructor sort.
cvc5_sort_dt_constructor_get_domain^⚠: Get the domain sorts of a datatype constructor sort. @param sort The sort. @param size The size of the resulting array of domain sorts. @return The domain sorts of a datatype constructor sort.
cvc5_sort_dt_get_arity^⚠: Get the arity of a datatype sort, which is the number of type parameters if the datatype is parametric, or 0 otherwise. @param sort The sort. @return The arity of a datatype sort.
cvc5_sort_dt_selector_get_codomain^⚠: Get the codomain sort of a given datatype selector sort. @param sort The sort. @return The codomain sort of a datatype selector sort.
cvc5_sort_dt_selector_get_domain^⚠: Get the domain sort of a given datatype selector sort. @param sort The sort. @return The domain sort of a datatype selector sort.
cvc5_sort_dt_tester_get_codomain^⚠: Get the codomain dort of a given datatype tester sort (the Boolean sort). @param sort The sort. @return The codomain sort of a datatype tester sort.
cvc5_sort_dt_tester_get_domain^⚠: Get the domain sort of a given datatype tester sort. @param sort The sort. @return The domain sort of a datatype tester sort.
cvc5_sort_ff_get_size^⚠: Get the size of a finite field sort. @param sort The sort. @return The size of the finite field sort. @note The returned char* pointer is only valid until the next call to this function.
cvc5_sort_fp_get_exp_size^⚠: Get the exponent size of a floating-point sort. @param sort The sort. @return The bit-width of the exponent of the floating-point sort.
cvc5_sort_fp_get_sig_size^⚠: Get the significand size of a floating-point sort. @param sort The sort. @return The width of the significand of the floating-point sort.
cvc5_sort_fun_get_arity^⚠: Get the aritye of a given function sort. @param sort The sort. @return The arity of a function sort.
cvc5_sort_fun_get_codomain^⚠: Get the codomain of a given function sort. @param sort The sort. @return The codomain sort of a function sort.
cvc5_sort_fun_get_domain^⚠: Get the domain of a given function sort. @param sort The sort. @param size The size of the resulting array of domain sorts. @return The domain sorts of a function sort.
cvc5_sort_get_datatype^⚠: Get the underlying datatype of a datatype sort. @param sort The sort. @return The underlying datatype of a datatype sort.
cvc5_sort_get_instantiated_parameters^⚠: Get the sorts used to instantiate the sort parameters of a given parametric sort (parametric datatype or uninterpreted sort constructor sort, see cvc5_sort_instantiate();
cvc5_sort_get_kind^⚠: Get the kind of the given sort. @param sort The sort. @return The kind of the sort.
cvc5_sort_get_symbol^⚠: Get the symbol of this Sort.
cvc5_sort_get_uninterpreted_sort_constructor^⚠: Get the associated uninterpreted sort constructor of an instantiated uninterpreted sort.
cvc5_sort_has_symbol^⚠: Determine if the given sort has a symbol (a name).
cvc5_sort_hash^⚠: Compute the hash value of a sort. @param sort The sort. @return The hash value of the sort.
cvc5_sort_instantiate^⚠: Instantiate a parameterized datatype sort or uninterpreted sort constructor sort.
cvc5_sort_is_abstract^⚠: Determine if given sort is an abstract sort. @param sort The sort. @return True if the sort is a abstract sort.
cvc5_sort_is_array^⚠: Determine if given sort is an array sort. @param sort The sort. @return True if the sort is an array sort.
cvc5_sort_is_bag^⚠: Determine if given sort is a Bag sort. @param sort The sort. @return True if the sort is a Bag sort.
cvc5_sort_is_boolean^⚠: Determine if given sort is the Boolean sort (SMT-LIB: Bool). @param sort The sort. @return True if given sort is the Boolean sort.
cvc5_sort_is_bv^⚠: Determine if given sort is a bit-vector sort (SMT-LIB: (_ BitVec i)). @param sort The sort. @return True if given sort is a bit-vector sort.
cvc5_sort_is_disequal^⚠: Compare two sorts for structural disequality. @param a The first sort. @param b The second sort. @return True if the sorts are not equal.
cvc5_sort_is_dt^⚠: Determine if given sort is a datatype sort. @param sort The sort. @return True if given sort is a datatype sort.
cvc5_sort_is_dt_constructor^⚠: Determine if given sort is a datatype constructor sort. @param sort The sort. @return True if given sort is a datatype constructor sort.
cvc5_sort_is_dt_selector^⚠: Determine if given sort is a datatype selector sort. @param sort The sort. @return True if given sort is a datatype selector sort.
cvc5_sort_is_dt_tester^⚠: Determine if given sort is a datatype tester sort. @param sort The sort. @return True if given sort is a datatype tester sort.
cvc5_sort_is_dt_updater^⚠: Determine if given sort is a datatype updater sort. @param sort The sort. @return True if given sort is a datatype updater sort.
cvc5_sort_is_equal^⚠: Compare two sorts for structural equality. @param a The first sort. @param b The second sort. @return True if the sorts are equal.
cvc5_sort_is_ff^⚠: Determine if given sort is a finite field sort. @param sort The sort. @return True if the sort is a finite field sort.
cvc5_sort_is_fp^⚠: Determine if given sort is a floatingpoint sort (SMT-LIB: (_ FloatingPoint eb sb)). @param sort The sort. @return True if given sort is a floating-point sort.
cvc5_sort_is_fun^⚠: Determine if given sort is a function sort. @param sort The sort. @return True if given sort is a function sort.
cvc5_sort_is_instantiated^⚠: Determine if given sort is an instantiated (parametric datatype or uninterpreted sort constructor) sort.
cvc5_sort_is_integer^⚠: Determine if given sort is the integer sort (SMT-LIB: Int). @param sort The sort. @return True if given sort is the integer sort.
cvc5_sort_is_nullable^⚠: Determine if given sort is a nullable sort. @param sort The sort. @return True if given sort is a nullable sort.
cvc5_sort_is_predicate^⚠: Determine if given sort is a predicate sort.
cvc5_sort_is_real^⚠: Determine if given sort is the real sort (SMT-LIB: Real). @param sort The sort. @return True if given sort is the real sort.
cvc5_sort_is_record^⚠: Determine if given sort is a record sort. @warning This function is experimental and may change in future versions. @param sort The sort. @return True if the sort is a record sort.
cvc5_sort_is_regexp^⚠: Determine if given sort is the regular expression sort (SMT-LIB: RegLan). @param sort The sort. @return True if given sort is the regular expression sort.
cvc5_sort_is_rm^⚠: Determine if given sort is the rounding mode sort (SMT-LIB: Cvc5RoundingMode). @param sort The sort. @return True if given sort is the rounding mode sort.
cvc5_sort_is_sequence^⚠: Determine if given sort is a Sequence sort. @param sort The sort. @return True if the sort is a Sequence sort.
cvc5_sort_is_set^⚠: Determine if given sort is a Set sort. @param sort The sort. @return True if the sort is a Set sort.
cvc5_sort_is_string^⚠: Determine if given sort is the string sort (SMT-LIB: String). @param sort The sort. @return True if given sort is the string sort.
cvc5_sort_is_tuple^⚠: Determine if given sort is a tuple sort. @param sort The sort. @return True if given sort is a tuple sort.
cvc5_sort_is_uninterpreted_sort^⚠: Determine if given sort is an uninterpreted sort. @param sort The sort. @return True if given sort is an uninterpreted sort.
cvc5_sort_is_uninterpreted_sort_constructor^⚠: Determine if given sort is an uninterpreted sort constructor.
cvc5_sort_kind_hash^⚠: Hash function for Cvc5SortKinds. @param kind The kind. @return The hash value.
cvc5_sort_kind_to_string^⚠: Get a string representation of a Cvc5SortKind. @param kind The sort kind. @return The string representation.
cvc5_sort_nullable_get_element_sort^⚠: Get the element sort of a nullable sort. @param sort The sort. @return The element sort of a nullable sort.
cvc5_sort_release^⚠: Release copy of sort, decrements reference counter of sort.
cvc5_sort_sequence_get_element_sort^⚠: Get the element sort of a sequence sort. @param sort The sort. @return The element sort of a sequence sort.
cvc5_sort_set_get_element_sort^⚠: Get the element sort of a given set sort. @param sort The sort. @return The element sort of a set sort.
cvc5_sort_substitute^⚠: Substitution of Sorts.
cvc5_sort_substitute_sorts^⚠: Simultaneous substitution of Sorts.
cvc5_sort_to_string^⚠: Get a string representation of a given sort. @param sort The sort. @return A string representation of the given sort. @note The returned char* pointer is only valid until the next call to this function.
cvc5_sort_tuple_get_element_sorts^⚠: Get the element sorts of a tuple sort. @param sort The sort. @param size The size of the resulting array of tuple element sorts. @return The element sorts of a tuple sort.
cvc5_sort_tuple_get_length^⚠: Get the length of a tuple sort. @param sort The sort. @return The length of a tuple sort.
cvc5_sort_uninterpreted_sort_constructor_get_arity^⚠: Get the arity of an uninterpreted sort constructor sort. @param sort The sort. @return The arity of an uninterpreted sort constructor sort.
cvc5_stat_get_double^⚠: Get the value of a double statistic. @param stat The statistic. @return The double value.
cvc5_stat_get_histogram^⚠: Get the value of a histogram statistic. @param stat The statistic. @param keys The resulting arrays with the keys of the statistic, map to the values given in the resulting values array.. @param values The resulting arrays with the values of the statistic. @param size The size of the resulting keys/values arrays.
cvc5_stat_get_int^⚠: Get the value of an integer statistic. @param stat The statistic. @return The integer value.
cvc5_stat_get_string^⚠: Get value of a string statistic. @param stat The statistic. @return The string value. @note The returned char pointer is only valid until the next call to this function.
cvc5_stat_is_default^⚠: Determine if a given statistics statistic holds the default value. @param stat The statistic. @return True if this is a defaulted statistic.
cvc5_stat_is_double^⚠: Determine if a given statistic holds a double value. @param stat The statistic. @return True if this value is a double.
cvc5_stat_is_histogram^⚠: Determine if a given statistic holds a histogram. @param stat The statistic. @return True if this value is a histogram.
cvc5_stat_is_int^⚠: Determine if a given statistic holds an integer value. @param stat The statistic. @return True if this value is an integer.
cvc5_stat_is_internal^⚠: Determine if a given statistic is intended for internal use only. @param stat The statistic. @return True if this is an internal statistic.
cvc5_stat_is_string^⚠: Determine if a given statistic holds a string value. @param stat The statistic. @return True if this value is a string.
cvc5_stat_to_string^⚠: Get a string representation of a given statistic. @param stat The statistic. @return The string representation. @note The returned char* pointer is only valid until the next call to this function.
cvc5_stats_get^⚠: Retrieve the statistic with the given name. @note Requires that a statistic with the given name actually exists. @param stat The statistics. @param name The name of the statistic. @return The statistic with the given name.
cvc5_stats_iter_has_next^⚠: Determine if statistics iterator has more statitics to query. @note Requires that iterator was initialized with cvc5_stats_iter_init(). @param stat The statistics. @return True if the iterator has more statistics to query.
cvc5_stats_iter_init^⚠: Initialize iteration over the statistics values. By default, only entries that are public and have been set are visible while the others are skipped. @param stat The statistics. @param internal If set to true, internal statistics are shown as well. @param dflt If set to true, defaulted statistics are shown as well.
cvc5_stats_iter_next^⚠: Get next statistic and increment iterator. @note Requires that iterator was initialized with cvc5_stats_iter_init() and that cvc5_stats_iter_has_next(). @param stat The statistics. @param name The output parameter for the name of the returned statistic. May be NULL to ignore. @note The returned char* pointer are only valid until the next call to this function. @return The next statistic.
cvc5_stats_to_string^⚠: Get a string representation of a given statistics object. @param stat The statistics. @return The string representation. @note The returned char* pointer is only valid until the next call to this function.
cvc5_synth_fun^⚠: Synthesize n-ary function.
cvc5_synth_fun_with_grammar^⚠: Synthesize n-ary function following specified syntactic constraints.
cvc5_synth_result_copy^⚠: Make copy of synthesis result, increases reference counter of result.
cvc5_synth_result_has_no_solution^⚠: Determine if the given result is from a synthesis query that has no solution. @param result The result. @return True if the synthesis query has no solution. In this case, it was determined that there was no solution.
cvc5_synth_result_has_solution^⚠: Determine if the given result is from a synthesis query that has a solution. @param result The result. @return True if the synthesis query has a solution.
cvc5_synth_result_hash^⚠: Compute the hash value of a synthesis result. @param result The synthesis result. @return The hash value of the synthesis result.
cvc5_synth_result_is_disequal^⚠: Operator overloading for disequality of two synthesis results. @param a The first synthesis result to compare to for disequality. @param b The second synthesis result to compare to for disequality. @return True if the synthesis results are disequal.
cvc5_synth_result_is_equal^⚠: Determine equality of two synthesis results. @param a The first synthesis result to compare to for equality. @param b The second synthesis result to compare to for equality. @return True if the synthesis results are equal.
cvc5_synth_result_is_null^⚠: Determine if a given synthesis result is empty (a nullary result) and not an actual result returned from a synthesis query. @param result The result. @return True if the given result is a nullary result.
cvc5_synth_result_is_unknown^⚠: Determine if the given result is from a synthesis query where its result could not be determined. @param result The result. @return True if the result of the synthesis query could not be determined.
cvc5_synth_result_release^⚠: Release copy of synthesis result, decrements reference counter of result.
cvc5_synth_result_to_string^⚠: Get the string representation of a given result. @param result The result. @return A string representation of the given synthesis result. @note The returned char* pointer is only valid until the next call to this function.
cvc5_term_compare^⚠: Compare two terms for ordering. @param a The first term. @param b The second term. @return An integer value indicating the ordering: 0 if both terms are equal, -1 if a < b, and 1 if b > a.
cvc5_term_copy^⚠: Make copy of term, increases reference counter of term.
cvc5_term_get_boolean_value^⚠: Get the value of a Boolean term as a native Boolean value. @note Asserts cvc5_term_is_boolean_value(). @param term The term. @return The representation of a Boolean value as a native Boolean value.
cvc5_term_get_bv_value^⚠: Get the string representation of a bit-vector value. @note Asserts cvc5_term_is_bv_value(). @param term The term. @param base 2 for binary, 10 for decimal, and 16 for hexadecimal. @return The string representation of a bit-vector value. @note The returned char* pointer is only valid until the next call to this function.
cvc5_term_get_cardinality_constraint^⚠: Get a cardinality constraint as a pair of its sort and upper bound. @note Asserts cvc5_term_is_cardinality_constraint(). @param term The term. @param sort The resulting sort. @param upper The resulting upper bound.
cvc5_term_get_child^⚠: Get the child term of a given term at a given index. @param term The term. @param index The index of the child. @return The child term at the given index.
cvc5_term_get_const_array_base^⚠: Determine the base (element stored at all indices) of a constant array. @note Requires that the term is a constant array (see isConstArray()). @param term The term. @return The base term.
cvc5_term_get_ff_value^⚠: Get the string representation of a finite field value (base 10).
cvc5_term_get_fp_value^⚠: Get the representation of a floating-point value as its exponent width, significand width and a bit-vector value term. @note Asserts cvc5_term_is_fp_value(). @param term The term. @param ew The resulting exponent width. @param sw The resulting significand width. @param val The resulting bit-vector value term.
cvc5_term_get_id^⚠: Get the id of a given term. @param term The term. @return The id of the term.
cvc5_term_get_int32_value^⚠: Get the int32_t representation of a given integral value. @note Requires that the term is an int32 value (see cvc5_term_is_int32_value()). @param term The term. @return The given term as int32_t value.
cvc5_term_get_int64_value^⚠: Get the int64_t representation of a given integral value. @note Requires that the term is an int64 value (see cvc5_term_is_int64_value()). @param term The term. @return The term as int64_t value.
cvc5_term_get_integer_value^⚠: Get a string representation of a given integral value. @note Requires that the term is an integral value (see cvc5_term_is_integer_value()). @param term The term. @return The integral term in (decimal) string representation. @note The returned char* pointer is only valid until the next call to this function.
cvc5_term_get_kind^⚠: Get the kind of a given term. @param term The term. @return The kind of the term.
cvc5_term_get_num_children^⚠: Get the number of children of a given term. @param term The term. @return The number of children of this term.
cvc5_term_get_op^⚠: Get the operator of a term with an operator.
cvc5_term_get_real32_value^⚠: Get the 32 bit integer representations of the numerator and denominator of a rational value. @note Requires that the term is a rational value and its numerator and denominator fit into 32 bit integer values (see cvc5_term_is_real32_value()). @param term The term. @param num The resulting int32_t representation of the numerator. @param den The resulting uint32_t representation of the denominator.
cvc5_term_get_real64_value^⚠: Get the 64 bit integer representations of the numerator and denominator of a rational value. @note Requires that the term is a rational value and its numerator and denominator fit into 64 bit integer values (see cvc5_term_is_real64_value()). @param term The term. @param num The resulting int64_t representation of the numerator. @param den The resulting uint64_t representation of the denominator.
cvc5_term_get_real_algebraic_number_defining_polynomial^⚠: Get the defining polynomial for a real algebraic number term, expressed in terms of the given variable. @note Asserts cvc5_term_is_real_algebraic_number(). @param term The real algebraic number term. @param v The variable over which to express the polynomial. @return The defining polynomial.
cvc5_term_get_real_algebraic_number_lower_bound^⚠: Get the lower bound for a real algebraic number value. @note Asserts cvc5_term_is_real_algebraic_number(). @param term The real algebraic number value. @return The lower bound.
cvc5_term_get_real_algebraic_number_upper_bound^⚠: Get the upper bound for a real algebraic number value. @note Asserts cvc5_term_is_real_algebraic_number(). @param term The real algebraic number value. @return The upper bound.
cvc5_term_get_real_or_integer_value_sign^⚠: Get the sign of a given integer or real value. @note Requires that given term is an integer or real value. @param term The value term. @return 0 if the term is zero, -1 if the term is a negative real or integer value, 1 if the term is a positive real or integer value.
cvc5_term_get_real_value^⚠: Get a string representation of a given rational value. @note Requires that the term is a rational value (see cvc5_term_is_real_value()). @param term The term. @return The representation of a rational value as a (rational) string. @note The returned char* pointer is only valid until the next call to this function.
cvc5_term_get_rm_value^⚠: Get the Cvc5RoundingMode value of a given rounding-mode value term. @note Asserts cvc5_term_is_rounding_mode_value(). @param term The term. @return The floating-point rounding mode value of the term.
cvc5_term_get_sequence_value^⚠: Get a sequence value as an array of terms. @note Asserts cvc5_term_is_sequence_value(). @param term The term. @param size The size of the resulting array. @return The representation of a sequence value as a vector of terms.
cvc5_term_get_set_value^⚠: Get a set value as an array of terms. @note Asserts cvc5_term_is_set_value(). @param term The term. @param size The size of the resulting array. @return The representation of a set value as an array of terms.
cvc5_term_get_skolem_id^⚠: Get skolem identifier of a term. @note Asserts isSkolem(). @warning This function is experimental and may change in future versions. @param term The skolem. @return The skolem identifier of the term.
cvc5_term_get_skolem_indices^⚠: Get the skolem indices of a term. @note Asserts isSkolem(). @warning This function is experimental and may change in future versions. @param term The skolem. @param size The size of the resulting array. @return The skolem indices of the term. This is list of terms that the skolem function is indexed by. For example, the array diff skolem Cvc5SkolemId::ARRAY_DEQ_DIFF is indexed by two arrays.
cvc5_term_get_sort^⚠: Get the sort of a given term. @param term The term. @return The sort of the term.
cvc5_term_get_string_value^⚠: Get the native string representation of a string value. @note Requires that the term is a string value (see cvc5_term_is_string_value()). @note This is not to be confused with cvc5_term_to_string(), which returns some string representation of the term, whatever data it may hold. @param term The term. @return The string term as a native string value.
cvc5_term_get_symbol^⚠: Get the symbol of a given term with a symbol.
cvc5_term_get_tuple_value^⚠: Get a tuple value as an array of terms. @note Asserts cvc5_term_is_tuple_value(). @param term The term. @param size The size of the resulting array. @return The representation of a tuple value as an array of terms.
cvc5_term_get_u32string_value^⚠: Get the native UTF-32 string representation of a string value. @note Requires that the term is a string value (see cvc5_term_is_string_value()). @note This is not to be confused with cvc5_term_to_string(), which returns some string representation of the term, whatever data it may hold. @param term The term. @return The string term as a native UTF-32 string value.
cvc5_term_get_uint32_value^⚠: Get the uint32_t representation of a given integral value. @note Requires that the term is an uint32 value (see cvc5_term_is_uint32_value()). @param term The term. @return The term as uint32_t value.
cvc5_term_get_uint64_value^⚠: Get the uint64_t representation of a given integral value. @note Requires that the term is an uint64 value (see cvc5_term_is_uint64_value()). @param term The term. @return The term as uint64_t value.
cvc5_term_get_uninterpreted_sort_value^⚠: Get a string representation of an uninterpreted sort value. @note Asserts cvc5_term_is_uninterpreted_sort_value(). @param term The term. @return The representation of an uninterpreted sort value as a string. @note The returned char* pointer is only valid until the next call to this function.
cvc5_term_has_op^⚠: Determine if a given term has an operator. @param term The term. @return True iff the term has an operator.
cvc5_term_has_symbol^⚠: Determine if a given term has a symbol (a name).
cvc5_term_hash^⚠: Compute the hash value of a term. @param term The term. @return The hash value of the term.
cvc5_term_is_boolean_value^⚠: Determine if a given term is a Boolean value. @param term The term. @return True if the term is a Boolean value.
cvc5_term_is_bv_value^⚠: Determine if a given term is a bit-vector value. @param term The term. @return True if the term is a bit-vector value.
cvc5_term_is_cardinality_constraint^⚠: Determine if a given term is a cardinality constraint. @param term The term. @return True if the term is a cardinality constraint.
cvc5_term_is_const_array^⚠: Determine if a given term is a constant array. @param term The term. @return True if the term is a constant array.
cvc5_term_is_disequal^⚠: Compare two terms for syntactic disequality. @param a The first term. @param b The second term. @return True if both term are syntactically disequal.
cvc5_term_is_equal^⚠: Compare two terms for syntactic equality. @param a The first term. @param b The second term. @return True if both term are syntactically identical.
cvc5_term_is_ff_value^⚠: Determine if a given term is a finite field value. @param term The term. @return True if the term is a finite field value.
cvc5_term_is_fp_nan^⚠: Determine if a given term is a floating-point NaN value. @param term The term. @return True if the term is the floating-point value for not a number.
cvc5_term_is_fp_neg_inf^⚠: Determine if a given term is a floating-point negative infinity value (-oo). @param term The term. @return True if the term is the floating-point value for negative. infinity.
cvc5_term_is_fp_neg_zero^⚠: Determine if a given term is a floating-point negative zero value (-zero). @param term The term. @return True if the term is the floating-point value for negative zero.
cvc5_term_is_fp_pos_inf^⚠: Determine if a given term is a floating-point positive infinity value (+oo). @param term The term. @return True if the term is the floating-point value for positive. infinity.
cvc5_term_is_fp_pos_zero^⚠: Determine if a given term is a floating-point positive zero value (+zero). @param term The term. @return True if the term is the floating-point value for positive zero.
cvc5_term_is_fp_value^⚠: Determine if a given term is a floating-point value. @param term The term. @return True if the term is a floating-point value.
cvc5_term_is_int32_value^⚠: Determine if a given term is an int32 value. @note This will return true for integer constants and real constants that have integer value. @param term The term. @return True if the term is an integer value that fits within int32_t.
cvc5_term_is_int64_value^⚠: Determine if a given term is an int64 value. @note This will return true for integer constants and real constants that have integral value. @param term The term. @return True if the term is an integral value that fits within int64_t.
cvc5_term_is_integer_value^⚠: Determine if a given term is an integral value. @param term The term. @return True if the term is an integer constant or a real constant that has an integral value.
cvc5_term_is_real32_value^⚠: Determine if a given term is a rational value whose numerator fits into an int32 value and its denominator fits into a uint32 value. @param term The term. @return True if the term is a rational and its numerator and denominator fit into 32 bit integer values.
cvc5_term_is_real64_value^⚠: Determine if a given term is a rational value whose numerator fits into an int64 value and its denominator fits into a uint64 value. @param term The term. @return True if the term is a rational value whose numerator and denominator fit within int64_t and uint64_t, respectively.
cvc5_term_is_real_algebraic_number^⚠: Determine if a given term is a real algebraic number. @param term The term. @return True if the term is a real algebraic number.
cvc5_term_is_real_value^⚠: Determine if a given term is a rational value. @note A term of kind PI is not considered to be a real value. @param term The term. @return True if the term is a rational value.
cvc5_term_is_rm_value^⚠: Determine if a given term is a floating-point rounding mode value. @param term The term. @return True if the term is a rounding mode value.
cvc5_term_is_sequence_value^⚠: Determine if a given term is a sequence value.
cvc5_term_is_set_value^⚠: Determine if a given term is a set value.
cvc5_term_is_skolem^⚠: Is the given term a skolem? @warning This function is experimental and may change in future versions. @param term The skolem. @return True if the term is a skolem function.
cvc5_term_is_string_value^⚠: Determine if a given term is a string value. @param term The term. @return True if the term is a string value.
cvc5_term_is_tuple_value^⚠: Determine if a given term is a tuple value. @param term The term. @return True if the term is a tuple value.
cvc5_term_is_uint32_value^⚠: Determine if a given term is an uint32 value. @note This will return true for integer constants and real constants that have integral value. @return True if the term is an integral value and fits within uint32_t.
cvc5_term_is_uint64_value^⚠: Determine if a given term is an uint64 value. @note This will return true for integer constants and real constants that have integral value. @param term The term. @return True if the term is an integral value that fits within uint64_t.
cvc5_term_is_uninterpreted_sort_value^⚠: Determine if a given term is an uninterpreted sort value. @param term The term. @return True if the term is an abstract value.
cvc5_term_manager_delete^⚠: Delete a cvc5 term manager instance. @param tm The term manager instance.
cvc5_term_manager_get_statistics^⚠: Get a snapshot of the current state of the statistic values of this term manager. The returned object is completely decoupled from the term manager and will not change when the term manager is used again. @param tm The term manager instance. @return A snapshot of the current state of the statistic values.
cvc5_term_manager_new^⚠: Construct a new instance of a cvc5 term manager. @return The cvc5 term manager.
cvc5_term_manager_print_stats_safe^⚠: Print the term manager statistics to the given file descriptor, suitable for usage in signal handlers. @param tm The term manager instance. @param fd The file descriptor.
cvc5_term_manager_release^⚠: Release all managed references.
cvc5_term_release^⚠: Release copy of term, decrements reference counter of term.
cvc5_term_substitute_term^⚠: Replace a given term t with term replacement in a given term.
cvc5_term_substitute_terms^⚠: Simultaneously replace given terms terms with terms replacements in a given term.
cvc5_term_to_string^⚠: Get a string representation of a given term. @param term The term. @return A string representation of the term. @note The returned char* pointer is only valid until the next call to this function.
cvc5_unknown_explanation_to_string^⚠: Get a string representation of a Cvc5UnknownExplanation. @param exp The unknown explanation. @return The string representation.

Type Aliases§

Cvc5Datatype: A cvc5 datatype.
Cvc5DatatypeConstructor: A cvc5 datatype constructor.
Cvc5DatatypeConstructorDecl: A cvc5 datatype constructor declaration. A datatype constructor declaration is a specification used for creating a datatype constructor.
Cvc5DatatypeDecl: A cvc5 datatype declaration. A datatype declaration is not itself a datatype (see Datatype), but a specification for creating a datatype sort.
Cvc5DatatypeSelector: A cvc5 datatype selector.
Cvc5Grammar: A Sygus Grammar. This can be used to define a context-free grammar of terms. Its interface coincides with the definition of grammars (GrammarDef) in the SyGuS IF 2.1 standard.
Cvc5Op: A cvc5 operator.
Cvc5OptionCategory
Cvc5OptionInfoKind: @}
Cvc5Proof: A cvc5 proof.
Cvc5ProofRewriteRule
Cvc5Result: Encapsulation of a three-valued solver result, with explanations.
Cvc5Sort: The sort of a cvc5 term.
Cvc5Stat: A cvc5 statistic.
Cvc5Statistics: A cvc5 statistics instance.
Cvc5SynthResult: Encapsulation of a solver synth result.
Cvc5Term: A cvc5 term.
char32_t
uint_least32_t
wchar_t

Crate cvc5_sys

Crate cvc5_sys Copy item path

§cvc5-sys

§Build

§Example

Modules§

Structs§

Enums§

Constants§

Functions§

Type Aliases§

Crate cvc5_sys