Tg nonlin#2

Open

BritikovKI wants to merge 245 commits intoadt-chcfrom

Commits on Aug 14, 2017

basic functionality of randomized invariants search

Grigory Fedyukovich
authored and
grigoryfedyukovich
committed
accurate processing of the coefficients and constants
grigoryfedyukovich
committed
benchmarks (mostly adapted from ICE)
grigoryfedyukovich
committed
more precise settings to aggressivepruning, frequencies, and priorities
grigoryfedyukovich
committed
enlarging the range of the coefficients and constants
grigoryfedyukovich
committed
distributivity rewriter of the code
grigoryfedyukovich
committed
limited support for nonlinear multiplication
grigoryfedyukovich
committed
some benchmarks from loop-acceleration and loop-new

samkaufman
authored and
grigoryfedyukovich
committed
MOD, DIV are parseable, but not solvable
grigoryfedyukovich
committed
added

samkaufman
authored and
grigoryfedyukovich
committed
two more benchmarks from loop-new

samkaufman
authored and
grigoryfedyukovich
committed
script to benchmark ICE/MCMC on win32

samkaufman
authored and
grigoryfedyukovich
committed
added --resume and --verbose to benchmark-others.py

samkaufman
authored and
grigoryfedyukovich
committed
refactored the priorities assignment
grigoryfedyukovich
committed
added more benchmarks over non-linear arithmetic
grigoryfedyukovich
committed
fixed the learning of several invariants in the row
grigoryfedyukovich
committed
propagating equalities in query implications
grigoryfedyukovich
committed
merged safe benchmarks from sam-contribs to the main bench; removed unsafe
grigoryfedyukovich
committed
fixed statistics mining for multiple invariants
grigoryfedyukovich
committed
fixed non-terminating ite-handling when the guard has negation
grigoryfedyukovich
committed
added more benchmarks
grigoryfedyukovich
committed
z3 benchmarking, mcmcify, other benchmark opts

samkaufman
authored and
grigoryfedyukovich
committed
support for constants on the rhs of div / mod
grigoryfedyukovich
committed
optimizing the prioritization
grigoryfedyukovich
committed
added more hard benchmarks
grigoryfedyukovich
committed
fixed lemma learning for multiple invariants / multiple queries
grigoryfedyukovich
committed
enhancing invariant grammars based on learned lemmas
grigoryfedyukovich
committed
small refactoring
grigoryfedyukovich
committed
naive bounded explorer; and benchmarks for which it has to find a counterexample, and freqhorn has to diverge
grigoryfedyukovich
committed
reconsidered preprocessing: no `shrink` option, and formula simplifications
grigoryfedyukovich
committed
reconsidered epsilon frequencies: now probabilistic
grigoryfedyukovich
committed
bigger space for the probabilities & priorities tuning; and a user-friendly interface
grigoryfedyukovich
committed
engine to generate an inductive validity core
grigoryfedyukovich
committed
refreshed the description online
grigoryfedyukovich
committed

Commits on Aug 30, 2017

the order and the duplicates in srcVars and dstVars is taken into account
grigoryfedyukovich
committed

Commits on Sep 1, 2017

k-inductive reasoning for programs with one loop
grigoryfedyukovich
committed

Commits on Sep 7, 2017

combined randomized sampling with k-induction
grigoryfedyukovich
committed

Commits on Sep 10, 2017

Commits on Sep 16, 2017

added benchmarks
grigoryfedyukovich
committed

Commits on Sep 21, 2017

checking invariance of itp-based bounded proofs
grigoryfedyukovich
committed

Commits on Sep 29, 2017

fixed stabilization of zero-frequencies (i.e., when epsilon disabled)
grigoryfedyukovich
committed

Commits on Oct 8, 2017

reconsidered the process of extracting subexpressions from code
grigoryfedyukovich
committed

Commits on Oct 18, 2017

fixed stabilization of epsilon-frequencies when freqs is disabled
grigoryfedyukovich
committed

Commits on Oct 23, 2017

revised algorithm of FreqHorn:
grigoryfedyukovich
committed

Commits on Oct 24, 2017

reclassified benchmarks
grigoryfedyukovich
committed

