projects
/
cvc5.git
/ tree
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
| tree
history
|
HEAD
(proof-new) Fix true explanations of propagations in pf equality engine (#5338)
[cvc5.git]
/
src
/
expr
/
drwxr-xr-x
..
-rw-r--r--
5610
CMakeLists.txt
blob
|
history
|
raw
-rw-r--r--
802
array.h
blob
|
history
|
raw
-rw-r--r--
3737
array_store_all.cpp
blob
|
history
|
raw
-rw-r--r--
2199
array_store_all.h
blob
|
history
|
raw
-rw-r--r--
1565
ascription_type.cpp
blob
|
history
|
raw
-rw-r--r--
1957
ascription_type.h
blob
|
history
|
raw
-rw-r--r--
3481
attribute.cpp
blob
|
history
|
raw
-rw-r--r--
19826
attribute.h
blob
|
history
|
raw
-rw-r--r--
15140
attribute_internals.h
blob
|
history
|
raw
-rw-r--r--
1738
attribute_unique_id.h
blob
|
history
|
raw
-rw-r--r--
2477
buffered_proof_generator.cpp
blob
|
history
|
raw
-rw-r--r--
2117
buffered_proof_generator.h
blob
|
history
|
raw
-rw-r--r--
1117
datatype_index.cpp
blob
|
history
|
raw
-rw-r--r--
1938
datatype_index.h
blob
|
history
|
raw
-rw-r--r--
27466
dtype.cpp
blob
|
history
|
raw
-rw-r--r--
26271
dtype.h
blob
|
history
|
raw
-rw-r--r--
19472
dtype_cons.cpp
blob
|
history
|
raw
-rw-r--r--
13276
dtype_cons.h
blob
|
history
|
raw
-rw-r--r--
2092
dtype_selector.cpp
blob
|
history
|
raw
-rw-r--r--
2421
dtype_selector.h
blob
|
history
|
raw
-rw-r--r--
1864
emptybag.cpp
blob
|
history
|
raw
-rw-r--r--
1735
emptybag.h
blob
|
history
|
raw
-rw-r--r--
2019
emptyset.cpp
blob
|
history
|
raw
-rw-r--r--
1779
emptyset.h
blob
|
history
|
raw
-rw-r--r--
3584
expr_iomanip.cpp
blob
|
history
|
raw
-rw-r--r--
4540
expr_iomanip.h
blob
|
history
|
raw
-rw-r--r--
2571
expr_manager_scope.h
blob
|
history
|
raw
-rw-r--r--
34307
expr_manager_template.cpp
blob
|
history
|
raw
-rw-r--r--
17277
expr_manager_template.h
blob
|
history
|
raw
-rw-r--r--
24315
expr_template.cpp
blob
|
history
|
raw
-rw-r--r--
18311
expr_template.h
blob
|
history
|
raw
-rw-r--r--
6517
kind_map.h
blob
|
history
|
raw
-rw-r--r--
2442
kind_template.cpp
blob
|
history
|
raw
-rw-r--r--
2920
kind_template.h
blob
|
history
|
raw
-rw-r--r--
7405
lazy_proof.cpp
blob
|
history
|
raw
-rw-r--r--
4452
lazy_proof.h
blob
|
history
|
raw
-rw-r--r--
10920
lazy_proof_chain.cpp
blob
|
history
|
raw
-rw-r--r--
6128
lazy_proof_chain.h
blob
|
history
|
raw
-rw-r--r--
1202
lazy_proof_set.cpp
blob
|
history
|
raw
-rw-r--r--
2003
lazy_proof_set.h
blob
|
history
|
raw
-rw-r--r--
5656
match_trie.cpp
blob
|
history
|
raw
-rw-r--r--
2526
match_trie.h
blob
|
history
|
raw
-rw-r--r--
5354
metakind_template.cpp
blob
|
history
|
raw
-rw-r--r--
6113
metakind_template.h
blob
|
history
|
raw
-rwxr-xr-x
7231
mkexpr
blob
|
history
|
raw
-rwxr-xr-x
9809
mkkind
blob
|
history
|
raw
-rwxr-xr-x
10363
mkmetakind
blob
|
history
|
raw
-rw-r--r--
3829
node.cpp
blob
|
history
|
raw
-rw-r--r--
49554
node.h
blob
|
history
|
raw
-rw-r--r--
18298
node_algorithm.cpp
blob
|
history
|
raw
-rw-r--r--
7905
node_algorithm.h
blob
|
history
|
raw
-rw-r--r--
48204
node_builder.h
blob
|
history
|
raw
-rw-r--r--
35621
node_manager.cpp
blob
|
history
|
raw
-rw-r--r--
55438
node_manager.h
blob
|
history
|
raw
-rw-r--r--
1411
node_manager_attributes.h
blob
|
history
|
raw
-rw-r--r--
3299
node_self_iterator.h
blob
|
history
|
raw
-rw-r--r--
4069
node_traversal.cpp
blob
|
history
|
raw
-rw-r--r--
4759
node_traversal.h
blob
|
history
|
raw
-rw-r--r--
2951
node_trie.cpp
blob
|
history
|
raw
-rw-r--r--
3961
node_trie.h
blob
|
history
|
raw
-rw-r--r--
2905
node_value.cpp
blob
|
history
|
raw
-rw-r--r--
15055
node_value.h
blob
|
history
|
raw
-rw-r--r--
3281
node_visitor.h
blob
|
history
|
raw
-rw-r--r--
13228
proof.cpp
blob
|
history
|
raw
-rw-r--r--
12013
proof.h
blob
|
history
|
raw
-rw-r--r--
10271
proof_checker.cpp
blob
|
history
|
raw
-rw-r--r--
7680
proof_checker.h
blob
|
history
|
raw
-rw-r--r--
6600
proof_generator.cpp
blob
|
history
|
raw
-rw-r--r--
5791
proof_generator.h
blob
|
history
|
raw
-rw-r--r--
2151
proof_node.cpp
blob
|
history
|
raw
-rw-r--r--
5134
proof_node.h
blob
|
history
|
raw
-rw-r--r--
5367
proof_node_algorithm.cpp
blob
|
history
|
raw
-rw-r--r--
2380
proof_node_algorithm.h
blob
|
history
|
raw
-rw-r--r--
10789
proof_node_manager.cpp
blob
|
history
|
raw
-rw-r--r--
8062
proof_node_manager.h
blob
|
history
|
raw
-rw-r--r--
4139
proof_node_to_sexpr.cpp
blob
|
history
|
raw
-rw-r--r--
2000
proof_node_to_sexpr.h
blob
|
history
|
raw
-rw-r--r--
8882
proof_node_updater.cpp
blob
|
history
|
raw
-rw-r--r--
5652
proof_node_updater.h
blob
|
history
|
raw
-rw-r--r--
8446
proof_rule.cpp
blob
|
history
|
raw
-rw-r--r--
38170
proof_rule.h
blob
|
history
|
raw
-rw-r--r--
2924
proof_step_buffer.cpp
blob
|
history
|
raw
-rw-r--r--
2875
proof_step_buffer.h
blob
|
history
|
raw
-rw-r--r--
3447
record.cpp
blob
|
history
|
raw
-rw-r--r--
2739
record.h
blob
|
history
|
raw
-rw-r--r--
7931
sequence.cpp
blob
|
history
|
raw
-rw-r--r--
5748
sequence.h
blob
|
history
|
raw
-rw-r--r--
11273
skolem_manager.cpp
blob
|
history
|
raw
-rw-r--r--
9571
skolem_manager.h
blob
|
history
|
raw
-rw-r--r--
3522
subs.cpp
blob
|
history
|
raw
-rw-r--r--
2946
subs.h
blob
|
history
|
raw
-rw-r--r--
3334
sygus_datatype.cpp
blob
|
history
|
raw
-rw-r--r--
4646
sygus_datatype.h
blob
|
history
|
raw
-rw-r--r--
4595
symbol_manager.cpp
blob
|
history
|
raw
-rw-r--r--
3780
symbol_manager.h
blob
|
history
|
raw
-rw-r--r--
21234
symbol_table.cpp
blob
|
history
|
raw
-rw-r--r--
7064
symbol_table.h
blob
|
history
|
raw
-rw-r--r--
5233
tconv_seq_proof_generator.cpp
blob
|
history
|
raw
-rw-r--r--
4891
tconv_seq_proof_generator.h
blob
|
history
|
raw
-rw-r--r--
5891
term_canonize.cpp
blob
|
history
|
raw
-rw-r--r--
3658
term_canonize.h
blob
|
history
|
raw
-rw-r--r--
3413
term_context.cpp
blob
|
history
|
raw
-rw-r--r--
6058
term_context.h
blob
|
history
|
raw
-rw-r--r--
2368
term_context_node.cpp
blob
|
history
|
raw
-rw-r--r--
2464
term_context_node.h
blob
|
history
|
raw
-rw-r--r--
2272
term_context_stack.cpp
blob
|
history
|
raw
-rw-r--r--
2152
term_context_stack.h
blob
|
history
|
raw
-rw-r--r--
18585
term_conversion_proof_generator.cpp
blob
|
history
|
raw
-rw-r--r--
10387
term_conversion_proof_generator.h
blob
|
history
|
raw
-rw-r--r--
17583
type.cpp
blob
|
history
|
raw
-rw-r--r--
17890
type.h
blob
|
history
|
raw
-rw-r--r--
1118
type_checker.h
blob
|
history
|
raw
-rw-r--r--
1939
type_checker_template.cpp
blob
|
history
|
raw
-rw-r--r--
5136
type_checker_util.h
blob
|
history
|
raw
-rw-r--r--
3180
type_matcher.cpp
blob
|
history
|
raw
-rw-r--r--
2323
type_matcher.h
blob
|
history
|
raw
-rw-r--r--
19299
type_node.cpp
blob
|
history
|
raw
-rw-r--r--
33007
type_node.h
blob
|
history
|
raw
-rw-r--r--
3653
type_properties_template.h
blob
|
history
|
raw
-rw-r--r--
3214
uninterpreted_constant.cpp
blob
|
history
|
raw
-rw-r--r--
1951
uninterpreted_constant.h
blob
|
history
|
raw
-rw-r--r--
1696
variable_type_map.h
blob
|
history
|
raw