CHANGELOG

List of major changes and improvements between releases
=======================================================


AVR 2.1.0
--------------------------
(16 January 2022)
 
 * AVR source code is now released!
 * Bump version to 2.1

AVR 2.0.24
--------------------------
(23 August 2020)
 
 * API
    - New K-induction engine

 * Backends
    - Improved support for BV arrays

 * Various
    - New UF abstraction mode for BMC engine
    - Minor corrections and improvements

AVR 2.0.23
--------------------------
(15 August 2020)
 
 * Various
    - New branch for HWMCC'20

AVR 2.0.22
--------------------------
(07 November 2019)
 
 * Frontend
    - BTOR2: Corrects init with arrays
    
 * Backend
    - Corrects trivial HWMCC19 error

AVR 2.0.21
--------------------------
(11 October 2019)
 
 * API
    - Modifications to pr workers
    - Removed btormc (for hwmcc 2019 submission)
    - Adds backend boolector (with cadical) config

 * Various
    - Minor corrections to witness printing

AVR 2.0.20
--------------------------
(10 October 2019)
 
 * Core
    - BMC: New technique
    - BMC: Simple, clean, incremental bmc
    - BMC: Supported by y2 and bt backends

AVR 2.0.19
--------------------------
(09 October 2019)
 
 * Frontend
    - BTOR2: Adds arithmetic overflow operators
    
 * Various
    - Adds multi-property and array support to btor2 witness
    - Minor corrections

AVR 2.0.18
--------------------------
(08 October 2019)
 
 * Various
    - Version with low verbosity for HWMCC 2019
    - Updates official name to AVR

Averroes 2.0.17
--------------------------
(07 October 2019)
 
 * API
    - Updates to pr
    - Now pr allows running btormc

 * Frontend
    - BTOR2: Corrections
    - Yosys: Corrections
    
 * Backend
    - Adds initial support for arrays inbt2 backend

Averroes 2.0.16
--------------------------
(19 September 2019)
 
 * API
    - New proof race (pr)
    - pr allows running multiple configs

 * Frontend
    - BTOR2: Corrections
    
 * Core
    - Minor changes
    - Auto config. abstraction fineness
    
 * Various
    - Adds printing cex with split opt.

Averroes 2.0.15
--------------------------
(11 September 2019)
 
 * API
    - Adds new frontend btor2
    - Minor other changes
    
 * Frontend
    - BTOR2: Limited support (without arrays)
    
 * Core
    - Minor changes
    
 * Various
    - JG frontend not linked hereonwards

Averroes 2.0.14
--------------------------
(20 August 2019)
 
 * API
    - Adds option --smt2 to enable printing in SMT-LIB v2 format
    - Adds option --dot to enable dot graphical visualization
    - Several other changes
    
 * Frontend
    - WIF: Several corrections
    
 * Core
    - Several improvements
    
 * Backend
    - Several improvements
    
 * Various
    - Several bug fixes

Averroes 2.0.13
--------------------------
(16 July 2019)
 
 * API
    - Adds option --jgpre to pass wif preprocessing options
    - Modifies option --abstract to configure extract/concat interpretation using "ec" level
    
 * Frontend
    - WIF: Several corrections
    - WIF: Disables incorrect clock simplifications
    
 * Core
    - Improvements to solver queries
    - Improvements to model retrieval from solver
    - Improvements to unsat core computation
    
 * Backend
    - Y2: Support for detailed stats printing
    
 * Various
    - Minor bug fixes

Averroes 2.0.12
--------------------------
(27 June 2019)
 
 * API
    - Adds option --lazy_assume to configure laziness of assumptions
    - Adds another level of finess in option --level
    
 * Frontend
    - WIF: Changes to clock simplification
    - WIF: Selection of property at an early stage
    - WIF: Procedure to pipe other WIF engines with AVR
    - WIF: Support for identifying boolean equalities
    - Minor corrections
    - Removes redundant preprocessings
    
 * Core
    - Changes to cube formation
    - Changes to solver reset config
    - Adds single solver mode as default
    - Handling of trivially proved properties
    - Corrections to refinement for handling assumptions
    - Adds structural preprocessing to remove irrelevant system portions
    - Reduces refinement queries
    - Support for adding input relations (in latches)
    
 * Backend
    - Y2: Support for caching hard constraints
    
 * Various
    - Minor bug fixes

