projects
/
cvc5.git
/ tree
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
| tree
history
|
HEAD
Add the combination engine (#4939)
[cvc5.git]
/
src
/
theory
/
drwxr-xr-x
..
-rw-r--r--
1173
CMakeLists.txt
blob
|
history
|
raw
drwxr-xr-x
-
arith
tree
|
history
drwxr-xr-x
-
arrays
tree
|
history
-rw-r--r--
795
assertion.cpp
blob
|
history
|
raw
-rw-r--r--
1551
assertion.h
blob
|
history
|
raw
-rw-r--r--
2598
atom_requests.cpp
blob
|
history
|
raw
-rw-r--r--
3128
atom_requests.h
blob
|
history
|
raw
drwxr-xr-x
-
booleans
tree
|
history
drwxr-xr-x
-
builtin
tree
|
history
drwxr-xr-x
-
bv
tree
|
history
-rw-r--r--
1665
care_graph.h
blob
|
history
|
raw
-rw-r--r--
2869
combination_care_graph.cpp
blob
|
history
|
raw
-rw-r--r--
1401
combination_care_graph.h
blob
|
history
|
raw
-rw-r--r--
3565
combination_engine.cpp
blob
|
history
|
raw
-rw-r--r--
3921
combination_engine.h
blob
|
history
|
raw
drwxr-xr-x
-
datatypes
tree
|
history
-rw-r--r--
3407
decision_manager.cpp
blob
|
history
|
raw
-rw-r--r--
5741
decision_manager.h
blob
|
history
|
raw
-rw-r--r--
3990
decision_strategy.cpp
blob
|
history
|
raw
-rw-r--r--
4922
decision_strategy.h
blob
|
history
|
raw
-rw-r--r--
3656
eager_proof_generator.cpp
blob
|
history
|
raw
-rw-r--r--
6872
eager_proof_generator.h
blob
|
history
|
raw
-rw-r--r--
909
ee_manager.cpp
blob
|
history
|
raw
-rw-r--r--
3027
ee_manager.h
blob
|
history
|
raw
-rw-r--r--
4749
ee_manager_distributed.cpp
blob
|
history
|
raw
-rw-r--r--
4512
ee_manager_distributed.h
blob
|
history
|
raw
-rw-r--r--
1591
ee_setup_info.h
blob
|
history
|
raw
-rw-r--r--
11165
engine_output_channel.cpp
blob
|
history
|
raw
-rw-r--r--
3783
engine_output_channel.h
blob
|
history
|
raw
-rw-r--r--
29375
evaluator.cpp
blob
|
history
|
raw
-rw-r--r--
5575
evaluator.h
blob
|
history
|
raw
-rw-r--r--
15459
ext_theory.cpp
blob
|
history
|
raw
-rw-r--r--
9693
ext_theory.h
blob
|
history
|
raw
drwxr-xr-x
-
fp
tree
|
history
-rw-r--r--
1613
interrupted.h
blob
|
history
|
raw
-rw-r--r--
20917
logic_info.cpp
blob
|
history
|
raw
-rw-r--r--
9243
logic_info.h
blob
|
history
|
raw
-rwxr-xr-x
6483
mkrewriter
blob
|
history
|
raw
-rwxr-xr-x
10487
mktheorytraits
blob
|
history
|
raw
-rw-r--r--
4643
model_manager.cpp
blob
|
history
|
raw
-rw-r--r--
4079
model_manager.h
blob
|
history
|
raw
-rw-r--r--
2736
model_manager_distributed.cpp
blob
|
history
|
raw
-rw-r--r--
1981
model_manager_distributed.h
blob
|
history
|
raw
-rw-r--r--
3026
output_channel.cpp
blob
|
history
|
raw
-rw-r--r--
8718
output_channel.h
blob
|
history
|
raw
drwxr-xr-x
-
quantifiers
tree
|
history
-rw-r--r--
46116
quantifiers_engine.cpp
blob
|
history
|
raw
-rw-r--r--
15575
quantifiers_engine.h
blob
|
history
|
raw
-rw-r--r--
8247
relevance_manager.cpp
blob
|
history
|
raw
-rw-r--r--
6250
relevance_manager.h
blob
|
history
|
raw
-rw-r--r--
12466
rep_set.cpp
blob
|
history
|
raw
-rw-r--r--
11656
rep_set.h
blob
|
history
|
raw
-rw-r--r--
15431
rewriter.cpp
blob
|
history
|
raw
-rw-r--r--
7614
rewriter.h
blob
|
history
|
raw
-rw-r--r--
2609
rewriter_attributes.h
blob
|
history
|
raw
-rw-r--r--
2458
rewriter_tables_template.h
blob
|
history
|
raw
drwxr-xr-x
-
sep
tree
|
history
drwxr-xr-x
-
sets
tree
|
history
-rw-r--r--
9111
shared_terms_database.cpp
blob
|
history
|
raw
-rw-r--r--
7646
shared_terms_database.h
blob
|
history
|
raw
-rw-r--r--
3391
smt_engine_subsolver.cpp
blob
|
history
|
raw
-rw-r--r--
3126
smt_engine_subsolver.h
blob
|
history
|
raw
-rw-r--r--
31162
sort_inference.cpp
blob
|
history
|
raw
-rw-r--r--
6024
sort_inference.h
blob
|
history
|
raw
drwxr-xr-x
-
strings
tree
|
history
-rw-r--r--
13290
subs_minimize.cpp
blob
|
history
|
raw
-rw-r--r--
3465
subs_minimize.h
blob
|
history
|
raw
-rw-r--r--
8861
substitutions.cpp
blob
|
history
|
raw
-rw-r--r--
5553
substitutions.h
blob
|
history
|
raw
-rw-r--r--
12009
term_registration_visitor.cpp
blob
|
history
|
raw
-rw-r--r--
4063
term_registration_visitor.h
blob
|
history
|
raw
-rw-r--r--
16872
theory.cpp
blob
|
history
|
raw
-rw-r--r--
35847
theory.h
blob
|
history
|
raw
-rw-r--r--
74289
theory_engine.cpp
blob
|
history
|
raw
-rw-r--r--
24693
theory_engine.h
blob
|
history
|
raw
-rw-r--r--
2350
theory_engine_proof_generator.cpp
blob
|
history
|
raw
-rw-r--r--
2731
theory_engine_proof_generator.h
blob
|
history
|
raw
-rw-r--r--
2505
theory_id.cpp
blob
|
history
|
raw
-rw-r--r--
1576
theory_id.h
blob
|
history
|
raw
-rw-r--r--
25220
theory_model.cpp
blob
|
history
|
raw
-rw-r--r--
19615
theory_model.h
blob
|
history
|
raw
-rw-r--r--
48053
theory_model_builder.cpp
blob
|
history
|
raw
-rw-r--r--
13161
theory_model_builder.h
blob
|
history
|
raw
-rw-r--r--
13269
theory_preprocessor.cpp
blob
|
history
|
raw
-rw-r--r--
3941
theory_preprocessor.h
blob
|
history
|
raw
-rw-r--r--
2854
theory_proof_step_buffer.cpp
blob
|
history
|
raw
-rw-r--r--
3254
theory_proof_step_buffer.h
blob
|
history
|
raw
-rw-r--r--
1489
theory_registrar.h
blob
|
history
|
raw
-rw-r--r--
2089
theory_rewriter.cpp
blob
|
history
|
raw
-rw-r--r--
4182
theory_rewriter.h
blob
|
history
|
raw
-rw-r--r--
2776
theory_state.cpp
blob
|
history
|
raw
-rw-r--r--
3033
theory_state.h
blob
|
history
|
raw
-rw-r--r--
3490
theory_test_utils.h
blob
|
history
|
raw
-rw-r--r--
1363
theory_traits_template.h
blob
|
history
|
raw
-rw-r--r--
4061
trust_node.cpp
blob
|
history
|
raw
-rw-r--r--
5966
trust_node.h
blob
|
history
|
raw
-rw-r--r--
5431
type_enumerator.h
blob
|
history
|
raw
-rw-r--r--
1420
type_enumerator_template.cpp
blob
|
history
|
raw
-rw-r--r--
2959
type_set.cpp
blob
|
history
|
raw
-rw-r--r--
2806
type_set.h
blob
|
history
|
raw
drwxr-xr-x
-
uf
tree
|
history
-rw-r--r--
4715
valuation.cpp
blob
|
history
|
raw
-rw-r--r--
5343
valuation.h
blob
|
history
|
raw