Commit 6cda0234 authored by Mathias Preiner's avatar Mathias Preiner
Browse files

Squashed commit of the following:

commit feaf62dbaad5e62755def46c891662b4efb76245
Author: Mathias Preiner <>
Date:   Wed May 26 16:18:02 2021 -0700

    Migrate benchmarks from pending repository.

commit a2d1d94a
Author: Mathias Preiner <>
Date:   Thu Feb 18 10:09:59 2021 -0800

parent b46af7e2
This diff is collapsed.
(set-info :smt-lib-version 2.6)
(set-logic QF_DT)
(set-info :source |
Generated by: Pierre Bouvier
Generated on: 2021-03-12
Application: Automatic decomposition of Petri Nets into Automata Networks
Target solver: CVC4, Z3
[1] Pierre Bouvier, Hubert Garavel, and Hernan Ponce de Leon.
"Automatic Decomposition of Petri Nets into Automata Networks -
A Synthetic Account". Proceedings PETRI NETS 2020, LNCS 12152,
[2] Hubert Garavel. "Nested-Unit Petri Nets". Journal of Logical
and Algebraic Methods in Programming, vol. 104, Elsevier, 2019.
In [1], several methods for decomposing an ordinary, safe Petri net
into a flat, unit-safe NUPN [2], have been proposed. These methods
are implemented in a complete tool chain involving SAT solvers, SMT
solvers, and tools for graph coloring and finding maximal cliques.
From a data set of 12,000+ NUPN models, 51,000+ SMT formulas have
been generated, out of which a subset of 1200 interesting formulas
to be used as SMT-LIB 2.6 benchmarks was carefully selected.
Original filename: vlsat3_b40.smt2
Specific parameters for the present benchmark:
- number of places: 36
- number of units: 14
- number of edges in the concurrency graph: 374
- number of variables: 36
- number of uninterpreted functions: 0
- number of asserts: 387
- total number of operators in asserts: 1341
(set-info :license "")
(set-info :category "industrial")
(set-info :status unsat)
(declare-datatype Unit ((u0) (u1) (u2) (u3) (u4) (u5) (u6) (u7) (u8) (u9) (u10) (u11) (u12) (u13)))
(declare-fun p1 () Unit)
(declare-fun p2 () Unit)
(declare-fun p3 () Unit)
(declare-fun p4 () Unit)
(declare-fun p5 () Unit)
(declare-fun p6 () Unit)
(declare-fun p7 () Unit)
(declare-fun p8 () Unit)
(declare-fun p9 () Unit)
(declare-fun p10 () Unit)
(declare-fun p11 () Unit)
(declare-fun p12 () Unit)
(declare-fun p13 () Unit)
(declare-fun p14 () Unit)
(declare-fun p15 () Unit)
(declare-fun p16 () Unit)
(declare-fun p17 () Unit)
(declare-fun p18 () Unit)
(declare-fun p19 () Unit)
(declare-fun p20 () Unit)
(declare-fun p21 () Unit)
(declare-fun p22 () Unit)
(declare-fun p23 () Unit)
(declare-fun p24 () Unit)
(declare-fun p25 () Unit)
(declare-fun p26 () Unit)
(declare-fun p27 () Unit)
(declare-fun p28 () Unit)
(declare-fun p29 () Unit)
(declare-fun p30 () Unit)
(declare-fun p31 () Unit)
(declare-fun p32 () Unit)
(declare-fun p33 () Unit)
(declare-fun p34 () Unit)
(declare-fun p35 () Unit)
(declare-fun p36 () Unit)
(assert (= p1 u0))
(assert (or (= p2 u0) (= p2 u1)))
(assert (or (= p3 u0) (= p3 u1) (= p3 u2)))
(assert (or (= p4 u0) (= p4 u1) (= p4 u2) (= p4 u3)))
(assert (or (= p5 u0) (= p5 u1) (= p5 u2) (= p5 u3) (= p5 u4)))
(assert (or (= p6 u0) (= p6 u1) (= p6 u2) (= p6 u3) (= p6 u4) (= p6 u5)))
(assert (or (= p7 u0) (= p7 u1) (= p7 u2) (= p7 u3) (= p7 u4) (= p7 u5) (= p7 u6)))
(assert (or (= p8 u0) (= p8 u1) (= p8 u2) (= p8 u3) (= p8 u4) (= p8 u5) (= p8 u6) (= p8 u7)))
(assert (or (= p9 u0) (= p9 u1) (= p9 u2) (= p9 u3) (= p9 u4) (= p9 u5) (= p9 u6) (= p9 u7) (= p9 u8)))
(assert (or (= p10 u0) (= p10 u1) (= p10 u2) (= p10 u3) (= p10 u4) (= p10 u5) (= p10 u6) (= p10 u7) (= p10 u8) (= p10 u9)))
(assert (or (= p11 u0) (= p11 u1) (= p11 u2) (= p11 u3) (= p11 u4) (= p11 u5) (= p11 u6) (= p11 u7) (= p11 u8) (= p11 u9) (= p11 u10)))
(assert (or (= p12 u0) (= p12 u1) (= p12 u2) (= p12 u3) (= p12 u4) (= p12 u5) (= p12 u6) (= p12 u7) (= p12 u8) (= p12 u9) (= p12 u10) (= p12 u11)))
(assert (or (= p13 u0) (= p13 u1) (= p13 u2) (= p13 u3) (= p13 u4) (= p13 u5) (= p13 u6) (= p13 u7) (= p13 u8) (= p13 u9) (= p13 u10) (= p13 u11) (= p13 u12)))
(assert (distinct p5 p31))
(assert (distinct p20 p25))
(assert (distinct p6 p28))
(assert (distinct p21 p28))
(assert (distinct p17 p20))
(assert (distinct p18 p19))
(assert (distinct p23 p26))
(assert (distinct p14 p31))
(assert (distinct p15 p30))
(assert (distinct p11 p22))
(assert (distinct p1 p28))
(assert (distinct p13 p20))
(assert (distinct p2 p27))
(assert (distinct p4 p5))
(assert (distinct p5 p24))
(assert (distinct p20 p32))
(assert (distinct p28 p32))
(assert (distinct p7 p22))
(assert (distinct p5 p34))
(assert (distinct p8 p12))
(assert (distinct p18 p36))
(assert (distinct p10 p14))
(assert (distinct p8 p18))
(assert (distinct p11 p15))
(assert (distinct p1 p21))
(assert (distinct p2 p18))
(assert (distinct p3 p11))
(assert (distinct p1 p15))
(assert (distinct p2 p12))
(assert (distinct p24 p33))
(assert (distinct p1 p33))
(assert (distinct p6 p14))
(assert (distinct p20 p21))
(assert (distinct p17 p24))
(assert (distinct p18 p31))
(assert (distinct p8 p25))
(assert (distinct p9 p20))
(assert (distinct p24 p28))
(assert (distinct p14 p19))
(assert (distinct p11 p26))
(assert (distinct p26 p30))
(assert (distinct p4 p11))
(assert (distinct p2 p7))
(assert (distinct p5 p10))
(assert (distinct p3 p22))
(assert (distinct p2 p33))
(assert (distinct p26 p34))
(assert (distinct p22 p36))
(assert (distinct p5 p20))
(assert (distinct p20 p28))
(assert (distinct p16 p20))
(assert (distinct p30 p36))
(assert (distinct p22 p30))
(assert (distinct p18 p22))
(assert (distinct p14 p26))
(assert (distinct p10 p26))
(assert (distinct p11 p19))
(assert (distinct p12 p20))
(assert (distinct p1 p25))
(assert (distinct p2 p30))
(assert (distinct p4 p24))
(assert (distinct p5 p29))
(assert (distinct p20 p27))
(assert (distinct p6 p18))
(assert (distinct p21 p26))
(assert (distinct p8 p33))
(assert (distinct p14 p29))
(assert (distinct p15 p24))
(assert (distinct p1 p18))
(assert (distinct p13 p18))
(assert (distinct p2 p25))
(assert (distinct p20 p34))
(assert (distinct p28 p34))
(assert (distinct p5 p32))
(assert (distinct p16 p24))
(assert (distinct p10 p34))
(assert (distinct p8 p14))
(assert (distinct p18 p34))
(assert (distinct p8 p20))
(assert (distinct p10 p22))
(assert (distinct p2 p16))
(assert (distinct p1 p13))
(assert (distinct p4 p14))
(assert (distinct p2 p10))
(assert (distinct p24 p35))
(assert (distinct p5 p15))
(assert (distinct p4 p20))
(assert (distinct p2 p36))
(assert (distinct p22 p35))
(assert (distinct p20 p23))
(assert (distinct p30 p35))
(assert (distinct p17 p30))
(assert (distinct p11 p32))
(assert (distinct p18 p29))
(assert (distinct p8 p27))
(assert (distinct p9 p26))
(assert (distinct p24 p30))
(assert (distinct p14 p17))
(assert (distinct p15 p20))
(assert (distinct p11 p28))
(assert (distinct p26 p28))
(assert (distinct p1 p6))
(assert (distinct p13 p30))
(assert (distinct p2 p5))
(assert (distinct p5 p8))
(assert (distinct p3 p24))
(assert (distinct p26 p32))
(assert (distinct p5 p18))
(assert (distinct p20 p30))
(assert (distinct p16 p22))
(assert (distinct p7 p28))
(assert (distinct p22 p28))
(assert (distinct p18 p20))
(assert (distinct p13 p35))
(assert (distinct p14 p24))
(assert (distinct p10 p24))
(assert (distinct p11 p21))
(assert (distinct p12 p22))
(assert (distinct p2 p28))
(assert (distinct p14 p36))
(assert (distinct p4 p26))
(assert (distinct p5 p27))
(assert (distinct p21 p24))
(assert (distinct p4 p32))
(assert (distinct p8 p35))
(assert (distinct p22 p23))
(assert (distinct p9 p34))
(assert (distinct p15 p26))
(assert (distinct p1 p16))
(assert (distinct p2 p23))
(assert (distinct p1 p10))
(assert (distinct p6 p11))
(assert (distinct p7 p18))
(assert (distinct p16 p26))
(assert (distinct p18 p32))
(assert (distinct p8 p22))
(assert (distinct p24 p25))
(assert (distinct p10 p20))
(assert (distinct p11 p25))
(assert (distinct p1 p3))
(assert (distinct p4 p8))
(assert (distinct p28 p29))
(assert (distinct p2 p8))
(assert (distinct p5 p13))
(assert (distinct p30 p31))
(assert (distinct p4 p22))
(assert (distinct p19 p22))
(assert (distinct p2 p34))
(assert (distinct p7 p11))
(assert (distinct p22 p33))
(assert (distinct p5 p23))
(assert (distinct p23 p36))
(assert (distinct p30 p33))
(assert (distinct p17 p28))
(assert (distinct p7 p33))
(assert (distinct p22 p27))
(assert (distinct p11 p34))
(assert (distinct p18 p27))
(assert (distinct p8 p29))
(assert (distinct p9 p24))
(assert (distinct p14 p23))
(assert (distinct p15 p22))
(assert (distinct p11 p30))
(assert (distinct p1 p4))
(assert (distinct p13 p28))
(assert (distinct p14 p35))
(assert (distinct p3 p26))
(assert (distinct p5 p16))
(assert (distinct p20 p24))
(assert (distinct p3 p32))
(assert (distinct p7 p30))
(assert (distinct p14 p30))
(assert (distinct p11 p23))
(assert (distinct p1 p29))
(assert (distinct p2 p26))
(assert (distinct p19 p36))
(assert (distinct p5 p25))
(assert (distinct p27 p36))
(assert (distinct p6 p22))
(assert (distinct p5 p35))
(assert (distinct p8 p11))
(assert (distinct p8 p17))
(assert (distinct p1 p22))
(assert (distinct p13 p14))
(assert (distinct p2 p21))
(assert (distinct p3 p8))
(assert (distinct p1 p8))
(assert (distinct p2 p15))
(assert (distinct p24 p32))
(assert (distinct p1 p34))
(assert (distinct p16 p28))
(assert (distinct p18 p30))
(assert (distinct p8 p24))
(assert (distinct p24 p27))
(assert (distinct p14 p18))
(assert (distinct p10 p18))
(assert (distinct p11 p27))
(assert (distinct p12 p28))
(assert (distinct p28 p31))
(assert (distinct p2 p6))
(assert (distinct p5 p11))
(assert (distinct p19 p24))
(assert (distinct p5 p21))
(assert (distinct p6 p26))
(assert (distinct p17 p18))
(assert (distinct p22 p25))
(assert (distinct p11 p36))
(assert (distinct p18 p25))
(assert (distinct p23 p28))
(assert (distinct p8 p31))
(assert (distinct p9 p30))
(assert (distinct p14 p21))
(assert (distinct p11 p16))
(assert (distinct p1 p26))
(assert (distinct p13 p26))
(assert (distinct p14 p33))
(assert (distinct p3 p28))
(assert (distinct p15 p36))
(assert (distinct p5 p30))
(assert (distinct p20 p26))
(assert (distinct p8 p32))
(assert (distinct p7 p24))
(assert (distinct p14 p28))
(assert (distinct p12 p18))
(assert (distinct p1 p19))
(assert (distinct p2 p24))
(assert (distinct p3 p5))
(assert (distinct p20 p33))
(assert (distinct p6 p20))
(assert (distinct p21 p36))
(assert (distinct p28 p33))
(assert (distinct p29 p36))
(assert (distinct p8 p13))
(assert (distinct p8 p19))
(assert (distinct p11 p14))
(assert (distinct p9 p18))
(assert (distinct p1 p20))
(assert (distinct p2 p19))
(assert (distinct p1 p14))
(assert (distinct p2 p13))
(assert (distinct p24 p34))
(assert (distinct p1 p32))
(assert (distinct p7 p14))
(assert (distinct p22 p34))
(assert (distinct p20 p22))
(assert (distinct p16 p30))
(assert (distinct p6 p33))
(assert (distinct p30 p34))
(assert (distinct p11 p33))
(assert (distinct p18 p28))
(assert (distinct p8 p26))
(assert (distinct p24 p29))
(assert (distinct p14 p16))
(assert (distinct p11 p29))
(assert (distinct p26 p31))
(assert (distinct p12 p30))
(assert (distinct p27 p30))
(assert (distinct p1 p7))
(assert (distinct p5 p9))
(assert (distinct p25 p36))
(assert (distinct p4 p18))
(assert (distinct p19 p26))
(assert (distinct p26 p35))
(assert (distinct p5 p19))
(assert (distinct p20 p29))
(assert (distinct p6 p24))
(assert (distinct p22 p31))
(assert (distinct p18 p23))
(assert (distinct p23 p30))
(assert (distinct p9 p28))
(assert (distinct p14 p27))
(assert (distinct p15 p18))
(assert (distinct p11 p18))
(assert (distinct p1 p24))
(assert (distinct p13 p24))
(assert (distinct p2 p31))
(assert (distinct p3 p30))
(assert (distinct p5 p28))
(assert (distinct p20 p36))
(assert (distinct p28 p36))
(assert (distinct p7 p26))
(assert (distinct p1 p17))
(assert (distinct p2 p22))
(assert (distinct p1 p11))
(assert (distinct p20 p35))
(assert (distinct p28 p35))
(assert (distinct p8 p15))
(assert (distinct p17 p36))
(assert (distinct p9 p14))
(assert (distinct p18 p35))
(assert (distinct p8 p21))
(assert (distinct p2 p17))
(assert (distinct p1 p12))
(assert (distinct p2 p11))
(assert (distinct p24 p36))
(assert (distinct p5 p14))
(assert (distinct p3 p18))
(assert (distinct p7 p8))
(assert (distinct p22 p32))
(assert (distinct p30 p32))
(assert (distinct p22 p26))
(assert (distinct p18 p26))
(assert (distinct p8 p28))
(assert (distinct p24 p31))
(assert (distinct p14 p22))
(assert (distinct p10 p30))
(assert (distinct p25 p30))
(assert (distinct p11 p31))
(assert (distinct p26 p29))
(assert (distinct p12 p24))
(assert (distinct p1 p5))
(assert (distinct p14 p34))
(assert (distinct p4 p28))
(assert (distinct p19 p28))
(assert (distinct p26 p33))
(assert (distinct p5 p17))
(assert (distinct p20 p31))
(assert (distinct p6 p30))
(assert (distinct p21 p30))
(assert (distinct p17 p22))
(assert (distinct p22 p29))
(assert (distinct p18 p21))
(assert (distinct p12 p35))
(assert (distinct p14 p25))
(assert (distinct p15 p28))
(assert (distinct p11 p20))
(assert (distinct p1 p30))
(assert (distinct p13 p22))
(assert (distinct p2 p29))
(assert (distinct p5 p26))
(assert (distinct p8 p36))
(assert (distinct p7 p20))
(assert (distinct p5 p36))
(assert (distinct p16 p36))
(assert (distinct p9 p11))
(assert (distinct p8 p16))
(assert (distinct p12 p14))
(assert (distinct p1 p23))
(assert (distinct p2 p20))
(assert (distinct p1 p9))
(assert (distinct p2 p14))
(assert (distinct p1 p35))
(assert (distinct p6 p8))
(assert (distinct p17 p26))
(assert (distinct p18 p33))
(assert (distinct p10 p11))
(assert (distinct p8 p23))
(assert (distinct p9 p22))
(assert (distinct p24 p26))
(assert (distinct p11 p24))
(assert (distinct p3 p14))
(assert (distinct p1 p2))
(assert (distinct p28 p30))
(assert (distinct p2 p9))
(assert (distinct p5 p12))
(assert (distinct p3 p20))
(assert (distinct p1 p36))
(assert (distinct p2 p35))
(assert (distinct p26 p36))
(assert (distinct p5 p22))
(assert (distinct p16 p18))
(assert (distinct p22 p24))
(assert (distinct p18 p24))
(assert (distinct p8 p30))
(assert (distinct p14 p20))
(assert (distinct p10 p28))
(assert (distinct p25 p28))
(assert (distinct p11 p17))
(assert (distinct p26 p27))
(assert (distinct p12 p26))
(assert (distinct p1 p27))
(assert (distinct p14 p32))
(assert (distinct p4 p30))
(assert (distinct p19 p30))
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment