File List

Here is a list of all files with brief descriptions:

[detail level 123456]

builds
armv7hl-redhat-linux-gnu
default-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
model_format_mode.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
quantifiers
options.h	Options.h
rewriterules
options.h	Options.h
strings
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 multi-precision rational constant
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 ]]
dump.h	Dump utility classes and functions
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
AUTHORS
COPYING
NEWS
README