Crate cvc5_sys 

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 = term_manager_new();
    let slv = new(tm);

    set_logic(slv, c"QF_LIA".as_ptr());
    set_option(slv, c"produce-models".as_ptr(), c"true".as_ptr());

    let int_sort = get_integer_sort(tm);
    let x = mk_const(tm, int_sort, c"x".as_ptr());
    let zero = mk_integer_int64(tm, 0);

    let gt = mk_term(tm, Kind::Gt, 2, [x, zero].as_ptr());
    assert_formula(slv, gt);

    let result = check_sat(slv);
    assert!(result_is_sat(result));

    delete(slv);
    term_manager_delete(tm);
}

Modules

parser

Structs

OptionInfo

\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:

OptionInfo_BoolInfo

Information for boolean option values.

OptionInfo_DoubleInfo

Information for double values.

OptionInfo_IntInfo

Information for int64 values.

OptionInfo_ModeInfo

Information for mode option values.

OptionInfo_StringInfo

Information for string option values.

OptionInfo_UIntInfo

Information for uint64 values.

Plugin

A cvc5 plugin.

Solver

TermManager

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

BlockModelsMode

Mode for blocking models.

FindSynthTarget

Find synthesis targets, used as an argument to Solver::findSynth. These specify various kinds of terms that can be found by this method.

InputLanguage

The different reasons for returning an “unknown” result.

Kind

The kind of a cvc5 Term.

LearnedLitType

Types of learned literals.

OptionCategory

Option category enumeration. Specifies the category of an option for user interface purposes.

OptionInfoKind

@}

ProofComponent

Components to include in a proof.

ProofFormat

Proof format used for proof printing.

ProofRewriteRule

\verbatim embed:rst:leading-asterisk This enumeration represents the rewrite rules used in a rewrite proof. Some of the rules are internal ad-hoc rewrites, while others are rewrites specified by the RARE DSL. This enumeration is used as the first argument to the :cpp:enumerator:DSL_REWRITE <cvc5::ProofRule::DSL_REWRITE> proof rule and the :cpp:enumerator:THEORY_REWRITE <cvc5::ProofRule::THEORY_REWRITE> proof rule. \endverbatim

ProofRule

\internal This documentation is target for the online documentation that can be found at https://cvc5.github.io/docs/latest/proofs/proof_rules.html \endinternal

RoundingMode

Rounding modes for floating-point numbers.

SkolemId

The kind of a cvc5 skolem. A skolem is a (family of) internal functions or constants that are introduced by cvc5. These symbols are treated as uninterpreted internally. We track their definition for the purposes of formal bookkeeping for the user of features like proofs, lemma exporting, simplification and so on.

SortKind

The kind of a cvc5 Sort.

UnknownExplanation

The different reasons for returning an “unknown” result.

Functions

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.

add_sygus_assume^⚠

Add a forumla to the set of Sygus assumptions.

add_sygus_constraint^⚠

Add a forumla to the set of Sygus constraints.

add_sygus_inv_constraint^⚠

Add a set of Sygus constraints to the current state that correspond to an invariant synthesis problem.

assert_formula^⚠

Assert a formula.

block_model^⚠

Block the current model. Can be called only if immediately preceded by a SAT or INVALID query.

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.

check_sat^⚠

Check satisfiability.

check_sat_assuming^⚠

Check satisfiability assuming the given formulas.

check_synth^⚠

Try to find a solution for the synthesis conjecture corresponding to the current list of functions-to-synthesize, universal variables and constraints.

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.

close_output^⚠

Close output file configured for an output tag via cvc5_get_output().

declare_dt^⚠

Create datatype sort.

declare_fun^⚠

Declare n-ary function symbol.

declare_oracle_fun^⚠

Declare an oracle function with reference to an implementation.

declare_pool^⚠

Declare a symbolic pool of terms with the given initial value.

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.

declare_sort^⚠

Declare uninterpreted sort.

declare_sygus_var^⚠

Append \p symbol to the current list of universal variables.

define_fun^⚠

Define n-ary function.

define_fun_rec^⚠

