User Tools

Site Tools



  • What has been implemented
  • Future needs
  • Adaptations required

Needs: support for

  • interpolants: nothing implemented so far inside CPROVER (Matt uses Princess and Wolverine)
  • nested data structures: implementation for Z3 partly exists (using data types, which are not yet SMT-LIB2 standard). There are problems with arrays in structs (flattening vs. SMT2 encoding), agreement on SMT2 subset that is supported by most solvers needed
  • arrays: currently implemented for Z3, but counterexamples (using UIF) are not read from the SMT2 output
  • floating point: implementation for MathSAT (other potential solvers: Z3, Sonolar, CVC4)
  • heap theory: will be implemented using new ACDL backend
  • UNSAT cores: some support for Z3
  • conflicting assumptions: MiniSAT2 feature, works
  • incremental BMC: support for MiniSAT2 is on the way; for SMT solvers, the current file-based interface is not suitable; we do not want to support solver-specific APIs

Action items:

  • Settle on a proper S-expression parser, probably bison based.
  • Switch to invoking solver as a process communicated with via a pipe (to reduce disk accesses & looking forward, allow us to do incremental solving).
  • Create regression tests, add to automated build. To include: checking our output is (at least) parseable by the solvers we want to support (Z3, CVC, yices?, MathSAT).

Lower priority:

  • Rewrite problem generation code – think about removing dependency on flattening stuff, since it seems likely this gets rid of some of the problem structure. It also concretely introduces problems indexing into structs.
  • Add support for interpolants.
  • Add unsat cores.
  • Floating point.
  • Heap theories.

Nobody has time to work on this until the end of October at the earliest. Martin, Peter, Bjoern and Matt plan to instigate a No Research November, in which we do no research in November and just work on the SMT2 backend.

smt2backendreboot.txt · Last modified: 2013/08/13 18:30 by bucheli