use super::*;
#[repr(C)]
#[derive(Debug, Copy, Clone)]
pub struct SymbolManager {
_unused: [u8; 0],
}
#[repr(C)]
#[derive(Debug, Copy, Clone)]
pub struct cvc5_cmd_t {
_unused: [u8; 0],
}
#[doc = " Encapsulation of a command.\n\n Commands are constructed by the input parser and can be invoked on\n the solver and symbol manager."]
pub type Command = *mut cvc5_cmd_t;
#[repr(C)]
#[derive(Debug, Copy, Clone)]
pub struct InputParser {
_unused: [u8; 0],
}
unsafe extern "C" {
#[doc = " Construct a new instance of a cvc5 symbol manager.\n @param tm The associated term manager instance.\n @return The cvc5 symbol manager instance."]
#[link_name = "\u{1}cvc5_symbol_manager_new"]
pub fn symbol_manager_new(tm: *mut TermManager) -> *mut SymbolManager;
}
unsafe extern "C" {
#[doc = " Delete a cvc5 symbol manager instance.\n @param sm The symbol manager instance."]
#[link_name = "\u{1}cvc5_symbol_manager_delete"]
pub fn symbol_manager_delete(sm: *mut SymbolManager);
}
unsafe extern "C" {
#[doc = " Determine if the logic of a given symbol manager has been set.\n @param sm The symbol manager instance.\n @return True if the logic has been set."]
#[link_name = "\u{1}cvc5_sm_is_logic_set"]
pub fn sm_is_logic_set(sm: *mut SymbolManager) -> bool;
}
unsafe extern "C" {
#[doc = " Get the logic configured for a given symbol manager.\n @note Asserts `cvc5_sm_is_logic_set()`.\n @param sm The symbol manager instance.\n @return The configured logic.\n @note The returned char* pointer is only valid until the next call to this\n function."]
#[link_name = "\u{1}cvc5_sm_get_logic"]
pub fn sm_get_logic(sm: *mut SymbolManager) -> *const ::std::os::raw::c_char;
}
unsafe extern "C" {
#[doc = " Get the list of sorts that have been declared via `declare-sort` commands.\n These are the sorts that are printed as part of a response to a\n `get-model` command.\n\n @param sm The symbol manager instance.\n @param size The size of the resulting sorts array.\n @return The declared sorts."]
#[link_name = "\u{1}cvc5_sm_get_declared_sorts"]
pub fn sm_get_declared_sorts(sm: *mut SymbolManager, size: *mut usize) -> *const Sort;
}
unsafe extern "C" {
#[doc = " Get the list of terms that have been declared via `declare-fun` and\n `declare-const`. These are the terms that are printed in response to a\n `get-model` command.\n\n @param sm The symbol manager instance.\n @param size The size of the resulting sorts array.\n @return The declared terms.terms"]
#[link_name = "\u{1}cvc5_sm_get_declared_terms"]
pub fn sm_get_declared_terms(sm: *mut SymbolManager, size: *mut usize) -> *const Term;
}
unsafe extern "C" {
#[doc = " Get the named terms that have been given to them via the :named attribute.\n\n @param sm The symbol manager instance.\n @param size The resulting size of `terms` and `names`.\n @param terms The resulting term that are mapped to the resulting `names`.\n @param names The resulting names.\n\n @note The resulting `terms` and `names` array pointers are only valid\n until the next call to this function."]
#[link_name = "\u{1}cvc5_sm_get_named_terms"]
pub fn sm_get_named_terms(
sm: *mut SymbolManager,
size: *mut usize,
terms: *mut *mut Term,
names: *mut *mut *const ::std::os::raw::c_char,
);
}
unsafe extern "C" {
#[doc = " Invoke a given command on the solver and symbol manager sm and return any\n resulting output as a string.\n @param cmd The command to invoke.\n @param cvc5 The solver to invoke the command on.\n @param sm The symbol manager to invoke the command on.\n @return The output of invoking the command.\n @note The returned char* pointer is only valid until the next call to this\n function."]
#[link_name = "\u{1}cvc5_cmd_invoke"]
pub fn cmd_invoke(
cmd: Command,
cvc5: *mut Solver,
sm: *mut SymbolManager,
) -> *const ::std::os::raw::c_char;
}
unsafe extern "C" {
#[doc = " Get a string representation of this command.\n @param cmd The command to invoke.\n @return The string representation.\n @note The returned char* pointer is only valid until the next call to this\n function."]
#[link_name = "\u{1}cvc5_cmd_to_string"]
pub fn cmd_to_string(cmd: Command) -> *const ::std::os::raw::c_char;
}
unsafe extern "C" {
#[doc = " Get the name for a given command, e.g., \"assert\".\n @param cmd The command to invoke.\n @return The name of the command.\n @note The returned char* pointer is only valid until the next call to this\n function."]
#[link_name = "\u{1}cvc5_cmd_get_name"]
pub fn cmd_get_name(cmd: Command) -> *const ::std::os::raw::c_char;
}
unsafe extern "C" {
#[doc = " Construct a new instance of a cvc5 input parser.\n @param cvc5 The associated solver instance.\n @param sm The associated symbol manager instance, contains a symbol table\n that maps symbols to terms and sorts. Must have a logic that is\n compatible with the solver. May be NULL to start with and\n initially empty symbol manager.\n @return The cvc5 symbol manager instance."]
#[link_name = "\u{1}cvc5_parser_new"]
pub fn parser_new(cvc5: *mut Solver, sm: *mut SymbolManager) -> *mut InputParser;
}
unsafe extern "C" {
#[doc = " Delete a cvc5 input parser instance.\n @param parser The input parser instance."]
#[link_name = "\u{1}cvc5_parser_delete"]
pub fn parser_delete(parser: *mut InputParser);
}
unsafe extern "C" {
#[doc = " Release all objects managed by the parser.\n\n This will free all memory used by any managed objects allocated by the\n parser.\n\n @note This invalidates all managed objects created by the parser.\n\n @param parser The parser instance."]
#[link_name = "\u{1}cvc5_parser_release"]
pub fn parser_release(parser: *mut InputParser);
}
unsafe extern "C" {
#[doc = " Get the associated solver instance of a given parser.\n @param parser The parser instance.\n @return The solver."]
#[link_name = "\u{1}cvc5_parser_get_solver"]
pub fn parser_get_solver(parser: *mut InputParser) -> *mut Solver;
}
unsafe extern "C" {
#[doc = " Get the associated symbol manager of a given parser.\n @param parser The parser instance.\n @return The symbol manager."]
#[link_name = "\u{1}cvc5_parser_get_sm"]
pub fn parser_get_sm(parser: *mut InputParser) -> *mut SymbolManager;
}
unsafe extern "C" {
#[doc = " Configure given file as input to a given input parser.\n @param parser The input parser instance.\n @param lang the input language (e.g., #CVC5_INPUT_LANGUAGE_SMT_LIB_2_6)\n @param filename The name of the file to configure."]
#[link_name = "\u{1}cvc5_parser_set_file_input"]
pub fn parser_set_file_input(
parser: *mut InputParser,
lang: InputLanguage,
filename: *const ::std::os::raw::c_char,
);
}
unsafe extern "C" {
#[doc = " Configure a given concrete input string as the input to a given input parser.\n @param parser The input parser instance.\n @param lang The input language of the input string.\n @param input The input string.\n @param name The name to use as input stream name for error messages."]
#[link_name = "\u{1}cvc5_parser_set_str_input"]
pub fn parser_set_str_input(
parser: *mut InputParser,
lang: InputLanguage,
input: *const ::std::os::raw::c_char,
name: *const ::std::os::raw::c_char,
);
}
unsafe extern "C" {
#[doc = " Configure that we will be feeding strings to a given input parser via\n `cvc5_parser_append_inc_str_input()` below.\n @param parser The input parser instance.\n @param lang The input language of the input string.\n @param name The name to use as input stream name for error messages."]
#[link_name = "\u{1}cvc5_parser_set_inc_str_input"]
pub fn parser_set_inc_str_input(
parser: *mut InputParser,
lang: InputLanguage,
name: *const ::std::os::raw::c_char,
);
}
unsafe extern "C" {
#[doc = " Append string to the input being parsed by this parser. Should be\n called after calling `cvc5_parser_set_inc_str_input()`.\n @param parser The input parser instance.\n @param input The input string."]
#[link_name = "\u{1}cvc5_parser_append_inc_str_input"]
pub fn parser_append_inc_str_input(
parser: *mut InputParser,
input: *const ::std::os::raw::c_char,
);
}
unsafe extern "C" {
#[doc = " Parse and return the next command. Will initialize the logic to \"ALL\"\n or the forced logic if no logic is set prior to this point and a command\n is read that requires initializing the logic.\n\n @param parser The input parser instance.\n @param error_msg Output parameter for the error message in case of a parse\n error, NULL if no error occurred.\n @return The parsed command. NULL if no command was read."]
#[link_name = "\u{1}cvc5_parser_next_command"]
pub fn parser_next_command(
parser: *mut InputParser,
error_msg: *mut *const ::std::os::raw::c_char,
) -> Command;
}
unsafe extern "C" {
#[doc = " Parse and return the next term. Requires setting the logic prior\n to this point.\n @param parser The input parser instance.\n @param error_msg Output parameter for the error message in case of a parse\n error, NULL if no error occurred.\n @return The parsed term. NULL if no term was read."]
#[link_name = "\u{1}cvc5_parser_next_term"]
pub fn parser_next_term(
parser: *mut InputParser,
error_msg: *mut *const ::std::os::raw::c_char,
) -> Term;
}
unsafe extern "C" {
#[doc = " Is this parser done reading input?\n @param parser The input parser instance.\n @return True if parser is done reading input."]
#[link_name = "\u{1}cvc5_parser_done"]
pub fn parser_done(parser: *mut InputParser) -> bool;
}