Define recursive function.

define_fun_rec_from_const^⚠

Define recursive function.

define_funs_rec^⚠

Define recursive functions.

delete^⚠

Delete a cvc5 solver instance. @param cvc5 The solver instance.

dt_cons_copy^⚠

Make copy of datatype constructor, increases reference counter of cons.

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.

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.

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.

dt_cons_decl_copy^⚠

Make copy of datatype constructor declaration, increases reference counter of decl.

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.

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.

dt_cons_decl_release^⚠

Release copy of datatype constructor declaration, decrements reference counter of decl.

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.

dt_cons_get_instantiated_term^⚠

Get the constructor term of this datatype constructor whose return type is sort.

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.

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.

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.

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.

dt_cons_get_term^⚠

Get the constructor term of a given datatype constructor.

dt_cons_get_tester_term^⚠

Get the tester term of a given datatype constructor.

dt_cons_hash^⚠

Compute the hash value of a datatype constructor. @param cons The datatype constructor. @return The hash value of the datatype constructor.

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.

dt_cons_release^⚠

Release copy of datatype constructor, decrements reference counter of cons.

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.

dt_copy^⚠

Make copy of datatype, increases reference counter of dt.

dt_decl_add_constructor^⚠

Add datatype constructor declaration. @param decl The datatype declaration. @param ctor The datatype constructor declaration to add.

dt_decl_copy^⚠

Make copy of datatype declaration, increases reference counter of decl.

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.

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.

dt_decl_hash^⚠

Compute the hash value of a datatype declaration. @param decl The datatype declaration. @return The hash value of the datatype declaration.

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.

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.

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.

dt_decl_release^⚠

Release copy of datatype declaration, decrements reference counter of decl.

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.

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.

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.

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.

dt_get_num_constructors^⚠

Get the number of constructors of a given datatype. @param dt The datatype. @return The number of constructors.

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.

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.

dt_hash^⚠

Compute the hash value of a datatype. @param dt The datatype. @return The hash value of the datatype.

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.

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.

dt_is_finite^⚠

Determine if a given datatype is finite. @param dt The datatype. @return True if the datatype is finite.

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.

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.

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.

dt_is_well_founded^⚠

Determine if a given datatype is well-founded.

dt_release^⚠

Release copy of datatype, decrements reference counter of dt.

dt_sel_copy^⚠

Make copy of datatype selector, increases reference counter of sel.

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.

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.

dt_sel_get_term^⚠

Get the selector term of a given datatype selector.

dt_sel_get_updater_term^⚠

Get the updater term of a given datatype selector.

dt_sel_hash^⚠

Compute the hash value of a datatype selector. @param sel The datatype selector. @return The hash value of the datatype selector.

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.

dt_sel_release^⚠

Release copy of datatype selector, decrements reference counter of sel.

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.

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.

find_synth^⚠

Find a target term of interest using sygus enumeration, with no provided grammar.

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.

find_synth_with_grammar^⚠

Find a target term of interest using sygus enumeration with a provided grammar.

get_abduct^⚠

Get an abduct.

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.

get_abduct_with_grammar^⚠

Get an abduct.

get_assertions^⚠

Get the list of asserted formulas.

get_boolean_sort^⚠

Get the Boolean sort. @param tm The term manager instance. @return Sort Boolean.

get_difficulty^⚠

Get a difficulty estimate for an asserted formula. This function is intended to be called immediately after any response to a checkSat.

get_info^⚠

Get info from the solver.

get_instantiations^⚠

@warning This function is experimental and may change in future versions.

get_integer_sort^⚠

Get the Integer sort. @param tm The term manager instance. @return Sort Integer.

get_interpolant^⚠

Get an interpolant.

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.

get_interpolant_with_grammar^⚠

Get an interpolant

get_learned_literals^⚠

Get a list of learned literals that are entailed by the current set of assertions.

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.

get_model^⚠

Get the model

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.

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.

get_option^⚠

Get the value of a given option.

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.

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.

get_output^⚠

Configure a file to write the output for a given tag.

