Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Pardinus v1.2.0 #40

Merged
merged 268 commits into from
Aug 10, 2020
Merged

Pardinus v1.2.0 #40

merged 268 commits into from
Aug 10, 2020

Conversation

nmacedo
Copy link
Member

@nmacedo nmacedo commented Aug 5, 2020

Features

  • support for advanced SAT iteration operations, distinction between configuration and path iteration
  • support for advanced iteration operations for decomposed strategy
  • support for unsat cores for temporal formulas
  • support for bounded model checking with the electrod backend
  • disabled iteration through formulas for non SAT backend

Minor

  • iteration implemented at the SAT level
  • fixed a bug on the releases translation
  • fixed a bug when translating constants under unrolled traces
  • fixed a bug when evaluating past expressions
  • better handling of unsupported features of different backends
  • better reporting of stats for iterative temporal and decomposed solving
  • travis integration
  • updated temporal operators nomenclature (before, after, releases, triggered)
  • decomposed strategy no longer automatically iterates over integrated problems, not compatible with new operations
  • alternative instance encoding with some-disj pattern
  • support for electrod 0.7.1

@nmacedo nmacedo changed the title Pardinus v1.2 Pardinus v1.2.0 Aug 10, 2020
@nmacedo nmacedo merged commit 483e9dc into master Aug 10, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

1 participant