Code

Tg nonlin#2

Code

Open

BritikovKI wants to merge 238 commits intoadt-chcBritikovKI/aeval:adt-chcfrom tg-nonlinBritikovKI/aeval:tg-nonlinCopy head branch name to clipboard

+67,128-5,646

Commits

Commits on Aug 14, 2017

• basic functionality of randomized invariants search

  

  Grigory Fedyukovich

  authored and

  grigoryfedyukovich

  committed
  52a69dc

• accurate processing of the coefficients and constants

  grigoryfedyukovich

  committed
  e0c883d

• benchmarks (mostly adapted from ICE)

  grigoryfedyukovich

  committed
  d008e94

• more precise settings to aggressivepruning, frequencies, and priorities

  grigoryfedyukovich

  committed
  e3c41df

• enlarging the range of the coefficients and constants

  grigoryfedyukovich

  committed
  9e79357

• distributivity rewriter of the code

  grigoryfedyukovich

  committed
  c03e0be

• limited support for nonlinear multiplication

  grigoryfedyukovich

  committed
  5baa6f9

• some benchmarks from loop-acceleration and loop-new

  

  samkaufman

  authored and

  grigoryfedyukovich

  committed
  fbac1b0

• MOD, DIV are parseable, but not solvable

  grigoryfedyukovich

  committed
  8046399

• added

  Show description for f90b0af
  

  samkaufman

  authored and

  grigoryfedyukovich

  committed
  f90b0af

• two more benchmarks from loop-new

  

  samkaufman

  authored and

  grigoryfedyukovich

  committed
  bd5c4cf

• script to benchmark ICE/MCMC on win32

  

  samkaufman

  authored and

  grigoryfedyukovich

  committed
  ed281e1

• added --resume and --verbose to benchmark-others.py

  

  samkaufman

  authored and

  grigoryfedyukovich

  committed
  d32dab1

• refactored the priorities assignment

  grigoryfedyukovich

  committed
  51773c2

• added more benchmarks over non-linear arithmetic

  grigoryfedyukovich

  committed
  b5006f4

• fixed the learning of several invariants in the row

  grigoryfedyukovich

  committed
  731b6e2

• propagating equalities in query implications

  grigoryfedyukovich

  committed
  4623ba0

• merged safe benchmarks from sam-contribs to the main bench; removed unsafe

  grigoryfedyukovich

  committed
  ffef311

• fixed statistics mining for multiple invariants

  grigoryfedyukovich

  committed
  704700b

• fixed non-terminating ite-handling when the guard has negation

  grigoryfedyukovich

  committed
  be6b108

• added more benchmarks

  grigoryfedyukovich

  committed
  1f758ad

• z3 benchmarking, mcmcify, other benchmark opts

  

  samkaufman

  authored and

  grigoryfedyukovich

  committed
  a629b5a

• support for constants on the rhs of div / mod

  grigoryfedyukovich

  committed
  1b251e6

• optimizing the prioritization

  grigoryfedyukovich

  committed
  a7d08d8

• added more hard benchmarks

  grigoryfedyukovich

  committed
  3d2368b

• fixed lemma learning for multiple invariants / multiple queries

  grigoryfedyukovich

  committed
  f96ab62

• enhancing invariant grammars based on learned lemmas

  grigoryfedyukovich

  committed
  c520600

• small refactoring

  grigoryfedyukovich

  committed
  54bfc4f

• naive bounded explorer; and benchmarks for which it has to find a counterexample, and freqhorn has to diverge

  grigoryfedyukovich

  committed
  9fd1ec2

• reconsidered preprocessing: no shrink option, and formula simplifications

  grigoryfedyukovich

  committed
  6c6480b

• reconsidered epsilon frequencies: now probabilistic

  grigoryfedyukovich

  committed
  f19ab3a

• bigger space for the probabilities & priorities tuning; and a user-friendly interface

  grigoryfedyukovich

  committed
  bb87c20

• engine to generate an inductive validity core

  grigoryfedyukovich

  committed
  d317c25

