projects
/
cvc5.git
/ tree
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
| tree
history
|
HEAD
Connect the relevance manager to TheoryEngine and use it in non-linear arithmetic...
[cvc5.git]
/
src
/
theory
/
arith
/
drwxr-xr-x
..
-rw-r--r--
92130
approx_simplex.cpp
blob
|
history
|
raw
-rw-r--r--
5053
approx_simplex.h
blob
|
history
|
raw
-rw-r--r--
12886
arith_ite_utils.cpp
blob
|
history
|
raw
-rw-r--r--
3227
arith_ite_utils.h
blob
|
history
|
raw
-rw-r--r--
7706
arith_msum.cpp
blob
|
history
|
raw
-rw-r--r--
6653
arith_msum.h
blob
|
history
|
raw
-rw-r--r--
26656
arith_rewriter.cpp
blob
|
history
|
raw
-rw-r--r--
2422
arith_rewriter.h
blob
|
history
|
raw
-rw-r--r--
1075
arith_state.cpp
blob
|
history
|
raw
-rw-r--r--
1597
arith_state.h
blob
|
history
|
raw
-rw-r--r--
8346
arith_static_learner.cpp
blob
|
history
|
raw
-rw-r--r--
2064
arith_static_learner.h
blob
|
history
|
raw
-rw-r--r--
6194
arith_utilities.cpp
blob
|
history
|
raw
-rw-r--r--
9969
arith_utilities.h
blob
|
history
|
raw
-rw-r--r--
1083
arithvar.cpp
blob
|
history
|
raw
-rw-r--r--
1313
arithvar.h
blob
|
history
|
raw
-rw-r--r--
2474
arithvar_node_map.h
blob
|
history
|
raw
-rw-r--r--
5262
attempt_solution_simplex.cpp
blob
|
history
|
raw
-rw-r--r--
3752
attempt_solution_simplex.h
blob
|
history
|
raw
-rw-r--r--
7926
bound_counts.h
blob
|
history
|
raw
-rw-r--r--
5267
callbacks.cpp
blob
|
history
|
raw
-rw-r--r--
4874
callbacks.h
blob
|
history
|
raw
-rw-r--r--
15077
congruence_manager.cpp
blob
|
history
|
raw
-rw-r--r--
5713
congruence_manager.h
blob
|
history
|
raw
-rw-r--r--
60916
constraint.cpp
blob
|
history
|
raw
-rw-r--r--
38243
constraint.h
blob
|
history
|
raw
-rw-r--r--
1657
constraint_forward.h
blob
|
history
|
raw
-rw-r--r--
16999
cut_log.cpp
blob
|
history
|
raw
-rw-r--r--
7119
cut_log.h
blob
|
history
|
raw
-rw-r--r--
3195
delta_rational.cpp
blob
|
history
|
raw
-rw-r--r--
7721
delta_rational.h
blob
|
history
|
raw
-rw-r--r--
25702
dio_solver.cpp
blob
|
history
|
raw
-rw-r--r--
12820
dio_solver.h
blob
|
history
|
raw
-rw-r--r--
9349
dual_simplex.cpp
blob
|
history
|
raw
-rw-r--r--
4279
dual_simplex.h
blob
|
history
|
raw
-rw-r--r--
13834
error_set.cpp
blob
|
history
|
raw
-rw-r--r--
10650
error_set.h
blob
|
history
|
raw
-rw-r--r--
27841
fc_simplex.cpp
blob
|
history
|
raw
-rw-r--r--
8825
fc_simplex.h
blob
|
history
|
raw
-rw-r--r--
6903
infer_bounds.cpp
blob
|
history
|
raw
-rw-r--r--
3956
infer_bounds.h
blob
|
history
|
raw
-rw-r--r--
6194
kinds
blob
|
history
|
raw
-rw-r--r--
46919
linear_equality.cpp
blob
|
history
|
raw
-rw-r--r--
23805
linear_equality.h
blob
|
history
|
raw
-rw-r--r--
1033
matrix.cpp
blob
|
history
|
raw
-rw-r--r--
25408
matrix.h
blob
|
history
|
raw
drwxr-xr-x
-
nl
tree
|
history
-rw-r--r--
36883
normal_form.cpp
blob
|
history
|
raw
-rw-r--r--
36884
normal_form.h
blob
|
history
|
raw
-rw-r--r--
16670
operator_elim.cpp
blob
|
history
|
raw
-rw-r--r--
4909
operator_elim.h
blob
|
history
|
raw
-rw-r--r--
18045
partial_model.cpp
blob
|
history
|
raw
-rw-r--r--
12158
partial_model.h
blob
|
history
|
raw
-rw-r--r--
8652
proof_checker.cpp
blob
|
history
|
raw
-rw-r--r--
1461
proof_checker.h
blob
|
history
|
raw
-rw-r--r--
9175
simplex.cpp
blob
|
history
|
raw
-rw-r--r--
7990
simplex.h
blob
|
history
|
raw
-rw-r--r--
5125
simplex_update.cpp
blob
|
history
|
raw
-rw-r--r--
10551
simplex_update.h
blob
|
history
|
raw
-rw-r--r--
34103
soi_simplex.cpp
blob
|
history
|
raw
-rw-r--r--
8707
soi_simplex.h
blob
|
history
|
raw
-rw-r--r--
5565
tableau.cpp
blob
|
history
|
raw
-rw-r--r--
4615
tableau.h
blob
|
history
|
raw
-rw-r--r--
1065
tableau_sizes.cpp
blob
|
history
|
raw
-rw-r--r--
1113
tableau_sizes.h
blob
|
history
|
raw
-rw-r--r--
4914
theory_arith.cpp
blob
|
history
|
raw
-rw-r--r--
3866
theory_arith.h
blob
|
history
|
raw
-rw-r--r--
194465
theory_arith_private.cpp
blob
|
history
|
raw
-rw-r--r--
27738
theory_arith_private.h
blob
|
history
|
raw
-rw-r--r--
858
theory_arith_private_forward.h
blob
|
history
|
raw
-rw-r--r--
4169
theory_arith_type_rules.h
blob
|
history
|
raw
-rw-r--r--
3031
type_enumerator.h
blob
|
history
|
raw