Commits · 230a34aadcbf62a7a7ced19beea7ab4be8d25923 · Marek Chalupa / slowbeast

Browse files

Mar 15, 2021
- Use new Polynomail class to rewrite expressions · 230a34aa
  Marek Chalupa authored Mar 10, 2021
  230a34aa
- Rewrite expressions to eliminate multiplication if possible · 3af7f2e6
  Marek Chalupa authored Mar 10, 2021
  
  3af7f2e6
Mar 08, 2021
- Fix creating fresh symbols · 96dc6f0d
  Marek Chalupa authored Mar 08, 2021
  
  96dc6f0d
Mar 05, 2021
- Improve abstract solving · 33ba009c
  Marek Chalupa authored Mar 05, 2021
  
  33ba009c
- solvers: use abstraction of multiplication while solving hard formulas · aa71d1a3
  Marek Chalupa authored Mar 05, 2021
  
  aa71d1a3
- Fix reducing equality bitwidth · e850dac0
  Marek Chalupa authored Mar 05, 2021
  
  e850dac0
Mar 04, 2021
- fix is_sat · a9ece260
  Marek Chalupa authored Mar 04, 2021
  
  a9ece260
- Fix missing attribute · 284ec51c
  Marek Chalupa authored Mar 04, 2021
  
  284ec51c
- Fix setting a timeout · e895cfa4
  Marek Chalupa authored Mar 04, 2021
  
  e895cfa4
- Use staged solving · b52ffc2d
  Marek Chalupa authored Mar 04, 2021
  b52ffc2d
- rename method · 06743847
  Marek Chalupa authored Mar 04, 2021
  
  06743847
- Implement timeout to solver · 701d75e2
  Marek Chalupa authored Mar 04, 2021
  
  701d75e2
- Fix bit-reduction procedure · 6de20dae
  Marek Chalupa authored Mar 04, 2021
  6de20dae
- solver: improve filtering of concrete values · d59ca224
  Marek Chalupa authored Mar 04, 2021
  
  d59ca224
- Add method for reducing the bitwidth of expressions · 249ce113
  Marek Chalupa authored Mar 04, 2021
  
  249ce113
Mar 03, 2021
- bself: do not execute paths in induction check while overapproximating · 94c2c490
  Marek Chalupa authored Mar 03, 2021
  94c2c490
- Fix an assertion · 1af9858b
  Marek Chalupa authored Mar 03, 2021
  
  1af9858b
- Do more efficient induction check in drop_clauses · b92a7c17
  Marek Chalupa authored Mar 03, 2021
  
  b92a7c17
- Implement more efficient check for inductivity · b8206d04
  Marek Chalupa authored Mar 03, 2021
  
  b8206d04
- kindse: wrap loop into new class · 813263da
  Marek Chalupa authored Mar 03, 2021
  813263da
- bself tail: return all re-usable sequences · 2ee0e948
  Marek Chalupa authored Mar 03, 2021
  
  2ee0e948
- bself: use multiple overapproximations · 56728e5f
  Marek Chalupa authored Mar 03, 2021
  
  56728e5f
- bself: move adding relations out from overapprox_set · 7f37826b
  Marek Chalupa authored Mar 03, 2021
  
  7f37826b
- bself: put back an assertion · 76d9ff71
  Marek Chalupa authored Mar 03, 2021
  
  76d9ff71
- bself: fix empty SIS · 51b2fa46
  Marek Chalupa authored Mar 03, 2021
  
  51b2fa46
- Do not abort when an exit path is infeasible · 15e92b3b
  Marek Chalupa authored Mar 03, 2021
  15e92b3b
- bself: fix simple sis with inductive complement · 172793fa
  Marek Chalupa authored Mar 03, 2021
  
  172793fa
Mar 02, 2021
- bself: return multiple simple starting sis · 128bd487
  Marek Chalupa authored Mar 02, 2021
  
  128bd487
- use uninitializedRead only if the pointer is resolvable · ba7d90bf
  Marek Chalupa authored Mar 02, 2021
  ba7d90bf
- conj/disj: work as identity if only one argument is passed · 214cb007
  Marek Chalupa authored Mar 02, 2021
  
  214cb007
- rename executePath -> execute_path · 369d672c
  Marek Chalupa authored Mar 02, 2021
  
  369d672c
- bself: do not inherit from Kind · ed81deef
  Marek Chalupa authored Mar 02, 2021
  ed81deef
- bself: do not pass toplevel executor to BSELFChecker · ee16d90f
  Marek Chalupa authored Mar 02, 2021
  ee16d90f
- kindse: rename to BSELF · fcb1a0a7
  Marek Chalupa authored Mar 02, 2021
  
  fcb1a0a7
- rename KindSEChecker -> BSELFChecker · a5d1ed2e
  Marek Chalupa authored Mar 02, 2021
  
  a5d1ed2e
- Adjust tests · e1b5652d
  Marek Chalupa authored Feb 24, 2021
  
  e1b5652d
Mar 01, 2021
- kindse: use new options · abc4269b
  Marek Chalupa authored Mar 01, 2021
  
  abc4269b
- Extend options · a237d150
  Marek Chalupa authored Mar 01, 2021
  
  a237d150
- Use BSELFOptions instead of KindSEOptions · 39f03c07
  Marek Chalupa authored Mar 01, 2021
  
  39f03c07
- kindse: Add BSELFOptions · 3b31ca50
  Marek Chalupa authored Mar 01, 2021
  
  3b31ca50