• refreshed the description online

  grigoryfedyukovich

  committed
  b19a8bd

Commits on Aug 30, 2017

• the order and the duplicates in srcVars and dstVars is taken into account

  grigoryfedyukovich

  committed
  f019198

Commits on Sep 1, 2017

• k-inductive reasoning for programs with one loop

  grigoryfedyukovich

  committed
  04e0fb9

Commits on Sep 7, 2017

• combined randomized sampling with k-induction

  grigoryfedyukovich

  committed
  020b8a8

Commits on Sep 10, 2017

• various tricks at the preprocessing,

  Show description for ac5faba
  grigoryfedyukovich

  committed
  ac5faba

• Corrected build commands in README

  samkaufman

  committed
  642d4d7

Commits on Sep 16, 2017

• added benchmarks

  Show description for 540ef17
  grigoryfedyukovich

  committed
  540ef17

Commits on Sep 21, 2017

• checking invariance of itp-based bounded proofs

  Show description for 5041af3
  grigoryfedyukovich

  committed
  5041af3

Commits on Sep 29, 2017

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

  grigoryfedyukovich

  committed
  a6e7676

Commits on Oct 8, 2017

• reconsidered the process of extracting subexpressions from code

  Show description for 8e84207
  grigoryfedyukovich

  committed
  8e84207

Commits on Oct 18, 2017

• fixed stabilization of epsilon-frequencies when freqs is disabled

  grigoryfedyukovich

  committed
  6024069

Commits on Oct 23, 2017

• revised algorithm of FreqHorn:

  Show description for ad16bac
  grigoryfedyukovich

  committed
  ad16bac

Commits on Oct 24, 2017

• reclassified benchmarks

  grigoryfedyukovich

  committed
  181bb5a

Commits on Oct 27, 2017

• various tiny fixes and optimizations

  grigoryfedyukovich

  committed
  074f1a3

Commits on Nov 3, 2017

• made the sampler design more modular

  Show description for 0e6087f
  grigoryfedyukovich

  committed
  0e6087f

Commits on Nov 10, 2017

• updated links to the paper and slides

  grigoryfedyukovich

  committed
  2b606d7

Commits on Nov 15, 2017

• fixed large-number handling in Expr

  grigoryfedyukovich

  committed
  0ffa615

Commits on Nov 27, 2017

• some tiny optimizations and code cleaning

  grigoryfedyukovich

  committed
  a2f027a

Commits on Jan 1, 2018

• lightweight CHC-preprocessing and some useful operations with CHCs

  grigoryfedyukovich

  committed
  208e8e2

• replacing variables in Exprs in batches

  grigoryfedyukovich

  committed
  9264c7a

Commits on Jan 10, 2018

• added a link to most recent paper

  grigoryfedyukovich

  committed
  31f69e8

Commits on Feb 16, 2018

• few new benchmarks

  grigoryfedyukovich

  committed
  b679f33

Commits on Feb 20, 2018

• Rebuilt Windows benchmarks

  samkaufman

  committed
  5366c61

• Consolidated bench ports from previous experiments

  samkaufman

  committed
  9645f77

• New MCMC benchmarks

  samkaufman

  committed
  bef9c42

Commits on Feb 22, 2018

• Moved to 3 trials with 1min timeout

  samkaufman

  committed
  92370f7

• Some new ICE benchmarks

  samkaufman

  committed
  aa58b7a

• Convenience script for comparing benchmark presence between algos.

  samkaufman

  committed
  9764d3a

• Resolved renamed benchmarks for MCMC

  samkaufman

  committed
  0cdd530

• dillig10 maps more closely to .c

  Show description for 18230fa
  samkaufman

  committed
  18230fa

• dillig15 fix

  samkaufman

  committed
  41227e6

• A bunch more ICE/Boogie benchmarks

  samkaufman

  committed
  3f32142

• bensistency.py: ASCII mode

  samkaufman

  committed
  ade79a9

• bouncy_three_counters_merged fix

  samkaufman

  committed
  d2191ed

Commits on Feb 23, 2018

