projects
/
cvc5.git
/ tree
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
| tree
history
|
HEAD
Reimplement support for relational triggers (#7063)
[cvc5.git]
/
src
/
theory
/
quantifiers
/
drwxr-xr-x
..
-rw-r--r--
7264
alpha_equivalence.cpp
blob
|
history
|
raw
-rw-r--r--
4624
alpha_equivalence.h
blob
|
history
|
raw
-rw-r--r--
13343
bv_inverter.cpp
blob
|
history
|
raw
-rw-r--r--
4055
bv_inverter.h
blob
|
history
|
raw
-rw-r--r--
75836
bv_inverter_utils.cpp
blob
|
history
|
raw
-rw-r--r--
2450
bv_inverter_utils.h
blob
|
history
|
raw
-rw-r--r--
9929
candidate_rewrite_database.cpp
blob
|
history
|
raw
-rw-r--r--
5406
candidate_rewrite_database.h
blob
|
history
|
raw
-rw-r--r--
8751
candidate_rewrite_filter.cpp
blob
|
history
|
raw
-rw-r--r--
6912
candidate_rewrite_filter.h
blob
|
history
|
raw
drwxr-xr-x
-
cegqi
tree
|
history
-rw-r--r--
87366
conjecture_generator.cpp
blob
|
history
|
raw
-rw-r--r--
16438
conjecture_generator.h
blob
|
history
|
raw
-rw-r--r--
4870
dynamic_rewrite.cpp
blob
|
history
|
raw
-rw-r--r--
4334
dynamic_rewrite.h
blob
|
history
|
raw
drwxr-xr-x
-
ematching
tree
|
history
-rw-r--r--
12351
entailment_check.cpp
blob
|
history
|
raw
-rw-r--r--
5654
entailment_check.h
blob
|
history
|
raw
-rw-r--r--
5878
equality_query.cpp
blob
|
history
|
raw
-rw-r--r--
3586
equality_query.h
blob
|
history
|
raw
-rw-r--r--
2660
expr_miner.cpp
blob
|
history
|
raw
-rw-r--r--
3424
expr_miner.h
blob
|
history
|
raw
-rw-r--r--
4584
expr_miner_manager.cpp
blob
|
history
|
raw
-rw-r--r--
4617
expr_miner_manager.h
blob
|
history
|
raw
-rw-r--r--
50046
extended_rewrite.cpp
blob
|
history
|
raw
-rw-r--r--
10093
extended_rewrite.h
blob
|
history
|
raw
-rw-r--r--
11990
first_order_model.cpp
blob
|
history
|
raw
-rw-r--r--
8365
first_order_model.h
blob
|
history
|
raw
drwxr-xr-x
-
fmf
tree
|
history
-rw-r--r--
9505
fun_def_evaluator.cpp
blob
|
history
|
raw
-rw-r--r--
2329
fun_def_evaluator.h
blob
|
history
|
raw
-rw-r--r--
7438
ho_term_database.cpp
blob
|
history
|
raw
-rw-r--r--
4644
ho_term_database.h
blob
|
history
|
raw
-rw-r--r--
3288
index_trie.cpp
blob
|
history
|
raw
-rw-r--r--
4179
index_trie.h
blob
|
history
|
raw
-rw-r--r--
2267
inst_match.cpp
blob
|
history
|
raw
-rw-r--r--
2818
inst_match.h
blob
|
history
|
raw
-rw-r--r--
10110
inst_match_trie.cpp
blob
|
history
|
raw
-rw-r--r--
8139
inst_match_trie.h
blob
|
history
|
raw
-rw-r--r--
7044
inst_strategy_enumerative.cpp
blob
|
history
|
raw
-rw-r--r--
4273
inst_strategy_enumerative.h
blob
|
history
|
raw
-rw-r--r--
4725
inst_strategy_pool.cpp
blob
|
history
|
raw
-rw-r--r--
2490
inst_strategy_pool.h
blob
|
history
|
raw
-rw-r--r--
24204
instantiate.cpp
blob
|
history
|
raw
-rw-r--r--
13935
instantiate.h
blob
|
history
|
raw
-rw-r--r--
1317
instantiation_list.cpp
blob
|
history
|
raw
-rw-r--r--
2045
instantiation_list.h
blob
|
history
|
raw
-rw-r--r--
2779
kinds
blob
|
history
|
raw
-rw-r--r--
4945
lazy_trie.cpp
blob
|
history
|
raw
-rw-r--r--
5646
lazy_trie.h
blob
|
history
|
raw
-rw-r--r--
987
master_eq_notify.cpp
blob
|
history
|
raw
-rw-r--r--
1926
master_eq_notify.h
blob
|
history
|
raw
-rw-r--r--
4942
proof_checker.cpp
blob
|
history
|
raw
-rw-r--r--
1519
proof_checker.h
blob
|
history
|
raw
-rw-r--r--
3474
quant_bound_inference.cpp
blob
|
history
|
raw
-rw-r--r--
4212
quant_bound_inference.h
blob
|
history
|
raw
-rw-r--r--
84321
quant_conflict_find.cpp
blob
|
history
|
raw
-rw-r--r--
11068
quant_conflict_find.h
blob
|
history
|
raw
-rw-r--r--
2035
quant_module.cpp
blob
|
history
|
raw
-rw-r--r--
6502
quant_module.h
blob
|
history
|
raw
-rw-r--r--
1759
quant_relevance.cpp
blob
|
history
|
raw
-rw-r--r--
2069
quant_relevance.h
blob
|
history
|
raw
-rw-r--r--
2579
quant_rep_bound_ext.cpp
blob
|
history
|
raw
-rw-r--r--
2298
quant_rep_bound_ext.h
blob
|
history
|
raw
-rw-r--r--
7316
quant_split.cpp
blob
|
history
|
raw
-rw-r--r--
2704
quant_split.h
blob
|
history
|
raw
-rw-r--r--
4577
quant_util.cpp
blob
|
history
|
raw
-rw-r--r--
4116
quant_util.h
blob
|
history
|
raw
-rw-r--r--
13896
quantifiers_attributes.cpp
blob
|
history
|
raw
-rw-r--r--
7648
quantifiers_attributes.h
blob
|
history
|
raw
-rw-r--r--
1612
quantifiers_inference_manager.cpp
blob
|
history
|
raw
-rw-r--r--
1988
quantifiers_inference_manager.h
blob
|
history
|
raw
-rw-r--r--
8243
quantifiers_macros.cpp
blob
|
history
|
raw
-rw-r--r--
3387
quantifiers_macros.h
blob
|
history
|
raw
-rw-r--r--
4024
quantifiers_modules.cpp
blob
|
history
|
raw
-rw-r--r--
3614
quantifiers_modules.h
blob
|
history
|
raw
-rw-r--r--
8156
quantifiers_preprocess.cpp
blob
|
history
|
raw
-rw-r--r--
2624
quantifiers_preprocess.h
blob
|
history
|
raw
-rw-r--r--
6218
quantifiers_registry.cpp
blob
|
history
|
raw
-rw-r--r--
5426
quantifiers_registry.h
blob
|
history
|
raw
-rw-r--r--
65469
quantifiers_rewriter.cpp
blob
|
history
|
raw
-rw-r--r--
12690
quantifiers_rewriter.h
blob
|
history
|
raw
-rw-r--r--
5068
quantifiers_state.cpp
blob
|
history
|
raw
-rw-r--r--
3105
quantifiers_state.h
blob
|
history
|
raw
-rw-r--r--
2020
quantifiers_statistics.cpp
blob
|
history
|
raw
-rw-r--r--
1462
quantifiers_statistics.h
blob
|
history
|
raw
-rw-r--r--
12966
query_generator.cpp
blob
|
history
|
raw
-rw-r--r--
4587
query_generator.h
blob
|
history
|
raw
-rw-r--r--
13628
relevant_domain.cpp
blob
|
history
|
raw
-rw-r--r--
5688
relevant_domain.h
blob
|
history
|
raw
-rw-r--r--
18567
single_inv_partition.cpp
blob
|
history
|
raw
-rw-r--r--
10760
single_inv_partition.h
blob
|
history
|
raw
-rw-r--r--
12593
skolemize.cpp
blob
|
history
|
raw
-rw-r--r--
5865
skolemize.h
blob
|
history
|
raw
-rw-r--r--
3378
solution_filter.cpp
blob
|
history
|
raw
-rw-r--r--
2562
solution_filter.h
blob
|
history
|
raw
drwxr-xr-x
-
sygus
tree
|
history
-rw-r--r--
17261
sygus_inst.cpp
blob
|
history
|
raw
-rw-r--r--
4753
sygus_inst.h
blob
|
history
|
raw
-rw-r--r--
23052
sygus_sampler.cpp
blob
|
history
|
raw
-rw-r--r--
13429
sygus_sampler.h
blob
|
history
|
raw
-rw-r--r--
19936
term_database.cpp
blob
|
history
|
raw
-rw-r--r--
11826
term_database.h
blob
|
history
|
raw
-rw-r--r--
2020
term_enumeration.cpp
blob
|
history
|
raw
-rw-r--r--
2323
term_enumeration.h
blob
|
history
|
raw
-rw-r--r--
4177
term_pools.cpp
blob
|
history
|
raw
-rw-r--r--
3316
term_pools.h
blob
|
history
|
raw
-rw-r--r--
4464
term_registry.cpp
blob
|
history
|
raw
-rw-r--r--
3848
term_registry.h
blob
|
history
|
raw
-rw-r--r--
18625
term_tuple_enumerator.cpp
blob
|
history
|
raw
-rw-r--r--
3972
term_tuple_enumerator.h
blob
|
history
|
raw
-rw-r--r--
14558
term_util.cpp
blob
|
history
|
raw
-rw-r--r--
7154
term_util.h
blob
|
history
|
raw
-rw-r--r--
5548
theory_quantifiers.cpp
blob
|
history
|
raw
-rw-r--r--
3753
theory_quantifiers.h
blob
|
history
|
raw
-rw-r--r--
4694
theory_quantifiers_type_rules.cpp
blob
|
history
|
raw
-rw-r--r--
1602
theory_quantifiers_type_rules.h
blob
|
history
|
raw