projects
/
cvc5.git
/ tree
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
| tree
history
|
HEAD
(proof-new) Make nl-ext factoring lemmas proof producing. (#5698)
[cvc5.git]
/
src
/
theory
/
arith
/
drwxr-xr-x
..
-rw-r--r--
92645
approx_simplex.cpp
blob
|
history
|
raw
-rw-r--r--
5052
approx_simplex.h
blob
|
history
|
raw
-rw-r--r--
12885
arith_ite_utils.cpp
blob
|
history
|
raw
-rw-r--r--
3226
arith_ite_utils.h
blob
|
history
|
raw
-rw-r--r--
814
arith_lemma.cpp
blob
|
history
|
raw
-rw-r--r--
1699
arith_lemma.h
blob
|
history
|
raw
-rw-r--r--
7705
arith_msum.cpp
blob
|
history
|
raw
-rw-r--r--
6652
arith_msum.h
blob
|
history
|
raw
-rw-r--r--
2054
arith_preprocess.cpp
blob
|
history
|
raw
-rw-r--r--
2990
arith_preprocess.h
blob
|
history
|
raw
-rw-r--r--
29176
arith_rewriter.cpp
blob
|
history
|
raw
-rw-r--r--
2613
arith_rewriter.h
blob
|
history
|
raw
-rw-r--r--
1076
arith_state.cpp
blob
|
history
|
raw
-rw-r--r--
1596
arith_state.h
blob
|
history
|
raw
-rw-r--r--
8322
arith_static_learner.cpp
blob
|
history
|
raw
-rw-r--r--
2063
arith_static_learner.h
blob
|
history
|
raw
-rw-r--r--
7103
arith_utilities.cpp
blob
|
history
|
raw
-rw-r--r--
10181
arith_utilities.h
blob
|
history
|
raw
-rw-r--r--
1082
arithvar.cpp
blob
|
history
|
raw
-rw-r--r--
1312
arithvar.h
blob
|
history
|
raw
-rw-r--r--
2473
arithvar_node_map.h
blob
|
history
|
raw
-rw-r--r--
5285
attempt_solution_simplex.cpp
blob
|
history
|
raw
-rw-r--r--
3751
attempt_solution_simplex.h
blob
|
history
|
raw
-rw-r--r--
7904
bound_counts.h
blob
|
history
|
raw
-rw-r--r--
7549
bound_inference.cpp
blob
|
history
|
raw
-rw-r--r--
3735
bound_inference.h
blob
|
history
|
raw
-rw-r--r--
5433
callbacks.cpp
blob
|
history
|
raw
-rw-r--r--
4967
callbacks.h
blob
|
history
|
raw
-rw-r--r--
23343
congruence_manager.cpp
blob
|
history
|
raw
-rw-r--r--
9378
congruence_manager.h
blob
|
history
|
raw
-rw-r--r--
73841
constraint.cpp
blob
|
history
|
raw
-rw-r--r--
40197
constraint.h
blob
|
history
|
raw
-rw-r--r--
1656
constraint_forward.h
blob
|
history
|
raw
-rw-r--r--
16998
cut_log.cpp
blob
|
history
|
raw
-rw-r--r--
7118
cut_log.h
blob
|
history
|
raw
-rw-r--r--
3194
delta_rational.cpp
blob
|
history
|
raw
-rw-r--r--
7720
delta_rational.h
blob
|
history
|
raw
-rw-r--r--
25717
dio_solver.cpp
blob
|
history
|
raw
-rw-r--r--
12819
dio_solver.h
blob
|
history
|
raw
-rw-r--r--
9465
dual_simplex.cpp
blob
|
history
|
raw
-rw-r--r--
4278
dual_simplex.h
blob
|
history
|
raw
-rw-r--r--
13833
error_set.cpp
blob
|
history
|
raw
-rw-r--r--
10649
error_set.h
blob
|
history
|
raw
-rw-r--r--
28049
fc_simplex.cpp
blob
|
history
|
raw
-rw-r--r--
8803
fc_simplex.h
blob
|
history
|
raw
-rw-r--r--
6919
infer_bounds.cpp
blob
|
history
|
raw
-rw-r--r--
3972
infer_bounds.h
blob
|
history
|
raw
-rw-r--r--
2456
inference_id.cpp
blob
|
history
|
raw
-rw-r--r--
3715
inference_id.h
blob
|
history
|
raw
-rw-r--r--
4607
inference_manager.cpp
blob
|
history
|
raw
-rw-r--r--
4279
inference_manager.h
blob
|
history
|
raw
-rw-r--r--
6879
kinds
blob
|
history
|
raw
-rw-r--r--
46901
linear_equality.cpp
blob
|
history
|
raw
-rw-r--r--
23804
linear_equality.h
blob
|
history
|
raw
-rw-r--r--
1032
matrix.cpp
blob
|
history
|
raw
-rw-r--r--
25407
matrix.h
blob
|
history
|
raw
drwxr-xr-x
-
nl
tree
|
history
-rw-r--r--
38466
normal_form.cpp
blob
|
history
|
raw
-rw-r--r--
37771
normal_form.h
blob
|
history
|
raw
-rw-r--r--
17248
operator_elim.cpp
blob
|
history
|
raw
-rw-r--r--
5000
operator_elim.h
blob
|
history
|
raw
-rw-r--r--
18044
partial_model.cpp
blob
|
history
|
raw
-rw-r--r--
12157
partial_model.h
blob
|
history
|
raw
-rw-r--r--
9224
proof_checker.cpp
blob
|
history
|
raw
-rw-r--r--
1460
proof_checker.h
blob
|
history
|
raw
-rw-r--r--
1315
proof_macros.h
blob
|
history
|
raw
-rw-r--r--
1548
rewrites.cpp
blob
|
history
|
raw
-rw-r--r--
2212
rewrites.h
blob
|
history
|
raw
-rw-r--r--
9174
simplex.cpp
blob
|
history
|
raw
-rw-r--r--
7989
simplex.h
blob
|
history
|
raw
-rw-r--r--
5124
simplex_update.cpp
blob
|
history
|
raw
-rw-r--r--
10550
simplex_update.h
blob
|
history
|
raw
-rw-r--r--
34253
soi_simplex.cpp
blob
|
history
|
raw
-rw-r--r--
8685
soi_simplex.h
blob
|
history
|
raw
-rw-r--r--
5564
tableau.cpp
blob
|
history
|
raw
-rw-r--r--
4614
tableau.h
blob
|
history
|
raw
-rw-r--r--
1064
tableau_sizes.cpp
blob
|
history
|
raw
-rw-r--r--
1092
tableau_sizes.h
blob
|
history
|
raw
-rw-r--r--
9872
theory_arith.cpp
blob
|
history
|
raw
-rw-r--r--
5353
theory_arith.h
blob
|
history
|
raw
-rw-r--r--
190719
theory_arith_private.cpp
blob
|
history
|
raw
-rw-r--r--
29345
theory_arith_private.h
blob
|
history
|
raw
-rw-r--r--
4201
theory_arith_type_rules.h
blob
|
history
|
raw
-rw-r--r--
3030
type_enumerator.h
blob
|
history
|
raw