• New Boogie/ICE benchmarks

  samkaufman

  committed
  58e1b64

• More ICE/Boogie benchmarks

  samkaufman

  committed
  144b663

• Added Windows AMI override

  samkaufman

  committed
  b83da84

Commits on Feb 27, 2018

• New analyses (minus charting)

  samkaufman

  committed
  469db67

• spacer compilation fix

  samkaufman

  committed
  eb920f6

Commits on Feb 28, 2018

• misc. fixes

  samkaufman

  committed
  3770911

Commits on Mar 1, 2018

• Fixed & initial analysis notebook

  samkaufman

  committed
  a3906ed

• more analyses

  samkaufman

  committed
  4361c98

Commits on Mar 2, 2018

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

  Show description for 89785ac
  samkaufman

  authored
  89785ac

Commits on Apr 18, 2018

• TACAS slides

  grigoryfedyukovich

  committed
  244dbed

Commits on May 4, 2018

• new experimental algorithm for synthesis of multiple invariants

  grigoryfedyukovich

  committed
  d558d02

Commits on May 7, 2018

• MultiFreqHorn: added bootstrapping, fixed few bugs

  grigoryfedyukovich

  committed
  e98cd44

Commits on May 9, 2018

• MultiFreqHorn: enlarged set of seeds by QE-based propagation

  grigoryfedyukovich

  committed
  00901fe

• MultiFreqHorn: weakening of propagated candidates

  grigoryfedyukovich

  committed
  84ef5da

Commits on May 10, 2018

• MultiFreqHorn: fixed lemma learning

  grigoryfedyukovich

  committed
  164164e

• small extension of the grammar

  grigoryfedyukovich

  committed
  3fd39d6

• behavior candidates changes

  kumarmadhukar

  committed
  58e01c5

• call behavior candidate changes

  kumarmadhukar

  committed
  ea0079a

• C benchmarks for behavior candidates

  kumarmadhukar

  committed
  1b78ae2

• armadillo in readme

  kumarmadhukar

  committed
  dba4133

• minor changes

  sumanthsprabhu

  committed
  e3b446c

• Make armaApproxEqual const

  Show description for 8e8d875
  sumanthsprabhu

  authored
  8e8d875

• Merge pull request #3 from sumanthsprabhu/rnd

  grigoryfedyukovich

  authored
  cf287ac

Commits on May 11, 2018

• MultiFreqHorn: normalizing the candidates before learning

  grigoryfedyukovich

  committed
  07cda6c

• Merge pull request #1 from grigoryfedyukovich/rnd

  Show description for 384823d
  sumanthsprabhu

  authored
  384823d

• MultiFreqHorn: normalizing the candidates before learning

  grigoryfedyukovich

  committed
  9f8a1b9

Commits on May 14, 2018

• Merge pull request #2 from grigoryfedyukovich/rnd

  Show description for 5932c8f
  sumanthsprabhu

  authored
  5932c8f

• A script to generate behaviors by running the program

  sumanthsprabhu

  authored
  f9c9e43

• Benchmark for behavioral candidates

  Show description for 395a4a1
  sumanthsprabhu

  authored
  395a4a1

• autmatic generation of models for multiple loops using SMT and seeding from behavioral candidates

  sumanthsprabhu

  committed
  68470c8

• Merge branch 'rnd' of https://github.com/sumanthsprabhu/aeval into rnd

  sumanthsprabhu

  committed
  9dfd50f

Commits on May 15, 2018

• MultiFreqHorn: new benchmarks

  grigoryfedyukovich

  committed
  9fdb1c0

• fix semicolons

  Show description for 859b809
  sumanthsprabhu

  authored
  859b809

• fix copying error

  sumanthsprabhu

  authored
  d5eebe7

• fix a minor copy bug

  sumanthsprabhu

  authored
  cad4138

• fixed tautological warning

  sumanthsprabhu

  authored
  8f0e709

• more careful handling of lin.combinations

  grigoryfedyukovich

  committed
  ef47554

Commits on May 16, 2018