Commits on Oct 27, 2017

various tiny fixes and optimizations
grigoryfedyukovich
committed

Commits on Nov 3, 2017

made the sampler design more modular
grigoryfedyukovich
committed

Commits on Nov 10, 2017

updated links to the paper and slides
grigoryfedyukovich
committed

Commits on Nov 15, 2017

fixed large-number handling in Expr
grigoryfedyukovich
committed

Commits on Nov 27, 2017

some tiny optimizations and code cleaning
grigoryfedyukovich
committed

Commits on Jan 1, 2018

Commits on Jan 10, 2018

added a link to most recent paper
grigoryfedyukovich
committed

Commits on Feb 16, 2018

few new benchmarks
grigoryfedyukovich
committed

Commits on Feb 20, 2018

Commits on Feb 23, 2018

Commits on Feb 27, 2018

Commits on Feb 28, 2018

misc. fixes
samkaufman
committed

Commits on Mar 1, 2018

Commits on Mar 2, 2018

Merge pull request #2 from grigoryfedyukovich/rnd-new-benchmarking
samkaufman
authored

Commits on Apr 18, 2018

TACAS slides
grigoryfedyukovich
committed

Commits on May 4, 2018

new experimental algorithm for synthesis of multiple invariants
grigoryfedyukovich
committed

Commits on May 7, 2018

MultiFreqHorn: added bootstrapping, fixed few bugs
grigoryfedyukovich
committed

Commits on May 9, 2018

Commits on May 11, 2018

Commits on May 16, 2018

Commits on May 18, 2018

Commits on May 19, 2018

MultiFreqHorn: solved more challenging benchs
grigoryfedyukovich
committed

Commits on May 20, 2018

MultiFreqHorn: flexible generation of behavioral candidates
grigoryfedyukovich
committed

Commits on May 21, 2018

MultiFreqHorn: optimized bootstrapping slightly
grigoryfedyukovich
committed

Commits on May 25, 2018

enforced current AE-VAL's limitation
grigoryfedyukovich
committed

Commits on May 27, 2018

MultiFreqHorn: several tiny optimizations
grigoryfedyukovich
committed

Commits on May 28, 2018

MultiFreqHorn: added new benchmarks
grigoryfedyukovich
committed

Commits on May 31, 2018

more careful handling of Z3 bugs
grigoryfedyukovich
committed

Commits on Jun 1, 2018

updated the help message; made --v3 default
grigoryfedyukovich
committed

Commits on Jun 14, 2018

identifying and solving non-recursive systems (using BMC)
grigoryfedyukovich
committed

Commits on Jun 17, 2018

support for pure smtlib2 inputs
grigoryfedyukovich
committed

Commits on Jul 9, 2018

basic support for mutual recursion
grigoryfedyukovich
committed

Commits on Aug 15, 2018

supported some basic reasoning about arrays
grigoryfedyukovich
committed

Commits on Aug 17, 2018

added more benchs with arrays
grigoryfedyukovich
committed

Commits on Aug 31, 2018

array invariants: a trick to sample inductive candidates
grigoryfedyukovich
committed

Commits on Sep 10, 2018

support for some systems with multiple array accesses per iteration
grigoryfedyukovich
committed

Commits on Sep 12, 2018

support for disjunctive array invariants
grigoryfedyukovich
committed

Commits on Sep 18, 2018

more accurate seed mining and candidate manipulation for array invariants
grigoryfedyukovich
committed

Commits on Sep 20, 2018

bootstrapping for array candidates
grigoryfedyukovich
committed

Commits on Sep 21, 2018

generalization of learned lemmas over several arrays
grigoryfedyukovich
committed

Commits on Sep 26, 2018

mining array seeds deeper
grigoryfedyukovich
committed

Commits on Oct 10, 2018

Commits on Nov 4, 2018

basic support for multiple Array invariants
grigoryfedyukovich
committed

Commits on Nov 6, 2018

more enhanced support for multiple Array invariants
grigoryfedyukovich
committed

Commits on Nov 8, 2018

reconsidered template generation for Arrays
grigoryfedyukovich
committed

Commits on Nov 14, 2018

Commits on Nov 30, 2018

