Commits · 38555b9dd41340c90b5ebc70374203e1c415c632 · Martin Jonáš / BWReducingSolver

Jun 25, 2019
- Do not let Z3 create let expressions. · 38555b9d
  Martin Jonáš authored Jun 25, 2019
  
  38555b9d
- Reduce also subexpressions of extract. · f16c36da
  Martin Jonáš authored Jun 25, 2019
  
  f16c36da
- Add concat and extract. · 85487924
  Martin Jonáš authored Jun 25, 2019
  
  85487924
Jun 20, 2019
- Extend: Fix ITE. · b013e4b2
  Martin Jonáš authored Jun 20, 2019
  
  b013e4b2
- Fix conversion to NNF. · 97c8b55f
  Martin Jonáš authored Jun 20, 2019
  
  97c8b55f
Jun 19, 2019
- Remove debug output. · ec2366a7
  Martin Jonáš authored Jun 19, 2019
  
  ec2366a7
- Add regression test. · 46b553b4
  Martin Jonáš authored Jun 19, 2019
  
  46b553b4
- Dual solver: Fix adding implicit existentials. · fae6c6ba
  Martin Jonáš authored Jun 19, 2019
  
  fae6c6ba
Jun 18, 2019
- Fixes. · fc62e279
  Martin Jonáš authored Jun 18, 2019
  
  fc62e279
Jun 14, 2019
- Plug-in the rewritten solver into main app. · 388ec2d9
  Martin Jonáš authored Jun 14, 2019
  
  388ec2d9
- Implement proper solver using extensions. · 0a6ca549
  Martin Jonáš authored Jun 14, 2019
  
  0a6ca549
Jun 12, 2019
- Call Boolector via Boost. · 58377f1e
  Martin Jonáš authored Jun 12, 2019
  
  58377f1e
- Start rewriting the solver. · e8fc958e
  Martin Jonáš authored Jun 12, 2019
  
  e8fc958e
- Add parser and tests. · 891d3851
  Martin Jonáš authored Jun 12, 2019
  
  891d3851
- Initial dirty version · 51ef708c
  Martin Jonáš authored Jun 12, 2019
  
  51ef708c