projects
/
cvc5.git
/ tree
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
| tree
history
|
HEAD
Refactor rewriting of arithmetic negation and subtraction (#8170)
[cvc5.git]
/
src
/
theory
/
arith
/
drwxr-xr-x
..
-rw-r--r--
89173
approx_simplex.cpp
blob
|
history
|
raw
-rw-r--r--
5063
approx_simplex.h
blob
|
history
|
raw
-rw-r--r--
1276
arith_evaluator.cpp
blob
|
history
|
raw
-rw-r--r--
830
arith_evaluator.h
blob
|
history
|
raw
-rw-r--r--
13169
arith_ite_utils.cpp
blob
|
history
|
raw
-rw-r--r--
3169
arith_ite_utils.h
blob
|
history
|
raw
-rw-r--r--
7782
arith_msum.cpp
blob
|
history
|
raw
-rw-r--r--
6713
arith_msum.h
blob
|
history
|
raw
-rw-r--r--
6316
arith_poly_norm.cpp
blob
|
history
|
raw
-rw-r--r--
2577
arith_poly_norm.h
blob
|
history
|
raw
-rw-r--r--
2480
arith_preprocess.cpp
blob
|
history
|
raw
-rw-r--r--
3147
arith_preprocess.h
blob
|
history
|
raw
-rw-r--r--
37099
arith_rewriter.cpp
blob
|
history
|
raw
-rw-r--r--
3174
arith_rewriter.h
blob
|
history
|
raw
-rw-r--r--
1029
arith_state.cpp
blob
|
history
|
raw
-rw-r--r--
1585
arith_state.h
blob
|
history
|
raw
-rw-r--r--
8029
arith_static_learner.cpp
blob
|
history
|
raw
-rw-r--r--
2039
arith_static_learner.h
blob
|
history
|
raw
-rw-r--r--
7313
arith_utilities.cpp
blob
|
history
|
raw
-rw-r--r--
9894
arith_utilities.h
blob
|
history
|
raw
-rw-r--r--
1074
arithvar.cpp
blob
|
history
|
raw
-rw-r--r--
1307
arithvar.h
blob
|
history
|
raw
-rw-r--r--
2458
arithvar_node_map.h
blob
|
history
|
raw
-rw-r--r--
5118
attempt_solution_simplex.cpp
blob
|
history
|
raw
-rw-r--r--
3764
attempt_solution_simplex.h
blob
|
history
|
raw
-rw-r--r--
7895
bound_counts.h
blob
|
history
|
raw
-rw-r--r--
7375
bound_inference.cpp
blob
|
history
|
raw
-rw-r--r--
3738
bound_inference.h
blob
|
history
|
raw
-rw-r--r--
5120
branch_and_bound.cpp
blob
|
history
|
raw
-rw-r--r--
2221
branch_and_bound.h
blob
|
history
|
raw
-rw-r--r--
5719
callbacks.cpp
blob
|
history
|
raw
-rw-r--r--
5043
callbacks.h
blob
|
history
|
raw
-rw-r--r--
23989
congruence_manager.cpp
blob
|
history
|
raw
-rw-r--r--
9320
congruence_manager.h
blob
|
history
|
raw
-rw-r--r--
75360
constraint.cpp
blob
|
history
|
raw
-rw-r--r--
39720
constraint.h
blob
|
history
|
raw
-rw-r--r--
1667
constraint_forward.h
blob
|
history
|
raw
-rw-r--r--
17029
cut_log.cpp
blob
|
history
|
raw
-rw-r--r--
7047
cut_log.h
blob
|
history
|
raw
-rw-r--r--
3222
delta_rational.cpp
blob
|
history
|
raw
-rw-r--r--
7743
delta_rational.h
blob
|
history
|
raw
-rw-r--r--
25539
dio_solver.cpp
blob
|
history
|
raw
-rw-r--r--
12675
dio_solver.h
blob
|
history
|
raw
-rw-r--r--
8211
dual_simplex.cpp
blob
|
history
|
raw
-rw-r--r--
4348
dual_simplex.h
blob
|
history
|
raw
-rw-r--r--
3958
equality_solver.cpp
blob
|
history
|
raw
-rw-r--r--
3524
equality_solver.h
blob
|
history
|
raw
-rw-r--r--
13452
error_set.cpp
blob
|
history
|
raw
-rw-r--r--
10659
error_set.h
blob
|
history
|
raw
-rw-r--r--
25638
fc_simplex.cpp
blob
|
history
|
raw
-rw-r--r--
8765
fc_simplex.h
blob
|
history
|
raw
-rw-r--r--
6954
infer_bounds.cpp
blob
|
history
|
raw
-rw-r--r--
3985
infer_bounds.h
blob
|
history
|
raw
-rw-r--r--
4795
inference_manager.cpp
blob
|
history
|
raw
-rw-r--r--
4444
inference_manager.h
blob
|
history
|
raw
-rw-r--r--
8574
kinds
blob
|
history
|
raw
-rw-r--r--
45311
linear_equality.cpp
blob
|
history
|
raw
-rw-r--r--
23715
linear_equality.h
blob
|
history
|
raw
-rw-r--r--
964
matrix.cpp
blob
|
history
|
raw
-rw-r--r--
25398
matrix.h
blob
|
history
|
raw
drwxr-xr-x
-
nl
tree
|
history
-rw-r--r--
38609
normal_form.cpp
blob
|
history
|
raw
-rw-r--r--
39012
normal_form.h
blob
|
history
|
raw
-rw-r--r--
13390
operator_elim.cpp
blob
|
history
|
raw
-rw-r--r--
5166
operator_elim.h
blob
|
history
|
raw
-rw-r--r--
18032
partial_model.cpp
blob
|
history
|
raw
-rw-r--r--
12137
partial_model.h
blob
|
history
|
raw
-rw-r--r--
1955
pp_rewrite_eq.cpp
blob
|
history
|
raw
-rw-r--r--
1560
pp_rewrite_eq.h
blob
|
history
|
raw
-rw-r--r--
12055
proof_checker.cpp
blob
|
history
|
raw
-rw-r--r--
1449
proof_checker.h
blob
|
history
|
raw
drwxr-xr-x
-
rewriter
tree
|
history
-rw-r--r--
1728
rewrites.cpp
blob
|
history
|
raw
-rw-r--r--
2454
rewrites.h
blob
|
history
|
raw
-rw-r--r--
9542
simplex.cpp
blob
|
history
|
raw
-rw-r--r--
8366
simplex.h
blob
|
history
|
raw
-rw-r--r--
5557
simplex_update.cpp
blob
|
history
|
raw
-rw-r--r--
10522
simplex_update.h
blob
|
history
|
raw
-rw-r--r--
30752
soi_simplex.cpp
blob
|
history
|
raw
-rw-r--r--
8203
soi_simplex.h
blob
|
history
|
raw
-rw-r--r--
5558
tableau.cpp
blob
|
history
|
raw
-rw-r--r--
4618
tableau.h
blob
|
history
|
raw
-rw-r--r--
1052
tableau_sizes.cpp
blob
|
history
|
raw
-rw-r--r--
1080
tableau_sizes.h
blob
|
history
|
raw
-rw-r--r--
13277
theory_arith.cpp
blob
|
history
|
raw
-rw-r--r--
6666
theory_arith.h
blob
|
history
|
raw
-rw-r--r--
165875
theory_arith_private.cpp
blob
|
history
|
raw
-rw-r--r--
29239
theory_arith_private.h
blob
|
history
|
raw
-rw-r--r--
6264
theory_arith_type_rules.cpp
blob
|
history
|
raw
-rw-r--r--
3191
theory_arith_type_rules.h
blob
|
history
|
raw
-rw-r--r--
3071
type_enumerator.h
blob
|
history
|
raw