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.
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
- Datatype sorts: Enumerations and Records
- 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
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.
Current support for outputs:
- SMTLIB (for writing and debugging)
- CVC5 API (for solving)
- Python >= 3.8
- cvc5
The sole copyright holder is Florian Schanda.
This library is licensed under the GNU GPL version 3 (or later).