Metadata-Version: 2.4
Name: pyvcg
Version: 1.0.10
Summary: Verification Condition Generator
Home-page: https://github.com/florianschanda/PyVCG
Author: Florian Schanda
Author-email: florian@schanda.org.uk
License: GNU General Public License v3
Project-URL: Bug Tracker, https://github.com/florianschanda/PyVCG/issues
Project-URL: Documentation, https://github.com/pages/florianschanda/PyVCG/
Project-URL: Source Code, https://github.com/florianschanda/PyVCG
Classifier: Development Status :: 5 - Production/Stable
Classifier: Intended Audience :: Developers
Classifier: Intended Audience :: Science/Research
Classifier: License :: OSI Approved :: GNU General Public License v3 or later (GPLv3+)
Classifier: Operating System :: POSIX :: Linux
Classifier: Topic :: Scientific/Engineering :: Mathematics
Classifier: Topic :: Software Development :: Compilers
Requires-Python: >=3.8
Description-Content-Type: text/markdown
License-File: LICENSE
Provides-Extra: api
Requires-Dist: cvc5==1.3.2; extra == "api"
Dynamic: author
Dynamic: author-email
Dynamic: classifier
Dynamic: description
Dynamic: description-content-type
Dynamic: home-page
Dynamic: license
Dynamic: license-file
Dynamic: project-url
Dynamic: provides-extra
Dynamic: requires-python
Dynamic: summary

# Verification Condition Generator

PyVCG is a utility library to generate VCs directly for
[CVC5](https://cvc5.github.io) or standard-compliant
[SMTLIB2](http://smtlib.cs.uiowa.edu/). 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](https://github.com/bmw-software-engineering/trlc).

Please refer to the [Changelog](https://github.com/florianschanda/PyVCG/blob/main/CHANGELOG.md) 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](https://smtlib.cs.uiowa.edu/theories-Ints.shtml),
  [Real](https://smtlib.cs.uiowa.edu/theories-Reals.shtml), and
  [String](https://cvc5.github.io/docs-ci/docs-main/theories/strings.html)
* Parametric sorts:
  [Sequences](https://cvc5.github.io/docs-ci/docs-main/theories/sequences.html)
* 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](https://pypi.org/project/cvc5)

### Development

* [GNU Make](https://www.gnu.org/software/make)
* [coverage](https://pypi.org/project/coverage)
* [pycodestyle](https://pypi.org/project/pycodestyle)
* [pylint](https://pypi.org/project/pylint)

## Copyright & License

The sole copyright holder is Florian Schanda.

This library is licensed under the [GNU GPL version 3](https://github.com/florianschanda/PyVCG/blob/main/LICENSE) (or
later).
