projects
/
cvc5.git
/ tree
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
| tree
history
|
HEAD
bv-to-int: avoid binarizing nodes twice (#5749)
[cvc5.git]
/
src
/
preprocessing
/
passes
/
drwxr-xr-x
..
-rw-r--r--
11163
ackermann.cpp
blob
|
history
|
raw
-rw-r--r--
3202
ackermann.h
blob
|
history
|
raw
-rw-r--r--
2207
apply_substs.cpp
blob
|
history
|
raw
-rw-r--r--
1464
apply_substs.h
blob
|
history
|
raw
-rw-r--r--
12310
bool_to_bv.cpp
blob
|
history
|
raw
-rw-r--r--
4155
bool_to_bv.h
blob
|
history
|
raw
-rw-r--r--
2408
bv_abstraction.cpp
blob
|
history
|
raw
-rw-r--r--
1678
bv_abstraction.h
blob
|
history
|
raw
-rw-r--r--
1636
bv_eager_atoms.cpp
blob
|
history
|
raw
-rw-r--r--
1376
bv_eager_atoms.h
blob
|
history
|
raw
-rw-r--r--
22680
bv_gauss.cpp
blob
|
history
|
raw
-rw-r--r--
3377
bv_gauss.h
blob
|
history
|
raw
-rw-r--r--
2929
bv_intro_pow2.cpp
blob
|
history
|
raw
-rw-r--r--
1420
bv_intro_pow2.h
blob
|
history
|
raw
-rw-r--r--
9055
bv_to_bool.cpp
blob
|
history
|
raw
-rw-r--r--
2313
bv_to_bool.h
blob
|
history
|
raw
-rw-r--r--
36646
bv_to_int.cpp
blob
|
history
|
raw
-rw-r--r--
10349
bv_to_int.h
blob
|
history
|
raw
-rw-r--r--
1390
extended_rewriter_pass.cpp
blob
|
history
|
raw
-rw-r--r--
1314
extended_rewriter_pass.h
blob
|
history
|
raw
-rw-r--r--
1550
foreign_theory_rewrite.cpp
blob
|
history
|
raw
-rw-r--r--
1629
foreign_theory_rewrite.h
blob
|
history
|
raw
-rw-r--r--
15232
fun_def_fmf.cpp
blob
|
history
|
raw
-rw-r--r--
3820
fun_def_fmf.h
blob
|
history
|
raw
-rw-r--r--
3251
global_negate.cpp
blob
|
history
|
raw
-rw-r--r--
1701
global_negate.h
blob
|
history
|
raw
-rw-r--r--
17229
ho_elim.cpp
blob
|
history
|
raw
-rw-r--r--
5842
ho_elim.h
blob
|
history
|
raw
-rw-r--r--
7863
int_to_bv.cpp
blob
|
history
|
raw
-rw-r--r--
1370
int_to_bv.h
blob
|
history
|
raw
-rw-r--r--
2772
ite_removal.cpp
blob
|
history
|
raw
-rw-r--r--
1316
ite_removal.h
blob
|
history
|
raw
-rw-r--r--
8786
ite_simp.cpp
blob
|
history
|
raw
-rw-r--r--
1461
ite_simp.h
blob
|
history
|
raw
-rw-r--r--
21996
miplib_trick.cpp
blob
|
history
|
raw
-rw-r--r--
1752
miplib_trick.h
blob
|
history
|
raw
-rw-r--r--
3789
nl_ext_purify.cpp
blob
|
history
|
raw
-rw-r--r--
1675
nl_ext_purify.h
blob
|
history
|
raw
-rw-r--r--
17339
non_clausal_simp.cpp
blob
|
history
|
raw
-rw-r--r--
3136
non_clausal_simp.h
blob
|
history
|
raw
-rw-r--r--
10278
pseudo_boolean_processor.cpp
blob
|
history
|
raw
-rw-r--r--
3368
pseudo_boolean_processor.h
blob
|
history
|
raw
-rw-r--r--
20381
quantifier_macros.cpp
blob
|
history
|
raw
-rw-r--r--
3556
quantifier_macros.h
blob
|
history
|
raw
-rw-r--r--
1933
quantifiers_preprocess.cpp
blob
|
history
|
raw
-rw-r--r--
1456
quantifiers_preprocess.h
blob
|
history
|
raw
-rw-r--r--
7088
real_to_int.cpp
blob
|
history
|
raw
-rw-r--r--
1498
real_to_int.h
blob
|
history
|
raw
-rw-r--r--
1256
rewrite.cpp
blob
|
history
|
raw
-rw-r--r--
1243
rewrite.h
blob
|
history
|
raw
-rw-r--r--
3678
sep_skolem_emp.cpp
blob
|
history
|
raw
-rw-r--r--
1243
sep_skolem_emp.h
blob
|
history
|
raw
-rw-r--r--
2933
sort_infer.cpp
blob
|
history
|
raw
-rw-r--r--
1500
sort_infer.h
blob
|
history
|
raw
-rw-r--r--
1585
static_learning.cpp
blob
|
history
|
raw
-rw-r--r--
1250
static_learning.h
blob
|
history
|
raw
-rw-r--r--
10643
sygus_inference.cpp
blob
|
history
|
raw
-rw-r--r--
2519
sygus_inference.h
blob
|
history
|
raw
-rw-r--r--
17493
synth_rew_rules.cpp
blob
|
history
|
raw
-rw-r--r--
3210
synth_rew_rules.h
blob
|
history
|
raw
-rw-r--r--
2562
theory_preprocess.cpp
blob
|
history
|
raw
-rw-r--r--
1320
theory_preprocess.h
blob
|
history
|
raw
-rw-r--r--
3345
theory_rewrite_eq.cpp
blob
|
history
|
raw
-rw-r--r--
1906
theory_rewrite_eq.h
blob
|
history
|
raw
-rw-r--r--
27272
unconstrained_simplifier.cpp
blob
|
history
|
raw
-rw-r--r--
2491
unconstrained_simplifier.h
blob
|
history
|
raw