• Merge pull request #3 from grigoryfedyukovich/rnd

  Show description for e7dc478
  sumanthsprabhu

  authored
  e7dc478

• Evaluate constants of abstracted variable

  Show description for efaf249
  sumanthsprabhu

  authored
  efaf249

Commits on May 17, 2018

• Merge pull request #5 from sumanthsprabhu/rnd

  Show description for 540deb6
  grigoryfedyukovich

  authored
  540deb6

• MultiFreqHorn: Houdini-style weakening and batching at the bootstrapping

  grigoryfedyukovich

  committed
  398f6b5

• Merge pull request #4 from grigoryfedyukovich/rnd

  Show description for 80fdccc
  sumanthsprabhu

  authored
  80fdccc

• fix generalisation of constants

  Show description for 68bd6b7
  sumanthsprabhu

  authored
  68bd6b7

Commits on May 18, 2018

• more careful handling of NIA-terms

  grigoryfedyukovich

  committed
  fd4dc15

• Merge pull request #6 from sumanthsprabhu/rnd

  Show description for 10ecb9a
  grigoryfedyukovich

  authored
  10ecb9a

Commits on May 19, 2018

• MultiFreqHorn: solved more challenging benchs

  grigoryfedyukovich

  committed
  2e86d9c

Commits on May 20, 2018

• MultiFreqHorn: flexible generation of behavioral candidates

  grigoryfedyukovich

  committed
  e01d98d

Commits on May 21, 2018

• MultiFreqHorn: optimized bootstrapping slightly

  grigoryfedyukovich

  committed
  35662c8

Commits on May 25, 2018

• enforced current AE-VAL's limitation

  grigoryfedyukovich

  committed
  df571e4

Commits on May 27, 2018

• MultiFreqHorn: several tiny optimizations

  grigoryfedyukovich

  committed
  b60b53c

Commits on May 28, 2018

• MultiFreqHorn: added new benchmarks

  grigoryfedyukovich

  committed
  935ba64

Commits on May 31, 2018

• more careful handling of Z3 bugs

  grigoryfedyukovich

  committed
  c6b8848

Commits on Jun 1, 2018

• updated the help message; made --v3 default

  grigoryfedyukovich

  committed
  40d22ec

Commits on Jun 14, 2018

• identifying and solving non-recursive systems (using BMC)

  grigoryfedyukovich

  committed
  a58a175

Commits on Jun 17, 2018

• support for pure smtlib2 inputs

  grigoryfedyukovich

  committed
  3d9f00a

Commits on Jul 9, 2018

• basic support for mutual recursion

  grigoryfedyukovich

  committed
  c5f7fd5

Commits on Aug 15, 2018

• supported some basic reasoning about arrays

  grigoryfedyukovich

  committed
  76cbb03

Commits on Aug 17, 2018

• added more benchs with arrays

  grigoryfedyukovich

  committed
  b6eb195

Commits on Aug 31, 2018

• array invariants: a trick to sample inductive candidates

  grigoryfedyukovich

  committed
  9b80f86

Commits on Sep 10, 2018

• support for some systems with multiple array accesses per iteration

  grigoryfedyukovich

  committed
  c3fdbe9

Commits on Sep 12, 2018

• support for disjunctive array invariants

  grigoryfedyukovich

  committed
  2077319

Commits on Sep 18, 2018

• more accurate seed mining and candidate manipulation for array invariants

  grigoryfedyukovich

  committed
  a4f1224

Commits on Sep 20, 2018

• bootstrapping for array candidates

  grigoryfedyukovich

  committed
  afe82f9

Commits on Sep 21, 2018

• generalization of learned lemmas over several arrays

  grigoryfedyukovich

  committed
  390fe6c

Commits on Sep 26, 2018

• mining array seeds deeper

  grigoryfedyukovich

  committed
  d5ce55e

Commits on Oct 10, 2018

• extended the generalization method for array candidates

  grigoryfedyukovich

  committed
  bb16e54

• supported invariants over NIA+Arrays

  grigoryfedyukovich

  committed
  b3e305f