a prototype of lazy unroller and verifier
grigoryfedyukovich
committed

Commits on Dec 13, 2018

handling of local variables fixed; more examples added
grigoryfedyukovich
committed

Commits on Apr 14, 2019

more careful preprocessing
grigoryfedyukovich
committed

Commits on Jul 25, 2019

guessing and bootstrapping
grigoryfedyukovich
committed

Commits on Aug 1, 2019

Houdini and candidate propagation
grigoryfedyukovich
committed

Commits on Sep 3, 2019

an option for counterexamples; help message
grigoryfedyukovich
committed

Commits on Sep 7, 2019

fixed the parsing bug
grigoryfedyukovich
committed

Commits on Apr 9, 2020

printing invariants
grigoryfedyukovich
committed

Commits on Apr 15, 2020

backward propagation and multi-abduction
grigoryfedyukovich
committed

Commits on May 5, 2020

revisited forward/backward alternation; improved decomposition
grigoryfedyukovich
committed

Commits on May 13, 2020

better fairness implementation for the decomposition
grigoryfedyukovich
committed

Commits on Jun 11, 2020

Changed CMakeLists.txt to the contents at https://github.com/grigoryfedyukovich/aeval/blob/mu/CMakeLists.txt. Explicitly cast boost::logic::tribool to bool in SMTUtils.hpp and NonlinCHCsolver.hpp

vnkommu
authored and
grigoryfedyukovich
committed

Commits on Jun 16, 2020

improved the simplification passes
grigoryfedyukovich
committed

Commits on Jun 25, 2020

arbitrary-precision arithmetic simplifications
grigoryfedyukovich
committed

Commits on Jul 1, 2020

extended the input language; improved the preprocessing and handling of arrays
grigoryfedyukovich
committed

Commits on Jul 2, 2020

added/moved some benchmarks
grigoryfedyukovich
committed

Commits on Jul 7, 2020

using QE for quantifier-free array invariants
grigoryfedyukovich
committed

Commits on Jul 22, 2020

improved preprocessing, propagation, and abduction
grigoryfedyukovich
committed

Commits on Jul 30, 2020

more precise select/store handling
grigoryfedyukovich
committed

Commits on Aug 6, 2020

repaired the counterexample generation; added benchs
grigoryfedyukovich
committed

Commits on Jun 7, 2021

Changes related to maximal specification synthesis PLDI'21 paper (#19)

sumanthsprabhu
and
mdrianaonk
authored

Commits on Jun 8, 2021

PLDI21 benchmarks

Sumanth Prabhu
authored and
grigoryfedyukovich
committed

Commits on Jun 15, 2021

change binary name; make maximal default; add an option to specify sygus path; comment logs; update README

sumanthsprabhu
authored and
grigoryfedyukovich
committed

Commits on Jun 16, 2021

polished the command-line interface a bit; formatted the code
grigoryfedyukovich
committed

Commits on Jun 24, 2021

updated the Z3 version
grigoryfedyukovich
committed

Commits on Aug 1, 2021

fixed MAX variable namings/types
grigoryfedyukovich
committed

Commits on May 16, 2022

SMT Parse switch to Nonliner [partial solution]
izlatkin
committed

Commits on May 20, 2022

Nonliner parse update + simplification + rid from rnrlinearVX solution
izlatkin
committed

Commits on May 21, 2022

TGTree.hpp added to explore nonlines paths
izlatkin
committed

Commits on Jun 3, 2022

TGTree.hpp updated to maintain duplicates chcs rules + pertial-integration TGTree to Nonlinear CHCSolver
izlatkin
committed

Commits on Jun 6, 2022

Commits on Jun 16, 2022

