pySMT 0.7.0: Class Based Walkers and Sorts

[Marco Gario]

pySMT 0.7.0 is out!

This release changes and simplifies the way we construct walkers by defining the mapping between methods and node types at the level of the class (as opposed to the instance). This makes it much easier and clean to extend existing walkers.See [1] for a representative example.

The other big change concerns a better handling of types/sorts. In brief, we are now able to handle the SMT-LIB declare-sort command. This brings us closer to a full handling of SMT-LIB!

Many other changes in this version are described in the release notes [2]. Thanks to everybody that provided feedback and patches for this release.


pySMT Team

[1] https://github.com/pysmt/pysmt/blob/master/pysmt/oracles.py#L174
[2] http://pysmt.readthedocs.io/en/latest/CHANGES.html#class-based-walkers-and-sorts

--

BACKWARDS INCOMPATIBLE CHANGES:

* Removed option "quantified" in Solver (PR #377)

* Removed deprecated CNFizer.printer method (PR #359)

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:

* PicoSAT: Upgrade to 965 (PR #425)

* Boolector: Upgrade to 2.4.1 (PR #422)

* CVC4: Fixed memory-leak (PR #419)

* Yices: Upgrade to 2.5.2 (PR #426)


Bugfix:

* Fixed assumption handling in the Boolector wrapper. Thanks to
  **Alexey Ignatiev** for contributing with this patch!

* Fix cyclic imports (PR #406). Thanks to **@rene-rex** for reporting
  this.

* Fixed SMT-LIB Script serialization to default to a daggified
  representation. (PR #418)

* Fixed SMT-LIB Parsing of declare-const . Thanks to
  **@ahmedirfan1983** for reporting this. (PR #429)

* Fixed logic detection when calling is_unsat (PR #428)