Skip to content
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.

Sign up for GitHub

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

Jump to bottom

Tg nonlin #2

Open
wants to merge 238 commits into
base: adt-chc
Choose a base branch
from
Open

Tg nonlin #2

wants to merge 238 commits into from

Conversation

BritikovKI
Copy link
Owner

No description provided.

Grigory Fedyukovich and others added 30 commits August 13, 2017 21:53
@grigoryfedyukovich
basic functionality of randomized invariants search
52a69dc
@grigoryfedyukovich
accurate processing of the coefficients and constants
e0c883d
@grigoryfedyukovich
benchmarks (mostly adapted from ICE)
d008e94
@grigoryfedyukovich
more precise settings to aggressivepruning, frequencies, and priorities
e3c41df
@grigoryfedyukovich
enlarging the range of the coefficients and constants
9e79357
@grigoryfedyukovich
distributivity rewriter of the code
c03e0be
@grigoryfedyukovich
limited support for nonlinear multiplication
5baa6f9
@samkaufman @grigoryfedyukovich
some benchmarks from loop-acceleration and loop-new
fbac1b0
@grigoryfedyukovich
MOD, DIV are parseable, but not solvable
8046399
@samkaufman @grigoryfedyukovich
added
f90b0af 
loop-new/count_by_1_variant_true-unreach-call_true-termination
@samkaufman @grigoryfedyukovich
two more benchmarks from loop-new
bd5c4cf
@samkaufman @grigoryfedyukovich
script to benchmark ICE/MCMC on win32
ed281e1
@samkaufman @grigoryfedyukovich
added --resume and --verbose to benchmark-others.py
d32dab1
@grigoryfedyukovich
refactored the priorities assignment
51773c2
@grigoryfedyukovich
added more benchmarks over non-linear arithmetic
b5006f4
@grigoryfedyukovich
fixed the learning of several invariants in the row
731b6e2
@grigoryfedyukovich
propagating equalities in query implications
4623ba0
@grigoryfedyukovich
merged safe benchmarks from sam-contribs to the main bench; removed u…
ffef311 
…nsafe
@grigoryfedyukovich
fixed statistics mining for multiple invariants
704700b
@grigoryfedyukovich
fixed non-terminating ite-handling when the guard has negation
be6b108
@grigoryfedyukovich
added more benchmarks
1f758ad
@samkaufman @grigoryfedyukovich
z3 benchmarking, mcmcify, other benchmark opts
a629b5a
@grigoryfedyukovich
support for constants on the rhs of div / mod
1b251e6
@grigoryfedyukovich
optimizing the prioritization
a7d08d8
@grigoryfedyukovich
added more hard benchmarks
3d2368b
@grigoryfedyukovich
fixed lemma learning for multiple invariants / multiple queries
f96ab62
@grigoryfedyukovich
enhancing invariant grammars based on learned lemmas
c520600
@grigoryfedyukovich
small refactoring
54bfc4f
@grigoryfedyukovich
naive bounded explorer; and benchmarks for which it has to find a cou…
9fd1ec2 
…nterexample, and freqhorn has to diverge
@grigoryfedyukovich
reconsidered preprocessing: no shrink option, and formula simplific…
6c6480b 
…ations
BritikovKI and others added 30 commits September 11, 2023 15:32
@BritikovKI
ADT-CHC: getting closer to an error
6a3b890
@BritikovKI
ADT-CHC: Horn Nonlin solver pops chcs
fdd699b
@BritikovKI
ADT-CHC: Horn Nonlin solver's not crashing anymore
94c6da0
@BritikovKI
ADT-CHC: Removed non-necessary prints
c585ef0
@BritikovKI
ADT-CHC: Debugging
676fe58
@BritikovKI
ADT-CHC: Removed Debugging
ad112e7
@BritikovKI
ADT-CHC: Removed Debugging
38d77ed
@BritikovKI
ADT-CHC: Removed Debugging
d78e3e2
@BritikovKI
DAG-fix: printouts
cf96abc
@BritikovKI
TGNolnlin: utilising latest parse
570cfd2
@BritikovKI
TG-Nonlin: same numbers of decls & CHCs, diff in the invVars
16620cc
@BritikovKI
Testgen: fixed few bugs, now adt-chc and tgnonlin work propperly
4a534a4
@grigoryfedyukovich
generating models for ADTs via accessors
2be6586
@grigoryfedyukovich
improved the test printing
e13cc77
@grigoryfedyukovich
more elaborated processing of array models
ba3818a
@grigoryfedyukovich
further processing of array models
17ffa0d
@BritikovKI
Quick if fix
af788b0
@BritikovKI
Added support of the multiple contracts
5a24613
@BritikovKI
Added support of the multiple contracts
a4037b8
@BritikovKI
INT2BV support
c1ec1a8
@BritikovKI
INT2BV support
2c28015
@BritikovKI
TgNonlin: optimized tree building(removed unnecessary checks)
f7095df
@BritikovKI
Simplified tree checks, fixed bug for set of benchmarks
a50015c
@BritikovKI
Added logical constraints, so possible test-generating trees are stil…
cc682dc 
…l considered
@BritikovKI
Z3 bytevecs: ZExprConverter
13760b0
@BritikovKI
Z3 bytevecs: marshaling
4577fbc
@BritikovKI
Z3 bytevecs: marshaling fix
b14e652
@BritikovKI
Z3 bytevecs: marshaling fix
1d02c65
@BritikovKI
Z3 bytevecs: abstracting BVs away
042f1e7
@BritikovKI
BV siplification: simplification put in place
e9512c8
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
7 participants
@BritikovKI @grigoryfedyukovich @samkaufman @kumarmadhukar @sumanthsprabhu @vnkommu @izlatkin