pySMT: A library for SMT formulae manipulation and solving
Intermediate release that collects 2 years of bugfixes and improvements.
Python 2 was deprecated in version 0.9.0, and this version removes the use of compatible code for that version.
FNode.substitute in SmtLibExecutionCache by @EnricoMagnago in https://github.com/pysmt/pysmt/pull/699
Full Changelog: https://github.com/pysmt/pysmt/compare/v0.9.0...v0.9.5
General:
PySMT as module (PR #573): It is now possible to do
python -m pysmt install
and
python -m pysmt shell
while the tool pystm-install is still available, using the module syntax makes it easier to understand which version of python will be used, in case multiple interpreters co-exist.
Added functions to obtain the symbols in SMTLIB script (PR #583)
Python 2 is not supported anymore. While it might still work, we will not actively test for it anymore.
Solvers:
Boolector: Incremental and Unsat cores support (PR #591, #567). Thanks Makai Mann for providing the patch.
Picosat: Fixed a bug related to solver reset (PR #567)
Boolector: Upgrade to 3.2.1
MathSAT: Upgrade to 5.6.1
Bugfix:
Collections.abc: fix deprecation warning (PR #574, PR #562). Thanks to Liana Hadarean and Caleb Donovick.
PysmtSyntaxError: Fix missing message constructor (PR #576). Thanks to Liana Hadarean for providing a fix.
Version: Static version in make_distrib.sh (PR #575)
Fix simplifier StrIndexOf capitalization (PR #563). Thanks to Makai Mann for providing the patch.
Sort the arguments of Times while simplifying (PR #561). Thanks to Ahmed Irfan for providing the patch.
Fix bug in deque pop in smtlib/parser (PR #558). Thanks to Sebastiano Mariani for providing the patch.
Function names quoted with ' instead of | when seraializing to smt2 (PR #584). Thanks Kevin Laeufer for reporting this.
Fix assertion tracking for boolector (PR #589). Thanks Makai Mann for providing the patch.
Handle one-bit shifts in btor (PR #592) Thanks Makai Mann for providing the patch.
Fix issue with bv conversion in Yices (PR #597). Thanks to @nano-o for reporting this.
Fix Mathsat signature for BV_CONCAT (PR #598). Thanks Makai Mann for providing the patch.
Support n-ary BVConcat (PR #621). Thanks to Ridwan Shariffdeen for reporting this.
Fix a correctness issue when reading from SMT-LIB interface (Issue #616, #615, PR #619). Thanks to Sergio Mover for reporting this.
Clear pending assertions in IncrementalTrackingSolver.assertions (PR #627). Thanks to Enrico Magnago for reporting this.
Various documentation fixes. Thanks to Matthew Fernandez, Guillem Francès, and Gianluca Redondi.
Disable multiprocessing in run_tests.sh script (PR #637). Thanks Patrick Trentin for reporting this.
BACKWARDS INCOMPATIBLE CHANGES:
Disabled support for interpolation in Z3, since this is not available anymore up-stream
Deprecation Warning:
This release is the last release to support Python 2.7. Starting from 0.9.0 only Python 3+ will be supported.
General:
Solver installation within site-package (PR #517). pysmt-install now installs the solvers within the site-package directory (by default). This makes it possible to work with virtual environments, and does not require anymore to export the Python path, greatly simplifying the installation process. Thanks to Radomi Stevanovic for contributing the patch.
Simplify shared lib usage (PR #494): Modify z3 and msat installers in order to make their shared binary objects (libraries/dlls) auto-discoverable, without the need for setting LD_LIBRARY_PATH/PATH. Thanks to Radomir Stevanovic for contributing the patch.
BV Simplification (PR #531): Multiple improvements on the simplification of BV expressions. Thanks to Haozhong Zhang for contributing the patch.
Ackermannization (PR #515): Add support for Ackermannization in pysmt.rewritings. Thanks to Yoni Zohar for contributing the patch.
FNode.bv_str: Multiple format for BV printing (PR #468)
Examples (PR #507): Extend model_checking example with PDR. Thanks to Cristian Mattarei for contributing the patch.
Docs: Tutorial on basic boolean solving (PR #535)
Tests: Removed old warning and other clean-ups (PR #532, #512)
Warnings (PR #497): Importing pysmt.shortcuts will only raise warnings within pySMT, instead of all warnings from external libraries.
Examples (PR #541): Add example for the theory of Strings
Top-Level Propagator (PR #544): Add a basic toplevel-propagation functionality to propagate definitions of the form: variable = constant, variable = variable, constant = constant . Thanks to Ahmed Irfan for providing this feature.
Clean-up debug print from SMT parser (PR #543): Thanks to Ahmed Irfan for providing this patch.
Solvers:
Yices: Upgrade to 2.6.0 (PR #509).
Boolector: Upgrade to 3.0.1-pre (7f5d32) (PR #514)
CVC4: Upgrade to 1.7-prerelease (PR #552) Known issue: Passing options to CVC4 fails sometimes.
Z3: Upgrade to 4.8.4 (PR #550). Removed support for interpolation. Known issue: Some tests on use of tactics exhibit some random failures on Travis.
Yices: Add support for OSX (PR #486). Thanks to Varun Patro for contributing the patch.
SMTLIB Solver (PR #524): Add support for custom sorts in SMT-LIB interface. Thanks to Yoni Zohar for contributing the patch.
MathSAT (PR #526): Add option to support preferred variables with polarity. Thanks to Cristian Mattarei for providing the patch.
Bugfix:
SmtLib parser (PR #521): Fix StopIteration error. The error would make it impossible to use the parser with Python 3.7. The fix changes the structure of the parser, in order to separate cases in which we know that there is a token to consume (function consume) and when we want to consume a token only if available (function consume_maybe). Thanks to @samuelkolb and Kangjing Huang for reporting this.
Boolector: Fixed bug in LShl and LShr conversion (PR #534)
Z3 (PR #530, #528): Fixed race condition during context deletion. The race condition would cause pySMT to segfault on certain situations. Thanks to Haozhong Zhang for helping us reproduce the issue and to @Johanvdberg for reporting it.
MathSAT (PR #518): Fix installation error on darwin. Thanks to Lenny Truong for contributing the patch.
Fix declare-sort bug (PR #501). Thanks to Yoni Zohar for contributing the patch.
Fix docstring for BVAShr (PR #503). Thanks to Mathias Preiner for contributing the patch.
Fix yices compilation on OSX without AVX2 instruction (PR #491)
Fix PysmtTypeError when reusing symbols in SMT-LIB define-fun (PR #502). Thanks to Yoni Zohar for contributing the patch.
Fix doublequote escaping (PR #489). Thanks to Lukas Dresel for contributing the patch.
Fix pySMT CLI for Python3 (PR #493). Thanks to Radomir Stevanovic for contributing the patch.
General:
Strings Theory (#458)
Add support for the theory of Strings as supported by CVC4.
Direct solver support is limited to CVC4, but the SMT-LIB interface can be used to integrate with other solvers (e.g., Z3).
This feature was largely implemented by Suresh Goduguluru and motivated by Clark Barrett.
SMT-LIB Parser: Improved performance with Cython (PR #432)
The SMT-LIB parser module is now compiled using Cython behind the scenes. By default pySMT will try to use the cython version but the behavior can be controlled via env variables::
PYSMT_CYTHON=False # disable Cython PYSMT_CYTHON=True # force Cython: Raises an error if cython or the # SMT-LIB parser module are not available. unset PYSMT_CYTHON # defaults to Cython but silently falls back to #pure-python version
The API of pysmt.smtlib.parser does not change and preserves
compatibility with previous versions.
Benchmarking on parse_all.py shows: ::
$ PYSMT_CYTHON=True python3.5 parse_all.py --count 500 The mean execution time was 2.34 seconds The max execution time was 59.77 seconds
$ PYSMT_CYTHON=False python3.5 parse_all.py --count 500 The mean execution time was 3.39 seconds The max execution time was 85.46 seconds
SMT-LIB Parser: Added Debugging Information (Line/Col number) (PR #430)
pysmt-install: Simplified solver version check (PR #431)
Extended infix notation to support:
Examples: Quantifier Elimination in LRA (PR #447)
Sorts: Stronger type checking for composite sorts (PR #449)
BvToNatural: Introduced new operator to convert bitvectors into natural numbers (PR #450)
Examples: Theory Combination (PR #451)
QE: Introduce new QE techniques based on Self-Substitution (PR #460)
Solvers:
Z3: Upgrade to 4.5.1 dev (082936bca6fb) (PR #407)
CVC4: Upgrade to 1.5 (PR #424)
MathSAT: Upgrade to 5.5.1 (PR #453)
MathSAT: Add Windows Support (PR #453)
Theories:
Bugfix:
Z3: Conversion of top-level ITE (PR #433)
Z3: Fixed exception handling (PR #473): Thanks to Bradley Ellert for reporting this.
Detect BV type in Array and Function when using infix notation (PR #436)
Support GMPY objects in BV construction (PR #441)
SMT-LIB: Fixed parsing of #x BV constants (PR #443): Thanks to @cdmcdonell for reporting this.
SMT-LIB: Remove trailing whitespace from bvrol and bvsext (PR #459)
Fixed type-checking of Equals, LT and LE (PR #452)
Examples: Revised Einstein example (PR #448): Thanks to Saul Fuhrmann for reporting the issue.
Examples: Fixed indexing and simple path condition in MC example (PR 454): Thanks to Cristian Mattarei for contributing this patch.
Fixed installer for picosat to use HTTPS (PR #481)
BACKWARDS INCOMPATIBLE CHANGES:
General:
Class-Based Walkers (PR #359):
Walkers behavior is now defined in the class definition. Processing an AND node always calls walk_and. This makes it possible to subclass and override methods, but at the same time call the
implementation of a super class, e.g.:
def walk_and(...):
return ParentWalker.walk_and(self, ....)
The utility method Walker.super is provided to automatically handle the dispatch of a node to the correct walk_* function, e.g.,:
def walk_bool_to_bool(...):
return ParentWalker._super(self, ....)
The method Walker.set_functions is deprecated, but kept for compatibility with old-style walkers. Using set_functions has the same effect as before. However, you cannot modify a subclass of a walker
using set_functions. You should not be using set_functions anymore!
The method Walker.set_handler is used to perform the same operation of set_function at the class level. The associated decorator @handles can be used to associate methods with nodetypes.
These changes make it possible to extend the walkers from outside pySMT, without relying on hacks like the Dynamic Walker Factory (DWF). See examples/ltl.py for a detailed example.
Introduce the support for custom sorts (PySMTTypes) (PR #375)
Two new classes are introduced: _Type and PartialType
PartialType is used to represent the concept of SMT-LIB "define-sort". The class _TypeDecl is used to represents a Type declaration, and as such cannot be used directly to instantiate a Symbol. This capture the semantics of declare-sort. A wrapper Type() is given to simplify its use, and making 0-arity sorts a special case. The following two statements are equivalent:
Type("Colors")
Type("Colors", 0)
0-ary type are instantiated by default. For n-ary types, the type needs to be instantiated. This can be done with the method TypeManager.get_type_instance or by using infix notation (if enabled):
type_manager.get_type_instance(Type(Pair, 2), Int, Int))
Type(Pair, 2)(Int, Int)
Type declarations and Type instances are memoized in the environment, and suitable shortucts have been introduced. Logics definition has been extended with the field custom_types to detect the use of custom types. Note: Due to the limited support of custom types by solvers, by default every SMT-LIB logic
is defined with custom_types=False.
Add shortcuts.to_smtlib() to easily dump an SMT-LIB formula
Add explicit support for BV and UFBV logics (PR #423): Thanks to Alexey Ignatiev for reporting this.
Solvers:
Bugfix:
is_unsat (PR #428)General:
Portfolio Solver (PR #284):
Created Portfolio class that uses multiprocessing to solve the
problem using multiple solvers. get_value and get_model work after a
SAT query. Other artifacts (unsat-core, interpolants) are not
supported.
Factory.is_* methods have been extended to include portfolio
key-word, and exported as is_* shortcuts. The syntax becomes:
is_sat(f, portfolio=["s1", "s2"])
Coverage has been significantly improved, thus giving raise to some clean-up of the tests and minor bug fixes. Thanks to Coveralls.io for providing free coverage analysis. (PR #353, PR #358, PR #372)
Introduce PysmtException, from which all exceptions must inherit. This also introduces hybrid exceptions that inherit both from the Standard Library and from PysmtException (i.e., PysmtValueError). Thanks to Alberto Griggio for suggesting this change. (PR #365)
Windows: Add support for installing Z3. Thanks to Samuele Gallerani for contributing this patch. (PR #385)
Arrays: Improved efficiency of array_value_get (PR #357)
Documentation: Thanks to the Hacktoberfest for sponsoring these activities:
smtlibscript_from_formula(): Allow the user to specify a custom logic. Thanks to Alberto Griggio for contributing this patch. (PR #360)
Solvers:
Bugfix:
pysmt-install --env. Thanks to Marco Roveri
(@marcoroveri) for pointing this out.BACKWARDS INCOMPATIBLE CHANGES:
Integer, Fraction and Numerals are now defined in pysmt.constants (see below for details). The breaking changes are:
Non-Recursive TreeWalker (PR #322)
Modified TreeWalker to be non-recursive. The algorithm works by keeping an explicit stack of the walking functions that are now required to be generators. See pysmt.printer.HRPrinter for an example. This removes the last piece of recursion in pySMT !
Times is now an n-ary operator (Issue #297 / PR #304)
Functions operating on the args of Times (e.g., rewritings) should be adjusted accordingly.
Simplified module pysmt.parsing into a unique file (PR #301)
The pysmt.parsing module was originally divided in two files: pratt.py and parser.py. These files were removed and the parser combined into a unique parsing.py file. Code importing those modules directly needs to be updated.
Use solver_options to specify solver-dependent options (PR #338):
Removed deprecated methods (PR #332):
General:
Support for GMPY2 to represent Fractions (PR #309).
Usage of GMPY2 can be controlled by setting the env variable PYSMT_GMPY to True or False. By default, pySMT tries to use GMPY2 if installed, and fallbacks on Python's Fraction otherwise.
Constants module: pysmt.constants (PR #309)
This module provides an abstraction for constants Integer and Fraction, supporting different ways of representing them internally. Additionally, this module provides several utility methods:
Conversion can be achieved via:
Add Version information (Issue #299 / PR #303)
install.py (pysmt-install) and shell.py gain a new --version option that uses git_version to display the version information.
Shortcuts: read_smtlib() and write_smtlib()
Docs: Completely Revised the documentation (PR #294)
Rewritings: TimesDistributor (PR #302)
Perform distributivity on an N-ary Times across addition and subtraction.
SizeOracle: Add MEASURE_BOOL_DAG measure (PR #319)
Measure the Boolean size of the formula. This is equivalent to replacing every theory expression with a fresh boolean variable, and measuring the DAG size of the formula. This can be used to estimate the Boolean complexity of the SMT formula.
PYSMT_SOLVERS controls available solvers (Issue #266 / PR #316):
Using the PYSMT_SOLVER system environment option, it is possible to restrict the set of installed solvers that are actually accessible to pySMT. For example, setting PYSMT_SOLVER="msat,z3" will limit the accessible solvers to msat and z3.
Protect FNodeContent.payload access (Issue #291 / PR 310)
All methods in FNode that access the payload now check that the FNode instance is of the correct type, e.g.:
FNode.symbol_name() checks that FNode.is_symbol()
This prevents from accessing the payload in a spurious way. Since this has an impact on every access to the payload, it has been implemented as an assertion, and can be disabled by running the interpreter with -O.
Solvers:
Z3 Converter Improvements (PR #321):
OSX: Z3 and MathSAT can be installed with pysmt-install (PR #244)
MathSAT: Upgrade to 5.3.13 (PR #305)
Yices: Upgrade to 2.5.1
Better handling of solver options (PR #338):
Solver constructor takes the optional dictionary solver_options
of options that are solver dependent. It is thus possible to
directly pass options to the underlying solver.
Bugfix:
array_value_assigned_values_map, returning the
incorrect values for an Array constant value. Thanks to
Daniel Ricardo dos Santos for pointing this out and submitting
the patch.get_unsat_core (PR #331), that could
lead to an unbounded mutual recursion. Thanks to Ahmed Irfan for
reporting this (PR #331)Theories:
General:
Solvers:
Bugfix:
BACKWARDS INCOMPATIBLE CHANGES:
MGSubstituter becomes the new default substitution method (PR #253)
When performing substitution with a mapping like {a: b, Not(a), c}, Not(a) is considered before a. The previous
behavior (MSSubstituter) would have substituted a first, and
then the rule for Not(a) would not have been applied.
Removed argument user_options from Solver()
Theories:
Added support for the Theory of Arrays.
In addition to the SMT-LIB definition, we introduce the concept of Constant Array as supported by MathSAT and Z3. The theory is currently implemented for MathSAT, Z3, Boolector, CVC4.
Thanks to Alberto Griggio, Satya Uppalapati and Ahmed Irfan for contributing through code and discussion to this feature.
General:
Simplifier: Enable simplification if IFF with constant: e.g., (a <-> False) into !a
Automatically enable Infix Notation by importing shortcuts.py (PR #267)
SMT-LIB: support for define-sort commands without arguments
Improved default options for shortcuts:
Improved handling of options in Solvers (PR #250):
Solver() takes **options as free keyword arguments. These options are checked by the class SolverOptions, in order to validate that these are meaningful options and perform a preliminary validation to catch typos etc. by raising a ValueError exception if the option is unknown.
It is now possible to do: Solver(name="bdd", dynamic_reordering=True)
Solvers:
Bugfixes:
General:
Solvers:
Bugfix: