projects
/
cvc5.git
/ tree
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
| tree
history
|
HEAD
(proof-new) New proofs in arith::Constraint::externalExplain (#5176)
[cvc5.git]
/
src
/
theory
/
arith
/
drwxr-xr-x
..
-rw-r--r--
92129
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--
26655
arith_rewriter.cpp
blob
|
history
|
raw
-rw-r--r--
2421
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--
8345
arith_static_learner.cpp
blob
|
history
|
raw
-rw-r--r--
2063
arith_static_learner.h
blob
|
history
|
raw
-rw-r--r--
6878
arith_utilities.cpp
blob
|
history
|
raw
-rw-r--r--
10154
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--
5261
attempt_solution_simplex.cpp
blob
|
history
|
raw
-rw-r--r--
3751
attempt_solution_simplex.h
blob
|
history
|
raw
-rw-r--r--
7925
bound_counts.h
blob
|
history
|
raw
-rw-r--r--
4582
bound_inference.cpp
blob
|
history
|
raw
-rw-r--r--
2825
bound_inference.h
blob
|
history
|
raw
-rw-r--r--
5393
callbacks.cpp
blob
|
history
|
raw
-rw-r--r--
4873
callbacks.h
blob
|
history
|
raw
-rw-r--r--
16350
congruence_manager.cpp
blob
|
history
|
raw
-rw-r--r--
7695
congruence_manager.h
blob
|
history
|
raw
-rw-r--r--
66714
constraint.cpp
blob
|
history
|
raw
-rw-r--r--
38719
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--
25701
dio_solver.cpp
blob
|
history
|
raw
-rw-r--r--
12819
dio_solver.h
blob
|
history
|
raw
-rw-r--r--
9348
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--
27840
fc_simplex.cpp
blob
|
history
|
raw
-rw-r--r--
8824
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--
2170
inference_id.cpp
blob
|
history
|
raw
-rw-r--r--
3549
inference_id.h
blob
|
history
|
raw
-rw-r--r--
4708
inference_manager.cpp
blob
|
history
|
raw
-rw-r--r--
4289
inference_manager.h
blob
|
history
|
raw
-rw-r--r--
6194
kinds
blob
|
history
|
raw
-rw-r--r--
46893
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--
37773
normal_form.h
blob
|
history
|
raw
-rw-r--r--
16675
operator_elim.cpp
blob
|
history
|
raw
-rw-r--r--
4938
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--
8651
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--
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--
34102
soi_simplex.cpp
blob
|
history
|
raw
-rw-r--r--
8706
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--
1112
tableau_sizes.h
blob
|
history
|
raw
-rw-r--r--
7741
theory_arith.cpp
blob
|
history
|
raw
-rw-r--r--
4608
theory_arith.h
blob
|
history
|
raw
-rw-r--r--
188919
theory_arith_private.cpp
blob
|
history
|
raw
-rw-r--r--
29422
theory_arith_private.h
blob
|
history
|
raw
-rw-r--r--
857
theory_arith_private_forward.h
blob
|
history
|
raw
-rw-r--r--
4175
theory_arith_type_rules.h
blob
|
history
|
raw
-rw-r--r--
3030
type_enumerator.h
blob
|
history
|
raw