-
Notifications
You must be signed in to change notification settings - Fork 76
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Sparsification of Affine Equality Matrix #1625
Draft
GollokG
wants to merge
176
commits into
goblint:master
Choose a base branch
from
CopperCableIsolator:master
base: master
Could not load branches
Branch not found: {{ refName }}
Loading
Could not load tags
Nothing to show
Loading
Are you sure you want to change the base?
Some commits from the old base branch may be removed from the timeline,
and old review comments may become outdated.
Draft
Changes from 1 commit
Commits
Show all changes
176 commits
Select commit
Hold shift + click to select a range
cb0eec6
Created SparseMatrix module
GollokG 5ba152c
Merge pull request #1 from CopperCableIsolator/affeq-sparsification
GollokG f931125
Merge remote-tracking branch 'upstream/master'
GollokG 69cc72f
changed type to lists
1b5f531
SparseMatrix list and get_col
GollokG b1c877a
Implement del_col and del_cols for SparseMatrix
GollokG bfbd373
added row functions and conversions between vectors and sparse lists
d0124f9
add_empty_columns untested
CopperCableIsolator dbc0fdc
merge
CopperCableIsolator d789459
Implement set_col for SparseMatrix
GollokG 8c23838
Add functions without side effects to ArrayVector and Vector interface
GollokG fd73a7c
Removed some _with functions from the AffineEqualityDomain
feniup 11e7dcd
sparseVector stumb
CopperCableIsolator d3b4072
Extracted operations
feniup 7141f97
Implement normalize SparseMatrix
GollokG 7c2cb08
sparseVector stumb
CopperCableIsolator 37d1bc0
Removed some _with functions from the AffineEqualityDomain
feniup 3e159ad
Some Vector Functions
CopperCableIsolator 9acc346
Implement some more SparseMatrix functions
GollokG 128d368
added rref_vec und rref_matrix ohne _with
89588ab
added new interface functions to sparsematrix
d3477c0
implemented reduce_col and remove_zero_rows and fixed some bugs
5a28e34
matrix_normalize_stub
CopperCableIsolator 090b31f
Merge branch 'master' of https://github.com/CopperCableIsolator/gobli…
CopperCableIsolator daec67b
Merge branch 'master' of https://github.com/CopperCableIsolator/gobli…
225c730
sexier sub function
CopperCableIsolator 420bde8
toMatrix vec funcs
CopperCableIsolator 4dbc81f
toVector
CopperCableIsolator af2fc0f
Change of_sparse_list param order and continued normalize function
GollokG acf5851
Split up vectorMatrix into multiple files; Removed VectorMatrix from …
feniup 32c378d
Merge remote-tracking branch 'origin/master' into file-splitting
feniup 5ce5ee8
Bugfix Matrix.map2i without side effects (different length lists)
GollokG 63506ea
Merge remote-tracking branch 'origin/master' into file-splitting
feniup 7643899
added missing module BatList
feniup 41bb6ed
RenamedFolder; Revealed modules to goblint_lib
feniup 6602d75
Directly revealed modules to goblint_lib
feniup b7d5c1a
Added missing ArrayVector module to goblint_lib
feniup b1beb54
Merge pull request #2 from CopperCableIsolator/file-splitting
feniup 8476f95
Vector List
CopperCableIsolator 5fb8041
someMatFuncs
CopperCableIsolator 8c3824f
some functions changed to use vectors
3234896
again
fb3442b
Merge branch 'master' of https://github.com/CopperCableIsolator/gobli…
251f1c9
Reimplemented some matrix functions to vector
GollokG 67c9ef4
Added find_opt and remove_nth to vector interface
GollokG 19ac2db
pushing is_zero_vec
47f4fa1
Merge branch 'master' of https://github.com/CopperCableIsolator/gobli…
a0e0f1b
Formatting
GollokG d768b46
vector functions
74ce9fe
Merge branch 'master' of https://github.com/CopperCableIsolator/gobli…
422dd54
Removed some _with functions from the AffineEqualityDomain
feniup 6afcb81
Implement inefficient rref functions
GollokG e7aa151
Merge branch 'master' into affine-equality-domain-without-with
feniup 7b4173a
ocp-indent on sparseMatrix.ml
feniup c8db710
del_cols and remove_at_indices
24fd057
commiting again for indentation
0e702ee
Merge branch 'master' of https://github.com/CopperCableIsolator/gobli…
0c9eb46
Vector functions
GollokG 0db8b61
some vector functions
f413d51
Merge branch 'master' into affine-equality-domain-without-with
GollokG d439b20
vector conversion to array
03fab15
Explicit types on normalize
GollokG f018a06
map2_preserve_zero
CopperCableIsolator 70dbf4d
exists, vector interface
CopperCableIsolator 215b25e
ups
CopperCableIsolator fd16be1
Merge branch 'master' of https://github.com/CopperCableIsolator/gobli…
680e56b
Reimplemented normalize in SparseMatrix, some TODOs missing
GollokG 40996b7
Renamed sparseMatrix.ml to match module name
feniup cb62292
Merge branch 'master' of github.com:CopperCableIsolator/goblint-spars…
feniup 702f258
builds now + reduce_col
e556c41
Merge branch 'master' of https://github.com/CopperCableIsolator/gobli…
bec7535
Moved swap, div, sub and normalize to new listMatrix.ml
GollokG ad34bc7
Renamed tV according to best practices
feniup bd81ac1
Implement vector findi and minor bugfix in ListMatrix normalize
GollokG 06a32ea
vectorfuncs, foldleftpreservezero
CopperCableIsolator 05a3dc5
Add normalize check for invalid affeq matrix
GollokG 409c01d
Vector function findi_val_opt
GollokG ad9f618
Adapting normalize and reordering deprecated functions in ListMatrix.ml
GollokG 33b8723
Implement Vector foldleft and apply_with_c
GollokG 785f75d
add column and helper functions
fe9513a
Fix del_cols duplicate edge case chech before comparing length
GollokG 7a8fab9
Fix set_nth in Vector
GollokG 519ee02
Remove double Mpqf definition
GollokG d3d998d
Renamed SparseMatrix to ListMatrix in goblint_lib.ml
feniup b339b78
Merge branch 'master' of github.com:CopperCableIsolator/goblint-spars…
feniup d68c719
Implement is_covered_by structure, but helper function still missing
GollokG 159d07e
bugfix in insert_at and reduce_col_with_vec
1f85d28
Implement more vector functions
GollokG 793df4a
Formatting
GollokG ffa0b54
Merge branch 'master' into affine-equality-domain-without-with
abdae29
Merge pull request #3 from CopperCableIsolator/affine-equality-domain…
charlotte-brandt 6021c42
Implement is_covered_by
GollokG 97a735b
small bugfixes
b17f33e
Finish normalize first version with dec2D
GollokG 80672a1
bugfix in find_val_opt and lin_independent
418de56
Fixed affeq_rows_are_valid helper for normalize
GollokG e10493a
better map2pz,better naming
CopperCableIsolator d2b0be7
small hickup
CopperCableIsolator 859ec26
normalize bug fix
67c1d5c
small naming
CopperCableIsolator 71768be
fold_left2_f_preserves_zero
CopperCableIsolator 0207a73
print for debugging
2bc4b66
Merge branch 'master' of https://github.com/CopperCableIsolator/gobli…
ef0cc36
Bugfixes in Vector and more Debug prints
GollokG c038dc7
Bugfix in Vector keep_vals and to_list; Implement set_nth in Vector"
GollokG 92b784a
Bugfix insert_val_at
GollokG 8ba5777
Bugfix Matrix map2i and Vector insert_val_at again
GollokG f6a415e
Add more debug-prints
GollokG 3e7d3d6
Bugfix in Vector rev and Matrix map2i again
GollokG 0c95dc7
Bugfix in Matrix del_cols and Vector remove_at_indices
GollokG c72c77d
arraymatrix passes tests again
09054a1
Reduced test suite; Simple normalized test with mxn-Matrix with m!=n;
feniup 99cf805
Merge branch 'master' of github.com:CopperCableIsolator/goblint-spars…
feniup 2968963
Added example source
feniup 4ef3acc
more debugging prints and added remove_zero_rows to rref_vec
968c533
Bugfixes in ListMatrix normalize
GollokG fe6b2a6
Added a solution vector to the normalize unit test
feniup 18acca5
Normalize test for a shuffeled matrix
feniup 43e042f
Normalize test for row elimination
feniup ef07123
Normalize tests with different domains
feniup 8d1c548
Normalize tests for idempotency and negation
feniup d71d7bd
bugfix in add_empty_columns, behavious still differs from arraymatrix
db97f30
add_emtpy_cols uses arraymatrix logic here + bugfix in normalize - on…
315dac6
appending and normalizing in is_covered_by - all tests pass
58e34c0
Normalize tests for empty matrix, two column matrix and a normalized …
feniup 9f7cec9
Added a newline
feniup 6673aae
Changed the assert failure text for when the normalization fails
feniup fe984fb
Add some is_covered_by tests
GollokG f44f2eb
Formatting
GollokG 79f890a
Added some comments on the test setup
feniup 4b34fda
Added some comments on the test setup
feniup 586cc38
Merge branch 'master' of https://github.com/CopperCableIsolator/gobli…
GollokG 1241795
bugfix in insert_zeros and use list funtionality again, uses apron st…
091b9fa
coveredddd
CopperCableIsolator a7a4e14
Fix normalize tests for floating point and fraction
GollokG b15b9d2
small tweak in findi_val_opt, could be even a tini tiny bit faster bu…
CopperCableIsolator 0f6509b
removed prints for benchmarking
9ea8cc2
Remove old copies in AffineEqualityDomain
GollokG ca91d48
Adapt sparseVector functions to tail recursive
GollokG 6883084
added Timingwraps to vector functions and alternative to findivalopt
61caba2
implemented different rref_vec that doesn't use normalize
c9be718
new rref_vec should be faster
fb1f36a
removed files with debug logs that I pushed by accident
0535677
Add apply_with_c_f_preserves_zero
GollokG c776a2b
Changed some calls in Domain to zero preserving
GollokG d3b18aa
Change rref_matrix without append and normalize, still have to benchmark
GollokG eba9d49
Remove some warnings of deprecated code
GollokG 21a839c
Merge branch 'master' into benchmarks
GollokG dd0000e
Merge branch 'benchmarks' into master
GollokG 2e80b94
removed second remove_nth
charlotte-brandt 1fa998f
Remove deprecated _with functions from Vector and Matrix interface
GollokG 1ea8040
Remove deprecated _with functions from Vector and Matrix interface
GollokG fd5689a
commenting some functions
charlotte-brandt 335d4ea
Merge branch 'master' of https://github.com/CopperCableIsolator/gobli…
charlotte-brandt 6186435
is_cons_vec
CopperCableIsolator d42bf5f
replace the last findi_val_opt
charlotte-brandt 0088812
ein paar maps ausgetauscht
CopperCableIsolator 92802e5
Optimize non zero-preserving Vector.map and Vector.map2i
GollokG 2c8901f
added test from lin2vareq to affeq that found mistake in dim_add
charlotte-brandt 4411280
Implement zero preserving Array Vector functions by calling normal fu…
GollokG 012104f
assert_rref
CopperCableIsolator 37190f4
assert_rref
CopperCableIsolator d7da9c7
small bugfix assert_rref
CopperCableIsolator bb15181
Bugfix rref_vec using reduce_col_with_vec
GollokG 0678f66
Change order of functions because of compilation error
GollokG 3b49ba5
Organize Vector and Matrix interface
GollokG 93463f2
Bugfix Vector is_const_vec
GollokG 6ae9bf1
Remove prints in ArrayMatrix
GollokG b8ba2bb
reordered function in vector so that they match the interface
charlotte-brandt 60f7b67
Reorder listMatrix; Some renaming
GollokG 8c931a7
Optimize get_col for sparse; Some timing_wraps for matrix
GollokG de6acc7
Fix semantics Matrix.map2, changed Matrix.map2i but might still have …
GollokG c01b627
comments
CopperCableIsolator 1a33f55
findi_f_false_at_zero
CopperCableIsolator aaadeaa
Add find2i_f_false_at_zero to ArrayVector and remove duplicate code f…
GollokG a82e652
Merge remote-tracking branch 'upstream/master'
GollokG File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Remove some warnings of deprecated code
- Loading branch information
commit eba9d498586c050fd2563d0ea637960972b19e3c
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -134,5 +134,4 @@ module ArrayVector: AbstractVector = | |
|
||
let find_first_non_zero v = | ||
failwith "TODO" | ||
|
||
end |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Check warning
Code scanning / Semgrep OSS
Semgrep Finding: semgrep.list-length-compare-n Warning