get_proof^⚠

Get a proof associated with the most recent call to checkSat.

get_quantifier_elimination^⚠

Do quantifier elimination.

get_quantifier_elimination_disjunct^⚠

Do partial quantifier elimination, which can be used for incrementally computing the result of a quantifier elimination.

get_real_sort^⚠

Get the Real sort. @param tm The term manager instance. @return Sort Real.

get_regexp_sort^⚠

Get the regular expression sort. @param tm The term manager instance. @return Sort RegExp.

get_rm_sort^⚠

Get the rounding mode sort. @param tm The term manager instance. @return The rounding mode sort.

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.

get_string_sort^⚠

Get the string sort. @param tm The term manager instance. @return Sort String.

get_sygus_assumptions^⚠

Get the list of sygus assumptions.

get_sygus_constraints^⚠

Get the list of sygus constraints.

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.

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.

get_timeout_core^⚠

Get a timeout core.

get_timeout_core_assuming^⚠

Get a timeout core of the given assumptions.

get_tm^⚠

Get the associated term manager of a cvc5 solver instance. @param cvc5 The solver instance. @return The term manager.

get_unsat_assumptions^⚠

Get the set of unsat (“failed”) assumptions.

get_unsat_core^⚠

Get the unsatisfiable core.

get_unsat_core_lemmas^⚠

Get the lemmas used to derive unsatisfiability.

get_value^⚠

Get the value of the given term in the current model.

get_value_sep_heap^⚠

When using separation logic, obtain the term for the heap.

get_value_sep_nil^⚠

When using separation logic, obtain the term for nil.

get_values^⚠

Get the values of the given terms in the current model.

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.

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.

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.

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.

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.

grammar_copy^⚠

Make copy of grammar, increases reference counter of grammar.

grammar_hash^⚠

Compute the hash value of a grammar. @param grammar The grammar. @return The hash value of the grammar.

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.

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.

grammar_release^⚠

Release copy of grammar, decrements reference counter of grammar.

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.

is_logic_set^⚠

Determine if cvc5_set_logic() has been called.

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.

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

kind_hash^⚠

Hash function for Cvc5Kinds. @param kind The kind. @return The hash value.

kind_to_string^⚠

Get a string representation of a Cvc5Kind. @param kind The kind. @return The string representation.

mk_abstract_sort^⚠

Create an abstract sort. An abstract sort represents a sort for a given kind whose parameters and arguments are unspecified.

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.

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.

mk_boolean^⚠

Create a Boolean constant. @param tm The term manager instance. @return The Boolean constant. @param val The value of the constant.

mk_bv^⚠

Create a bit-vector constant of a given bit-width from a given string of base 2, 10 or 16.

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.

mk_bv_uint64^⚠

Create a bit-vector constant of given size and value.

mk_cardinality_constraint^⚠

Create a cardinality constraint for an uninterpreted sort.

mk_const^⚠

Create a free constant.

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.

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.

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.

mk_dt_decl_with_params^⚠

Create a datatype declaration. Create sorts parameter with cvc5_mk_param_sort().

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.

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.

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.

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.

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.

mk_false^⚠

Create a Boolean false constant. @param tm The term manager instance. @return The false constant.

mk_ff_elem^⚠

Create a finite field constant in a given field from a given string of base n.

mk_ff_sort^⚠

Create a finite-field sort from a given string of base n.

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.

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.

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.

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.

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.

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.

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.

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.

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.

mk_grammar^⚠

Create a Sygus grammar. The first non-terminal is treated as the starting non-terminal, so the order of non-terminals matters.

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)

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.

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.

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.

mk_nullable_lift^⚠

Create a term that lifts kind to nullable terms.

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.

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.

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.

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.

mk_op^⚠

Create operator of Kind:

mk_op_from_str^⚠

Create operator of kind:

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.

mk_pi^⚠

Create a constant representing the number Pi. @param tm The term manager instance. @return A constant representing Pi.

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.

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.

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.

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.

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.

mk_regexp_all^⚠

Create a regular expression all (re.all) term. @param tm The term manager instance. @return The all term.

