Add priorities to getNextDecision. Properly handle case for finite types + unbounded...
[cvc5.git] / src / theory /
drwxr-xr-x   ..
-rw-r--r-- 18 .gitignore
drwxr-xr-x - arith
drwxr-xr-x - arrays
-rw-r--r-- 2592 atom_requests.cpp
-rw-r--r-- 3161 atom_requests.h
drwxr-xr-x - booleans
drwxr-xr-x - builtin
drwxr-xr-x - bv
drwxr-xr-x - datatypes
drwxr-xr-x - example
drwxr-xr-x - fp
drwxr-xr-x - idl
-rw-r--r-- 1612 interrupted.h
-rw-r--r-- 48093 ite_utilities.cpp
-rw-r--r-- 10856 ite_utilities.h
-rw-r--r-- 16894 logic_info.cpp
-rw-r--r-- 8168 logic_info.h
-rw-r--r-- 593 logic_info.i
-rwxr-xr-x 6846 mkrewriter
-rwxr-xr-x 10976 mktheorytraits
-rw-r--r-- 9177 output_channel.h
drwxr-xr-x - quantifiers
-rw-r--r-- 76015 quantifiers_engine.cpp
-rw-r--r-- 18450 quantifiers_engine.h
-rw-r--r-- 16901 rep_set.cpp
-rw-r--r-- 4838 rep_set.h
-rw-r--r-- 9561 rewriter.cpp
-rw-r--r-- 3486 rewriter.h
-rw-r--r-- 2633 rewriter_attributes.h
-rw-r--r-- 2610 rewriter_tables_template.h
drwxr-xr-x - sep
drwxr-xr-x - sets
-rw-r--r-- 8971 shared_terms_database.cpp
-rw-r--r-- 7552 shared_terms_database.h
-rw-r--r-- 31401 sort_inference.cpp
-rw-r--r-- 4153 sort_inference.h
drwxr-xr-x - strings
-rw-r--r-- 8825 substitutions.cpp
-rw-r--r-- 5528 substitutions.h
-rw-r--r-- 12232 term_registration_visitor.cpp
-rw-r--r-- 4057 term_registration_visitor.h
-rw-r--r-- 20020 theory.cpp
-rw-r--r-- 33211 theory.h
-rw-r--r-- 81807 theory_engine.cpp
-rw-r--r-- 27608 theory_engine.h
-rw-r--r-- 40589 theory_model.cpp
-rw-r--r-- 9176 theory_model.h
-rw-r--r-- 1490 theory_registrar.h
-rw-r--r-- 4112 theory_test_utils.h
-rw-r--r-- 1388 theory_traits_template.h
-rw-r--r-- 5277 type_enumerator.h
-rw-r--r-- 1538 type_enumerator_template.cpp
drwxr-xr-x - uf
-rw-r--r-- 25461 unconstrained_simplifier.cpp
-rw-r--r-- 1913 unconstrained_simplifier.h
-rw-r--r-- 3086 valuation.cpp
-rw-r--r-- 4709 valuation.h