projects
/
cvc5.git
/ tree
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
| tree
history
|
HEAD
Add node utils for the arithmetic rewriter (#8012)
[cvc5.git]
/
src
/
theory
/
drwxr-xr-x
..
-rw-r--r--
1743
CMakeLists.txt
blob
|
history
|
raw
drwxr-xr-x
-
arith
tree
|
history
drwxr-xr-x
-
arrays
tree
|
history
-rw-r--r--
777
assertion.cpp
blob
|
history
|
raw
-rw-r--r--
1498
assertion.h
blob
|
history
|
raw
-rw-r--r--
2622
atom_requests.cpp
blob
|
history
|
raw
-rw-r--r--
3140
atom_requests.h
blob
|
history
|
raw
drwxr-xr-x
-
bags
tree
|
history
drwxr-xr-x
-
booleans
tree
|
history
drwxr-xr-x
-
builtin
tree
|
history
drwxr-xr-x
-
bv
tree
|
history
-rw-r--r--
1634
care_graph.h
blob
|
history
|
raw
-rw-r--r--
3299
combination_care_graph.cpp
blob
|
history
|
raw
-rw-r--r--
1440
combination_care_graph.h
blob
|
history
|
raw
-rw-r--r--
4220
combination_engine.cpp
blob
|
history
|
raw
-rw-r--r--
4509
combination_engine.h
blob
|
history
|
raw
drwxr-xr-x
-
datatypes
tree
|
history
-rw-r--r--
3430
decision_manager.cpp
blob
|
history
|
raw
-rw-r--r--
5713
decision_manager.h
blob
|
history
|
raw
-rw-r--r--
4083
decision_strategy.cpp
blob
|
history
|
raw
-rw-r--r--
4943
decision_strategy.h
blob
|
history
|
raw
-rw-r--r--
3736
difficulty_manager.cpp
blob
|
history
|
raw
-rw-r--r--
3109
difficulty_manager.h
blob
|
history
|
raw
-rw-r--r--
1553
ee_manager.cpp
blob
|
history
|
raw
-rw-r--r--
3202
ee_manager.h
blob
|
history
|
raw
-rw-r--r--
10422
ee_manager_central.cpp
blob
|
history
|
raw
-rw-r--r--
5213
ee_manager_central.h
blob
|
history
|
raw
-rw-r--r--
3517
ee_manager_distributed.cpp
blob
|
history
|
raw
-rw-r--r--
2653
ee_manager_distributed.h
blob
|
history
|
raw
-rw-r--r--
2719
ee_setup_info.h
blob
|
history
|
raw
-rw-r--r--
5244
engine_output_channel.cpp
blob
|
history
|
raw
-rw-r--r--
3456
engine_output_channel.h
blob
|
history
|
raw
-rw-r--r--
30076
evaluator.cpp
blob
|
history
|
raw
-rw-r--r--
6447
evaluator.h
blob
|
history
|
raw
-rw-r--r--
15541
ext_theory.cpp
blob
|
history
|
raw
-rw-r--r--
12887
ext_theory.h
blob
|
history
|
raw
drwxr-xr-x
-
fp
tree
|
history
-rw-r--r--
2257
incomplete_id.cpp
blob
|
history
|
raw
-rw-r--r--
3032
incomplete_id.h
blob
|
history
|
raw
-rw-r--r--
27281
inference_id.cpp
blob
|
history
|
raw
-rw-r--r--
35899
inference_id.h
blob
|
history
|
raw
-rw-r--r--
1650
inference_id_proof_annotator.cpp
blob
|
history
|
raw
-rw-r--r--
2318
inference_id_proof_annotator.h
blob
|
history
|
raw
-rw-r--r--
5709
inference_manager_buffered.cpp
blob
|
history
|
raw
-rw-r--r--
7113
inference_manager_buffered.h
blob
|
history
|
raw
-rw-r--r--
1626
interrupted.h
blob
|
history
|
raw
-rw-r--r--
20765
logic_info.cpp
blob
|
history
|
raw
-rw-r--r--
9447
logic_info.h
blob
|
history
|
raw
-rwxr-xr-x
6462
mkrewriter
blob
|
history
|
raw
-rwxr-xr-x
10358
mktheorytraits
blob
|
history
|
raw
-rw-r--r--
5144
model_manager.cpp
blob
|
history
|
raw
-rw-r--r--
5081
model_manager.h
blob
|
history
|
raw
-rw-r--r--
4216
model_manager_distributed.cpp
blob
|
history
|
raw
-rw-r--r--
2111
model_manager_distributed.h
blob
|
history
|
raw
-rw-r--r--
2390
output_channel.cpp
blob
|
history
|
raw
-rw-r--r--
6787
output_channel.h
blob
|
history
|
raw
drwxr-xr-x
-
quantifiers
tree
|
history
-rw-r--r--
24536
quantifiers_engine.cpp
blob
|
history
|
raw
-rw-r--r--
7698
quantifiers_engine.h
blob
|
history
|
raw
-rw-r--r--
14888
relevance_manager.cpp
blob
|
history
|
raw
-rw-r--r--
10569
relevance_manager.h
blob
|
history
|
raw
-rw-r--r--
12621
rep_set.cpp
blob
|
history
|
raw
-rw-r--r--
11668
rep_set.h
blob
|
history
|
raw
-rw-r--r--
16390
rewriter.cpp
blob
|
history
|
raw
-rw-r--r--
6024
rewriter.h
blob
|
history
|
raw
-rw-r--r--
2582
rewriter_attributes.h
blob
|
history
|
raw
-rw-r--r--
2758
rewriter_tables_template.h
blob
|
history
|
raw
drwxr-xr-x
-
sep
tree
|
history
drwxr-xr-x
-
sets
tree
|
history
-rw-r--r--
5374
shared_solver.cpp
blob
|
history
|
raw
-rw-r--r--
5335
shared_solver.h
blob
|
history
|
raw
-rw-r--r--
2755
shared_solver_distributed.cpp
blob
|
history
|
raw
-rw-r--r--
2206
shared_solver_distributed.h
blob
|
history
|
raw
-rw-r--r--
10327
shared_terms_database.cpp
blob
|
history
|
raw
-rw-r--r--
8734
shared_terms_database.h
blob
|
history
|
raw
-rw-r--r--
1280
skolem_lemma.cpp
blob
|
history
|
raw
-rw-r--r--
1959
skolem_lemma.h
blob
|
history
|
raw
-rw-r--r--
5109
smt_engine_subsolver.cpp
blob
|
history
|
raw
-rw-r--r--
5552
smt_engine_subsolver.h
blob
|
history
|
raw
-rw-r--r--
31305
sort_inference.cpp
blob
|
history
|
raw
-rw-r--r--
6142
sort_inference.h
blob
|
history
|
raw
drwxr-xr-x
-
strings
tree
|
history
-rw-r--r--
13168
subs_minimize.cpp
blob
|
history
|
raw
-rw-r--r--
3420
subs_minimize.h
blob
|
history
|
raw
-rw-r--r--
8218
substitutions.cpp
blob
|
history
|
raw
-rw-r--r--
5314
substitutions.h
blob
|
history
|
raw
-rw-r--r--
10507
term_registration_visitor.cpp
blob
|
history
|
raw
-rw-r--r--
6007
term_registration_visitor.h
blob
|
history
|
raw
-rw-r--r--
20542
theory.cpp
blob
|
history
|
raw
-rw-r--r--
30487
theory.h
blob
|
history
|
raw
-rw-r--r--
67705
theory_engine.cpp
blob
|
history
|
raw
-rw-r--r--
20617
theory_engine.h
blob
|
history
|
raw
-rw-r--r--
3720
theory_engine_proof_generator.cpp
blob
|
history
|
raw
-rw-r--r--
2733
theory_engine_proof_generator.h
blob
|
history
|
raw
-rw-r--r--
2283
theory_eq_notify.h
blob
|
history
|
raw
-rw-r--r--
4344
theory_id.cpp
blob
|
history
|
raw
-rw-r--r--
3038
theory_id.h
blob
|
history
|
raw
-rw-r--r--
1743
theory_inference.cpp
blob
|
history
|
raw
-rw-r--r--
4030
theory_inference.h
blob
|
history
|
raw
-rw-r--r--
19858
theory_inference_manager.cpp
blob
|
history
|
raw
-rw-r--r--
20586
theory_inference_manager.h
blob
|
history
|
raw
-rw-r--r--
26337
theory_model.cpp
blob
|
history
|
raw
-rw-r--r--
19251
theory_model.h
blob
|
history
|
raw
-rw-r--r--
49186
theory_model_builder.cpp
blob
|
history
|
raw
-rw-r--r--
12029
theory_model_builder.h
blob
|
history
|
raw
-rw-r--r--
18011
theory_preprocessor.cpp
blob
|
history
|
raw
-rw-r--r--
7467
theory_preprocessor.h
blob
|
history
|
raw
-rw-r--r--
2496
theory_rewriter.cpp
blob
|
history
|
raw
-rw-r--r--
5572
theory_rewriter.h
blob
|
history
|
raw
-rw-r--r--
3643
theory_state.cpp
blob
|
history
|
raw
-rw-r--r--
4072
theory_state.h
blob
|
history
|
raw
-rw-r--r--
1476
theory_traits_template.h
blob
|
history
|
raw
-rw-r--r--
10427
trust_substitutions.cpp
blob
|
history
|
raw
-rw-r--r--
5625
trust_substitutions.h
blob
|
history
|
raw
-rw-r--r--
5862
type_enumerator.h
blob
|
history
|
raw
-rw-r--r--
1484
type_enumerator_template.cpp
blob
|
history
|
raw
-rw-r--r--
2944
type_set.cpp
blob
|
history
|
raw
-rw-r--r--
2742
type_set.h
blob
|
history
|
raw
drwxr-xr-x
-
uf
tree
|
history
-rw-r--r--
6190
valuation.cpp
blob
|
history
|
raw
-rw-r--r--
7974
valuation.h
blob
|
history
|
raw