cvc4-1.4
|
▼ builds | |
► armv7hl-redhat-linux-gnu | |
► production-abc-proof | |
► src | |
► expr | |
expr.h | Expr.h |
expr_manager.h | Expr_manager.h |
kind.h | Kind.h |
► util | |
tls.h | Header to define CVC4_THREAD whether or not TLS is supported by the compiler/runtime platform |
▼ src | |
► bindings | |
► compat | |
► c | |
c_interface.h | |
c_interface_defs.h | |
► compat | |
cvc3_compat.h | CVC3 compatibility layer for CVC4 |
► context | |
cdhashmap_forward.h | This is a forward declaration header to declare the CDHashMap<> template |
cdhashset_forward.h | This is a forward declaration header to declare the CDSet<> template |
cdinsert_hashmap_forward.h | This is a forward declaration header to declare the CDInsertHashMap<> template |
cdlist_forward.h | This is a forward declaration header to declare the CDList<> template |
cdtrail_hashmap_forward.h | This is a forward declaration header to declare the CDTrailHashMap<> template |
► decision | |
options.h | Options.h |
► expr | |
command.h | Implementation of the command pattern on SmtEngines |
expr_stream.h | A stream interface for expressions |
options.h | Options.h |
pickler.h | This is a "pickler" for expressions |
symbol_table.h | Convenience class for scoping variable and type declarations |
type.h | Interface for expression types |
variable_type_map.h | [[ Add one-line brief description here ]] |
► include | |
cvc4.h | Main header file for CVC4 library functionality |
cvc4_private_library.h | #-inclusion of this file marks a header as private and generates a warning when the file is included improperly |
cvc4_public.h | Macros that should be defined everywhere during the building of the libraries and driver binary, and also exported to the user |
cvc4parser_public.h | Macros that should be defined everywhere during the building of the libraries and driver binary, and also exported to the user |
► lib | |
clock_gettime.h | Replacement for clock_gettime() for systems without it (like Mac OS X) |
ffs.h | Replacement for ffs() for systems without it (like Win32) |
strtok_r.h | Replacement for strtok_r() for systems without it (like Win32) |
► main | |
options.h | Options.h |
► options | |
base_options.h | Base_options.h |
option_exception.h | Options-related exceptions |
options.h | Global (command-line, set-option, ...) parameters for SMT |
► parser | |
input.h | Base for parser inputs |
options.h | Options.h |
parser.h | A collection of state for use by parser implementations |
parser_builder.h | A builder for parsers |
parser_exception.h | Exception class for parse errors |
► printer | |
modes.h | [[ Add one-line brief description here ]] |
options.h | Options.h |
► proof | |
options.h | Options.h |
► prop | |
options.h | Options.h |
sat_solver_factory.h | SAT Solver |
► smt | |
logic_exception.h | An exception that is thrown when a feature is used outside the logic that CVC4 is currently using |
modal_exception.h | An exception that is thrown when an interactive-only feature while CVC4 is being used in a non-interactive setting |
options.h | Options.h |
simplification_mode.h | [[ Add one-line brief description here ]] |
smt_engine.h | SmtEngine: the main public entry point of libcvc4 |
► theory | |
► arith | |
arith_heuristic_pivot_rule.h | [[ Add one-line brief description here ]] |
arith_propagation_mode.h | [[ Add one-line brief description here ]] |
arith_unate_lemma_mode.h | [[ Add one-line brief description here ]] |
options.h | Options.h |
► arrays | |
options.h | Options.h |
► booleans | |
options.h | Options.h |
► builtin | |
options.h | Options.h |
► bv | |
options.h | Options.h |
► datatypes | |
options.h | Options.h |
► idl | |
options.h | Options.h |
► quantifiers | |
options.h | Options.h |
► sets | |
options.h | Options.h |
► strings | |
options.h | Options.h |
► uf | |
options.h | Options.h |
logic_info.h | A class giving information about a logic (group a theory modules and configuration information) |
options.h | Options.h |
theoryof_mode.h | Option selection for theoryOf() operation |
► util | |
abstract_value.h | Representation of abstract values |
array.h | Array types |
array_store_all.h | Representation of a constant array (an array in which the element is the same for all indices) |
ascription_type.h | A class representing a type ascription |
bitvector.h | [[ Add one-line brief description here ]] |
bool.h | A hash function for Boolean |
cardinality.h | Representation of cardinality |
chain.h | [[ Add one-line brief description here ]] |
channel.h | [[ Add one-line brief description here ]] |
configuration.h | Interface to a public class that provides compile-time information about the CVC4 library |
datatype.h | A class representing a Datatype definition |
divisible.h | [[ Add one-line brief description here ]] |
emptyset.h | [[ Add one-line brief description here ]] |
exception.h | CVC4's exception base class and some associated utilities |
gmp_util.h | [[ Add one-line brief description here ]] |
hash.h | [[ Add one-line brief description here ]] |
integer_cln_imp.h | A multiprecision integer constant; wraps a CLN multiprecision integer |
integer_gmp_imp.h | A multiprecision integer constant; wraps a GMP multiprecision integer |
language.h | Definition of input and output languages |
lemma_input_channel.h | [[ Add one-line brief description here ]] |
lemma_output_channel.h | Mechanism for communication about new lemmas |
predicate.h | Representation of predicates for predicate subtyping |
proof.h | [[ Add one-line brief description here ]] |
rational_cln_imp.h | Multiprecision rational constants; wraps a CLN multiprecision rational |
rational_gmp_imp.h | Multiprecision rational constants; wraps a GMP multiprecision rational |
record.h | A class representing a Record definition |
regexp.h | [[ Add one-line brief description here ]] |
result.h | Encapsulation of the result of a query |
sexpr.h | Simple representation of S-expressions |
statistics.h | [[ Add one-line brief description here ]] |
subrange_bound.h | Representation of subrange bounds |
tuple.h | Tuple operators |
uninterpreted_constant.h | Representation of constants of uninterpreted sorts |