Averroes 2.0.11
--------------------------
(05 June 2019)
 
 * API
    - Adds option --level to configure abstraction fineness
    - Changes option --granularity. Granularity levels now upto 2 (default 0)
    
 * Various
    - Minor bug fixes
    - More stats collection
    
 * Experimental
    - Changes to cube formation when --random enabled

Averroes 2.0.10
--------------------------
(23 May 2019)
 
 * Experimental
    - Adds interpolation option for refinement

Averroes 2.0.9
--------------------------
(15 May 2019)
 
 * Various
    - Minor bug fix
    
 * Experimental
    - JG frontend support in WIF (Word-level Interface Format)

Averroes 2.0.8
--------------------------
(03 Apr 2019)
 
 * Various
    - Minor modifications to vmt frontend
    
 * Experimental
    - Config changes for I4
    - Printing of inductive invariant in smt2 format

Averroes 2.0.7
--------------------------
(12 Mar 2019)
 
 * API
    - Changes option --granularity. Granularity levels now upto 4 (default 1)
    
 * Various
    - Minor corrections

Averroes 2.0.6
--------------------------
(11 Mar 2019)
 
 * Core
    - Changes to data structures for improved performance
    - Improved learning from initial formula
    
 * Various
    - Improves subsumption checking

Averroes 2.0.5
--------------------------
(08 Mar 2019)
 
 * Backend
    - Corrections to all backends
    - Shifted to Yices backend for all queries
    
 * Various
    - Improves vmt parsing
    - Changes to stats printing

Averroes 2.0.4
--------------------------
(25 Feb 2019)
 
 * API
    - Changes default for option --abstract to sa (instead of sa+uf)
    
 * Backend
    - Corrections to Yices 2 backend
    - Updates MathSAT to v5.5.4
    - Upgrades to MathSAT backend
    - Shifted to MathSAT backend for all queries
    
 * Various
    - Adds learning from intitial state formula
    - Improved cube formation for integers/arrays
    
 * Notes
    - sa+uf (using option -a) is experimental only with MathSAT backend

Averroes 2.0.3
--------------------------

 * Various
    - Shifted to yices2 backend for all queries
    - Corrections and improvements to refinement
    - Extended support for vmt frontend (QF bitvectors + linear integer arithmetic + arrays)
    
Averroes 2.0.2
--------------------------

 * API
    - Changes option --file to positional argument
    - Adds option --granularity
    - Auto detect yosys path
    - Adds option --memory (in progress)
    - Adds option --property
    - Adds option --effort_mininv
    - Adds printing property info to cerr
    - Adds option --init to read init state from a file
    - Adds option --vmt to read .vmt file (limited)
    - Adds option --abstract to configure abstraction
    
 * Various
    - Support for async flops (as sync flops)
    - Adds option to select a single property
    - Adds option to minimize inductive invariant
    - Corrects --split optimization
    - Corrects assume support
    - Shifted to Z3 backend for concrete queries
    - Changes to abstract queries
    - Changes to symbolic learning
    - Improved generalization and refinement
    
 * Experimental
    - Adds memory abstraction
    - Adds support for global connect (as buffer) for .ilang
    - Adds unique clock identification procedure for .ilang
    - Adds .vmt frontend (limited to QF_BV)
    - Option --abstract is experimental

 * Notes
    - Option --init uses pattern matching (hence can go wrong)
    - Option --init cannot handle partial register assignment

Averroes 2.0.1
--------------------------

 * API
    - Removed option --allowinp
    - Updates to yosys commands
    - Uses .tcl for interacting with yosys
    - Adds intermediate data files in folder data
    
 * Various
    - Improvements to extraction, concatenation operation interpretation
    - Adds abstract commutativity to operations like +, *, bitwise
    - Automatically trigerring allow_inp lazily
    - Counterexample printing in file cex.txt
    - Limits frame summary printing
    - Many bugfixes and small improvements

 * Experimental
    - Support for multi-clock domains
    - Support for .vmt format (requires MathSAT and latest yosys)
    - Support for .smv format using .smv to .vmt (requires nuXmv)