mk_regexp_allchar^⚠

Create a regular expression allchar (re.allchar) term. @param tm The term manager instance. @return The allchar term.

mk_regexp_none^⚠

Create a regular expression none (re.none) term. @param tm The term manager instance. @return The none term.

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.

mk_sep_emp^⚠

Create a separation logic empty term.

mk_sep_nil^⚠

Create a separation logic nil term.

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.

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.

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.

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.

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.

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.

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

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.

mk_true^⚠

Create a Boolean true constant. @param tm The term manager instance. @return The true constant.

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.

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.

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.

mk_uninterpreted_sort_constructor_sort^⚠

Create an uninterpreted sort constructor sort.

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.

mk_unresolved_dt_sort^⚠

Create an unresolved datatype sort.

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.

modes_block_models_mode_to_string^⚠

Get a string representation of a Cvc5BlockModelsMode. @param mode The mode. @return The string representation.

modes_find_synth_target_to_string^⚠

Get a string representation of a Cvc5FindSynthTarget. @param target The synthesis find target. @return The string representation.

modes_input_language_to_string^⚠

Get a string representation of a Cvc5InputLanguage. @param lang The input language. @return The string representation.

modes_learned_lit_type_to_string^⚠

Get a string representation of a Cvc5LearnedLitType. @param type The learned literal type. @return The string representation.

modes_option_category_to_string^⚠

Get a string representation of a Cvc5OptionCategory. @param cat The option category. @return The string representation.

modes_proof_component_to_string^⚠

Get a string representation of a Cvc5ProofComponent. @param pc The proof component. @return The string representation.

modes_proof_format_to_string^⚠

Get a string representation of a Cvc5ProofFormat. @param format The proof format. @return The string representation.

new^⚠

Construct a new instance of a cvc5 solver. @param tm The associated term manager instance. @return The cvc5 solver instance.

op_copy^⚠

Make copy of operator, increases reference counter of op.

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.

op_get_kind^⚠

Get the kind of a given operator. @param op The operator. @return The kind of the operator.

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.

op_hash^⚠

Compute the hash value of an operator. @param op The operator. @return The hash value of the operator.

op_is_disequal^⚠

Compare two operators for syntactic disequality.

op_is_equal^⚠

Compare two operators for syntactic equality.

op_is_indexed^⚠

Determine if a given operator is indexed. @param op The operator. @return True iff the operator is indexed.

op_release^⚠

Release copy of operator, decrements reference counter of op.

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.

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.

pop^⚠

Pop (a) level(s) from the assertion stack.

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.

proof_copy^⚠

Make copy of proof, increases reference counter of proof.

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.

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.

proof_get_result^⚠

Get the conclusion of the root step of a given proof. @param proof The proof. @return The conclusion term.

proof_get_rewrite_rule^⚠

Get the proof rewrite rule used by the root step of the proof.

proof_get_rule^⚠

Get the proof rule used by the root step of a given proof. @return The proof rule.

proof_hash^⚠

Compute the hash value of a proof. @param proof The proof. @return The hash value of the proof.

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.

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.

proof_release^⚠

Release copy of proof, decrements reference counter of proof.

proof_rewrite_rule_hash^⚠

Hash function for Cvc5ProofRewriteRule. @param rule The proof rewrite rule. @return The hash value.

proof_rewrite_rule_to_string^⚠

Get a string representation of a Cvc5ProofRewriteRule. @param rule The proof rewrite rule. @return The string representation.

proof_rule_hash^⚠

Hash function for Cvc5ProofRule. @param rule The proof rule. @return The hash value.

proof_rule_to_string^⚠

Get a string representation of a Cvc5ProofRule. @param rule The proof rule. @return The string representation.

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.

push^⚠

Push (a) level(s) to the assertion stack.

reset_assertions^⚠

Remove all assertions.

result_copy^⚠

Make copy of result, increases reference counter of result.

result_get_unknown_explanation^⚠

Get the explanation for an unknown result. @param result The result. @return An explanation for an unknown query result.

result_hash^⚠

