Skip to main content

Cvc5DatatypeDecl

Type Alias Cvc5DatatypeDecl 

Source
pub type Cvc5DatatypeDecl = *mut cvc5_dt_decl_t;
Expand description

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

The interface for a datatype declaration coincides with the syntax for the SMT-LIB 2.6 command declare-datatype, or a single datatype within the declare-datatypes command.

Datatype sorts can be constructed from a Cvc5DatatypeDecl using:

  • cvc5_mk_datatype_sort()
  • cvc5_mk_datatype_sorts()