Commits on Nov 4, 2018

• basic support for multiple Array invariants

  grigoryfedyukovich

  committed
  b2f4568

Commits on Nov 6, 2018

• more enhanced support for multiple Array invariants

  grigoryfedyukovich

  committed
  6c51777

Commits on Nov 8, 2018

• reconsidered template generation for Arrays

  Show description for 44f9b76
  grigoryfedyukovich

  committed
  44f9b76

Commits on Nov 14, 2018

• optimized candidate propagation for Arrays

  grigoryfedyukovich

  committed
  1bad65f

• added new benchmarks over Arrays

  Show description for db4e948
  grigoryfedyukovich

  committed
  db4e948

Commits on Nov 30, 2018

• a prototype of lazy unroller and verifier

  Show description for 716019b
  grigoryfedyukovich

  committed
  716019b

Commits on Dec 13, 2018

• handling of local variables fixed; more examples added

  grigoryfedyukovich

  committed
  61323d1

Commits on Apr 14, 2019

• more careful preprocessing

  grigoryfedyukovich

  committed
  ba1516b

Commits on Jul 25, 2019

• guessing and bootstrapping

  grigoryfedyukovich

  committed
  4dce9dd

Commits on Aug 1, 2019

• Houdini and candidate propagation

  grigoryfedyukovich

  committed
  7e474ac

Commits on Sep 3, 2019

• an option for counterexamples; help message

  grigoryfedyukovich

  committed
  e23db22

Commits on Sep 7, 2019

• fixed the parsing bug

  grigoryfedyukovich

  committed
  2e0153c

Commits on Apr 9, 2020

• printing invariants

  Show description for 1a50bfb
  grigoryfedyukovich

  committed
  1a50bfb

Commits on Apr 15, 2020

• backward propagation and multi-abduction

  grigoryfedyukovich

  committed
  f9b0a13

Commits on May 5, 2020

• revisited forward/backward alternation; improved decomposition

  grigoryfedyukovich

  committed
  342e43e

Commits on May 13, 2020

• better fairness implementation for the decomposition

  grigoryfedyukovich

  committed
  daae6ce

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
  c390929

Commits on Jun 16, 2020

• improved the simplification passes

  grigoryfedyukovich

  committed
  8428376

Commits on Jun 25, 2020

• arbitrary-precision arithmetic simplifications

  grigoryfedyukovich

  committed
  bc08a00

Commits on Jul 1, 2020

• extended the input language; improved the preprocessing and handling of arrays

  grigoryfedyukovich

  committed
  3279d35

Commits on Jul 2, 2020

• added/moved some benchmarks

  grigoryfedyukovich

  committed
  4391345

Commits on Jul 7, 2020

• using QE for quantifier-free array invariants

  grigoryfedyukovich

  committed
  43d7273

Commits on Jul 22, 2020

• improved preprocessing, propagation, and abduction

  Show description for aca656f
  grigoryfedyukovich

  committed
  aca656f

Commits on Jul 30, 2020

• more precise select/store handling

  grigoryfedyukovich

  committed
  b840567

Commits on Aug 6, 2020

• repaired the counterexample generation; added benchs

  grigoryfedyukovich

  committed
  f12bc8f

Commits on Jun 7, 2021

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

  Show description for 600ef24
  

  sumanthsprabhu

  and

  mdrianaonk

  authored
  600ef24

Commits on Jun 8, 2021

• PLDI21 benchmarks

  

  Sumanth Prabhu

  authored and

  grigoryfedyukovich

  committed
  0cd94f7

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
  0384d46

Commits on Jun 16, 2021

• polished the command-line interface a bit; formatted the code

  grigoryfedyukovich

  committed
  e61ada8

Commits on Jun 24, 2021

• updated the Z3 version

  grigoryfedyukovich

  committed
  c956685

Commits on Aug 1, 2021

• fixed MAX variable namings/types

  grigoryfedyukovich

  committed
  fbb296d

Commits on May 16, 2022