Compute the hash value of a result. @param result The result. @return The hash value of the result.

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.

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.

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.

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.

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.

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.

result_release^⚠

Release copy of result, decrements reference counter of result.

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.

rm_to_string^⚠

Get a string representation of a Cvc5RoundingMode. @param rm The rounding mode. @return The string representation.

set_info^⚠

Set info.

set_logic^⚠

Set logic.

set_option^⚠

Set option.

simplify^⚠

Simplify a formula without doing “much” work.

skolem_id_hash^⚠

Hash function for Cvc5SkolemId. @param id The skolem id. @return The hash value.

skolem_id_to_string^⚠

Get a string representation of a Cvc5SkolemId. @param id The skolem id. @return The string representation.

sort_abstract_get_kind^⚠

Get the kind of an abstract sort, which denotes the sort kinds that the abstract sort denotes.

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.

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.

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.

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.

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.

sort_copy^⚠

Make copy of sort, increases reference counter of sort.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

sort_fun_get_arity^⚠

Get the aritye of a given function sort. @param sort The sort. @return The arity of a function sort.

sort_fun_get_codomain^⚠

Get the codomain of a given function sort. @param sort The sort. @return The codomain sort of a function sort.

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.

sort_get_datatype^⚠

Get the underlying datatype of a datatype sort. @param sort The sort. @return The underlying datatype of a datatype sort.

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();

sort_get_kind^⚠

Get the kind of the given sort. @param sort The sort. @return The kind of the sort.

sort_get_symbol^⚠

Get the symbol of this Sort.

sort_get_uninterpreted_sort_constructor^⚠

Get the associated uninterpreted sort constructor of an instantiated uninterpreted sort.

sort_has_symbol^⚠

Determine if the given sort has a symbol (a name).

sort_hash^⚠

Compute the hash value of a sort. @param sort The sort. @return The hash value of the sort.

sort_instantiate^⚠

Instantiate a parameterized datatype sort or uninterpreted sort constructor sort.

sort_is_abstract^⚠

Determine if given sort is an abstract sort. @param sort The sort. @return True if the sort is a abstract sort.

sort_is_array^⚠

Determine if given sort is an array sort. @param sort The sort. @return True if the sort is an array sort.

sort_is_bag^⚠

Determine if given sort is a Bag sort. @param sort The sort. @return True if the sort is a Bag sort.

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.

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.

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.

sort_is_dt^⚠

Determine if given sort is a datatype sort. @param sort The sort. @return True if given sort is a datatype sort.

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.

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.

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.

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.

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.

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.

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.

sort_is_fun^⚠

Determine if given sort is a function sort. @param sort The sort. @return True if given sort is a function sort.

sort_is_instantiated^⚠

Determine if given sort is an instantiated (parametric datatype or uninterpreted sort constructor) sort.

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.

sort_is_nullable^⚠

Determine if given sort is a nullable sort. @param sort The sort. @return True if given sort is a nullable sort.

sort_is_predicate^⚠

Determine if given sort is a predicate sort.

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.

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.

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.

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.

sort_is_sequence^⚠

Determine if given sort is a Sequence sort. @param sort The sort. @return True if the sort is a Sequence sort.

sort_is_set^⚠

Determine if given sort is a Set sort. @param sort The sort. @return True if the sort is a Set sort.

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.

sort_is_tuple^⚠

Determine if given sort is a tuple sort. @param sort The sort. @return True if given sort is a tuple sort.

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.

sort_is_uninterpreted_sort_constructor^⚠

Determine if given sort is an uninterpreted sort constructor.

sort_kind_hash^⚠

Hash function for Cvc5SortKinds. @param kind The kind. @return The hash value.

sort_kind_to_string^⚠

Get a string representation of a Cvc5SortKind. @param kind The sort kind. @return The string representation.

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.

sort_release^⚠

Release copy of sort, decrements reference counter of sort.

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.

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.

sort_substitute^⚠

Substitution of Sorts.

sort_substitute_sorts^⚠

Simultaneous substitution of Sorts.

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.

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.

