projects
/
cvc5.git
/ tree
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
| tree
history
|
HEAD
Fix issues related to eliminating extended arithmetic operators (#5475)
[cvc5.git]
/
src
/
theory
/
quantifiers
/
drwxr-xr-x
..
-rw-r--r--
4615
alpha_equivalence.cpp
blob
|
history
|
raw
-rw-r--r--
3767
alpha_equivalence.h
blob
|
history
|
raw
-rw-r--r--
11338
anti_skolem.cpp
blob
|
history
|
raw
-rw-r--r--
2713
anti_skolem.h
blob
|
history
|
raw
-rw-r--r--
13202
bv_inverter.cpp
blob
|
history
|
raw
-rw-r--r--
4055
bv_inverter.h
blob
|
history
|
raw
-rw-r--r--
75900
bv_inverter_utils.cpp
blob
|
history
|
raw
-rw-r--r--
2437
bv_inverter_utils.h
blob
|
history
|
raw
-rw-r--r--
9916
candidate_rewrite_database.cpp
blob
|
history
|
raw
-rw-r--r--
5351
candidate_rewrite_database.h
blob
|
history
|
raw
-rw-r--r--
8748
candidate_rewrite_filter.cpp
blob
|
history
|
raw
-rw-r--r--
6884
candidate_rewrite_filter.h
blob
|
history
|
raw
drwxr-xr-x
-
cegqi
tree
|
history
-rw-r--r--
87009
conjecture_generator.cpp
blob
|
history
|
raw
-rw-r--r--
16177
conjecture_generator.h
blob
|
history
|
raw
-rw-r--r--
4709
dynamic_rewrite.cpp
blob
|
history
|
raw
-rw-r--r--
4327
dynamic_rewrite.h
blob
|
history
|
raw
drwxr-xr-x
-
ematching
tree
|
history
-rw-r--r--
16875
equality_infer.cpp
blob
|
history
|
raw
-rw-r--r--
3536
equality_infer.h
blob
|
history
|
raw
-rw-r--r--
8177
equality_query.cpp
blob
|
history
|
raw
-rw-r--r--
4812
equality_query.h
blob
|
history
|
raw
-rw-r--r--
2858
expr_miner.cpp
blob
|
history
|
raw
-rw-r--r--
3221
expr_miner.h
blob
|
history
|
raw
-rw-r--r--
4552
expr_miner_manager.cpp
blob
|
history
|
raw
-rw-r--r--
4780
expr_miner_manager.h
blob
|
history
|
raw
-rw-r--r--
51036
extended_rewrite.cpp
blob
|
history
|
raw
-rw-r--r--
9749
extended_rewrite.h
blob
|
history
|
raw
-rw-r--r--
14458
first_order_model.cpp
blob
|
history
|
raw
-rw-r--r--
7641
first_order_model.h
blob
|
history
|
raw
drwxr-xr-x
-
fmf
tree
|
history
-rw-r--r--
9175
fun_def_evaluator.cpp
blob
|
history
|
raw
-rw-r--r--
2021
fun_def_evaluator.h
blob
|
history
|
raw
-rw-r--r--
2866
inst_match.cpp
blob
|
history
|
raw
-rw-r--r--
3114
inst_match.h
blob
|
history
|
raw
-rw-r--r--
13690
inst_match_trie.cpp
blob
|
history
|
raw
-rw-r--r--
15137
inst_match_trie.h
blob
|
history
|
raw
-rw-r--r--
10464
inst_strategy_enumerative.cpp
blob
|
history
|
raw
-rw-r--r--
4157
inst_strategy_enumerative.h
blob
|
history
|
raw
-rw-r--r--
27693
instantiate.cpp
blob
|
history
|
raw
-rw-r--r--
14663
instantiate.h
blob
|
history
|
raw
-rw-r--r--
2563
kinds
blob
|
history
|
raw
-rw-r--r--
4952
lazy_trie.cpp
blob
|
history
|
raw
-rw-r--r--
5651
lazy_trie.h
blob
|
history
|
raw
-rw-r--r--
3894
proof_checker.cpp
blob
|
history
|
raw
-rw-r--r--
1500
proof_checker.h
blob
|
history
|
raw
-rw-r--r--
84024
quant_conflict_find.cpp
blob
|
history
|
raw
-rw-r--r--
10835
quant_conflict_find.h
blob
|
history
|
raw
-rw-r--r--
5433
quant_epr.cpp
blob
|
history
|
raw
-rw-r--r--
3195
quant_epr.h
blob
|
history
|
raw
-rw-r--r--
1472
quant_relevance.cpp
blob
|
history
|
raw
-rw-r--r--
2114
quant_relevance.h
blob
|
history
|
raw
-rw-r--r--
2467
quant_rep_bound_ext.cpp
blob
|
history
|
raw
-rw-r--r--
2203
quant_rep_bound_ext.h
blob
|
history
|
raw
-rw-r--r--
6729
quant_split.cpp
blob
|
history
|
raw
-rw-r--r--
2540
quant_split.h
blob
|
history
|
raw
-rw-r--r--
5593
quant_util.cpp
blob
|
history
|
raw
-rw-r--r--
9194
quant_util.h
blob
|
history
|
raw
-rw-r--r--
11802
quantifiers_attributes.cpp
blob
|
history
|
raw
-rw-r--r--
8129
quantifiers_attributes.h
blob
|
history
|
raw
-rw-r--r--
3526
quantifiers_modules.cpp
blob
|
history
|
raw
-rw-r--r--
3476
quantifiers_modules.h
blob
|
history
|
raw
-rw-r--r--
69624
quantifiers_rewriter.cpp
blob
|
history
|
raw
-rw-r--r--
12679
quantifiers_rewriter.h
blob
|
history
|
raw
-rw-r--r--
940
quantifiers_state.cpp
blob
|
history
|
raw
-rw-r--r--
1119
quantifiers_state.h
blob
|
history
|
raw
-rw-r--r--
13015
query_generator.cpp
blob
|
history
|
raw
-rw-r--r--
4584
query_generator.h
blob
|
history
|
raw
-rw-r--r--
12158
relevant_domain.cpp
blob
|
history
|
raw
-rw-r--r--
5569
relevant_domain.h
blob
|
history
|
raw
-rw-r--r--
18622
single_inv_partition.cpp
blob
|
history
|
raw
-rw-r--r--
10835
single_inv_partition.h
blob
|
history
|
raw
-rw-r--r--
12853
skolemize.cpp
blob
|
history
|
raw
-rw-r--r--
5639
skolemize.h
blob
|
history
|
raw
-rw-r--r--
3342
solution_filter.cpp
blob
|
history
|
raw
-rw-r--r--
2540
solution_filter.h
blob
|
history
|
raw
drwxr-xr-x
-
sygus
tree
|
history
-rw-r--r--
16833
sygus_inst.cpp
blob
|
history
|
raw
-rw-r--r--
4780
sygus_inst.h
blob
|
history
|
raw
-rw-r--r--
23405
sygus_sampler.cpp
blob
|
history
|
raw
-rw-r--r--
13279
sygus_sampler.h
blob
|
history
|
raw
-rw-r--r--
38449
term_database.cpp
blob
|
history
|
raw
-rw-r--r--
17283
term_database.h
blob
|
history
|
raw
-rw-r--r--
2939
term_enumeration.cpp
blob
|
history
|
raw
-rw-r--r--
2744
term_enumeration.h
blob
|
history
|
raw
-rw-r--r--
18890
term_util.cpp
blob
|
history
|
raw
-rw-r--r--
10683
term_util.h
blob
|
history
|
raw
-rw-r--r--
5434
theory_quantifiers.cpp
blob
|
history
|
raw
-rw-r--r--
3181
theory_quantifiers.h
blob
|
history
|
raw
-rw-r--r--
5704
theory_quantifiers_type_rules.h
blob
|
history
|
raw