TGTree.hpp support early trees return for getNext(): if the tree has no ambiguity and can be definitely defined. Tree init updated, entries chcs added which are not presented in "dst" (Used to be o…
izlatkin
committed

Commits on Jun 17, 2022

small ToDo: add chc_index for Termination nodes
izlatkin
committed

Commits on Jun 23, 2022

Commits on Jun 30, 2022

switch z3 to latest build, TGTree - add trees deallocation
izlatkin
committed

Commits on Jul 1, 2022

index_cycle_chc added in ruleManage to identify the cycle start index. The benchmarks with -1 have no cycle (mostly constructor benchmarks or private functions calls only from constructor)
izlatkin
committed

Commits on Jul 2, 2022

re-generation of queries; new skeleton
grigoryfedyukovich
committed

Commits on Jul 3, 2022

fillTodos implementation, fill skeleton of the new implementation
izlatkin
committed

Commits on Jul 8, 2022

get model, find bnd-variables for sat cases
izlatkin
committed

Commits on Jul 10, 2022

Commits on Jul 12, 2022

filter names, precise test printing
grigoryfedyukovich
committed

Commits on Jul 14, 2022

Commits on Jul 19, 2022

fillTodos added two conditions
izlatkin
committed

Commits on Sep 9, 2022

dump query to the smt2 file (tg_query.smt2); add time stamps for each request to the solver to track performance and memory leak
izlatkin
committed

Commits on Sep 21, 2022

dot.file for SAT queries
izlatkin
committed

Commits on Sep 23, 2022

fixed query generation
grigoryfedyukovich
committed

Commits on Sep 27, 2022

Commits on Sep 28, 2022

duplication trees bug fix, adjustment of number of quires for each bnb & mkNewQuery
izlatkin
committed

Commits on Sep 29, 2022

fixed the interface/constructor handling
grigoryfedyukovich
committed

Commits on Oct 4, 2022

printing constructor calls in test file
grigoryfedyukovich
committed

Commits on Oct 10, 2022

another fix for test printing
grigoryfedyukovich
committed

Commits on Nov 7, 2022

tiny fix multiple contract case
izlatkin
committed

Commits on Aug 22, 2023

Commits on Aug 23, 2023

Commits on Aug 31, 2023

Optimization: additional restrictions based on transition invs
BritikovKI
committed

Commits on Sep 11, 2023

ADT-CHC: getting closer to an error
BritikovKI
committed

Commits on Sep 12, 2023

ADT-CHC: Horn Nonlin solver pops chcs
BritikovKI
committed

Commits on Sep 13, 2023

ADT-CHC: Horn Nonlin solver's not crashing anymore
BritikovKI
committed

Commits on Sep 20, 2023

Commits on Sep 25, 2023

ADT-CHC: Removed Debugging
BritikovKI
committed

Commits on Sep 26, 2023

Commits on Oct 25, 2023

DAG-fix: printouts
BritikovKI
committed

Commits on Nov 3, 2023

TGNolnlin: utilising latest parse
BritikovKI
committed

Commits on Nov 12, 2023

TG-Nonlin: same numbers of decls & CHCs, diff in the invVars
BritikovKI
committed

Commits on Dec 6, 2023

Testgen: fixed few bugs, now adt-chc and tgnonlin work propperly
BritikovKI
committed

Commits on Dec 27, 2023

generating models for ADTs via accessors
grigoryfedyukovich
committed

Commits on Dec 29, 2023

improved the test printing
grigoryfedyukovich
committed

Commits on Jan 4, 2024

Commits on Feb 16, 2024

Quick if fix
BritikovKI
committed

Commits on Feb 29, 2024

Commits on Mar 14, 2024

INT2BV support
BritikovKI
committed

Commits on Apr 4, 2024

INT2BV support
BritikovKI
committed

Commits on Aug 2, 2024

TgNonlin: optimized tree building(removed unnecessary checks)
BritikovKI
committed

Commits on Aug 9, 2024

Simplified tree checks, fixed bug for set of benchmarks
BritikovKI
committed

Commits on Aug 12, 2024

Added logical constraints, so possible test-generating trees are still considered
BritikovKI
committed

Commits on Sep 30, 2024

Z3 bytevecs: ZExprConverter
BritikovKI
committed

Commits on Oct 3, 2024

Commits on Oct 4, 2024

Z3 bytevecs: abstracting BVs away
BritikovKI
committed

Commits on Nov 4, 2024

BV siplification: simplification put in place
BritikovKI
committed

Commits on Jan 22, 2025

Func summarization (#11)
BritikovKI
authored

Commits on Jan 29, 2025

Refactoring: Few more removals
BritikovKI
committed