sort_tuple_get_length^⚠

Get the length of a tuple sort. @param sort The sort. @return The length of a tuple sort.

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.

stat_get_double^⚠

Get the value of a double statistic. @param stat The statistic. @return The double value.

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.

stat_get_int^⚠

Get the value of an integer statistic. @param stat The statistic. @return The integer value.

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.

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.

stat_is_double^⚠

Determine if a given statistic holds a double value. @param stat The statistic. @return True if this value is a double.

stat_is_histogram^⚠

Determine if a given statistic holds a histogram. @param stat The statistic. @return True if this value is a histogram.

stat_is_int^⚠

Determine if a given statistic holds an integer value. @param stat The statistic. @return True if this value is an integer.

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.

stat_is_string^⚠

Determine if a given statistic holds a string value. @param stat The statistic. @return True if this value is a string.

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.

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.

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.

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.

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.

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.

synth_fun^⚠

Synthesize n-ary function.

synth_fun_with_grammar^⚠

Synthesize n-ary function following specified syntactic constraints.

synth_result_copy^⚠

Make copy of synthesis result, increases reference counter of result.

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.

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.

synth_result_hash^⚠

Compute the hash value of a synthesis result. @param result The synthesis result. @return The hash value of the synthesis result.

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.

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.

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.

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.

synth_result_release^⚠

Release copy of synthesis result, decrements reference counter of result.

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.

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.

term_copy^⚠

Make copy of term, increases reference counter of term.

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.

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.

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.

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.

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.

term_get_ff_value^⚠

Get the string representation of a finite field value (base 10).

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.

term_get_id^⚠

Get the id of a given term. @param term The term. @return The id of the term.

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.

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.

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.

term_get_kind^⚠

Get the kind of a given term. @param term The term. @return The kind of the term.

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.

term_get_op^⚠

Get the operator of a term with an operator.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

term_get_sort^⚠

Get the sort of a given term. @param term The term. @return The sort of the term.

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.

term_get_symbol^⚠

Get the symbol of a given term with a symbol.

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.

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.

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.

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.

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.

term_has_op^⚠

Determine if a given term has an operator. @param term The term. @return True iff the term has an operator.

term_has_symbol^⚠

Determine if a given term has a symbol (a name).

term_hash^⚠

Compute the hash value of a term. @param term The term. @return The hash value of the term.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

term_is_sequence_value^⚠

Determine if a given term is a sequence value.

term_is_set_value^⚠

Determine if a given term is a set value.

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.

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.

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.

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.

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.

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.

term_manager_delete^⚠

Delete a cvc5 term manager instance. @param tm The term manager instance.

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.

term_manager_new^⚠

Construct a new instance of a cvc5 term manager. @return The cvc5 term manager.

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.

term_manager_release^⚠

Release all managed references.

term_release^⚠

Release copy of term, decrements reference counter of term.

term_substitute_term^⚠

Replace a given term t with term replacement in a given term.

term_substitute_terms^⚠

Simultaneously replace given terms terms with terms replacements in a given term.

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.

unknown_explanation_to_string^⚠

Get a string representation of a Cvc5UnknownExplanation. @param exp The unknown explanation. @return The string representation.

Type Aliases

Datatype

A cvc5 datatype.

DatatypeConstructor

A cvc5 datatype constructor.

DatatypeConstructorDecl

A cvc5 datatype constructor declaration. A datatype constructor declaration is a specification used for creating a datatype constructor.

DatatypeDecl

A cvc5 datatype declaration. A datatype declaration is not itself a datatype (see Datatype), but a specification for creating a datatype sort.

DatatypeSelector

A cvc5 datatype selector.

Grammar

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.

Op

A cvc5 operator.

Proof

A cvc5 proof.

Result

Encapsulation of a three-valued solver result, with explanations.

Sort

The sort of a cvc5 term.

Stat

A cvc5 statistic.

Statistics

A cvc5 statistics instance.

SynthResult

Encapsulation of a solver synth result.

Term

A cvc5 term.

__uint32_t

__uint_least32_t

char32_t

wchar_t