Verification Condition Generator

PyVCG is a utility library to generate VCs directly for CVC5 or standard-compliant SMTLIB2. The interface is deliberately generic and it should be easy to add API support for other solvers in the future.

This is pretty limited for now as the initial target is the expression language of TRLC.

Please refer to the Changelog for what's new.

Features

This library provides a wrapper around SMTLIB with some additional features:

• SMTLIB Scripts
• Automatic (minimal) logic discovery
• Basic sorts: Bool, Int, Real, and String
• Parametric sorts: Sequences
• Convenience wrappers around datatype sorts:
  • Enumerations
  • Records (including self-recursive records)
  • Optionals
• Uninterpreted functions
• Quantifiers
• Boolean expressions: not, and, or, xor, implication
• If-then-else expressions
• Comparisons: =, <, >, <=, >=
• Int -> Real conversion
• Real -> Int conversion (smtlib rounding (round-to-negative) and arithmetic rounding (round-nearest-away))
• Unary arithmetic: -, abs
• Binary Int arithmetic: +, -, *, smtlib div, smtlib mod, python div, ada remainder
• Binary Real arithmetic: +, -, *, /
• String operations: length, contains, prefix, suffix, concatenation
• Sequence operations: length, contains, access, concatenation
• Record operations: access, check for null (for recursive records)
• Optional operations: value, check for null

In addition this library provides a graph to build VCs with multiple paths; and generating VCs for all paths. FastWP and higher-level modelling for language features (e.g. ite, loops) are planned later.

Drivers

Current support for outputs:

• SMTLIB File Output (for debugging)
• CVC5 via Python API (for solving)
• CVC5 via Binary + SMTLIB (for solving)

When getting models, both API and SMTLIB drivers translate back to Python values. For example if you have an optional Int, then asking for the model value you will get e.g. None, 0, 1, ...

Dependencies

Run-time

• Python >= 3.8
• cvc5

Development

• GNU Make
• coverage
• pycodestyle
• pylint

Copyright & License

The sole copyright holder is Florian Schanda.

This library is licensed under the GNU GPL version 3 (or later).