• SMT Parse switch to Nonliner [partial solution]

  izlatkin

  committed
  e1c0c03

Commits on May 20, 2022

• Nonliner parse update + simplification + rid from rnrlinearVX solution

  izlatkin

  committed
  cee0d04

Commits on May 21, 2022

• TGTree.hpp added to explore nonlines paths

  izlatkin

  committed
  f760b7b

Commits on Jun 3, 2022

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

  izlatkin

  committed
  a950790

Commits on Jun 6, 2022

• TGTree.hpp updated to store and track chc_index. Multiple queries are mocked up and currently ignored.

  izlatkin

  committed
  b6af2ad

• draft of the Tree->SSA convertor

  grigoryfedyukovich

  committed
  c9dda06

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…

  Show description for dfcfc79
  izlatkin

  committed
  dfcfc79

Commits on Jun 17, 2022

• small ToDo: add chc_index for Termination nodes

  izlatkin

  committed
  006169c

Commits on Jun 23, 2022

• pruning decls that have false-interpretations

  grigoryfedyukovich

  committed
  f36e9cc

• fixed arg types

  grigoryfedyukovich

  committed
  4f72bdc

Commits on Jun 30, 2022

• switch z3 to latest build, TGTree - add trees deallocation

  izlatkin

  committed
  b3c15d3

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
  c5ccec9

Commits on Jul 2, 2022

• re-generation of queries; new skeleton

  grigoryfedyukovich

  committed
  458059b

Commits on Jul 3, 2022

• fillTodos implementation, fill skeleton of the new implementation

  izlatkin

  committed
  43c45fe

Commits on Jul 8, 2022

• get model, find bnd-variables for sat cases

  izlatkin

  committed
  d2f37d8

Commits on Jul 10, 2022

• tree generation bug fix

  izlatkin

  committed
  568aa5b

• README.md actualized

  izlatkin

  committed
  f5f4d94

Commits on Jul 12, 2022

• filter names, precise test printing

  grigoryfedyukovich

  committed
  eaf37c7

Commits on Jul 14, 2022

• contracts signature added as --keys parameter

  izlatkin

  committed
  276bb9d

• using contracts signature for tests printing

  grigoryfedyukovich

  committed
  6157e7b

Commits on Jul 19, 2022

• fillTodos added two conditions

  izlatkin

  committed
  80ceb00

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
  80d3870

Commits on Sep 21, 2022

• dot.file for SAT queries

  izlatkin

  committed
  250cbcf

Commits on Sep 23, 2022

• fixed query generation

  grigoryfedyukovich

  committed
  8294885

Commits on Sep 27, 2022

• fix in mkNewQuery to handle switch between different cur_bnb numbers +

  Show description for 752e1f2
  izlatkin

  committed
  752e1f2

• proper fix for mkNewQuery

  grigoryfedyukovich

  committed
  1c878b0

Commits on Sep 28, 2022

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

  izlatkin

  committed
  e374142

Commits on Sep 29, 2022

• fixed the interface/constructor handling

  grigoryfedyukovich

  committed
  9ec33ac

Commits on Oct 4, 2022

• printing constructor calls in test file

  grigoryfedyukovich

  committed
  21ab929

Commits on Oct 10, 2022

• another fix for test printing

  grigoryfedyukovich

  committed
  631b9cf

Commits on Nov 7, 2022

• tiny fix multiple contract case

  izlatkin

  committed
  0595834

Commits on Aug 22, 2023

• CHC-ADT: tests

  BritikovKI

  committed
  d10500f

• ADT-CHC: merged most of the ADT-CHC changes into tg-nonlin

  BritikovKI

  committed
  979796e

• ADT-CHC: quickfix in progress

  BritikovKI

  committed
  47bdeec

Commits on Aug 23, 2023

• ADT-CHC: Fixes for compilation

  BritikovKI

  committed
  9f7472e

• ADT-CHC: Fixes for compilation

  BritikovKI

  committed
  5cf545e

Commits on Aug 24, 2023

• ADT-CHC: merged tg-nonlin with adt-chc to building condition

  BritikovKI

  committed
  1a201eb

