projects
/
cvc5.git
/ tree
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
| tree
history
|
HEAD
Fix spurious antecedant for symbolic regular expressions (#6284)
[cvc5.git]
/
src
/
theory
/
drwxr-xr-x
..
-rw-r--r--
1589
CMakeLists.txt
blob
|
history
|
raw
drwxr-xr-x
-
arith
tree
|
history
drwxr-xr-x
-
arrays
tree
|
history
-rw-r--r--
786
assertion.cpp
blob
|
history
|
raw
-rw-r--r--
1541
assertion.h
blob
|
history
|
raw
-rw-r--r--
2597
atom_requests.cpp
blob
|
history
|
raw
-rw-r--r--
3145
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--
1653
care_graph.h
blob
|
history
|
raw
-rw-r--r--
3224
combination_care_graph.cpp
blob
|
history
|
raw
-rw-r--r--
1446
combination_care_graph.h
blob
|
history
|
raw
-rw-r--r--
3700
combination_engine.cpp
blob
|
history
|
raw
-rw-r--r--
4573
combination_engine.h
blob
|
history
|
raw
drwxr-xr-x
-
datatypes
tree
|
history
-rw-r--r--
3406
decision_manager.cpp
blob
|
history
|
raw
-rw-r--r--
5701
decision_manager.h
blob
|
history
|
raw
-rw-r--r--
3989
decision_strategy.cpp
blob
|
history
|
raw
-rw-r--r--
4906
decision_strategy.h
blob
|
history
|
raw
-rw-r--r--
4756
eager_proof_generator.cpp
blob
|
history
|
raw
-rw-r--r--
7453
eager_proof_generator.h
blob
|
history
|
raw
-rw-r--r--
1492
ee_manager.cpp
blob
|
history
|
raw
-rw-r--r--
3129
ee_manager.h
blob
|
history
|
raw
-rw-r--r--
3767
ee_manager_distributed.cpp
blob
|
history
|
raw
-rw-r--r--
3542
ee_manager_distributed.h
blob
|
history
|
raw
-rw-r--r--
1787
ee_setup_info.h
blob
|
history
|
raw
-rw-r--r--
6564
engine_output_channel.cpp
blob
|
history
|
raw
-rw-r--r--
3630
engine_output_channel.h
blob
|
history
|
raw
-rw-r--r--
29221
evaluator.cpp
blob
|
history
|
raw
-rw-r--r--
5574
evaluator.h
blob
|
history
|
raw
-rw-r--r--
15615
ext_theory.cpp
blob
|
history
|
raw
-rw-r--r--
11803
ext_theory.h
blob
|
history
|
raw
drwxr-xr-x
-
fp
tree
|
history
-rw-r--r--
20163
inference_id.cpp
blob
|
history
|
raw
-rw-r--r--
30180
inference_id.h
blob
|
history
|
raw
-rw-r--r--
5516
inference_manager_buffered.cpp
blob
|
history
|
raw
-rw-r--r--
6724
inference_manager_buffered.h
blob
|
history
|
raw
-rw-r--r--
1605
interrupted.h
blob
|
history
|
raw
-rw-r--r--
4035
lazy_tree_proof_generator.cpp
blob
|
history
|
raw
-rw-r--r--
7777
lazy_tree_proof_generator.h
blob
|
history
|
raw
-rw-r--r--
21129
logic_info.cpp
blob
|
history
|
raw
-rw-r--r--
9263
logic_info.h
blob
|
history
|
raw
-rwxr-xr-x
6208
mkrewriter
blob
|
history
|
raw
-rwxr-xr-x
10096
mktheorytraits
blob
|
history
|
raw
-rw-r--r--
7061
model_manager.cpp
blob
|
history
|
raw
-rw-r--r--
5805
model_manager.h
blob
|
history
|
raw
-rw-r--r--
3803
model_manager_distributed.cpp
blob
|
history
|
raw
-rw-r--r--
2119
model_manager_distributed.h
blob
|
history
|
raw
-rw-r--r--
2451
output_channel.cpp
blob
|
history
|
raw
-rw-r--r--
7065
output_channel.h
blob
|
history
|
raw
drwxr-xr-x
-
quantifiers
tree
|
history
-rw-r--r--
22753
quantifiers_engine.cpp
blob
|
history
|
raw
-rw-r--r--
7580
quantifiers_engine.h
blob
|
history
|
raw
-rw-r--r--
8266
relevance_manager.cpp
blob
|
history
|
raw
-rw-r--r--
6249
relevance_manager.h
blob
|
history
|
raw
-rw-r--r--
12453
rep_set.cpp
blob
|
history
|
raw
-rw-r--r--
11645
rep_set.h
blob
|
history
|
raw
-rw-r--r--
17903
rewriter.cpp
blob
|
history
|
raw
-rw-r--r--
7298
rewriter.h
blob
|
history
|
raw
-rw-r--r--
2600
rewriter_attributes.h
blob
|
history
|
raw
-rw-r--r--
2466
rewriter_tables_template.h
blob
|
history
|
raw
drwxr-xr-x
-
sep
tree
|
history
drwxr-xr-x
-
sets
tree
|
history
-rw-r--r--
4657
shared_solver.cpp
blob
|
history
|
raw
-rw-r--r--
4904
shared_solver.h
blob
|
history
|
raw
-rw-r--r--
2940
shared_solver_distributed.cpp
blob
|
history
|
raw
-rw-r--r--
2293
shared_solver_distributed.h
blob
|
history
|
raw
-rw-r--r--
10370
shared_terms_database.cpp
blob
|
history
|
raw
-rw-r--r--
8932
shared_terms_database.h
blob
|
history
|
raw
-rw-r--r--
1195
skolem_lemma.cpp
blob
|
history
|
raw
-rw-r--r--
1881
skolem_lemma.h
blob
|
history
|
raw
-rw-r--r--
3325
smt_engine_subsolver.cpp
blob
|
history
|
raw
-rw-r--r--
3491
smt_engine_subsolver.h
blob
|
history
|
raw
-rw-r--r--
31196
sort_inference.cpp
blob
|
history
|
raw
-rw-r--r--
6047
sort_inference.h
blob
|
history
|
raw
drwxr-xr-x
-
strings
tree
|
history
-rw-r--r--
13277
subs_minimize.cpp
blob
|
history
|
raw
-rw-r--r--
3464
subs_minimize.h
blob
|
history
|
raw
-rw-r--r--
7255
substitutions.cpp
blob
|
history
|
raw
-rw-r--r--
4958
substitutions.h
blob
|
history
|
raw
-rw-r--r--
10313
term_registration_visitor.cpp
blob
|
history
|
raw
-rw-r--r--
6134
term_registration_visitor.h
blob
|
history
|
raw
-rw-r--r--
16362
theory.cpp
blob
|
history
|
raw
-rw-r--r--
33283
theory.h
blob
|
history
|
raw
-rw-r--r--
67406
theory_engine.cpp
blob
|
history
|
raw
-rw-r--r--
21772
theory_engine.h
blob
|
history
|
raw
-rw-r--r--
3742
theory_engine_proof_generator.cpp
blob
|
history
|
raw
-rw-r--r--
2787
theory_engine_proof_generator.h
blob
|
history
|
raw
-rw-r--r--
2270
theory_eq_notify.h
blob
|
history
|
raw
-rw-r--r--
4301
theory_id.cpp
blob
|
history
|
raw
-rw-r--r--
3021
theory_id.h
blob
|
history
|
raw
-rw-r--r--
1717
theory_inference.cpp
blob
|
history
|
raw
-rw-r--r--
4016
theory_inference.h
blob
|
history
|
raw
-rw-r--r--
16685
theory_inference_manager.cpp
blob
|
history
|
raw
-rw-r--r--
19758
theory_inference_manager.h
blob
|
history
|
raw
-rw-r--r--
25432
theory_model.cpp
blob
|
history
|
raw
-rw-r--r--
19151
theory_model.h
blob
|
history
|
raw
-rw-r--r--
48121
theory_model_builder.cpp
blob
|
history
|
raw
-rw-r--r--
11829
theory_model_builder.h
blob
|
history
|
raw
-rw-r--r--
18477
theory_preprocessor.cpp
blob
|
history
|
raw
-rw-r--r--
8320
theory_preprocessor.h
blob
|
history
|
raw
-rw-r--r--
7190
theory_proof_step_buffer.cpp
blob
|
history
|
raw
-rw-r--r--
4716
theory_proof_step_buffer.h
blob
|
history
|
raw
-rw-r--r--
2088
theory_rewriter.cpp
blob
|
history
|
raw
-rw-r--r--
4181
theory_rewriter.h
blob
|
history
|
raw
-rw-r--r--
3903
theory_state.cpp
blob
|
history
|
raw
-rw-r--r--
4355
theory_state.h
blob
|
history
|
raw
-rw-r--r--
1331
theory_traits_template.h
blob
|
history
|
raw
-rw-r--r--
4142
trust_node.cpp
blob
|
history
|
raw
-rw-r--r--
5974
trust_node.h
blob
|
history
|
raw
-rw-r--r--
8375
trust_substitutions.cpp
blob
|
history
|
raw
-rw-r--r--
5015
trust_substitutions.h
blob
|
history
|
raw
-rw-r--r--
5507
type_enumerator.h
blob
|
history
|
raw
-rw-r--r--
1365
type_enumerator_template.cpp
blob
|
history
|
raw
-rw-r--r--
2948
type_set.cpp
blob
|
history
|
raw
-rw-r--r--
2795
type_set.h
blob
|
history
|
raw
drwxr-xr-x
-
uf
tree
|
history
-rw-r--r--
5926
valuation.cpp
blob
|
history
|
raw
-rw-r--r--
7440
valuation.h
blob
|
history
|
raw