• ADT-CHC: merged tg-nonlin with adt-chc to building condition

  BritikovKI

  committed
  64e68af

• ADT-CHC: parse fix, maybe smth missed

  BritikovKI

  committed
  f13abbd

• TG-NONLIN: fixes for nonlin inputs

  BritikovKI

  committed
  8835acc

• TG-NONLIN: fixes for nonlin inputs

  BritikovKI

  committed
  812baa3

• TG-NONLIN: fixes for nonlin inputs

  BritikovKI

  committed
  f049da6

Commits on Aug 31, 2023

• Optimization: additional restrictions based on transition invs

  BritikovKI

  committed
  e096376

Commits on Sep 11, 2023

• ADT-CHC: getting closer to an error

  BritikovKI

  committed
  6a3b890

Commits on Sep 12, 2023

• ADT-CHC: Horn Nonlin solver pops chcs

  BritikovKI

  committed
  fdd699b

Commits on Sep 13, 2023

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

  BritikovKI

  committed
  94c6da0

Commits on Sep 20, 2023

• ADT-CHC: Removed non-necessary prints

  BritikovKI

  committed
  c585ef0

• ADT-CHC: Debugging

  BritikovKI

  committed
  676fe58

Commits on Sep 25, 2023

• ADT-CHC: Removed Debugging

  BritikovKI

  committed
  ad112e7

Commits on Sep 26, 2023

• ADT-CHC: Removed Debugging

  BritikovKI

  committed
  38d77ed

• ADT-CHC: Removed Debugging

  BritikovKI

  committed
  d78e3e2

Commits on Oct 25, 2023

• DAG-fix: printouts

  BritikovKI

  committed
  cf96abc

Commits on Nov 3, 2023

• TGNolnlin: utilising latest parse

  BritikovKI

  committed
  570cfd2

Commits on Nov 12, 2023

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

  BritikovKI

  committed
  16620cc

Commits on Dec 6, 2023

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

  BritikovKI

  committed
  4a534a4

Commits on Dec 27, 2023

• generating models for ADTs via accessors

  grigoryfedyukovich

  committed
  2be6586

Commits on Dec 29, 2023

• improved the test printing

  grigoryfedyukovich

  committed
  e13cc77

Commits on Jan 4, 2024

• more elaborated processing of array models

  grigoryfedyukovich

  committed
  ba3818a

• further processing of array models

  grigoryfedyukovich

  committed
  17ffa0d

Commits on Feb 16, 2024

• Quick if fix

  BritikovKI

  committed
  af788b0

Commits on Feb 29, 2024

• Added support of the multiple contracts

  BritikovKI

  committed
  5a24613

• Added support of the multiple contracts

  BritikovKI

  committed
  a4037b8

Commits on Mar 14, 2024

• INT2BV support

  BritikovKI

  committed
  c1ec1a8

Commits on Apr 4, 2024

• INT2BV support

  BritikovKI

  committed
  2c28015

Commits on Aug 2, 2024

• TgNonlin: optimized tree building(removed unnecessary checks)

  BritikovKI

  committed
  f7095df

Commits on Aug 9, 2024

• Simplified tree checks, fixed bug for set of benchmarks

  BritikovKI

  committed
  a50015c

Commits on Aug 12, 2024

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

  BritikovKI

  committed
  cc682dc

Commits on Sep 30, 2024

• Z3 bytevecs: ZExprConverter

  BritikovKI

  committed
  13760b0

Commits on Oct 3, 2024

• Z3 bytevecs: marshaling

  BritikovKI

  committed
  4577fbc

• Z3 bytevecs: marshaling fix

  BritikovKI

  committed
  b14e652

• Z3 bytevecs: marshaling fix

  BritikovKI

  committed
  1d02c65

Commits on Oct 4, 2024

• Z3 bytevecs: abstracting BVs away

  BritikovKI

  committed
  042f1e7

Commits on Nov 4, 2024

• BV siplification: simplification put in place

  BritikovKI

  committed
  e9512c8